case h.e'_6
R : Type ?u.1410438
M : Type ?u.1410441
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1410477
M₁ : Type ?u.1410480
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.1411279
M₃ : Type ?u.1411282
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1411870
K : Type ?u.1411873
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
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₂ M₂
e : M₂ ≃ₗ[R₂] M₂'
h : Nondegenerate (↑(congr e) B)
⊢ B = ↑(congr (LinearEquiv.symm e)) (↑(congr e) B)
R : Type ?u.1410438
M : Type ?u.1410441
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1410477
M₁ : Type ?u.1410480
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.1411279
M₃ : Type ?u.1411282
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1411870
K : Type ?u.1411873
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
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₂ M₂
e : M₂ ≃ₗ[R₂] M₂'
h : Nondegenerate (↑(congr e) B)
⊢ Nondegenerate B
convert h.congr e.symm
no goals
case h.e'_6
R : Type ?u.1410438
M : Type ?u.1410441
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
R₁ : Type ?u.1410477
M₁ : Type ?u.1410480
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.1411279
M₃ : Type ?u.1411282
inst✝⁷ : CommRing R₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R₃ M₃
V : Type ?u.1411870
K : Type ?u.1411873
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
inst✝¹ : AddCommMonoid M₂'
inst✝ : Module R₂ M₂'
B : BilinForm R₂ M₂
e : M₂ ≃ₗ[R₂] M₂'
h : Nondegenerate (↑(congr e) B)
⊢ B = ↑(congr (LinearEquiv.symm e)) (↑(congr e) B)
rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]