awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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 }
i : (↑ps : Type u_3)
left : Membership.mem (γ := Finset (↑ps : Type u_3)) univ i
⊢ Membership.mem (α := ι) s ((f'e : (a : (↑ps : Type u_3)) → ι) i : ι)

Tactic:
exact (hf' i).1

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
right : (f'e : (a : (↑ps : Type u_3)) → ι) (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯) = x
⊢ ∃ (a : (↑ps : Type u_3)),
    Membership.mem (γ := Finset (↑ps : Type u_3)) univ a ∧ (f'e : (a : (↑ps : Type u_3)) → ι) a = x

Tactic:
use ⟨p x, hps.symm ▸ Set.mem_image_of_mem _ hx⟩, mem_univ _

Premises used: Finset.mem_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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

Tactic:
hi _ (hf' _).1 _ hx ?_

Premises used: And.left, Classical.choose
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
right : p (f' (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯)) = p x
⊢ (f'e : (a : (↑ps : Type u_3)) → ι) (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯) = x

Tactic:
refine hi _ (hf' _).1 _ hx ?_

Premises used: And.left
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
right right₁ : (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯) : P) = p x
⊢ p (f' (Subtype.mk (p := fun (x : P) ↦ x ∈ ps) (p x) ⋯)) = p x

Tactic:
rw [(hf' _).2]

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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

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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
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)
⊢ centroid k s p = centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)

Tactic:
rw [← hu, centroid_map]

Premises used: Finset.centroid_map
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
e_p : ∀ (x : (↑ps : Type u_3)), (p ∘ (⇑f'e : (a : (↑ps : Type u_3)) → ι)) x = (↑x : P)
⊢ 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:
congr with x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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)
e_p : p (f' x) = (↑x : P)
⊢ (p ∘ (⇑f'e : (a : (↑ps : Type u_3)) → ι)) x = (↑x : P)

Tactic:
change p (f' x) = ↑x
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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)
e_p e_p₁ : (↑x : P) = (↑x : P)
⊢ p (f' x) = (↑x : P)

Tactic:
rw [(hf' x).2]

Premises used: And.right
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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₂
rw₁ 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))
⊢ centroid k s 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]

Premises used: Finset.centroid_eq_centroid_image_of_inj_on, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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₂
classical₁ 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))
⊢ centroid k s 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]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
have h := s.sum_centroidWeights_eq_one_of_nonempty k hs
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
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)
⊢ centroid k s p -ᵥ p₀ = centroid k s fun (i : ι) ↦ p i -ᵥ p₀

Tactic:
simp only [centroid_def]

Premises used: Finset.centroid_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
⊢ (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:
grind [sum_smul_vsub_const_eq_affineCombination_vsub, affineCombination_eq_linear_combination]

Premises used: Finset.affineCombination_eq_linear_combination, Finset.sum_smul_vsub_const_eq_affineCombination_vsub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
h : Ne.{u_1 + 1} (α := k) (↑(#s) : k) 0
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (centroid k s p)

Tactic:
affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_cast_card_ne_zero h) p

Premises used: Set.Mem, affineCombination_mem_affineSpan, Finset.centroid, Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
inst_4 : CharZero k
s : Finset ι
p : ι → P
h : #s ≠ 0
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (centroid k s p)

Tactic:
affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_card_ne_zero k h) p

Premises used: Set.Mem, affineCombination_mem_affineSpan, Finset.sum_centroidWeights_eq_one_of_card_ne_zero, Finset.centroid
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
inst_4 : CharZero k
s : Finset ι
p : ι → P
h : s.Nonempty
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (centroid k s p)

Tactic:
affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_nonempty k h) p

Premises used: Set.Mem, affineCombination_mem_affineSpan, Finset.sum_centroidWeights_eq_one_of_nonempty, Finset.centroid
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
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
inst_4 : CharZero k
s : Finset ι
p : ι → P
n : ℕ
h : #s = n + 1
⊢ Membership.mem (γ := AffineSubspace k P) (affineSpan k (Set.range p)) (centroid k s p)

Tactic:
affineCombination_mem_affineSpan (s.sum_centroidWeights_eq_one_of_card_eq_add_one k h) p

Premises used: Set.Mem, affineCombination_mem_affineSpan, Finset.sum_centroidWeights_eq_one_of_card_eq_add_one, Finset.centroid
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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)
⊢ ∀ (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'

Premises used: mem_affineSpan_pair_iff_exists_lineMap_eq
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'
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)
⊢ ∃ (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'

Tactic:
obtain ⟨r, rfl⟩ := hp' i

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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
i : (↑s : Type u_4)
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)
⊢ 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 :
          (j : ι) → k) :
      P)
    ((AffineMap.lineMap (p (↑i : ι)) ((Finset.affineCombination k (fs i) p : (a : ι → k) → P) (w i)) : (a : k) → P) r :
      P)

Tactic:
simp [hfs]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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
i : (↑s : Type u_4)
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:
exact ⟨r, by simp [hfs]⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Ceva
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'

Tactic:
have hp'' : ∀ i : s, ∃ r : k, (fs i).affineCombination k p
      (AffineMap.lineMap (Pi.single (i : ι) 1) (w i) r) = p' := by
    intro i
    simp_rw [mem_affineSpan_pair_iff_exists_lineMap_eq] at hp'
    obtain ⟨r, rfl⟩ := hp' i
    exact ⟨r, by simp [hfs]⟩