awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
refine : AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι')) → AffineIndependent k p
⊢ AffineIndependent.{u_1, u_2, u_3, u_4} k (ι := ι) (p ∘ (⇑e : (a : ι) → ι')) ↔ AffineIndependent k p

Tactic:
refine ⟨?_, AffineIndependent.comp_embedding e.toEmbedding⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 : ι) → ι'))
h₁ :
  ∀ (x : ι'),
    p x = (p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)) x
⊢ p = p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 : ι) → ι'))
x : ι'
⊢ p x = (p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι)) x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 : ι') → ι)

Tactic:
have : p = p ∘ e ∘ e.symm.toEmbedding := by
    ext
    simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 : ι') → ι)
rw :
  AffineIndependent k (ι := ι')
    (p ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι))
⊢ AffineIndependent k p

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι))

Tactic:
h.comp_embedding e.symm.toEmbedding

Premises used: AffineIndependent.comp_embedding, Equiv.toEmbedding, Equiv.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 ∘ comp.{u_5 + 1, u_4 + 1, u_5 + 1} (β := ι) (⇑e : (a : ι) → ι') (⇑e.symm.toEmbedding : (a : ι') → ι))

Tactic:
exact h.comp_embedding e.symm.toEmbedding

Premises used: AffineIndependent.comp_embedding, Equiv.toEmbedding, Equiv.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
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))
⊢ AffineIndependent k ![p₂, p₁, p₃]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap 0 1)]

Premises used: affineIndependent_equiv, Equiv.swap, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]

Tactic:
h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
h₁ : ![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![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))

Tactic:
convert! h using 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
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
⊢ ![p₂, p₁, p₃] ∘ (⇑(Equiv.swap 0 1) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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, ⋯⟩)
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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ (![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:
fin_cases x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
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))
⊢ AffineIndependent k ![p₁, p₃, p₂]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap 1 2)]

Premises used: affineIndependent_equiv, Equiv.swap, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
h₁ : ![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![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))

Tactic:
convert! h using 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
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
⊢ ![p₁, p₃, p₂] ∘ (⇑(Equiv.swap 1 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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, ⋯⟩)
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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ (![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:
fin_cases x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
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))
⊢ AffineIndependent k ![p₃, p₂, p₁]

Tactic:
rw [← affineIndependent_equiv (Equiv.swap 0 2)]

Premises used: affineIndependent_equiv, Equiv.swap, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
h₁ : ![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![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))

Tactic:
convert! h using 1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
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
⊢ ![p₃, p₂, p₁] ∘ (⇑(Equiv.swap 0 2) : (a : Fin (Nat.succ 0).succ.succ) → Fin (Nat.succ 0).succ.succ) = ![p₁, p₂, p₃]

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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, ⋯⟩)
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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ (![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:
fin_cases x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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₃]
⊢ 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, ⋯⟩ : Fin (Nat.succ 0).succ.succ)) =
    ![p₁, p₂, p₃] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
s t : Set P
ha : AffineIndependent k (P := P) fun (x : (↑t : Type u_3)) ↦ (↑x : P)
hs : s ⊆ t
⊢ AffineIndependent k (P := P) fun (x : (↑s : Type u_3)) ↦ (↑x : P)

Tactic:
ha.comp_embedding (s.embeddingOfSubset t hs)

Premises used: Set.Mem, AffineIndependent.comp_embedding, Set.embeddingOfSubset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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 := P) fun (x : (↑(Set.range p) : Type u_3)) ↦ (↑x : P)
hi : Injective p
⊢ AffineIndependent k p

Tactic:
ha.comp_embedding
    (⟨fun i => ⟨p i, Set.mem_range_self _⟩, fun _ _ h => hi (Subtype.mk_eq_mk.1 h)⟩ :
      ι ↪ Set.range p)

Premises used: Set.mem_range_self, AffineIndependent.comp_embedding, Function.Embedding.mk, Subtype.mk, Subtype.mk_eq_mk, Iff.mp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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
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
⊢ w i = 0

Tactic:
obtain ⟨fs', w', hfs's, hw', he⟩ := eq_affineCombination_of_mem_affineSpan_image hm

Premises used: eq_affineCombination_of_mem_affineSpan_image
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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)
rw : (↑fs' : Set ι).indicator w' i = 0
⊢ (↑fs : Set ι).indicator w i = 0

Tactic:
rw [ha.indicator_eq_of_affineCombination_eq fs fs' w w' hw hw' he]

Premises used: AffineIndependent.indicator_eq_of_affineCombination_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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

Tactic:
Set.indicator_of_notMem (Set.notMem_subset hfs's his) w'

Premises used: Set.indicator_of_notMem, Set.notMem_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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

Tactic:
exact Set.indicator_of_notMem (Set.notMem_subset hfs's his) w'

Premises used: Set.indicator_of_notMem, Set.notMem_subset
-- Module: Mathlib.LinearAlgebra.AffineSpace.Independent
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

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'