awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
t : Set P
ht : Eq (α := AffineSubspace k P) (affineSpan k t) ⊤
s : Set P
hst : s ⊆ t
h_tot : Eq (α := AffineSubspace k P) (affineSpan k s) (affineSpan k t)
h_ind :
  AffineIndependent.{u_5, u_6, u_7, u_7} k (P := P) (ι := { x : P // x ∈ s }) (Subtype.val (p := fun (x : P) ↦ x ∈ s))
rw : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
rw₁ : Eq (α := AffineSubspace k P) (affineSpan k t) ⊤
rw₂ rw₃ : Eq.{u_7 + 1} (α := AffineSubspace k P) ⊤ ⊤
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range (ι := (↑s : Type u_7)) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) ⊤

Tactic:
rw [Subtype.range_coe, h_tot, ht]

Premises used: Subtype.range_coe
-- Module: Mathlib.LinearAlgebra.AffineSpace.Basis
Goal:
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : DivisionRing k
inst_3 : Module k V
⊢ ∃ (s : Set P) (b : AffineBasis (↑s : Type u_7) k P),
    Eq (α := (a : (↑s : Type u_7)) → P) (⇑b : (a : (↑s : Type u_7)) → P) (Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
let ⟨s, _, hs⟩ := exists_affine_subbasis (AffineSubspace.span_univ k V P)
  ⟨s, hs⟩

Premises used: Exists, AffineSubspace.span_univ, Exists.intro, AffineBasis.exists_affine_subbasis, Subtype.val, Eq, DFunLike.coe, _private.0.AffineBasis.exists_affineBasis.match_1
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
i : ι
⊢ centroidWeights k s i = (↑(#s) : k)⁻¹

Tactic:
rfl

Premises used: Finset.centroidWeights, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
⊢ centroidWeights k s = Function.const ι (↑(#s) : k)⁻¹

Tactic:
rfl

Premises used: Finset.centroidWeights, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
h : Ne.{u_1 + 1} (α := k) (↑(#s) : k) 0
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
h : #s ≠ 0
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
h : s.Nonempty
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
s.sum_centroidWeights_eq_one_of_card_ne_zero k (ne_of_gt (card_pos.2 h))

Premises used: Iff.mpr, ne_of_gt, Finset.sum_centroidWeights_eq_one_of_card_ne_zero, Finset.card_pos
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
n : ℕ
h : #s = n + 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
s.sum_centroidWeights_eq_one_of_card_ne_zero k (h.symm ▸ Nat.succ_ne_zero n)

Premises used: Eq.rec, Finset.sum_centroidWeights_eq_one_of_card_ne_zero, Nat.succ_ne_zero, Eq.symm
-- 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
⊢ centroid k s p = (affineCombination k s p : (a : ι → k) → P) (centroidWeights k s)

Tactic:
rfl

Premises used: Finset.centroid, 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
s : Finset P
rw :
  Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P) (centroidWeights k univ) :
      P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)
⊢ centroid k (ι := ↥s) univ (Subtype.val (p := fun (x : P) ↦ x ∈ s)) = centroid k s id

Tactic:
rw [centroid, centroid, ← s.attach_affineCombination_coe]

Premises used: Finset.attach_affineCombination_coe, 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
s : Finset P
h : Eq (α := ↥s → k) (centroidWeights k univ) (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))
⊢ Eq.{u_3 + 1} (α := P)
    ((affineCombination k univ (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P) (centroidWeights k univ) :
      P)
    ((affineCombination k s.attach (Subtype.val (p := fun (x : P) ↦ x ∈ s)) : (a : ↥s → k) → P)
        (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) :
      P)

Tactic:
congr
-- 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
s : Finset P
h : ∀ (x : ↥s), centroidWeights k univ x = (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) x
⊢ Eq (α := ↥s → k) (centroidWeights k univ) (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))

Tactic:
ext
-- 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
s : Finset P
x : ↥s
⊢ centroidWeights k univ x = (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) x

Tactic:
simp
-- 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
p : ι → P
i : ι
⊢ centroid k {i} p = p i

Tactic:
simp [centroid_def, affineCombination_apply]

Premises used: Finset.affineCombination_apply, 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
inst_4 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
pos : ∀ (h : i₁ = i₂), centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁
neg : ∀ (h : ¬i₁ = i₂), centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁
⊢ centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
by_cases h : i₁ = i₂
-- 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 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
h : i₁ = i₂
⊢ centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
simp [h]
-- 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 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
rw : Ne.{u_1 + 1} (α := k) (↑(HAdd.hAdd (α := ℕ) 1 1) : k) 0
⊢ Ne.{u_1 + 1} (α := k) (↑(card (α := ι) {i₁, i₂}) : k) 0

Tactic:
rw [card_insert_of_notMem (notMem_singleton.2 h), card_singleton]

Premises used: Finset.notMem_singleton, Iff.mpr, Finset.card_insert_of_notMem, Finset.card_singleton
-- 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 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ Ne.{u_1 + 1} (α := k) (↑(HAdd.hAdd (α := ℕ) 1 1) : k) 0

Tactic:
simpa using Invertible.ne_zero _

Premises used: Invertible.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 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
⊢ Ne.{u_1 + 1} (α := k) (↑(card (α := ι) {i₁, i₂}) : k) 0

Tactic:
have hc : (#{i₁, i₂} : k) ≠ 0 := by
      rw [card_insert_of_notMem (notMem_singleton.2 h), card_singleton]
      simpa using Invertible.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 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : Ne.{u_1 + 1} (α := k) (↑(card (α := ι) {i₁, i₂}) : k) 0
neg :
  HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((weightedVSubOfPoint {i₁, i₂} p (p i₁) : (a : ι → k) → V) (centroidWeights k {i₁, i₂}) : V) (p i₁) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁
⊢ centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
rw [centroid_def,
      affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
        (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]

Premises used: Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Finset.sum_centroidWeights_eq_one_of_cast_card_ne_zero, 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
inst_4 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
h : ¬i₁ = i₂
hc : Ne.{u_1 + 1} (α := k) (↑(card (α := ι) {i₁, i₂}) : k) 0
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V)
      ((weightedVSubOfPoint {i₁, i₂} p (p i₁) : (a : ι → k) → V) (centroidWeights k {i₁, i₂}) : V) (p i₁) =
    HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁

Tactic:
simp [h, one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- 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
inst_4 : Invertible (α := k) 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
centroid_pair k p 0 1

Premises used: Finset.centroid_pair, OfNat.ofNat
-- 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
inst_4 : Invertible (α := k) 2
p : Fin 2 → P
⊢ centroid k {0, 1} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p 1 -ᵥ p 0) +ᵥ p 0

Tactic:
convert! centroid_pair k p 0 1

Premises used: Finset.centroid_pair, OfNat.ofNat
-- 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
ι₂ : Type u_5
s₂ : Finset ι₂
e : ι₂ ↪ ι
p : ι → P
⊢ centroid k (map e s₂) p = centroid k s₂ (p ∘ (⇑e : (a : ι₂) → ι))

Tactic:
simp [centroid_def, affineCombination_map, centroidWeights]

Premises used: Finset.affineCombination_map, Finset.centroidWeights, Finset.centroid_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
⊢ centroidWeightsIndicator k s = (↑s : Set ι).indicator (centroidWeights k s)

Tactic:
rfl

Premises used: Finset.centroidWeightsIndicator, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : Fintype ι
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, centroidWeightsIndicator k s i) (∑ i ∈ s, centroidWeights k s i)

Tactic:
sum_indicator_subset _ (subset_univ _)

Premises used: Finset.centroidWeightsIndicator, Finset.sum_indicator_subset, Finset.subset_univ
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
h : #s ≠ 0
rw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, centroidWeightsIndicator k s i) 1

Tactic:
rw [sum_centroidWeightsIndicator]

Premises used: Finset.sum_centroidWeightsIndicator
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
h : #s ≠ 0
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
s.sum_centroidWeights_eq_one_of_card_ne_zero k h

Premises used: Finset.sum_centroidWeights_eq_one_of_card_ne_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
h : #s ≠ 0
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_card_ne_zero k h

Premises used: Finset.sum_centroidWeights_eq_one_of_card_ne_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
h : s.Nonempty
rw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, centroidWeightsIndicator k s i) 1

Tactic:
rw [sum_centroidWeightsIndicator]

Premises used: Finset.sum_centroidWeightsIndicator
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
h : s.Nonempty
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
s.sum_centroidWeights_eq_one_of_nonempty k h

Premises used: Finset.sum_centroidWeights_eq_one_of_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
h : s.Nonempty
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_nonempty k h

Premises used: Finset.sum_centroidWeights_eq_one_of_nonempty
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
n : ℕ
h : #s = n + 1
rw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i : ι, centroidWeightsIndicator k s i) 1

Tactic:
rw [sum_centroidWeightsIndicator]

Premises used: Finset.sum_centroidWeightsIndicator
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
n : ℕ
h : #s = n + 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
s.sum_centroidWeights_eq_one_of_card_eq_add_one k h

Premises used: Finset.sum_centroidWeights_eq_one_of_card_eq_add_one
-- Module: Mathlib.LinearAlgebra.AffineSpace.Centroid
Goal:
k : Type u_1
inst : DivisionRing k
ι : Type u_4
s : Finset ι
inst_1 : CharZero k
inst_2 : Fintype ι
n : ℕ
h : #s = n + 1
⊢ Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1

Tactic:
exact s.sum_centroidWeights_eq_one_of_card_eq_add_one k h

Premises used: Finset.sum_centroidWeights_eq_one_of_card_eq_add_one
-- 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 : Fintype ι
p : ι → P
⊢ centroid k s p = (affineCombination k univ p : (a : ι → k) → P) (centroidWeightsIndicator k s)

Tactic:
affineCombination_indicator_subset _ _ (subset_univ _)

Premises used: Finset.centroidWeightsIndicator, Finset.affineCombination_indicator_subset, Finset.centroid, Finset.subset_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)) ⋯
⊢ ∀ (x : (↑(p '' (↑s : Set ι)) : Type u_3)), f x ∈ s ∧ p (f x) = (↑x : P)

Tactic:
have hf : ∀ x, f x ∈ s ∧ p (f x) = x := fun x => x.property.choose_spec
-- 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) ⋯)
⊢ ∀ (x : (↑ps : Type u_3)), f' x ∈ s ∧ p (f' x) = (↑x : P)

Tactic:
have hf' : ∀ x, f' x ∈ s ∧ p (f' x) = x := fun x => hf ⟨x, hps ▸ x.property⟩
-- 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)
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)
rw₃ rw₄ : p (f' y) = p (f' y)
⊢ x = y

Tactic:
rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]

Premises used: Subtype.ext_iff, 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)
⊢ 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]
-- 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 }
h : ∀ (x : ι), x ∈ map f'e univ ↔ x ∈ s
⊢ map f'e univ = s

Tactic:
ext 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 }
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
⊢ x ∈ map f'e univ ↔ x ∈ s

Tactic:
rw [mem_map]

Premises used: Finset.mem_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 }
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
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
⊢ (∃ (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
-- 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:
(hf' i).1

Premises used: Set.Mem, setOf, And.left, Classical.choose