awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι2 : Type u_5
f : ι2 ↪ ι
p : ι → P
ha : AffineIndependent k p
intro intro₁ intro₂ intro₃ intro₄ intro₅ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₆ intro₇ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs), w i0 = 0
intro₈ :
  ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
    (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V))
    (i0 : ι2) (hi0 : i0 ∈ fs),
    let w' : (i : ι) → k := fun (i : ι) ↦
      if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
      else 0;
    ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2), w i0 = 0
⊢ AffineIndependent.{u_1, u_2, u_3, u_5} k (ι := ι2) (p ∘ (⇑f : (a : ι2) → ι))
have intro₉ : ∀ (fs : Finset ι2) (w : ι2 → k) (hw : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs, w i) 0)
  (hs : Eq.{u_2 + 1} (α := V) ((fs.weightedVSub (p ∘ (⇑f : (a : ι2) → ι)) : (a : ι2 → k) → V) w : V) (0 : V)) (i0 : ι2)
  (hi0 : i0 ∈ fs),
  let fs' := map f fs;
  let w' : (i : ι) → k := fun (i : ι) ↦
    if h : ∃ (i2 : ι2), (f : (a : ι2) → ι) i2 = i then w (h.choose (p := fun (i2 : ι2) ↦ (f : (a : ι2) → ι) i2 = i))
    else 0;
  ∀ (hw' : ∀ (i2 : ι2), w' ((f : (a : ι2) → ι) i2) = w i2) (hw's : Eq.{u_1 + 1} (α := k) (∑ i ∈ fs', w' i) 0), w i0 = 0
Tactic: classical
    intro fs w hw hs i0 hi0
    let fs' := fs.map f
    let w' i := if h : ∃ i2, f i2 = i then w h.choose else 0
    have hw' : ∀ i2 : ι2, w' (f i2) = w i2 := by
      intro i2
      have h : ∃ i : ι2, f i = f i2 := ⟨i2, rfl⟩
      have hs : h.choose = i2 := f.injective h.choose_spec
      simp_rw [w', dif_pos h, hs]
    have hw's : ∑ i ∈ fs', w' i = 0 := by
      rw [← hw, Finset.sum_map]
      simp [hw']
    have hs' : fs'.weightedVSub p w' = (0 : V) := by
      rw [← hs, Finset.weightedVSub_map]
      congr with i
      simp_all only [comp_apply]
    rw [← ha fs' w' hw's hs' (f i0) ((Finset.mem_map' _).2 hi0), hw']
-- 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
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
⊢ AffineIndependent k (P := P) fun (x : (↑(Set.range p) : Type u_3)) ↦ (↑x : P)
have hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
Tactic: have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
fe : Embedding.{u_3 + 1, u_4 + 1} (↑(Set.range p) : Type u_3) ι := { toFun := f, inj' := ⋯ }
⊢ AffineIndependent k (P := P) fun (x : (↑(Set.range p) : Type u_3)) ↦ (↑x : P)
have h : ∀ (x : (↑(Set.range p) : Type u_3)),
  Eq (α := (self : { x : P // x ∈ Set.range p }) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ Set.range p))
    (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι))
Tactic: convert! ha.comp_embedding fe
-- 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
p : ι → P
ha : AffineIndependent k p
f : (↑(Set.range p) : Type u_3) → ι :=
  fun (x : (↑(Set.range p) : Type u_3)) ↦ Exists.choose (p := fun (y : ι) ↦ p y = (↑x : P)) ⋯
hf : ∀ (x : (↑(Set.range p) : Type u_3)), p (f x) = (↑x : P)
fe : Embedding.{u_3 + 1, u_4 + 1} (↑(Set.range p) : Type u_3) ι := { toFun := f, inj' := ⋯ }
x : (↑(Set.range p) : Type u_3)
⊢ Eq (α := (self : { x : P // x ∈ Set.range p }) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ Set.range p))
    (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι))
have h : ∀ (x : { x : P // x ∈ Set.range p }), (↑x : P) = (p ∘ (⇑fe : (a : (↑(Set.range p) : Type u_3)) → ι)) x
Tactic: ext
-- 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
e : ι ≃ ι'
p : ι' → P
⊢ AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι')) ↔ AffineIndependent k p
have refine : AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι')) → AffineIndependent k p
Tactic: refine ⟨?_, AffineIndependent.comp_embedding e.toEmbedding⟩
-- 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
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι'))
⊢ p = p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)
have h₁ : ∀ (x : ι'),
  p x = (p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)) x
Tactic: ext
-- 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
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι'))
⊢ AffineIndependent k p
have this : p = p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)
Tactic: have : p = p ∘ e ∘ e.symm.toEmbedding := by
    ext
    simp
-- 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
e : ι ≃ ι'
p : ι' → P
h : AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι'))
this : p = p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)
⊢ AffineIndependent k p
have rw : AffineIndependent k (ι := ι')
  (p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι))
Tactic: rw [this]
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k ![p₂, p₁, p₃]
have rw : AffineIndependent k (ι := Fin (Nat.succ 0).succ.succ)
  (![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ))
Tactic: rw [← affineIndependent_equiv (Equiv.swap 0 1)]
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k (ι := Fin (Nat.succ 0).succ.succ)
    (![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ))
have h₁ : ![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]
Tactic: convert! h using 1
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ ![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]
have h₁ : ∀ (x : Fin (Nat.succ 0).succ.succ),
  (![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
Tactic: ext x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₁ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₂, p₁, p₃]
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
h₁ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₂, p₁, p₃]
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ (![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₂ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₂, p₁, p₃]
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
h₁ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₂, p₁, p₃]
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₂, p₁, p₃]
      (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ (![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₃ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₂, p₁, p₃]
    (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k ![p₁, p₃, p₂]
have rw : AffineIndependent k (ι := Fin (Nat.succ 0).succ.succ)
  (![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ))
Tactic: rw [← affineIndependent_equiv (Equiv.swap 1 2)]
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k (ι := Fin (Nat.succ 0).succ.succ)
    (![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ))
have h₁ : ![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]
Tactic: convert! h using 1
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ ![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]
have h₁ : ∀ (x : Fin (Nat.succ 0).succ.succ),
  (![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
Tactic: ext x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₁ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₁, p₃, p₂]
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
h₁ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₁, p₃, p₂]
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ (![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₂ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₁, p₃, p₂]
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
h₁ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₁, p₃, p₂]
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₁, p₃, p₂]
      (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ (![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₃ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₁, p₃, p₂]
    (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k ![p₃, p₂, p₁]
have rw : AffineIndependent k (ι := Fin (Nat.succ 0).succ.succ)
  (![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ))
Tactic: rw [← affineIndependent_equiv (Equiv.swap 0 2)]
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ AffineIndependent k (ι := Fin (Nat.succ 0).succ.succ)
    (![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ))
have h₁ : ![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]
Tactic: convert! h using 1
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
⊢ ![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]
have h₁ : ∀ (x : Fin (Nat.succ 0).succ.succ),
  (![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
Tactic: ext x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
⊢ (![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₁ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₃, p₂, p₁]
    (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
h₁ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₃, p₂, p₁]
      (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ (![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₂ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₃, p₂, p₁]
    (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
p₁ p₂ p₃ : P
h : AffineIndependent k ![p₁, p₂, p₃]
x : Fin (Nat.succ 0).succ.succ
h₁ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₃, p₂, p₁]
      (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₂ :
  comp (α := Fin (Nat.succ 0).succ.succ) ![p₃, p₂, p₁]
      (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
      ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ (![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)) x =
    ![p₁, p₂, p₃] x
have h₃ : comp (α := Fin (Nat.succ 0).succ.succ) ![p₃, p₂, p₁]
    (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, sorry⟩ : Fin (Nat.succ 0).succ.succ)) =
  ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, sorry⟩)
Tactic: fin_cases x
Cleared hypotheses: x
-- 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
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
⊢ w i = 0
have obtain : ∀ (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
Tactic: obtain ⟨fs', w', hfs's, hw', he⟩ := eq_affineCombination_of_mem_affineSpan_image hm
-- 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
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)
⊢ (↑fs : Set ι).indicator w i = 0
have rw : (↑fs' : Set ι).indicator w' i = 0
Tactic: rw [ha.indicator_eq_of_affineCombination_eq fs fs' w w' hw hw' he]