awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * HMul.hMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) *
      (s * HMul.hMul (β := R) s ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)) =
    s * HMul.hMul (β := R) r ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) *
      (r * HMul.hMul (β := R) s ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
⊢ r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ r * r * s * s ≠ 0

Tactic:
simp [hr, hs]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ r * r * s * s ≠ 0

Tactic:
have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
hrs : r * r * s * s ≠ 0
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
le_of_eq <| mul_right_injective₀ hrs this

Premises used: mul_right_injective₀, le_of_eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
this :
  r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) =
    r * r * s * s *
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
hrs : r * r * s * s ≠ 0
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
exact le_of_eq <| mul_right_injective₀ hrs this

Premises used: mul_right_injective₀, le_of_eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
neg :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) (r • x) : R)
      ((((B : (a : M) → M →ₗ[R] R) (s • y) : M →ₗ[R] R) : (a : M) → R) (s • y) : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) (s • y) : R)
      ((((B : (a : M) → M →ₗ[R] R) (s • y) : M →ₗ[R] R) : (a : M) → R) (r • x) : R)
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
suffices
        (B (r • x) (r • x)) * (B (s • y) (s • y)) = (B (r • x) (s • y)) * (B (s • y) (r • x)) by
      simp only [map_smul, smul_apply, smul_eq_mul] at this
      rw [show r * (r * (B x) x) * (s * (s * (B y) y)) = (r * r * s * s) * ((B x) x * (B y) y) by
        ring, show s * (r * (B x) y) * (r * (s * (B y) x)) = (r * r * s * s) * ((B x) y * (B y) x)
        by ring] at this
      have hrs : r * r * s * s ≠ 0 := by simp [hr, hs]
      exact le_of_eq <| mul_right_injective₀ hrs this
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
rwa : s • y = -(r • x)
rwa₁ rwa₂ rwa₃ rwa₄ : r • x + s • y = 0
⊢ s • y = -r • x

Tactic:
rwa [neg_smul, ← add_eq_zero_iff_eq_neg']

Premises used: neg_smul, add_eq_zero_iff_eq_neg'
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
r s : R
hl : r • x + s • y = 0
h0 : ∀ (_ : r = 0), s ≠ 0
hr : ¬r = 0
hs : ¬s = 0
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) (r • x) : R)
      ((((B : (a : M) → M →ₗ[R] R) (s • y) : M →ₗ[R] R) : (a : M) → R) (s • y) : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (r • x) : M →ₗ[R] R) : (a : M) → R) (s • y) : R)
      ((((B : (a : M) → M →ₗ[R] R) (s • y) : M →ₗ[R] R) : (a : M) → R) (r • x) : R)

Tactic:
simp [show s • y = - r • x by rwa [neg_smul, ← add_eq_zero_iff_eq_neg']]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
mpr :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) →
    ¬LinearIndependent R ![x, y]
⊢ LinearIndependent R ![x, y] →
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
contrapose!
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
h :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ ¬LinearIndependent R ![x, y]

Tactic:
not_linearIndependent_of_apply_mul_apply_eq B hp x y (le_antisymm
      (apply_mul_apply_le_of_forall_zero_le B hle x y) h)

Premises used: LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le, le_antisymm, LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
hle : ∀ (z : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) z : R)
h :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ ¬LinearIndependent R ![x, y]

Tactic:
exact not_linearIndependent_of_apply_mul_apply_eq B hp x y (le_antisymm
      (apply_mul_apply_le_of_forall_zero_le B hle x y) h)

Premises used: LinearMap.BilinForm.apply_mul_apply_le_of_forall_zero_le, le_antisymm, LinearMap.BilinForm.not_linearIndependent_of_apply_mul_apply_eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
rw :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R) =
    HMul.hMul (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
rw₂ rw₃ :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rw [sq, ← hB.eq, RingHom.id_apply]

Premises used: RingHom.id_apply, sq, LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
rw :
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    LinearIndependent R ![x, y]
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    LinearIndependent R ![x, y]

Tactic:
rw [show B x y ^ 2 = B x y * B y x by rw [sq, ← hB.eq, RingHom.id_apply]]
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    LinearIndependent R ![x, y]

Tactic:
apply_mul_apply_lt_iff_linearIndependent B hp x y

Premises used: LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
hB : IsSymm B
x y : M
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) <
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) ↔
    LinearIndependent R ![x, y]

Tactic:
exact apply_mul_apply_lt_iff_linearIndependent B hp x y

Premises used: LinearMap.BilinForm.apply_mul_apply_lt_iff_linearIndependent
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
⊢ (∀ (i j : ι),
      Eq.{u_1 + 1} (α := R)
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
          R)
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)) →
    B.IsSymm

Tactic:
fun h ↦ ⟨fun x y ↦ ?_⟩

Premises used: LinearMap.IsSymm.mk
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
refine :
  ∀
    (h :
      ∀ (i j : ι),
        Eq.{u_1 + 1} (α := R)
          (star
              ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((b : (a : ι) → M) j : M)) :
            R)
          ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R))
    (x y : M),
    Eq (α := R) ((starRingEnd R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ (∀ (i j : ι),
      Eq.{u_1 + 1} (α := R)
        (star
            ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
          R)
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)) →
    B.IsSymm

Tactic:
refine fun h ↦ ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M))) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
obtain :
  ∀ (fx : M → R) (tx : Finset M) (ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M))
    (hx : ∑ a ∈ tx, fx a • a = x),
    Eq (α := R) ((starRingEnd R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ Eq (α := R) ((starRingEnd R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
obtain ⟨fx, tx, ix, -, hx⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : x ∈ Submodule.span R (Set.range b))

Premises used: Submodule.mem_span_iff_exists_finset_subset, Iff.mp
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Star
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid M
inst_3 : Module R M
B : M →ₗ⋆[R] M →ₗ[R] R
ι : Type u_4
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      (star ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M)) :
        R)
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
x y : M
fx : M → R
tx : Finset M
ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_2, u_4 + 1} (ι := ι) (⇑b : (a : ι) → M))) y

Tactic:
simp