case mp
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
⊢ IsSymm B → ↑(flipHom R₂) B = B

case mpr
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
⊢ ↑(flipHom R₂) B = B → IsSymm B
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
⊢ IsSymm B ↔ ↑(flipHom R₂) B = B
constructor
case mp
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : IsSymm B
⊢ ↑(flipHom R₂) B = B
case mp
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
⊢ IsSymm B → ↑(flipHom R₂) B = B
intro h
case mp.H
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : IsSymm B
x : M
⊢ ∀ (y : M), bilin (↑(flipHom R₂) B) x y = bilin B x y
case mp
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : IsSymm B
⊢ ↑(flipHom R₂) B = B
ext x
case mp.H
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : IsSymm B
x y : M
⊢ bilin (↑(flipHom R₂) B) x y = bilin B x y
case mp.H
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : IsSymm B
x : M
⊢ ∀ (y : M), bilin (↑(flipHom R₂) B) x y = bilin B x y
intro y
no goals
case mp.H
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : IsSymm B
x y : M
⊢ bilin (↑(flipHom R₂) B) x y = bilin B x y
exact h y x
case mpr
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : ↑(flipHom R₂) B = B
x y : M
⊢ bilin B x y = bilin B y x
case mpr
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
⊢ ↑(flipHom R₂) B = B → IsSymm B
intro h x y
no goals
case mpr
R : Type u_2
M : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
R₁ : Type ?u.931439
M₁ : Type ?u.931442
inst✝¹⁶ : Ring R₁
inst✝¹⁵ : AddCommGroup M₁
inst✝¹⁴ : Module R₁ M₁
R₂ : Type u_1
M₂ : Type ?u.932054
inst✝¹³ : CommSemiring R₂
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : Module R₂ M₂
R₃ : Type ?u.932241
M₃ : Type ?u.932244
inst✝¹⁰ : CommRing R₃
inst✝⁹ : AddCommGroup M₃
inst✝⁸ : Module R₃ M₃
V : Type ?u.932832
K : Type ?u.932835
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.934049
M₂'' : Type ?u.934052
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : AddCommMonoid M₂''
inst✝² : Module R₂ M₂'
inst✝¹ : Module R₂ M₂''
inst✝ : Algebra R₂ R
h : ↑(flipHom R₂) B = B
x y : M
⊢ bilin B x y = bilin B y x
conv_lhs => rw [← h]