case mk
R : Type u_1
M : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.69116
M₁ : Type ?u.69119
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.69728
M₂ : Type ?u.69731
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.69918
M₃ : Type ?u.69921
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type ?u.70509
K : Type ?u.70512
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₁
D : BilinForm R M
bilin✝ : M → M → R
bilin_add_left✝ : ∀ (x y z : M), bilin✝ (x + y) z = bilin✝ x z + bilin✝ y z
bilin_smul_left✝ : ∀ (a : R) (x y : M), bilin✝ (a • x) y = a * bilin✝ x y
bilin_add_right✝ : ∀ (x y z : M), bilin✝ x (y + z) = bilin✝ x y + bilin✝ x z
bilin_smul_right✝ : ∀ (a : R) (x y : M), bilin✝ x (a • y) = a * bilin✝ x y
h :
  { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
        bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ }.bilin =
    D.bilin
⊢ { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
      bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ } =
    D
R : Type u_1
M : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.69116
M₁ : Type ?u.69119
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.69728
M₂ : Type ?u.69731
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.69918
M₃ : Type ?u.69921
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type ?u.70509
K : Type ?u.70512
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₁
B D : BilinForm R M
h : B.bilin = D.bilin
⊢ B = D
cases B
case mk.mk
R : Type u_1
M : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.69116
M₁ : Type ?u.69119
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.69728
M₂ : Type ?u.69731
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.69918
M₃ : Type ?u.69921
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type ?u.70509
K : Type ?u.70512
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₁
bilin✝¹ : M → M → R
bilin_add_left✝¹ : ∀ (x y z : M), bilin✝¹ (x + y) z = bilin✝¹ x z + bilin✝¹ y z
bilin_smul_left✝¹ : ∀ (a : R) (x y : M), bilin✝¹ (a • x) y = a * bilin✝¹ x y
bilin_add_right✝¹ : ∀ (x y z : M), bilin✝¹ x (y + z) = bilin✝¹ x y + bilin✝¹ x z
bilin_smul_right✝¹ : ∀ (a : R) (x y : M), bilin✝¹ x (a • y) = a * bilin✝¹ x y
bilin✝ : M → M → R
bilin_add_left✝ : ∀ (x y z : M), bilin✝ (x + y) z = bilin✝ x z + bilin✝ y z
bilin_smul_left✝ : ∀ (a : R) (x y : M), bilin✝ (a • x) y = a * bilin✝ x y
bilin_add_right✝ : ∀ (x y z : M), bilin✝ x (y + z) = bilin✝ x y + bilin✝ x z
bilin_smul_right✝ : ∀ (a : R) (x y : M), bilin✝ x (a • y) = a * bilin✝ x y
h :
  { bilin := bilin✝¹, bilin_add_left := bilin_add_left✝¹, bilin_smul_left := bilin_smul_left✝¹,
        bilin_add_right := bilin_add_right✝¹, bilin_smul_right := bilin_smul_right✝¹ }.bilin =
    { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
        bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ }.bilin
⊢ { bilin := bilin✝¹, bilin_add_left := bilin_add_left✝¹, bilin_smul_left := bilin_smul_left✝¹,
      bilin_add_right := bilin_add_right✝¹, bilin_smul_right := bilin_smul_right✝¹ } =
    { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
      bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ }
case mk
R : Type u_1
M : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.69116
M₁ : Type ?u.69119
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.69728
M₂ : Type ?u.69731
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.69918
M₃ : Type ?u.69921
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type ?u.70509
K : Type ?u.70512
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₁
D : BilinForm R M
bilin✝ : M → M → R
bilin_add_left✝ : ∀ (x y z : M), bilin✝ (x + y) z = bilin✝ x z + bilin✝ y z
bilin_smul_left✝ : ∀ (a : R) (x y : M), bilin✝ (a • x) y = a * bilin✝ x y
bilin_add_right✝ : ∀ (x y z : M), bilin✝ x (y + z) = bilin✝ x y + bilin✝ x z
bilin_smul_right✝ : ∀ (a : R) (x y : M), bilin✝ x (a • y) = a * bilin✝ x y
h :
  { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
        bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ }.bilin =
    D.bilin
⊢ { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
      bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ } =
    D
cases D
no goals
case mk.mk
R : Type u_1
M : Type u_2
inst✝¹⁴ : Semiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
R₁ : Type ?u.69116
M₁ : Type ?u.69119
inst✝¹¹ : Ring R₁
inst✝¹⁰ : AddCommGroup M₁
inst✝⁹ : Module R₁ M₁
R₂ : Type ?u.69728
M₂ : Type ?u.69731
inst✝⁸ : CommSemiring R₂
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
R₃ : Type ?u.69918
M₃ : Type ?u.69921
inst✝⁵ : CommRing R₃
inst✝⁴ : AddCommGroup M₃
inst✝³ : Module R₃ M₃
V : Type ?u.70509
K : Type ?u.70512
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₁
bilin✝¹ : M → M → R
bilin_add_left✝¹ : ∀ (x y z : M), bilin✝¹ (x + y) z = bilin✝¹ x z + bilin✝¹ y z
bilin_smul_left✝¹ : ∀ (a : R) (x y : M), bilin✝¹ (a • x) y = a * bilin✝¹ x y
bilin_add_right✝¹ : ∀ (x y z : M), bilin✝¹ x (y + z) = bilin✝¹ x y + bilin✝¹ x z
bilin_smul_right✝¹ : ∀ (a : R) (x y : M), bilin✝¹ x (a • y) = a * bilin✝¹ x y
bilin✝ : M → M → R
bilin_add_left✝ : ∀ (x y z : M), bilin✝ (x + y) z = bilin✝ x z + bilin✝ y z
bilin_smul_left✝ : ∀ (a : R) (x y : M), bilin✝ (a • x) y = a * bilin✝ x y
bilin_add_right✝ : ∀ (x y z : M), bilin✝ x (y + z) = bilin✝ x y + bilin✝ x z
bilin_smul_right✝ : ∀ (a : R) (x y : M), bilin✝ x (a • y) = a * bilin✝ x y
h :
  { bilin := bilin✝¹, bilin_add_left := bilin_add_left✝¹, bilin_smul_left := bilin_smul_left✝¹,
        bilin_add_right := bilin_add_right✝¹, bilin_smul_right := bilin_smul_right✝¹ }.bilin =
    { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
        bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ }.bilin
⊢ { bilin := bilin✝¹, bilin_add_left := bilin_add_left✝¹, bilin_smul_left := bilin_smul_left✝¹,
      bilin_add_right := bilin_add_right✝¹, bilin_smul_right := bilin_smul_right✝¹ } =
    { bilin := bilin✝, bilin_add_left := bilin_add_left✝, bilin_smul_left := bilin_smul_left✝,
      bilin_add_right := bilin_add_right✝, bilin_smul_right := bilin_smul_right✝ }
congr