awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1
s : Set ι
hm :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s))
    ((affineCombination k fs p : (a : ι → k) → P) w : P)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : (↑fs' : Set ι) ⊆ s
hw' : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 1
he :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs p : (a : ι → k) → P) w : P)
    ((affineCombination k fs' p : (a : ι → k) → P) w' : P)
⊢ w i = 0
have hi' : (↑fs : Set ι).indicator w i = 0
Tactic: have hi' : (fs : Set ι).indicator w i = 0 := by
    rw [ha.indicator_eq_of_affineCombination_eq fs fs' w w' hw hw' he]
    exact Set.indicator_of_notMem (Set.notMem_subset hfs's his) w'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
p : ι → P
ha : AffineIndependent k p
fs : Finset ι
w : ι → k
hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1
s : Set ι
hm :
  Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (p '' s))
    ((affineCombination k fs p : (a : ι → k) → P) w : P)
i : ι
hifs : i ∈ fs
his : i ∉ s
fs' : Finset ι
w' : ι → k
hfs's : (↑fs' : Set ι) ⊆ s
hw' : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 1
he :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs p : (a : ι → k) → P) w : P)
    ((affineCombination k fs' p : (a : ι → k) → P) w' : P)
hi' : (↑fs : Set ι).indicator w i = 0
⊢ w i = 0
have hi'₁ : i ∈ (↑fs : Set ι) → w i = 0
Tactic: rw [Set.indicator_apply_eq_zero] at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) w₂ : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
⊢ (↑(map e s₂) : Set ι).indicator (extend (⇑e : (a : ι₂) → ι) w₂ 0) = (↑s₁ : Set ι).indicator w₁
have hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
Tactic: have hw₂e : extend e w₂ 0 ∘ e = w₂ := extend_comp e.injective _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k s₂ (p ∘ (⇑e : (a : ι₂) → ι)) : (a : ι₂ → k) → P) w₂ : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ (↑(map e s₂) : Set ι).indicator (extend (⇑e : (a : ι₂) → ι) w₂ 0) = (↑s₁ : Set ι).indicator w₁
have h₁ : Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
  ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
Tactic: rw [← hw₂e, ← affineCombination_map] at h
Cleared hypotheses: h, hw₂e
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ (↑(map e s₂) : Set ι).indicator (extend (⇑e : (a : ι₂) → ι) w₂ 0) = (↑s₁ : Set ι).indicator w₁
have refine : Eq.{u_1 + 1} (α := k) (∑ i ∈ map e s₂, extend (⇑e : (a : ι₂) → ι) w₂ 0 i) 1
Tactic: refine (ha.indicator_eq_of_affineCombination_eq s₁ (s₂.map e) _ _ hw₁ ?_ h.symm).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ map e s₂, extend (⇑e : (a : ι₂) → ι) w₂ 0 i) 1
have rw : Eq.{u_1 + 1} (α := k)
  (∑ x ∈ s₂,
    extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
      ((e : (a : ι₂) → ι) x : ι))
  1
Tactic: rw [sum_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
ι₂ : Type u_5
p : ι → P
ha : AffineIndependent k p
s₁ : Finset ι
s₂ : Finset ι₂
w₁ : ι → k
w₂ : ι₂ → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₁, w₁ i) 1
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ s₂, w₂ i) 1
e : ι₂ ↪ ι
h :
  Eq.{u_3 + 1} (α := P) ((affineCombination k (map e s₂) p : (a : ι → k) → P) (extend (⇑e : (a : ι₂) → ι) w₂ 0) : P)
    ((affineCombination k s₁ p : (a : ι → k) → P) w₁ : P)
hw₂e : comp.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) (extend (⇑e : (a : ι₂) → ι) w₂ 0) (⇑e : (a : ι₂) → ι) = w₂
⊢ Eq.{u_1 + 1} (α := k)
    (∑ x ∈ s₂,
      extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
        ((e : (a : ι₂) → ι) x : ι))
    1
