awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B C : BilinForm R M
hB : B.IsSymm
hC : C.IsSymm
h :
  ∀ (x : M),
    Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
⊢ Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
have H : HSub.hSub (β := R)
      (HSub.hSub (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) (x + y) : 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) /
    2 =
  HSub.hSub (β := R)
      (HSub.hSub (α := R) (β := R) ((((C : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
        ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R))
      ((((C : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) /
    2
Tactic: rw [hB.polarization, hC.polarization]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
⊢ (∀ (i j : ι),
      Eq.{u_1 + 1} (α := R)
        ((((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
have refine : ∀
  (h :
    ∀ (i j : ι),
      Eq.{u_1 + 1} (α := R)
        ((((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.{u_1 + 1} (α := 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: refine fun h ↦ ⟨fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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.{u_1 + 1} (α := 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)
have obtain : ∀ (fx : M → R) (tx : Finset M) (ix : (↑tx : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M))
  (hx : ∑ a ∈ tx, fx a • a = x),
  Eq.{u_1 + 1} (α := 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: obtain ⟨fx, tx, ix, -, hx⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : x ∈ Submodule.span R (Set.range b))
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
⊢ Eq.{u_1 + 1} (α := 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)
have obtain : ∀ (fy : M → R) (ty : Finset M) (iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M))
  (hy : ∑ a ∈ ty, fy a • a = y),
  Eq.{u_1 + 1} (α := 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: obtain ⟨fy, ty, iy, -, hy⟩ := Submodule.mem_span_iff_exists_finset_subset.1
      (by simp : y ∈ Submodule.span R (Set.range b))
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
⊢ Eq.{u_1 + 1} (α := 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)
have rw : Eq.{u_1 + 1} (α := R)
  ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ tx, fx a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ ty, fy a • a) : R)
  ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ ty, fy a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ tx, fx a • a) : R)
Tactic: rw [← hx, ← hy]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
⊢ Eq.{u_1 + 1} (α := R)
    ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ tx, fx a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ ty, fy a • a) : R)
    ((((B : (a : M) → M →ₗ[R] R) (∑ a ∈ ty, fy a • a) : M →ₗ[R] R) : (a : M) → R) (∑ a ∈ tx, fx a • a) : R)
have simp : Eq.{u_1 + 1} (α := R)
  (∑ x ∈ ty,
    ∑ i ∈ tx, fy x * HMul.hMul (β := R) (fx i) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
  (∑ x ∈ tx,
    ∑ i ∈ ty, fx x * HMul.hMul (β := R) (fy i) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
Tactic: simp only [map_sum, map_smul, coe_sum, Finset.sum_apply, smul_apply, smul_eq_mul,
      Finset.mul_sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ ty,
      ∑ i ∈ tx, fy x * HMul.hMul (β := R) (fx i) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty, fx x * HMul.hMul (β := R) (fy i) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
have rw : Eq.{u_1 + 1} (α := R)
  (∑ y ∈ tx,
    ∑ x ∈ ty, fy x * HMul.hMul (β := R) (fx y) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
  (∑ x ∈ tx,
    ∑ i ∈ ty, fx x * HMul.hMul (β := R) (fy i) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
Tactic: rw [Finset.sum_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y ∈ tx,
      ∑ x ∈ ty, fy x * HMul.hMul (β := R) (fx y) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
    (∑ x ∈ tx,
      ∑ i ∈ ty, fx x * HMul.hMul (β := R) (fy i) ((((B : (a : M) → M →ₗ[R] R) i : M →ₗ[R] R) : (a : M) → R) x : R))
have refine : ∀ (b₁ : M) (h₁ : b₁ ∈ tx) (b₂ : M) (h₂ : b₂ ∈ ty),
  fy b₂ * HMul.hMul (β := R) (fx b₁) ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂ : R) =
    fx b₁ * HMul.hMul (β := R) (fy b₂) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
Tactic: refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₁ : M
h₁ : b₁ ∈ tx
b₂ : M
h₂ : b₂ ∈ ty
⊢ fy b₂ * HMul.hMul (β := R) (fx b₁) ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂ : R) =
    fx b₁ * HMul.hMul (β := R) (fy b₂) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
have rw : fx b₁ * HMul.hMul (β := R) (fy b₂) ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂ : R) =
  fx b₁ * HMul.hMul (β := R) (fy b₂) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
Tactic: rw [mul_left_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₁ : M
h₁ : b₁ ∈ tx
b₂ : M
h₂ : b₂ ∈ ty
⊢ fx b₁ * HMul.hMul (β := R) (fy b₂) ((((B : (a : M) → M →ₗ[R] R) b₁ : M →ₗ[R] R) : (a : M) → R) b₂ : R) =
    fx b₁ * HMul.hMul (β := R) (fy b₂) ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) b₁ : R)
have obtain : ∀ (i : ι) (h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)),
  fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy b₂)
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) b₂ : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy b₂)
        ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: obtain ⟨i, rfl⟩ := ix h₁
Cleared hypotheses: b₁, h₁
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
b₂ : M
h₂ : b₂ ∈ ty
i : ι
h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)
⊢ fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy b₂)
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) b₂ : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy b₂)
        ((((B : (a : M) → M →ₗ[R] R) b₂ : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have obtain : ∀ (j : ι) (h₂ : Membership.mem (α := M) ty ((b : (a : ι) → M) j : M)),
  fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy ((b : (a : ι) → M) j))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy ((b : (a : ι) → M) j))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: obtain ⟨j, rfl⟩ := iy h₂
Cleared hypotheses: b₂, h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
ι : Type u_8
b : Basis ι R M
h :
  ∀ (i j : ι),
    Eq.{u_1 + 1} (α := R)
      ((((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_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hx : ∑ a ∈ tx, fx a • a = x
fy : M → R
ty : Finset M
iy : (↑ty : Set M) ⊆ Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M)
hy : ∑ a ∈ ty, fy a • a = y
i : ι
h₁ : Membership.mem (α := M) tx ((b : (a : ι) → M) i : M)
j : ι
h₂ : Membership.mem (α := M) ty ((b : (a : ι) → M) j : M)
⊢ fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy ((b : (a : ι) → M) j))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) j : M) : R) =
    fx ((b : (a : ι) → M) i) *
      HMul.hMul (β := R) (fy ((b : (a : ι) → M) j))
        ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
have rw : fx ((b : (a : ι) → M) i) *
    HMul.hMul (β := R) (fy ((b : (a : ι) → M) j))
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R) =
  fx ((b : (a : ι) → M) i) *
    HMul.hMul (β := R) (fy ((b : (a : ι) → M) j))
      ((((B : (a : M) → M →ₗ[R] R) ((b : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R) ((b : (a : ι) → M) i : M) : R)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
⊢ B.Nondegenerate
have h₁ : B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)
Tactic: convert! h.congr e.symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
⊢ B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)
have h₁ : B = (congr (e ≪≫ₗ e.symm) : (a : BilinForm R M) → BilinForm R M) B
Tactic: rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
h₁ : B = (congr (e ≪≫ₗ e.symm) : (a : BilinForm R M) → BilinForm R M) B
⊢ B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)
have h₂ : B = (congr (LinearEquiv.refl R M) : (a : BilinForm R M) → BilinForm R M) B
Tactic: rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
h₁ : B = (congr (e ≪≫ₗ e.symm) : (a : BilinForm R M) → BilinForm R M) B
h₂ : B = (congr (LinearEquiv.refl R M) : (a : BilinForm R M) → BilinForm R M) B
⊢ B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)
have h₃ : B = (LinearEquiv.refl R (BilinForm R M) : (a : BilinForm R M) → BilinForm R M) B
Tactic: rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
M' : Type u_8
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
B : BilinForm R M
e : M ≃ₗ[R] M'
h : Nondegenerate.{u_1, u_8} (R := R) (M := M') ((congr e : (a : BilinForm R M) → BilinForm R M') B)
h₁ : B = (congr (e ≪≫ₗ e.symm) : (a : BilinForm R M) → BilinForm R M) B
h₂ : B = (congr (LinearEquiv.refl R M) : (a : BilinForm R M) → BilinForm R M) B
h₃ : B = (LinearEquiv.refl R (BilinForm R M) : (a : BilinForm R M) → BilinForm R M) B
⊢ B = (congr e.symm : (a : BilinForm R M') → BilinForm R M) ((congr e : (a : BilinForm R M) → BilinForm R M') B)
have h₄ : B = B
Tactic: rw [congr_congr, e.self_trans_symm, congr_refl, LinearEquiv.refl_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
⊢ φ = ψ
have h₁ : ∀ (w : M₁), Eq (α := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)
Tactic: ext w
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ Eq (α := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)
have h₁ : ∀ (y : M₁),
  Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁)
              (HSub.hSub (α := M₁) (β := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)) :
            M₁ →ₗ[R₁] R₁) :
          (a : M₁) → R₁)
        y :
      R₁)
    (0 : R₁)
