awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : t = 1
⊢ False
have ht₁ : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) 1
Tactic: subst ht1
Cleared hypotheses: t, ht, h0, ht1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : t = 1
ht₁ : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) 1
⊢ False
have h0₁ : Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
  ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) 1 : P)
Tactic: subst ht1
Cleared hypotheses: t, ht, h0, ht1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) 1
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) 1 : P)
⊢ False
have h0₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points)) (s.touchpoint signs i)
Tactic: rw [AffineMap.lineMap_apply_one] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : ¬t = 1
⊢ False
have neg : dist ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t) (s.exsphere signs).center <
  (s.exsphere signs).radius
Tactic: refine (h.isTangentAt_touchpoint j).isTangent.notMem_of_dist_lt ?_ h0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : ¬t = 1
⊢ dist ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t) (s.exsphere signs).center <
    (s.exsphere signs).radius
have neg : |t| < 1
Tactic: simp only [exsphere_center, dist_lineMap_left, Real.norm_eq_abs, h.dist_excenter,
            exsphere_radius, h.exradius_pos, mul_lt_iff_lt_one_left]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : ¬t = 1
⊢ |t| < 1
have neg : -1 < t ∧ t < 1
Tactic: rw [abs_lt]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : ¬t = 1
⊢ -1 < t ∧ t < 1
have ht0 : 0 ≤ t
Tactic: rcases ht with ⟨ht0, ht1'⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : ¬t = 1
ht0 : 0 ≤ t
⊢ -1 < t ∧ t < 1
have ht1' : t ≤ 1
Tactic: rcases ht with ⟨ht0, ht1'⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
h0 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
ht1 : ¬t = 1
ht0 : 0 ≤ t
ht1' : t ≤ 1
⊢ -1 < t
have linarith : t ≤ -1 → -1 + (0 - t) + (t - -1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
⊢ Continuous.{0, u_2} (X := ℝ) (Y := P) (⇑(AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) : (a : ℝ) → P)
have refine_2 : Continuous.{0, u_2} (X := ℝ) (Y := P)
  (⇑(↑(ContinuousAffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) : ℝ →ᵃ[ℝ] P) : (a : ℝ) → P)
Tactic: rw [← ContinuousAffineMap.lineMap_toAffineMap]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) r : P) :
          ℝ) :
      SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
have hc : ContinuousOn (Y := SignType)
  (fun (t : ℝ) ↦
    (SignType.sign : (a : ℝ) → SignType)
      ((s.signedInfDist j : (a : P) → ℝ)
          ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
        ℝ))
  (Set.Icc 0 1)
Tactic: have hc : ContinuousOn (fun (t : ℝ) ↦ SignType.sign
      (s.signedInfDist j (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) t)))
      (Set.Icc 0 1) := by
    refine continuousOn_of_forall_continuousAt
      fun t ht ↦ ((continuousAt_sign_of_ne_zero ?_).comp
        (((s.signedInfDist j).cont.comp ?_).continuousAt))
    · intro h0
      rw [← abs_eq_zero, abs_signedInfDist_eq_dist_of_mem_affineSpan_range] at h0
      · rw [orthogonalProjectionSpan, dist_orthogonalProjection_eq_zero_iff] at h0
        by_cases ht1 : t = 1
        · subst ht1
          rw [AffineMap.lineMap_apply_one] at h0
          exact h.touchpoint_notMem_affineSpan_of_ne hne h0
        · refine (h.isTangentAt_touchpoint j).isTangent.notMem_of_dist_lt ?_ h0
          simp only [exsphere_center, dist_lineMap_left, Real.norm_eq_abs, h.dist_excenter,
            exsphere_radius, h.exradius_pos, mul_lt_iff_lt_one_left]
          rw [abs_lt]
          rcases ht with ⟨ht0, ht1'⟩
          exact ⟨by linarith, ht1'.lt_of_ne ht1⟩
      · exact AffineMap.lineMap_mem _ h.excenter_mem_affineSpan_range
          (s.touchpoint_mem_affineSpan_simplex _ _)
    · rw [← ContinuousAffineMap.lineMap_toAffineMap]
      exact ContinuousAffineMap.cont _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
