awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst_4 : Group G
inst_5 : Group G'
inst_6 : DistribMulAction G V
inst_7 : DistribMulAction G' V
inst_8 : SMulCommClass G k V
inst_9 : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
⊢ Eq (α := AffineSubspace k V) (affineSpan k (range (HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)))) ⊤
have rw : Eq (α := AffineSubspace k V) (affineSpan k (range fun (i : ι) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V))) ⊤
Tactic: rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst_4 : Group G
inst_5 : Group G'
inst_6 : DistribMulAction G V
inst_7 : DistribMulAction G' V
inst_8 : SMulCommClass G k V
inst_9 : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
rw :
  Eq (α := AffineSubspace k V) (affineSpan k (range fun (i : ι) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V))) ⊤
⊢ Eq (α := AffineSubspace k V) (affineSpan k (range (HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)))) ⊤
have rw₁ : Eq (α := AffineSubspace k V)
  (affineSpan k (HSMul.hSMul (β := Set V) a (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V)))) ⊤
Tactic: rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst_4 : Group G
inst_5 : Group G'
inst_6 : DistribMulAction G V
inst_7 : DistribMulAction G' V
inst_8 : SMulCommClass G k V
inst_9 : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
rw :
  Eq (α := AffineSubspace k V) (affineSpan k (range fun (i : ι) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V))) ⊤
rw₁ :
  Eq (α := AffineSubspace k V)
    (affineSpan k (HSMul.hSMul (β := Set V) a (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V)))) ⊤
⊢ Eq (α := AffineSubspace k V) (affineSpan k (range (HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)))) ⊤
have rw₂ : HSMul.hSMul (β := AffineSubspace k V) a (affineSpan k (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V))) = ⊤
Tactic: rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst_4 : Group G
inst_5 : Group G'
inst_6 : DistribMulAction G V
inst_7 : DistribMulAction G' V
inst_8 : SMulCommClass G k V
inst_9 : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
rw :
  Eq (α := AffineSubspace k V) (affineSpan k (range fun (i : ι) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V))) ⊤
rw₁ :
  Eq (α := AffineSubspace k V)
    (affineSpan k (HSMul.hSMul (β := Set V) a (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V)))) ⊤
rw₂ : HSMul.hSMul (β := AffineSubspace k V) a (affineSpan k (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V))) = ⊤
⊢ Eq (α := AffineSubspace k V) (affineSpan k (range (HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)))) ⊤
have rw₃ : HSMul.hSMul (β := AffineSubspace k V) a ⊤ = ⊤
Tactic: rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
G : Type u_3
G' : Type u_4
k : Type u_5
V : Type u_6
P : Type u_7
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b_1 : AffineBasis ι k P
s : Finset ι
i j : ι
e : ι ≃ ι'
inst_4 : Group G
inst_5 : Group G'
inst_6 : DistribMulAction G V
inst_7 : DistribMulAction G' V
inst_8 : SMulCommClass G k V
inst_9 : SMulCommClass G' k V
a : G
b : AffineBasis ι k V
rw :
  Eq (α := AffineSubspace k V) (affineSpan k (range fun (i : ι) ↦ HSMul.hSMul (β := V) a ((b : (a : ι) → V) i : V))) ⊤
rw₁ :
  Eq (α := AffineSubspace k V)
    (affineSpan k (HSMul.hSMul (β := Set V) a (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V)))) ⊤
rw₂ : HSMul.hSMul (β := AffineSubspace k V) a (affineSpan k (range.{u_6, u_1 + 1} (ι := ι) (⇑b : (a : ι) → V))) = ⊤
rw₃ : HSMul.hSMul (β := AffineSubspace k V) a ⊤ = ⊤
⊢ Eq (α := AffineSubspace k V) (affineSpan k (range (HSMul.hSMul (β := (a : ι) → V) a (⇑b : (a : ι) → V)))) ⊤
have rw₄ : Eq.{u_6 + 1} (α := AffineSubspace k V) ⊤ ⊤
Tactic: rw [Pi.smul_def, ← smul_set_range, ← AffineSubspace.smul_span, b.tot,
          AffineSubspace.smul_top (Group.isUnit a)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).basisOf i = a • b.basisOf i
