awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x : G
⊢ HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) x -
      HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L) x =
    0
have apply : Eq (α := G → L)
  (∑ i ∈ s,
    HSMul.hSMul (α := L) (β := G → L)
      ((fun (j : G →* L) ↦
          HMul.hMul (β := L) (g j) ((j : (a : G) → L) x : L) - HMul.hMul (β := L) (g j) ((a : (a : G) → L) x : L))
        i)
      (⇑i : (a : G) → L))
  0
Tactic: apply ih (fun j => g j * j x - g j * a x) _ i his
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x : G
⊢ Eq (α := G → L)
    (∑ i ∈ s,
      HSMul.hSMul (α := L) (β := G → L)
        ((fun (j : G →* L) ↦
            HMul.hMul (β := L) (g j) ((j : (a : G) → L) x : L) - HMul.hMul (β := L) (g j) ((a : (a : G) → L) x : L))
          i)
        (⇑i : (a : G) → L))
    0
have h : ∀ (y : G),
  Eq.{u_7 + 1} (α := L)
    ((∑ i ∈ s,
        HSMul.hSMul (α := L) (β := G → L)
          ((fun (j : G →* L) ↦
              HMul.hMul (β := L) (g j) ((j : (a : G) → L) x : L) - HMul.hMul (β := L) (g j) ((a : (a : G) → L) x : L))
            i)
          (⇑i : (a : G) → L))
      y)
    (0 y)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
⊢ HSub.hSub (α := L)
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L)) =
    HSub.hSub (α := L)
      (∑ i ∈ insert a s, g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L)))
have refine_1 : ∀ (i : G →* L),
  HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)
Tactic: congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
refine_1 :
  ∀ (i : G →* L),
    HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
      g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)
⊢ HSub.hSub (α := L)
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L)) =
    HSub.hSub (α := L)
      (∑ i ∈ insert a s, g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L))
      (∑ i ∈ insert a s,
        HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L)))
have refine_2 : ∀ (i : G →* L),
  HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
Tactic: congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i_1 : G →* L
his : i_1 ∈ s
x y : G
i : G →* L
⊢ HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)
have refine_1 : g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L) =
  g i * HMul.hMul (α := L) (β := L) ((i : (a : G) → L) x : L) ((i : (a : G) → L) y : L)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i_1 : G →* L
his : i_1 ∈ s
x y : G
i : G →* L
⊢ HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
have refine_2 : g i * HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L) ((i : (a : G) → L) y : L) =
  HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
Tactic: rw [mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i_1 : G →* L
his : i_1 ∈ s
x y : G
i : G →* L
refine_2 :
  g i * HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L) ((i : (a : G) → L) y : L) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
⊢ HMul.hMul (β := L) (HMul.hMul (β := L) (g i) ((a : (a : G) → L) x : L)) ((i : (a : G) → L) y : L) =
    HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
have refine_2₁ : HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L)) =
  HMul.hMul (α := L) ((a : (a : G) → L) x : L) (HMul.hMul (β := L) (g i) ((i : (a : G) → L) y : L))
Tactic: rw [mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
i : G →* L
his : i ∈ s
x y : G
⊢ (∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) (x * y) -
      HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L)
        ((∑ i ∈ insert a s, HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L)) y : L) =
    0
have rw : 0 (x * y) - HMul.hMul (α := L) (β := L) ((a : (a : G) → L) x : L) (0 y : L) = 0
Tactic: rw [hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
⊢ ∀ i ∈ insert a s, g i = 0
have h1 : ∀ (i : G →* L) (his : i ∈ s),
  HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
Tactic: have h1 (i) (his : i ∈ s) : (g i • i : G → L) = g i • a := by
    ext x
    rw [← sub_eq_zero]
    apply ih (fun j => g j * j x - g j * a x) _ i his
    ext y
    -- After that, it's just a chase scene.
    calc
      (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y =
          (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by simp [sub_mul]
      _ = (∑ i ∈ insert a s, g i * i x * i y) -
            ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
      _ = (∑ i ∈ insert a s, g i * (i x * i y)) -
            ∑ i ∈ insert a s, a x * (g i * i y) := by
        congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
        · rw [mul_assoc]
        · rw [mul_assoc, mul_left_comm]
      _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) -
            a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by simp [Finset.mul_sum]
      _ = 0 := by rw [hg]; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
⊢ ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
have by_contra! : ∀ (hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)), False
Tactic: by_contra! hia
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ False
have has₁ : i ∉ s
Tactic: obtain rfl : i = a := MonoidHom.ext hia
Cleared hypotheses: a, has, hg, h1, hia
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
has₁ : i ∉ s
⊢ False
have hg₁ : Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
Tactic: obtain rfl : i = a := MonoidHom.ext hia
Cleared hypotheses: a, has, hg, h1, hia
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
has₁ : i ∉ s
hg₁ : Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
⊢ False
have h1₁ : ∀ (i_1 : G →* L) (his : i_1 ∈ s),
  HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i_1 : (a : G) → L) =
    HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i : (a : G) → L)