hc :
  ContinuousOn (Y := SignType)
    (fun (t : ℝ) ↦
      (SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
          ℝ))
    (Set.Icc 0 1)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) r : P) :
          ℝ) :
      SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
have refine : Membership.mem (α := SignType) (γ := Set SignType)
  ((fun (t : ℝ) ↦
      (SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
          ℝ)) ''
    Set.Icc 0 1)
  ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
Tactic: refine ((isConnected_Icc zero_le_one).image _ hc).isPreconnected.subsingleton
    (Set.mem_image_of_mem _ hr) ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
hc :
  ContinuousOn (Y := SignType)
    (fun (t : ℝ) ↦
      (SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
          ℝ))
    (Set.Icc 0 1)
⊢ Membership.mem (α := SignType) (γ := Set SignType)
    ((fun (t : ℝ) ↦
        (SignType.sign : (a : ℝ) → SignType)
          ((s.signedInfDist j : (a : P) → ℝ)
              ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
            ℝ)) ''
      Set.Icc 0 1)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
have h₁ : s.excenter signs = (AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) 0
Tactic: convert! Set.mem_image_of_mem _ (Set.left_mem_Icc.2 (zero_le_one' ℝ))
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
have rw : Eq (α := SignType)
  ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
  ((SignType.sign : (a : ℝ) → SignType)
      ((s.signedInfDist j : (a : P) → ℝ)
          ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) 1 : P) :
        ℝ) :
    SignType)
Tactic: rw [← h.sign_signedInfDist_lineMap_excenter_touchpoint hne (r := 1) ⟨zero_le_one, le_rfl⟩]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i ↔
    w = s.touchpointWeights signs i
have mp : (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i →
  w = s.touchpointWeights signs i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
mp :
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i →
    w = s.touchpointWeights signs i
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i ↔
    w = s.touchpointWeights signs i
have mpr : w = s.touchpointWeights signs i →
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i →
    w = s.touchpointWeights signs i
have mp : Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) : P) →
  w = s.touchpointWeights signs i
Tactic: rw [← s.affineCombination_touchpointWeights]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (s.reindex e).touchpointWeights signs i =
    s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have rw : (Finset.affineCombination ℝ Finset.univ (s.reindex e).points : (a : Fin (m + 1) → ℝ) → P)
    (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
  (s.reindex e).touchpoint signs i
Tactic: rw [eq_comm, ← affineCombination_eq_touchpoint_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
rw :
  (Finset.affineCombination ℝ Finset.univ (s.reindex e).points : (a : Fin (m + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    (s.reindex e).touchpoint signs i
⊢ (s.reindex e).touchpointWeights signs i =
    s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have rw₁ : Eq (α := ℝ)
  (∑ j : Fin (m + 1),
    (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)))
      j)
  1
Tactic: rw [eq_comm, ← affineCombination_eq_touchpoint_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.reindex e).points : (a : Fin (m + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    (s.reindex e).touchpoint signs i
have rw : Eq.{u_2 + 1} (α := P)
  ((Finset.affineCombination ℝ Finset.univ
          { points := s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)), independent := sorry :
              Simplex ℝ P m }.points :
        (a : Fin (m + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
    P)
  ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
    P)
Tactic: rw [touchpoint_reindex, ← affineCombination_touchpointWeights, reindex]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ
            { points := s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)), independent := ⋯ :
                Simplex ℝ P m }.points :
          (a : Fin (m + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
have dsimp : Eq.{u_2 + 1} (α := P)
  ((Finset.affineCombination ℝ Finset.univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
        (a : Fin (m + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
    P)
  ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
    P)
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
          (a : Fin (m + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
have rw : Eq.{u_2 + 1} (α := P)
  ((Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points : (a : Fin (n + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs)
        ((e.symm.toEmbedding : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
    P)
  ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs)
        ((e.symm.toEmbedding : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
    P)
Tactic: rw [← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ Eq (α := ℝ)
    (∑ j : Fin (m + 1),
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)))
        j)
    1
have rw : (Finset.map e.symm.toEmbedding Finset.univ).sum
    (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) =
  1
Tactic: rw [Finset.sum_comp_equiv]