case h.H
R : Type ?u.598553
M : Type ?u.598556
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.598592
M₁ : Type ?u.598595
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.599394
M₃ : Type ?u.599397
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.599985
K : Type ?u.599988
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type u_3
M₂'' : Type ?u.601205
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
e : M₂ ≃ₗ[R₂] M₂'
x✝¹ : BilinForm R₂ M₂'
x✝ y✝ : M₂
⊢ bilin (↑(LinearEquiv.symm (congr e)) x✝¹) x✝ y✝ = bilin (↑(congr (LinearEquiv.symm e)) x✝¹) x✝ y✝
R : Type ?u.598553
M : Type ?u.598556
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.598592
M₁ : Type ?u.598595
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.599394
M₃ : Type ?u.599397
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.599985
K : Type ?u.599988
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type u_3
M₂'' : Type ?u.601205
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
e : M₂ ≃ₗ[R₂] M₂'
⊢ LinearEquiv.symm (congr e) = congr (LinearEquiv.symm e)
ext
case h.H
R : Type ?u.598553
M : Type ?u.598556
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.598592
M₁ : Type ?u.598595
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.599394
M₃ : Type ?u.599397
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.599985
K : Type ?u.599988
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type u_3
M₂'' : Type ?u.601205
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
e : M₂ ≃ₗ[R₂] M₂'
x✝¹ : BilinForm R₂ M₂'
x✝ y✝ : M₂
⊢ bilin (↑(LinearEquiv.symm (congr e)) x✝¹) x✝ y✝ = bilin x✝¹ (↑e x✝) (↑e y✝)
case h.H
R : Type ?u.598553
M : Type ?u.598556
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.598592
M₁ : Type ?u.598595
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.599394
M₃ : Type ?u.599397
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.599985
K : Type ?u.599988
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type u_3
M₂'' : Type ?u.601205
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
e : M₂ ≃ₗ[R₂] M₂'
x✝¹ : BilinForm R₂ M₂'
x✝ y✝ : M₂
⊢ bilin (↑(LinearEquiv.symm (congr e)) x✝¹) x✝ y✝ = bilin (↑(congr (LinearEquiv.symm e)) x✝¹) x✝ y✝
simp only [congr_apply, LinearEquiv.symm_symm]
no goals
case h.H
R : Type ?u.598553
M : Type ?u.598556
inst✝¹⁸ : Semiring R
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
R₁ : Type ?u.598592
M₁ : Type ?u.598595
inst✝¹⁵ : Ring R₁
inst✝¹⁴ : AddCommGroup M₁
inst✝¹³ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type u_2
inst✝¹² : CommSemiring R₂
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : Module R₂ M₂
R₃ : Type ?u.599394
M₃ : Type ?u.599397
inst✝⁹ : CommRing R₃
inst✝⁸ : AddCommGroup M₃
inst✝⁷ : Module R₃ M₃
V : Type ?u.599985
K : Type ?u.599988
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type u_3
M₂'' : Type ?u.601205
inst✝³ : AddCommMonoid M₂'
inst✝² : AddCommMonoid M₂''
inst✝¹ : Module R₂ M₂'
inst✝ : Module R₂ M₂''
e : M₂ ≃ₗ[R₂] M₂'
x✝¹ : BilinForm R₂ M₂'
x✝ y✝ : M₂
⊢ bilin (↑(LinearEquiv.symm (congr e)) x✝¹) x✝ y✝ = bilin x✝¹ (↑e x✝) (↑e y✝)
rfl