awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
this : Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)
hsum :
  ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
⊢ w i = 0
have this₁ : HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
    ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
  0
Tactic: simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
s : Finset n
w : n → K₁
hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0
i : n
hi : i ∈ s
hsum :
  ∑ j ∈ s,
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)
this :
  HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
      ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
    0
⊢ w i = 0
have apply : Eq.{u_13 + 1} (α := K) ((I₁ : (a : K₁) → K) (w i) : K) (0 : K)
Tactic: apply (map_eq_zero I₁).mp
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
⊢ LinearIndependent K₁ v
have rw : ∀ (s : Finset n) (g : n → K₁), Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
    have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
    simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this
    apply (map_eq_zero I₁).mp
    exact (smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
⊢ LinearIndependent K₁ v
have rw₄ : ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (this :
    Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)),
  w i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
    have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
    simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this
    apply (map_eq_zero I₁).mp
    exact (smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
rw₄ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this :
      Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)),
    w i = 0
⊢ LinearIndependent K₁ v
have rw₅ : ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (this :
    Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V))
  (hsum :
    ∑ j ∈ s,
        HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)),
  w i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
    have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
    simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this
    apply (map_eq_zero I₁).mp
    exact (smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
K : Type u_13
K₁ : Type u_14
V : Type u_16
V₁ : Type u_17
n : Type u_19
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Field K₁
inst_4 : AddCommGroup V₁
inst_5 : Module K₁ V₁
I₁ I₁' : K₁ →+* K
B : V₁ →ₛₗ[I₁] V₁ →ₛₗ[I₁'] V
v : n → V₁
hv₁ : B.IsOrthoᵢ v
hv₂ : ∀ (i : n), ¬B.IsOrtho (v i) (v i)
rw rw₁ rw₂ rw₃ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s), w i = 0
rw₄ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this :
      Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V)),
    w i = 0
rw₅ :
  ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
    (this :
      Eq.{u_16 + 1} (α := V) (((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (∑ i ∈ s, w i • v i) : (a : V₁) → V) (v i) : V) (0 : V))
    (hsum :
      ∑ j ∈ s,
          HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
            ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
        HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V)),
    w i = 0
⊢ LinearIndependent K₁ v
have rw₆ : ∀ (s : Finset n) (w : n → K₁) (hs : Eq.{u_17 + 1} (α := V₁) (∑ i ∈ s, w i • v i) 0) (i : n) (hi : i ∈ s)
  (hsum :
    ∑ j ∈ s,
        HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w j) : K)
          ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v j) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
      HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V))
  (this :
    HSMul.hSMul.{u_13, u_16, u_16} (α := K) (β := V) ((I₁ : (a : K₁) → K) (w i) : K)
        ((((B : (a : V₁) → V₁ →ₛₗ[I₁'] V) (v i) : V₁ →ₛₗ[I₁'] V) : (a : V₁) → V) (v i) : V) =
      0),
  w i = 0
Tactic: classical
    rw [linearIndependent_iff']
    intro s w hs i hi
    have : B (s.sum fun i : n ↦ w i • v i) (v i) = 0 := by rw [hs, map_zero, zero_apply]
    have hsum : (s.sum fun j : n ↦ I₁ (w j) • B (v j) (v i)) = I₁ (w i) • B (v i) (v i) := by
      apply Finset.sum_eq_single_of_mem i hi
      intro j _hj hij
      rw [isOrthoᵢ_def.1 hv₁ _ _ hij, smul_zero]
    simp_rw [B.map_sum₂, map_smulₛₗ₂, hsum] at this
    apply (map_eq_zero I₁).mp
    exact (smul_eq_zero.mp this).elim _root_.id (hv₂ i · |>.elim)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
p : Submodule R₁ M₁
x x_1 : ↥p
⊢ Eq.{u_5 + 1} (α := M)
      ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₛₗ[I₂] M) x : LinearMap.{u_2, u_1, u_6, u_5} I₂ (↥p) M) : (a : ↥p) → M)
          x_1 :
        M)
      (0 : M) →
    Eq.{u_5 + 1} (α := M)
      ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₛₗ[I₂] M) x_1 : LinearMap.{u_2, u_1, u_6, u_5} I₂ (↥p) M) : (a : ↥p) → M)
          x :
        M)
      (0 : M)