have a₁ : ∀ (j : { j : ι // j ≠ i }),
  Eq.{u_6 + 1} (α := V) (((a • b).basisOf i : (a : { j : ι // j ≠ i }) → V) j : V)
    ((a • b.basisOf i : (a : { j : ι // j ≠ i }) → V) j : V)
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst : AddCommGroup V
inst_1 : Ring k
inst_2 : Module k V
inst_3 : Group G
inst_4 : DistribMulAction G V
inst_5 : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).coord i =
    (b.coord i).comp (LinearMap.toAffineMap (↑(LinearEquiv.symm (DistribMulAction.toLinearEquiv k V a)) : V →ₗ[k] V))
have h : ∀ (v : V),
  Eq.{u_5 + 1} (α := k) (((a • b).coord i : (a : V) → k) v : k)
    (((b.coord i).comp
            (LinearMap.toAffineMap (↑(LinearEquiv.symm (DistribMulAction.toLinearEquiv k V a)) : V →ₗ[k] V)) :
          (a : V) → k)
        v :
      k)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) (Finset.centroid k s (⇑b : (a : ι) → P)) : k) ((↑s.card : k)⁻¹ : k)
have rw : Eq.{u_5 + 1} (α := k)
  ((b.coord i : (a : P) → k)
      ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Finset.centroidWeights k s) : P) :
    k)
  ((↑s.card : k)⁻¹ : k)
Tactic: rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
rw :
  Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k)
        ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Finset.centroidWeights k s) : P) :
      k)
    ((↑s.card : k)⁻¹ : k)
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) (Finset.centroid k s (⇑b : (a : ι) → P)) : k) ((↑s.card : k)⁻¹ : k)
have rw₁ : Finset.centroidWeights k s i = (↑s.card : k)⁻¹
Tactic: rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
rw :
  Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k)
        ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Finset.centroidWeights k s) : P) :
      k)
    ((↑s.card : k)⁻¹ : k)
rw₁ : Finset.centroidWeights k s i = (↑s.card : k)⁻¹
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) (Finset.centroid k s (⇑b : (a : ι) → P)) : k) ((↑s.card : k)⁻¹ : k)
have rw₂ : Eq.{u_5 + 1} (α := k) (Function.const ι (↑s.card : k)⁻¹ i) (↑s.card : k)⁻¹
Tactic: rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
Goal:
ι : Type u_1
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
inst_4 : CharZero k
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∈ s
rw :
  Eq.{u_5 + 1} (α := k)
    ((b.coord i : (a : P) → k)
        ((Finset.affineCombination k s (⇑b : (a : ι) → P) : (a : ι → k) → P) (Finset.centroidWeights k s) : P) :
      k)
    ((↑s.card : k)⁻¹ : k)
rw₁ : Finset.centroidWeights k s i = (↑s.card : k)⁻¹
rw₂ : Eq.{u_5 + 1} (α := k) (Function.const ι (↑s.card : k)⁻¹ i) (↑s.card : k)⁻¹
⊢ Eq.{u_5 + 1} (α := k) ((b.coord i : (a : P) → k) (Finset.centroid k s (⇑b : (a : ι) → P)) : k) ((↑s.card : k)⁻¹ : k)
have rw₃ : Eq.{u_5 + 1} (α := k) (↑s.card : k)⁻¹ (↑s.card : k)⁻¹
Tactic: rw [Finset.centroid,
    b.coord_apply_combination_of_mem hi (s.sum_centroidWeights_eq_one_of_nonempty _ ⟨i, hi⟩),
    Finset.centroidWeights, Function.const_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
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 ⊆ t,
    ∃ (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))
have obtain : ∀ (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))),
  ∃ s ⊆ t,
    ∃ (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: obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affineIndependent k V t
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
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))
⊢ ∃ s ⊆ t,
    ∃ (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))
