awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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
⊢ 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)

Tactic:
rw [hB.polarization, hC.polarization]

Premises used: LinearMap.BilinForm.IsSymm.polarization
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
⊢ 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:
simp_rw [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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 : B = C
⊢ ∀ (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)

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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

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

Premises used: LinearMap.BilinForm.IsSymm.mk
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ (∀ (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

Tactic:
refine fun h ↦ ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M))) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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))

Premises used: Submodule.mem_span_iff_exists_finset_subset, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
⊢ Membership.mem (γ := Submodule R M) (Submodule.span R (Set.range.{u_2, u_8 + 1} (ι := ι) (⇑b : (a : ι) → M))) y

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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))

Premises used: Submodule.mem_span_iff_exists_finset_subset, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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:
rw [← hx, ← hy]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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))
⊢ 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:
simp only [map_sum, map_smul, coe_sum, Finset.sum_apply, smul_apply, smul_eq_mul,
      Finset.mul_sum]

Premises used: Finset.mul_sum, LinearMap.smul_apply, Finset.sum_apply, LinearMap.coe_sum, map_sum, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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))
⊢ 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:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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))

Tactic:
Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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:
refine Finset.sum_congr rfl (fun b₁ h₁ ↦ Finset.sum_congr rfl fun b₂ h₂ ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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:
rw [mul_left_comm]

Premises used: mul_left_comm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
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)
⊢ 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:
obtain ⟨i, rfl⟩ := ix h₁

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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)
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)
⊢ 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 ⟨j, rfl⟩ := iy h₂

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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)
rw 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)
⊢ 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:
rw [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LE R
B : BilinForm R M
⊢ B.IsNonneg ↔ ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: _private.0.LinearMap.BilinForm.isNonneg_def.match_1, Iff.intro, LinearMap.BilinForm.IsNonneg.mk
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LE R
B : BilinForm R M
⊢ B.IsNonneg ↔ LinearMap.IsNonneg B

Tactic:
isNonneg_def.trans LinearMap.isNonneg_def.symm

Premises used: LinearMap.BilinForm.isNonneg_def, Iff.trans, LinearMap.isNonneg_def, Iff.symm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Preorder R
⊢ IsNonneg.{u_1, u_2} (R := R) (M := M) 0

Tactic:
isNonneg_iff.2 LinearMap.isNonneg_zero

Premises used: Iff.mpr, LinearMap.BilinForm.isNonneg_iff, LinearMap.isNonneg_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
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
inst_3 : LE R
⊢ B.IsPosSemidef ↔ B.IsSymm ∧ B.IsNonneg

Tactic:
⟨fun h ↦ ⟨h.isSymm, h.isNonneg⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

Premises used: LinearMap.BilinForm.IsPosSemidef, LinearMap.BilinForm.IsPosSemidef.isNonneg, LinearMap.BilinForm.IsPosSemidef.isSymm, LinearMap.BilinForm.IsPosSemidef.mk, _private.0.LinearMap.BilinForm.isPosSemidef_def.match_1, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LE R
B : BilinForm R M
⊢ B.IsPosSemidef ↔ LinearMap.IsPosSemidef B

Tactic:
isPosSemidef_def.trans <| (isSymm_iff.and isNonneg_iff).trans LinearMap.isPosSemidef_def.symm

Premises used: LinearMap.isPosSemidef_def, LinearMap.BilinForm.isNonneg_iff, LinearMap.BilinForm.isSymm_iff, LinearMap.BilinForm.isPosSemidef_def, Iff.and, Iff.trans, Iff.symm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Preorder R
⊢ IsPosSemidef.{u_1, u_2} (R := R) (M := M) 0

Tactic:
isPosSemidef_iff.2 LinearMap.isPosSemidef_zero

Premises used: Iff.mpr, LinearMap.BilinForm.isPosSemidef_iff, LinearMap.isPosSemidef_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Properties
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Preorder R
inst_4 : AddLeftMono R
B C : BilinForm R M
hB : B.IsPosSemidef
hC : C.IsPosSemidef
⊢ (B + C).IsPosSemidef

Tactic:
isPosSemidef_iff.2 ((isPosSemidef_iff.1 hB).add (isPosSemidef_iff.1 hC))

Premises used: Iff.mpr, LinearMap.BilinForm.isPosSemidef_iff, LinearMap.IsPosSemidef.add, Iff.mp