case h.H
R : Type u_2
M : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
R₁ : Type ?u.234780
M₁ : Type ?u.234783
inst✝¹² : Ring R₁
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.235395
inst✝⁹ : CommSemiring R₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₂ M₂
R₃ : Type ?u.235582
M₃ : Type ?u.235585
inst✝⁶ : CommRing R₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R₃ M₃
V : Type ?u.236173
K : Type ?u.236176
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
D : BilinForm R M
D₁ : BilinForm R₁ M₁
inst✝ : Algebra R₂ R
A : BilinForm R M
x✝ y✝ : M
⊢ bilin (↑(LinearEquiv.trans (flipHom R₂) (flipHom R₂)) A) x✝ y✝ =
    bilin (↑(LinearEquiv.refl R₂ (BilinForm R M)) A) x✝ y✝
R : Type u_2
M : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
R₁ : Type ?u.234780
M₁ : Type ?u.234783
inst✝¹² : Ring R₁
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.235395
inst✝⁹ : CommSemiring R₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₂ M₂
R₃ : Type ?u.235582
M₃ : Type ?u.235585
inst✝⁶ : CommRing R₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R₃ M₃
V : Type ?u.236173
K : Type ?u.236176
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
D : BilinForm R M
D₁ : BilinForm R₁ M₁
inst✝ : Algebra R₂ R
⊢ LinearEquiv.trans (flipHom R₂) (flipHom R₂) = LinearEquiv.refl R₂ (BilinForm R M)
ext A
no goals
case h.H
R : Type u_2
M : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
R₁ : Type ?u.234780
M₁ : Type ?u.234783
inst✝¹² : Ring R₁
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.235395
inst✝⁹ : CommSemiring R₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₂ M₂
R₃ : Type ?u.235582
M₃ : Type ?u.235585
inst✝⁶ : CommRing R₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R₃ M₃
V : Type ?u.236173
K : Type ?u.236176
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
B : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
D : BilinForm R M
D₁ : BilinForm R₁ M₁
inst✝ : Algebra R₂ R
A : BilinForm R M
x✝ y✝ : M
⊢ bilin (↑(LinearEquiv.trans (flipHom R₂) (flipHom R₂)) A) x✝ y✝ =
    bilin (↑(LinearEquiv.refl R₂ (BilinForm R M)) A) x✝ y✝
simp