Tactic: obtain rfl : i = a := MonoidHom.ext hia
Cleared hypotheses: a, has, hg, h1, hia
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
i : G →* L
his : i ∈ s
hia : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
has₁ : i ∉ s
hg₁ : Eq (α := G → L) (∑ i ∈ insert i s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1₁ :
  ∀ (i_1 : G →* L) (his : i_1 ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i_1 : (a : G) → L) =
      HSMul.hSMul (β := (a : G) → L) (g i_1) (⇑i : (a : G) → L)
⊢ False
have hia₁ : ∀ (y : G), Eq.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((i : (a : G) → L) y : L)
Tactic: obtain rfl : i = a := MonoidHom.ext hia
Cleared hypotheses: a, has, hg, h1, hia
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
⊢ ∀ i ∈ insert a s, g i = 0
have h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
Tactic: have h2 (i) (his : i ∈ s) : ∃ y, i y ≠ a y := by
    by_contra! hia
    obtain rfl : i = a := MonoidHom.ext hia
    contradiction
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
⊢ g i = 0
have let : ∀ (y : G) (hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)), g i = 0
Tactic: let ⟨y, hy⟩ := h2 i his
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
y : G
hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ g i = 0
have h : HSMul.hSMul (β := L) (g i) ((i : (a : G) → L) y : L) = HSMul.hSMul (β := L) (g i) ((a : (a : G) → L) y : L)
Tactic: have h : g i • i y = g i • a y := congr_fun (h1 i his) y
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
i : G →* L
his : i ∈ s
y : G
hy : Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h : HSMul.hSMul (β := L) (g i) ((i : (a : G) → L) y : L) = HSMul.hSMul (β := L) (g i) ((a : (a : G) → L) y : L)
⊢ g i = 0
have h₁ : g i = 0 ∨ HSub.hSub (α := L) (β := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L) = 0
Tactic: rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (hypothesis)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
⊢ ∀ i ∈ insert a s, g i = 0
have h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
Tactic: have h3 (i) (his : i ∈ s) : g i = 0 := by
    let ⟨y, hy⟩ := h2 i his
    have h : g i • i y = g i • a y := congr_fun (h1 i his) y
    rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
    exact h.resolve_right (sub_ne_zero_of_ne hy)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Basic (goal)
Goal:
G : Type u_6
inst : MulOneClass G
L : Type u_7
inst_1 : CommRing L
inst_2 : IsDomain L
this_1 : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := @DistribMulAction.toMulAction _ _ _ AddCommMonoid.toAddMonoid _
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih :
  ∀ (g : (G →* L) → L),
    Eq (α := G → L) (∑ i ∈ s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : Eq (α := G → L) (∑ i ∈ insert a s, HSMul.hSMul (β := G → L) (g i) (⇑i : (a : G) → L)) 0
h1 :
  ∀ (i : G →* L) (his : i ∈ s),
    HSMul.hSMul (β := (a : G) → L) (g i) (⇑i : (a : G) → L) = HSMul.hSMul (β := (a : G) → L) (g i) (⇑a : (a : G) → L)
h2 : ∀ (i : G →* L) (his : i ∈ s), ∃ (y : G), Ne.{u_7 + 1} (α := L) ((i : (a : G) → L) y : L) ((a : (a : G) → L) y : L)
h3 : ∀ (i : G →* L) (his : i ∈ s), g i = 0
⊢ g a * 1 = HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1
have rw : HMul.hMul (β := L) (g a) ((a : (a : G) → L) 1 : L) = HSMul.hSMul (β := (a : G) → L) (g a) (⇑a : (a : G) → L) 1
Tactic: rw [← a.map_one]