awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
x y : (↑ps : Type u_3)
h : f' x = f' y
rw : (↑x : P) = (↑y : P)
rw₁ : p (f' x) = (↑y : P)
rw₂ : p (f' x) = p (f' y)
⊢ x = y
have rw₃ : p (f' y) = p (f' y)
Tactic: rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
⊢ centroid k s p = centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
have hf'i : Function.Injective f'
Tactic: have hf'i : Function.Injective f' := by
    intro x y h
    rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
⊢ map f'e univ = s
have h : ∀ (x : ι), x ∈ map f'e univ ↔ x ∈ s
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
x : ι
⊢ x ∈ map f'e univ ↔ x ∈ s
have h : (∃ (a : (↑ps : Type u_3)),
    Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x) ↔
  x ∈ s
Tactic: rw [mem_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
x : ι
⊢ (∃ (a : (↑ps : Type u_3)),
      Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x) ↔
    x ∈ s
have h : (∃ (a : (↑ps : Type u_3)),
    Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x) →
  x ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
x : ι
h :
  (∃ (a : (↑ps : Type u_3)),
      Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x) →
    x ∈ s
⊢ (∃ (a : (↑ps : Type u_3)),
      Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x) ↔
    x ∈ s
have h₁ : x ∈ s →
  ∃ (a : (↑ps : Type u_3)),
    Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ ∃ (a : (↑ps : Type u_3)),
    Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x
have right : (f'e : (a : (↑ps : Type u_3)) → ι) (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) sorry) = x
Tactic: use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ (f'e : (a : (↑ps : Type u_3)) → ι) (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯) = x
have right : p (f' (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) sorry)) = p x
Tactic: refine hi _ (hf' _).1 _ hx ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
x : ι
hx : x ∈ s
⊢ p (f' (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯)) = p x
have right : (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) sorry) : P) = p x
Tactic: rw [(hf' _).2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
⊢ centroid k s p = centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
have hu : map f'e univ = s
Tactic: have hu : Finset.univ.map f'e = s := by
    ext x
    rw [mem_map]
    constructor
    · rintro ⟨i, _, rfl⟩
      exact (hf' i).1
    · intro hx
      use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _
      refine hi _ (hf' _).1 _ hx ?_
      rw [(hf' _).2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k s p = centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
have rw : centroid k (ι := (↑ps : Type u_3)) univ (p ∘ (⇑f'e : (a : (↑ps : Type u_3)) → ι)) =
  centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
Tactic: rw [← hu, centroid_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
⊢ centroid k (ι := (↑ps : Type u_3)) univ (p ∘ (⇑f'e : (a : (↑ps : Type u_3)) → ι)) =
    centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
have e_p : ∀ (x : (↑ps : Type u_3)), (p ∘ (⇑f'e : (a : (↑ps : Type u_3)) → ι)) x = (↑x : P)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : (↑ps : Type u_3)
⊢ (p ∘ (⇑f'e : (a : (↑ps : Type u_3)) → ι)) x = (↑x : P)
have e_p : p (f' x) = (↑x : P)
Tactic: change p (f' x) = ↑x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
ps : Set P
inst_4 : Fintype (↑ps : Type u_3)
hps : ps = p '' (↑s : Set ι)
f : (↑(p '' (↑s : Set ι)) : Type u_3) → ι :=
  fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ Exists.choose (p := fun (a : ι) ↦ a ∈ (↑s : Set ι) ∧ p a = (↑x : P)) ⋯
hf : ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)
f' : (↑ps : Type u_3) → ι :=
  fun (x : (↑ps : Type u_3)) ↦ f (Subtype.mk (p := fun (x : P) ↦ x ∈ p '' (↑s : Set ι)) (↑x : P) ⋯)
hf' : ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)
hf'i : Function.Injective f'
f'e : Function.Embedding.{u_3 + 1, u_4 + 1} (↑ps : Type u_3) ι := { toFun := f', inj' := hf'i }
hu : map f'e univ = s
x : (↑ps : Type u_3)
⊢ p (f' x) = (↑x : P)
have e_p : (↑x : P) = (↑x : P)
Tactic: rw [(hf' x).2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' (↑s : Set ι) = p₂ '' (↑s₂ : Set ι₂)
⊢ centroid k s p = centroid k s₂ p₂
have rw : (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)) = centroid k s₂ p₂
Tactic: rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' (↑s : Set ι) = p₂ '' (↑s₂ : Set ι₂)
rw : (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)) = centroid k s₂ p₂
⊢ centroid k s p = centroid k s₂ p₂
have rw₁ : Eq.{u_3 + 1} (α := P) (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
  (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
Tactic: rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' (↑s : Set ι) = p₂ '' (↑s₂ : Set ι₂)
⊢ centroid k s p = centroid k s₂ p₂
have classical : (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)) = centroid k s₂ p₂
Tactic: classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
ι₂ : Type u_5
s₂ : Finset ι₂
p : ι → P
hi : ∀ i ∈ s, ∀ j ∈ s, p i = p j → i = j
p₂ : ι₂ → P
hi₂ : ∀ i ∈ s₂, ∀ j ∈ s₂, p₂ i = p₂ j → i = j
he : p '' (↑s : Set ι) = p₂ '' (↑s₂ : Set ι₂)
classical : (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P)) = centroid k s₂ p₂
⊢ centroid k s p = centroid k s₂ p₂
have classical₁ : Eq.{u_3 + 1} (α := P) (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
  (centroid k univ fun (x : (↑(p '' (↑s : Set ι)) : Type u_3)) ↦ (↑x : P))
Tactic: classical rw [s.centroid_eq_centroid_image_of_inj_on k hi rfl,
      s₂.centroid_eq_centroid_image_of_inj_on k hi₂ he]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_4 : CharZero k
p : ι → P
p₀ : P
hs : s.Nonempty
⊢ centroid k s p -ᵥ p₀ = centroid k s fun (i : ι) ↦ p i -ᵥ p₀
have h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
Tactic: have h := s.sum_centroidWeights_eq_one_of_nonempty k hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
inst : DivisionRing k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
ι : Type u_4
s : Finset ι
inst_4 : CharZero k
p : ι → P
p₀ : P
hs : s.Nonempty
h : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
⊢ centroid k s p -ᵥ p₀ = centroid k s fun (i : ι) ↦ p i -ᵥ p₀
have simp : (affineCombination k s p : (a : ι → k) → P) (centroidWeights k s) -ᵥ p₀ =
  (affineCombination k s fun (i : ι) ↦ p i -ᵥ p₀ : (a : ι → k) → V) (centroidWeights k s)
Tactic: simp only [centroid_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (hypothesis)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
hp' :
  ∀ (i : (↑s : Type u_4)),
    Membership.mem (γ := AffineSubspace k P)
      (affineSpan k
        (insert (p (↑i : ι)) (singleton (α := P) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i) : P))))
      p'
i : (↑s : Type u_4)
⊢ ∃ (r : k),
    (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
          (j : ι) → k) =
      p'
have hp'₁ : ∀ (i : (↑s : Type u_4)),
  ∃ (r : k),
    (AffineMap.lineMap (p (↑i : ι)) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i)) : (a : k) → P) r =
      p'
Tactic: simp_rw [mem_affineSpan_pair_iff_exists_lineMap_eq] at hp'
Cleared hypotheses: hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ceva (goal)
Goal:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : ι → P
hp : AffineIndependent k p
s : Set ι
hs : s.Nonempty
fs : (↑s : Type u_4) → Finset ι
hfs : ∀ (i : (↑s : Type u_4)), (↑i : ι) ∈ fs i
w : (↑s : Type u_4) → ι → k
hw : ∀ (i : (↑s : Type u_4)), Eq.{u_1 + 1} (α := k) (∑ j ∈ fs i, w i j) 1
p' : P
i : (↑s : Type u_4)
hp' :
  ∀ (i : (↑s : Type u_4)),
    ∃ (r : k),
      (AffineMap.lineMap (p (↑i : ι)) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i)) : (a : k) → P) r =
        p'
⊢ ∃ (r : k),
    (Finset.affineCombination k (fs i) p : (a : ι → k) → P)
        ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r :
          (j : ι) → k) =
      p'
have obtain : ∀ (r : k)
  (hp' :
    ∀ (i_1 : (↑s : Type u_4)),
      ∃ (r_1 : k),
        Eq.{u_3 + 1} (α := P)
          ((AffineMap.lineMap (p (↑i_1 : ι)) ((Finset.affineCombination k (fs i_1) p : (a : ι → k) → P) (w i_1)) :
                (a : k) → P)
              r_1 :
            P)
          ((AffineMap.lineMap (p (↑i : ι)) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i)) :
                (a : k) → P)
              r :
            P)),
  ∃ (r_1 : k),
    Eq.{u_3 + 1} (α := P)
      ((Finset.affineCombination k (fs i) p : (a : ι → k) → P)
          ((AffineMap.lineMap (Pi.single (M := fun (j : ι) ↦ k) (↑i : ι) 1) (w i) : (a : k) → (j : ι) → k) r_1 :
            (j : ι) → k) :
        P)
      ((AffineMap.lineMap (p (↑i : ι)) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i)) : (a : k) → P)
          r :
        P)
Tactic: obtain ⟨r, rfl⟩ := hp' i
Cleared hypotheses: p', hp'