have h₁ : ∀ (i : ι₂) (hi : i ∈ s₂),
  extend.{u_5 + 1, u_4 + 1, u_1 + 1} (β := ι) ((⇑e : (a : ι₂) → ι) : (a : ι₂) → ι) w₂ (0 : ι → k)
      ((e : (a : ι₂) → ι) i : ι) =
    w₂ i
Tactic: convert! hw₂ with i hi
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
⊢ AffineIndependent k p
have inl : ∀ (h : IsEmpty ι), AffineIndependent k p
Tactic: rcases isEmpty_or_nonempty ι with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
inl : ∀ (h : IsEmpty ι), AffineIndependent k p
⊢ AffineIndependent k p
have inr : ∀ (h : Nonempty ι), AffineIndependent k p
Tactic: rcases isEmpty_or_nonempty ι with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
h : Nonempty ι
⊢ AffineIndependent k p
have inr : ∀ (i : ι), AffineIndependent k p
Tactic: obtain ⟨i⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
i : ι
⊢ AffineIndependent k p
have inr : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
Tactic: rw [affineIndependent_iff_linearIndependent_vsub k p i]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hai : AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
i : ι
⊢ LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
have hai₁ : LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
  (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)
Tactic: simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub] at hai
Cleared hypotheses: hai
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
have inl : ∀ (h : IsEmpty ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
Tactic: rcases isEmpty_or_nonempty ι with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
inl : ∀ (h : IsEmpty ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
have inr : ∀ (h : Nonempty ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
Tactic: rcases isEmpty_or_nonempty ι with h | h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
h : Nonempty ι
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
have inr : ∀ (i : ι), AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
Tactic: obtain ⟨i⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
hai : AffineIndependent k p
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
have hai₁ : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
Tactic: rw [affineIndependent_iff_linearIndependent_vsub k p i] at hai
Cleared hypotheses: hai
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
⊢ AffineIndependent.{u_1, u_5, u_6, u_4} k (P := P₂) ((⇑f : (a : P) → P₂) ∘ p)
have inr : LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
  (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)
Tactic: simp_rw [affineIndependent_iff_linearIndependent_vsub k (f ∘ p) i, Function.comp_apply, ←
    f.linearMap_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
⊢ f.linear.ker = ⊥
have rwa : Injective.{u_2 + 1, u_5 + 1} (α := V) (β := V₂) (⇑f.linear : (a : V) → V₂)
Tactic: rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
p : ι → P
f : P →ᵃ[k] P₂
hf : Injective.{u_3 + 1, u_6 + 1} (α := P) (β := P₂) (⇑f : (a : P) → P₂)
i : ι
hai : LinearIndependent.{u_4, u_1, u_2} k (M := V) fun (i_1 : { x : ι // x ≠ i }) ↦ p (↑i_1 : ι) -ᵥ p i
⊢ LinearIndependent.{u_4, u_1, u_5} k (M := V₂) fun (i_1 : { x : ι // x ≠ i }) ↦
    (f.linear : (a : V) → V₂) (p (↑i_1 : ι) -ᵥ p i)
have hf' : f.linear.ker = ⊥
Tactic: have hf' : LinearMap.ker f.linear = ⊥ := by rwa [LinearMap.ker_eq_bot, f.linear_injective_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
V₂ : Type u_5
P₂ : Type u_6
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
s : Set P
e : P ≃ᵃ[k] P₂
⊢ AffineIndependent.{u_1, u_5, u_6, u_6} k (P := P₂) (ι :=
      { x : P₂ // Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x })
      (Subtype.val (p := fun (x : P₂) ↦ Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x)) ↔
    AffineIndependent.{u_1, u_2, u_3, u_3} k (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
have this : Eq (α := { x : P // x ∈ s } → P₂) ((⇑e : (a : P) → P₂) ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))
  (comp (β := { x : P₂ // Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x })
    (Subtype.val (p := fun (x : P₂) ↦ Membership.mem (γ := Set P₂) ((⇑e : (a : P) → P₂) '' s) x))
    (⇑((↑e : P ≃ P₂).image s) : (a : (↑s : Type u_3)) → (↑((⇑(↑e : P ≃ P₂) : (a : P) → P₂) '' s) : Type u_6)))
Tactic: have : e ∘ ((↑) : s → P) = ((↑) : e '' s → P₂) ∘ (e : P ≃ P₂).image s := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
⊢ Eq (α := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) (affineSpan k (p '' (s₁ ∩ s₂)))
have h : ∀ (p' : P),
  Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) p' ↔
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s₁ ∩ s₂))) p'
Tactic: ext p'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
p' : P
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' s₁) ⊓ affineSpan k (p '' s₂)) p' ↔
    Membership.mem (γ := AffineSubspace k P) (affineSpan k (p '' (s₁ ∩ s₂))) p'
have h : ((∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ↔
  ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
Tactic: simp_rw [AffineSubspace.mem_inf_iff, Set.image_eq_range, mem_affineSpan_iff_eq_affineCombination,
    ← Finset.eq_affineCombination_subset_iff_eq_affineCombination_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
p' : P
⊢ ((∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
      ∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₂ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ↔
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
have h : ((∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) →
  ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
p' : P
h :
  ((∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
      ∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₂ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) →
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
⊢ ((∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₁ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
      ∃ (fs : Finset ι),
        (↑fs : Set ι) ⊆ s₂ ∧
          ∃ (w : ι → k),
            Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ↔
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
have h₁ : (∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) →
  (∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₁ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w) ∧
    ∃ (fs : Finset ι),
      (↑fs : Set ι) ⊆ s₂ ∧
        ∃ (w : ι → k), Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧ p' = (affineCombination k fs p : (a : ι → k) → P) w
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Independent (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
inst_4 : Nontrivial k
p : ι → P
ha : AffineIndependent k p
s₁ s₂ : Set ι
fs₁ : Finset ι
hfs₁ : (↑fs₁ : Set ι) ⊆ s₁
w₁ : ι → k
hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1
fs₂ : Finset ι
hfs₂ : (↑fs₂ : Set ι) ⊆ s₂
w₂ : ι → k
hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1
hw₁₂ :
  Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
    ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)
⊢ ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)
have h : ∀
  (ha :
    ∀ (s1 s2 : Finset ι) (w1 w2 : ι → k),
      Eq.{u_1 + 1} (α := k) (∑ i ∈ s1, w1 i) 1 →
        Eq.{u_1 + 1} (α := k) (∑ i ∈ s2, w2 i) 1 →
          Eq.{u_3 + 1} (α := P) ((affineCombination k s1 p : (a : ι → k) → P) w1 : P)
              ((affineCombination k s2 p : (a : ι → k) → P) w2 : P) →
            (↑s1 : Set ι).indicator w1 = (↑s2 : Set ι).indicator w2)
  (s₁ s₂ : Set ι) (fs₁ : Finset ι) (hfs₁ : (↑fs₁ : Set ι) ⊆ s₁) (w₁ : ι → k)
  (hw₁ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₁, w₁ i) 1) (fs₂ : Finset ι) (hfs₂ : (↑fs₂ : Set ι) ⊆ s₂) (w₂ : ι → k)
  (hw₂ : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs₂, w₂ i) 1)
  (hw₁₂ :
    Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
      ((affineCombination k fs₂ p : (a : ι → k) → P) w₂ : P)),
  ∃ (fs : Finset ι),
    (↑fs : Set ι) ⊆ s₁ ∩ s₂ ∧
      ∃ (w : ι → k),
        Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 1 ∧
          Eq.{u_3 + 1} (α := P) ((affineCombination k fs₁ p : (a : ι → k) → P) w₁ : P)
            ((affineCombination k fs p : (a : ι → k) → P) w : P)
Tactic: rw [affineIndependent_iff_indicator_eq_of_affineCombination_eq] at ha
Cleared hypotheses: ha, s₁, s₂, fs₁, hfs₁, w₁, hw₁, fs₂, hfs₂, w₂, hw₂, hw₁₂