awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
h :
  ∀ (val : ι),
    Eq.{u_4 + 1} (α := M)
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
h₁ :
  ∀ (val : ι),
    Eq.{u_5 + 1} (α := M')
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).2
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).2
⊢ Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
have h₂ : ∀ (val : ι'),
  Eq.{u_4 + 1} (α := M)
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).1
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).1
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
h :
  ∀ (val : ι),
    Eq.{u_4 + 1} (α := M)
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).1
h₁ :
  ∀ (val : ι),
    Eq.{u_5 + 1} (α := M')
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).2
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inl val) :
            (a : R) → M × M')
          1).2
h₂ :
  ∀ (val : ι'),
    Eq.{u_4 + 1} (α := M)
      ((linearCombination R
                (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
              lsingle (Sum.inr val) :
            (a : R) → M × M')
          1).1
      (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
                (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
              lsingle (Sum.inr val) :
            (a : R) → M × M')
          1).1
⊢ Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
have h₃ : ∀ (val : ι'),
  Eq.{u_5 + 1} (α := M')
    ((linearCombination R
              (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).2
    (((prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
              (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) ∘ₗ
            lsingle (Sum.inr val) :
          (a : R) → M × M')
        1).2
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ LinearIndependent R (M := M × M')
    (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v'))
have this : Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
  (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
  (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
    (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
Tactic: have : linearCombination R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) =
      .prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (sumFinsuppLEquivProdFinsupp R).toLinearMap := by ext (_ | _) <;> simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  Eq (α := (ι ⊕ ι' →₀ R) →ₗ[R] M × M')
    (linearCombination R (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v')))
    (prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
      (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R)))
⊢ LinearIndependent R (M := M × M')
    (Sum.elim ((⇑(inl R M M') : (a : M) → M × M') ∘ v) ((⇑(inr R M M') : (a : M') → M × M') ∘ v'))
have rw : Injective (α := ι ⊕ ι' →₀ R) (β := M × M')
  (⇑(prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
        (↑(sumFinsuppLEquivProdFinsupp R) : (ι ⊕ ι' →₀ R) →ₗ[R] (ι →₀ R) × (ι' →₀ R))) :
    (a : ι ⊕ ι' →₀ R) → M × M')
Tactic: rw [LinearIndependent, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
⊢ LinearIndependent R (M := M × M')
    fun
      (x :
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))) ↦
    (↑x : M × M')
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val val_1 : (↑s : Type u_4)
eq :
  Eq (α := (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inl val))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inl val_1))
⊢ Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5)) (Sum.inl val) (Sum.inl val_1)
have eq₁ : (↑val : M) = (↑val_1 : M)
Tactic: simp [hs.ne_zero, ht.ne_zero] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
val val_1 : (↑t : Type u_5)
eq :
  Eq (α := (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inr val))
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      (fun (i : (↑t : Type u_5)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
      (Sum.inr val_1))
⊢ Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5)) (Sum.inr val) (Sum.inr val_1)
have eq₁ : (↑val : M') = (↑val_1 : M')
Tactic: simp [hs.ne_zero, ht.ne_zero] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
⊢ LinearIndependent R (M := M × M')
    fun
      (x :
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))) ↦
    (↑x : M × M')
have refine : Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) → M × M')
  ((fun
        (x :
          (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
            Type (max u_4 u_5))) ↦
      (↑x : M × M')) ∘
    (⇑e :
      (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
        (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))))
  (Sum.elim (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
    (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')))
Tactic: refine (linearIndependent_equiv' e ?_).mp (linearIndependent_inl_union_inr' hs ht)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R (M := M) fun (x : (↑s : Type u_4)) ↦ (↑x : M)
ht : LinearIndependent R (M := M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')
h : Nontrivial R
e : Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) ≃
  (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5)) :=
  Equiv.ofBijective
    (Sum.elim
      (fun (i : (↑s : Type u_4)) ↦
        Subtype.mk (p := fun (x : M × M') ↦
          Membership.mem (γ := Set (M × M'))
            ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
          ((inl R M M' : (a : M) → M × M') (↑i : M)) ⋯)
      fun (i : (↑t : Type u_5)) ↦
      Subtype.mk (p := fun (x : M × M') ↦
        Membership.mem (γ := Set (M × M'))
          ((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) x)
        ((inr R M M' : (a : M') → M × M') (↑i : M')) ⋯)
    ⋯
⊢ Eq (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5) → M × M')
    ((fun
          (x :
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5))) ↦
        (↑x : M × M')) ∘
      (⇑e :
        (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
          (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) : Type (max u_4 u_5))))
    (Sum.elim (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
      (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M')))
have h : ∀ (val : (↑s : Type u_4)),
  Eq.{u_4 + 1} (α := M)
    (Function.comp (α := Sum.{u_4, u_5} (↑s : Type u_4) (↑t : Type u_5))
        (fun
            (x :
              (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
                Type (max u_4 u_5))) ↦
          (↑x : M × M'))
        (⇑e :
          (a : (↑s : Type u_4) ⊕ (↑t : Type u_5)) →
            (↑((⇑(inl R M M') : (a : M) → M × M') '' s ∪ (⇑(inr R M M') : (a : M') → M × M') '' t) :
              Type (max u_4 u_5)))
        (Sum.inl val)).1
    (Sum.elim (β := (↑t : Type u_5))
        (Function.comp (β := M) (⇑(inl R M M') : (a : M) → M × M') fun (x : (↑s : Type u_4)) ↦ (↑x : M))
        (Function.comp (β := M') (⇑(inr R M M') : (a : M') → M × M') fun (x : (↑t : Type u_5)) ↦ (↑x : M'))
        (Sum.inl val)).1
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
⊢ LinearIndepOn R v (⋃ I ∈ c, (↑I : Set ι))
have rw : ∀ (f : ι →₀ R),
  Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f →
    ∀ (g : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g →
        Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
            ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) →
          f = g
Tactic: rw [linearIndepOn_iffₛ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
⊢ f = g
have inl : ∀ (hc : IsChain r ∅)
  (hfsupp :
    Membership.mem (γ := Submodule R (ι →₀ R))
      (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f)
  (hgsupp :
    Membership.mem (γ := Submodule R (ι →₀ R))
      (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g),
  f = g
Tactic: rcases eq_empty_or_nonempty c with (rfl | hn)
Cleared hypotheses: c, hc, hfsupp, hgsupp
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
inl :
  ∀ (hc : IsChain r ∅)
    (hfsupp :
      Membership.mem (γ := Submodule R (ι →₀ R))
        (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f)
    (hgsupp :
      Membership.mem (γ := Submodule R (ι →₀ R))
        (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g),
    f = g
⊢ f = g
have inr : ∀ (hn : c.Nonempty), f = g
Tactic: rcases eq_empty_or_nonempty c with (rfl | hn)
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
f g : ι →₀ R
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hc : IsChain r ∅
hfsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f
hgsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g
⊢ f = g
have inl : 0 = g
Tactic: rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
f g : ι →₀ R
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hc : IsChain r ∅
hfsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) f
hgsupp :
  Membership.mem (γ := Submodule R (ι →₀ R))
    (Finsupp.supported R R (⋃ (I : X), ⋃ (_ : Membership.mem (γ := Set X) ∅ I), (↑I : Set ι))) g
inl : 0 = g
⊢ f = g
have inl₁ : Eq (α := ι →₀ R) 0 0
Tactic: rw [show f = 0 by simpa using hfsupp, show g = 0 by simpa using hgsupp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (hypothesis)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
⊢ f = g
have this : Std.Refl r
Tactic: haveI : Std.Refl r := ⟨fun _ => Set.Subset.refl _⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
v : ι → M
indep : Set ι → Prop := fun (s : Set ι) ↦ LinearIndepOn R v s
X : Type (max 0 u') := { I : Set ι // indep I }
r : X → X → Prop := fun (I J : X) ↦ (↑I : Set ι) ⊆ (↑J : Set ι)
c : Set X
hc : IsChain r c
f : ι →₀ R
hfsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) f
g : ι →₀ R
hgsupp : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R (⋃ I ∈ c, (↑I : Set ι))) g
hsum :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
hn : c.Nonempty
this : Std.Refl r
⊢ f = g
have inr : ∀ (I : X) (_I_mem : I ∈ c) (hI : (↑f.support : Set ι) ∪ (↑g.support : Set ι) ⊆ (↑I : Set ι)), f = g
Tactic: obtain ⟨I, _I_mem, hI⟩ : ∃ I ∈ c, (f.support ∪ g.support : Set ι) ⊆ I :=
      f.support.coe_union _ ▸ hc.directedOn.exists_mem_subset_of_finset_subset_biUnion hn <| by
        simpa using And.intro hfsupp hgsupp