have refine : Eq.{u_7 + 1} (α := AffineSubspace k P)
  (affineSpan k (range (ι := (↑s : Type u_7)) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) ⊤
Tactic: refine ⟨s, hst, ⟨(↑), h_ind, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
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))
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range (ι := (↑s : Type u_7)) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) ⊤
have rw : Eq (α := AffineSubspace k P) (affineSpan k s) ⊤
Tactic: rw [Subtype.range_coe, h_tot, ht]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Basis (goal)
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) ⊤
⊢ Eq.{u_7 + 1} (α := AffineSubspace k P)
    (affineSpan k (range (ι := (↑s : Type u_7)) (Subtype.val (p := fun (x : P) ↦ x ∈ s)))) ⊤
have rw₂ : Eq.{u_7 + 1} (α := AffineSubspace k P) ⊤ ⊤
Tactic: rw [Subtype.range_coe, h_tot, ht]
-- 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
s : Finset P
⊢ centroid k (ι := ↥s) univ (Subtype.val (p := fun (x : P) ↦ x ∈ s)) = centroid k s id
have 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)
Tactic: rw [centroid, centroid, ← s.attach_affineCombination_coe]
-- 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
s : Finset P
⊢ 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)
have h : Eq (α := ↥s → k) (centroidWeights k univ) (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))
Tactic: congr
-- 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
s : Finset P
⊢ Eq (α := ↥s → k) (centroidWeights k univ) (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s))
have h : ∀ (x : ↥s), centroidWeights k univ x = (centroidWeights k s ∘ Subtype.val (p := fun (x : P) ↦ x ∈ s)) x
Tactic: ext
-- 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
inst_4 : DecidableEq ι
inst_5 : Invertible (α := k) 2
p : ι → P
i₁ i₂ : ι
⊢ centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁
have 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₁
Tactic: by_cases h : i₁ = i₂
-- 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
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₁
⊢ centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁
have 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₁
Tactic: by_cases h : i₁ = i₂
-- 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
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
have rw : Ne.{u_1 + 1} (α := k) (↑(HAdd.hAdd (α := ℕ) 1 1) : k) 0
Tactic: rw [card_insert_of_notMem (notMem_singleton.2 h), card_singleton]
-- 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
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₁
have hc : 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 _
-- 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
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
⊢ centroid k {i₁, i₂} p = HSMul.hSMul.{u_1, u_2, u_2} (α := k) 2⁻¹ (p i₂ -ᵥ p i₁) +ᵥ p i₁
have 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₁
Tactic: rw [centroid_def,
      affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _
        (sum_centroidWeights_eq_one_of_cast_card_ne_zero _ hc) (p i₁)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
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 : ι, centroidWeightsIndicator k s i) 1
have rw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
Tactic: rw [sum_centroidWeightsIndicator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
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 : ι, centroidWeightsIndicator k s i) 1
have rw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
Tactic: rw [sum_centroidWeightsIndicator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Centroid (goal)
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 : ι, centroidWeightsIndicator k s i) 1
have rw : Eq.{u_1 + 1} (α := k) (∑ i ∈ s, centroidWeights k s i) 1
Tactic: rw [sum_centroidWeightsIndicator]
-- 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)) ⋯
⊢ centroid k s p = centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
have hf : ∀ (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
-- 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) ⋯)
⊢ centroid k s p = centroid k univ fun (x : (↑ps : Type u_3)) ↦ (↑x : P)
have hf' : ∀ (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⟩
-- 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
⊢ x = y
have rw : (↑x : P) = (↑y : P)
Tactic: 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)
x y : (↑ps : Type u_3)
h : f' x = f' y
rw : (↑x : P) = (↑y : P)
⊢ x = y
have rw₁ : p (f' x) = (↑y : P)
Tactic: 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)
x y : (↑ps : Type u_3)
h : f' x = f' y
rw : (↑x : P) = (↑y : P)
rw₁ : p (f' x) = (↑y : P)
⊢ x = y
have rw₂ : p (f' x) = p (f' y)
Tactic: rw [Subtype.ext_iff, ← (hf' x).2, ← (hf' y).2, h]