case H
R : Type u_2
M : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
R₁ : Type ?u.194705
M₁ : Type ?u.194708
inst✝¹² : Ring R₁
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.195320
inst✝⁹ : CommSemiring R₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₂ M₂
R₃ : Type ?u.195507
M₃ : Type ?u.195510
inst✝⁶ : CommRing R₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R₃ M₃
V : Type ?u.196098
K : Type ?u.196101
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
A : M
⊢ ∀ (y : M), bilin (↑(flipHomAux R₂) (↑(flipHomAux R₂) A✝)) A y = bilin A✝ A y
R : Type u_2
M : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
R₁ : Type ?u.194705
M₁ : Type ?u.194708
inst✝¹² : Ring R₁
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.195320
inst✝⁹ : CommSemiring R₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₂ M₂
R₃ : Type ?u.195507
M₃ : Type ?u.195510
inst✝⁶ : CommRing R₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R₃ M₃
V : Type ?u.196098
K : Type ?u.196101
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
⊢ ↑(flipHomAux R₂) (↑(flipHomAux R₂) A) = A
ext A
no goals
case H
R : Type u_2
M : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
R₁ : Type ?u.194705
M₁ : Type ?u.194708
inst✝¹² : Ring R₁
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.195320
inst✝⁹ : CommSemiring R₂
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : Module R₂ M₂
R₃ : Type ?u.195507
M₃ : Type ?u.195510
inst✝⁶ : CommRing R₃
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : Module R₃ M₃
V : Type ?u.196098
K : Type ?u.196101
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
A : M
⊢ ∀ (y : M), bilin (↑(flipHomAux R₂) (↑(flipHomAux R₂) A✝)) A y = bilin A✝ A y
simp [flipHomAux]