have simp_rw : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x_1 : M₁) : M)
    (0 : M) →
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (↑x_1 : M₁) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (↑x : M₁) : M)
    (0 : M)
Tactic: simp_rw [domRestrict₁₂_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.flip.ker = B.ker
have h : ∀ (x : M₁), x ∈ B.flip.ker ↔ x ∈ B.ker
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsRefl
⊢ B.ker = ⊥ ↔ B.flip.ker = ⊥
have rwa : B.ker = ⊥ ↔ B.ker = ⊥
Tactic: rwa [ker_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
x y : M
H1 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
have rw : Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) : R) (0 : R)
Tactic: rw [← H.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
M : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x x_1 : ↥p
⊢ Eq (α := R)
    ((I : (a : R) → R)
        ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₗ[R] R) x : LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥p) R) :
              (a : ↥p) → R)
            x_1 :
          R) :
      R)
    ((((B.domRestrict₁₂ p p : (a : ↥p) → ↥p →ₗ[R] R) x_1 : LinearMap.{u_1, u_1, u_5, u_1} (RingHom.id R) (↥p) R) :
          (a : ↥p) → R)
        x :
      R)
have simp_rw : Eq (α := R) ((I : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) (↑x : M) : M →ₗ[R] R) : (a : M) → R) (↑x_1 : M) : R) : R)
  ((((B : (a : M) → M →ₗ[R] R) (↑x_1 : M) : M →ₗ[R] R) : (a : M) → R) (↑x : M) : R)
Tactic: simp_rw [domRestrict₁₂_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
have simp_rw : (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) =
  HAdd.hAdd (β := M)
    (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
Tactic: simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
simp_rw :
  (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
have simp_rw₁ : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) : M)
  ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (a + b + c) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
Tactic: simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
simp_rw :
  (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
simp_rw₁ :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (a + b + c) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
have simp_rw₂ : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) 0 : M)
  (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) 0 : (a : M₁) → M) c : M)
Tactic: simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
simp_rw :
  (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
simp_rw₁ :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (a + b + c) : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (a + b + c) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
simp_rw₂ :
  Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) 0 : M)
    (((B : (a : M₁) → M₁ →ₛₗ[I₂] M) 0 : (a : M₁) → M) c : M)
⊢ HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
have simp_rw₃ : Eq.{u_5 + 1} (α := M) (0 : M) ((0 : (a : M₁) → M) c : M)
Tactic: simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
have this : HAdd.hAdd (β := M)
    (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
  HAdd.hAdd (β := M)
    (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
Tactic: have : B a a + B a b + B a c = B a c + B b c + B c c := by
    simp_rw [← map_add, ← map_add₂, hAdd, map_zero, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
inst_6 : IsCancelAdd M
a b c : M₁
hAdd : a + b + c = 0
this :
  HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) a : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M) =
    HAdd.hAdd (β := M)
      (HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
        ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M))
      ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) c : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
have this₁ : HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) b : M) =
  HAdd.hAdd (α := M) (β := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) a : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) b : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) c : M)
Tactic: rw [H, H, zero_add, add_zero, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
⊢ Eq.{u_5 + 1} (α := M) (-(((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M)
    ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M)
have H1 : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) (y + x) : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) (y + x) : M) (0 : M)
Tactic: have H1 : B (y + x) (y + x) = 0 := self_eq_zero H (y + x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
Goal:
R : Type u_1
R₁ : Type u_2
M : Type u_5
M₁ : Type u_6
inst : CommSemiring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : CommSemiring R₁
inst_4 : AddCommMonoid M₁
inst_5 : Module R₁ M₁
I₁ I₂ : R₁ →+* R
B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M
H : B.IsAlt
x y : M₁
h : Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((((B : (a : M₁) → M₁ →ₛₗ[I₂] M) y : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) x : M) (0 : M)
have rw : Eq.{u_5 + 1} (α := M) (-(((B : (a : M₁) → M₁ →ₛₗ[I₂] M) x : M₁ →ₛₗ[I₂] M) : (a : M₁) → M) y : M) (0 : M)
Tactic: rw [← neg H, h, neg_zero]