Tactic: refine eq_of_sub_eq_zero (b.1 _ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁)
              (HSub.hSub (α := M₁) (β := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)) :
            M₁ →ₗ[R₁] R₁) :
          (a : M₁) → R₁)
        v :
      R₁)
    (0 : R₁)
have h₁ : HSub.hSub (α := R₁) (β := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((φ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
  0
Tactic: rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
h₁ :
  HSub.hSub (α := R₁) (β := R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((φ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
⊢ Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁)
              (HSub.hSub (α := M₁) (β := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)) :
            M₁ →ₗ[R₁] R₁) :
          (a : M₁) → R₁)
        v :
      R₁)
    (0 : R₁)
have h₂ : HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
  0
Tactic: rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R₁ : Type u_3
M₁ : Type u_4
inst : CommRing R₁
inst_1 : AddCommGroup M₁
inst_2 : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
h₁ :
  HSub.hSub (α := R₁) (β := R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((φ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
h₂ :
  HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
      ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁) ((ψ : (a : M₁) → M₁) w) : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
    0
⊢ Eq.{u_3 + 1} (α := R₁)
    ((((B : (a : M₁) → M₁ →ₗ[R₁] R₁)
              (HSub.hSub (α := M₁) (β := M₁) ((φ : (a : M₁) → M₁) w : M₁) ((ψ : (a : M₁) → M₁) w : M₁)) :
            M₁ →ₗ[R₁] R₁) :
          (a : M₁) → R₁)
        v :
      R₁)
    (0 : R₁)
have h₃ : HSub.hSub (α := R₁) (β := R₁) ((((B.compLeft φ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁)
    ((((B.compLeft ψ : (a : M₁) → M₁ →ₗ[R₁] R₁) w : M₁ →ₗ[R₁] R₁) : (a : M₁) → R₁) v : R₁) =
  0
Tactic: rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]