awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
have h : {t.points i₂, t.points i₃} = t.points '' {i₁}ᶜ
Tactic: simp
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (t.points i₁) (Simplex.incenter t)
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! t.sSameSide_point_incenter i₁
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SOppSide (affineSpan ℝ {t.points i₂, t.points i₃}) (Simplex.excenter t {i₁}) (t.points i₁)
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! t.sOppSide_excenter_singleton_point i₁
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SOppSide (affineSpan ℝ {t.points i₂, t.points i₃}) (t.points i₁) (Simplex.excenter t {i₁})
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! t.sOppSide_point_excenter_singleton i₁
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (Simplex.excenter t {i₂}) (t.points i₁)
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! t.sSameSide_excenter_singleton_point h₁₂
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (t.points i₁) (Simplex.excenter t {i₂})
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! t.sSameSide_point_excenter_singleton h₁₂
-- 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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {t.points i₂, t.points i₃})
    ((Simplex.exsphere t signs).orthRadius (Simplex.touchpoint t signs i₁))
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! (t.excenterExists signs).affineSpan_faceOpposite_eq_orthRadius i₁
-- 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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
have hc : Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}
Tactic: have hc : {i₁}ᶜ = ({i₂, i₃} : Set (Fin 3)) := by grind
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw ℝ (t.points i₁) (Simplex.touchpoint t ∅ i₂) (t.points i₃)
have rw : Simplex.touchpoint t ∅ i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) sorry).interior
Tactic: rw [← t.mem_interior_face_iff_sbtw h₁₃]
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.touchpoint t ∅ i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) ⋯).interior
have h : Simplex.face t (fs := {i₁, i₃}) sorry = Simplex.faceOpposite t i₂
Tactic: convert! t.touchpoint_empty_mem_interior_faceOpposite i₂
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.face t (fs := {i₁, i₃}) ⋯ = Simplex.face t ⋯
have h : Eq (α := Finset (Fin (HAdd.hAdd (α := ℕ) 2 1))) {i₂}ᶜ {i₁, i₃}
Tactic: convert! rfl using 2
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw ℝ (t.points i₁) (Simplex.touchpoint t {i₂} i₂) (t.points i₃)
have rw : Simplex.touchpoint t {i₂} i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) sorry).interior
Tactic: rw [← t.mem_interior_face_iff_sbtw h₁₃]
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.touchpoint t {i₂} i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) ⋯).interior
have h : Simplex.face t (fs := {i₁, i₃}) sorry = Simplex.faceOpposite t i₂
Tactic: convert! t.touchpoint_singleton_mem_interior_faceOpposite i₂
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw ℝ (Simplex.touchpoint t {i₁} i₂) (t.points i₃) (t.points i₁)
have rw : Sbtw ℝ
  ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P) (Simplex.touchpointWeights t {i₁} i₂))
  (t.points i₃) (t.points i₁)
Tactic: rw [← Affine.Simplex.affineCombination_touchpointWeights]
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)
have hw : Eq (α := ℝ) (∑ j : Fin (2 + 1), Simplex.touchpointWeights t {i₁} i₂ j) 1
Tactic: have hw := t.sum_touchpointWeights {i₁} i₂
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Eq (α := ℝ) (∑ j : Fin (2 + 1), Simplex.touchpointWeights t {i₁} i₂ j) 1
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)
have hw₁ : Eq (α := ℝ) (∑ j ∈ {i₁, i₂, i₃}, Simplex.touchpointWeights t {i₁} i₂ j) 1
Tactic: rw [(by clear hw; decide +revert : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃})] at hw
Cleared hypotheses: hw
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Eq (α := ℝ) (∑ j ∈ {i₁, i₂, i₃}, Simplex.touchpointWeights t {i₁} i₂ j) 1
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)
have hw₁ : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
Tactic: simp only [Nat.reduceAdd, Finset.mem_insert, h₁₂, Finset.mem_singleton, h₁₃, or_self,
    not_false_eq_true, Finset.sum_insert, h₂₃, Simplex.touchpointWeights_eq_zero,
    Finset.sum_singleton, zero_add] at hw
Cleared hypotheses: hw
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
⊢ Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
have h : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)),
  Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
Tactic: ext i
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
have h : i = i₁ ∨ i = i₂ ∨ i = i₃
Tactic: have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear hw; decide +revert
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
have h₁ : ∀ (h₁₂ : i ≠ i₂) (h₁₃ : i ≠ i₃) (hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1),
  Simplex.touchpointWeights t {i} i₂ i =
    Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i
Tactic: rcases h with rfl | rfl | rfl
Cleared hypotheses: i₁, h₁₂, h₁₃, hw, h
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ :
  ∀ (h₁₂ : i ≠ i₂) (h₁₃ : i ≠ i₃)
    (hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1),
    Simplex.touchpointWeights t {i} i₂ i =
      Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
have h₂ : ∀ (h₁₂ : i₁ ≠ i) (h₂₃ : i ≠ i₃)
  (hw : Simplex.touchpointWeights t {i₁} i i₁ + Simplex.touchpointWeights t {i₁} i i₃ = 1),
  Simplex.touchpointWeights t {i₁} i i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i i₃) i
Tactic: rcases h with rfl | rfl | rfl
Cleared hypotheses: i₂, h₁₂, h₂₃, hw, h
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ :
  ∀ (h₁₂ : i ≠ i₂) (h₁₃ : i ≠ i₃)
    (hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1),
    Simplex.touchpointWeights t {i} i₂ i =
      Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i
h₂ :
  ∀ (h₁₂ : i₁ ≠ i) (h₂₃ : i ≠ i₃)
    (hw : Simplex.touchpointWeights t {i₁} i i₁ + Simplex.touchpointWeights t {i₁} i i₃ = 1),
    Simplex.touchpointWeights t {i₁} i i =
      Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i i₃) i
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
have h₃ : ∀ (h₁₃ : i₁ ≠ i) (h₂₃ : i₂ ≠ i)
  (hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i = 1),
  Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i (Simplex.touchpointWeights t {i₁} i₂ i) i
Tactic: rcases h with rfl | rfl | rfl
Cleared hypotheses: i₃, h₁₃, h₂₃, hw, h
-- 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
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1
⊢ Simplex.touchpointWeights t {i} i₂ i =
    Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i
have h : Simplex.touchpointWeights t {i} i₂ i = 1 - Simplex.touchpointWeights t {i} i₂ i₃
Tactic: rw [Finset.affineCombinationLineMapWeights_apply_left h₁₃]
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)
have h : Simplex.touchpointWeights t {i₁} i₂ =
  Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
Tactic: have h : t.touchpointWeights {i₁} i₂ =
      Finset.affineCombinationLineMapWeights i₁ i₃ (t.touchpointWeights {i₁} i₂ i₃) := by
    ext i
    have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear hw; decide +revert
    rcases h with rfl | rfl | rfl
    · rw [Finset.affineCombinationLineMapWeights_apply_left h₁₃]
      simp [← hw]
    · simp [h₁₂.symm, h₂₃]
    · simp [h₁₃]
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
h :
  Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)
have rw : t.points i₁ ≠ t.points i₃ ∧
  Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
    (Set.image (α := ℝ) (⇑(AffineMap.lineMap (t.points i₁) (t.points i₃)) : (a : ℝ) → P) (Set.Ioi 1))
    ((AffineMap.lineMap (t.points i₁) (t.points i₃) : (a : ℝ) → P) (Simplex.touchpointWeights t {i₁} i₂ i₃) : P)
Tactic: rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
    (Finset.mem_univ _), sbtw_iff_right_ne_and_left_mem_image_Ioi]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
⊢ inversion c (dist x c) x = x
have inl : inversion x (dist x x) x = x
Tactic: rcases eq_or_ne x c with (rfl | hne)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
inl : inversion x (dist x x) x = x
⊢ inversion c (dist x c) x = x
have inr : ∀ (hne : x ≠ c), inversion c (dist x c) x = x
Tactic: rcases eq_or_ne x c with (rfl | hne)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
hne : x ≠ c
⊢ inversion c (dist x c) x = x
have inr : dist x c ≠ 0
Tactic: rw [inversion, div_self, one_pow, one_smul, vsub_vadd]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
⊢ inversion c (dist c x) x = x
have rw : inversion c (dist x c) x = x
Tactic: rw [dist_comm, inversion_dist_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
rw : inversion c (dist x c) x = x
⊢ inversion c (dist c x) x = x
have rw₁ : x = x
Tactic: rw [dist_comm, inversion_dist_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
⊢ dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
have inl : dist (inversion x R x) x = HPow.hPow (β := ℕ) R 2 / dist x x
Tactic: rcases eq_or_ne x c with (rfl | hx)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
inl : dist (inversion x R x) x = HPow.hPow (β := ℕ) R 2 / dist x x
⊢ dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
have inr : ∀ (hx : x ≠ c), dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
Tactic: rcases eq_or_ne x c with (rfl | hx)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
hx : x ≠ c
⊢ dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
have this : dist x c ≠ 0
Tactic: have : dist x c ≠ 0 := dist_ne_zero.2 hx
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
have inr : dist (HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c) c = HPow.hPow (β := ℕ) R 2 / dist x c
Tactic: simp only [inversion]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist (HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c) c = HPow.hPow (β := ℕ) R 2 / dist x c
have inr : dist x c * dist ((HPow.hPow (β := ℕ) R 2 / HPow.hPow (β := ℕ) (dist x c) 2) • (x -ᵥ c) +ᵥ c) c = HPow.hPow (β := ℕ) R 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
hx : x ≠ c
this : dist x c ≠ 0
⊢ dist x c * dist ((HPow.hPow (β := ℕ) R 2 / HPow.hPow (β := ℕ) (dist x c) 2) • (x -ᵥ c) +ᵥ c) c =
    HPow.hPow (β := ℕ) R 2
have inr : dist x c * (R * R / (dist x c * dist x c) * dist x c) = R * R
Tactic: simp only [sq, dist_vadd_left, norm_smul, norm_div, norm_mul, Real.norm_eq_abs, abs_mul_abs_self,
    abs_dist, ← dist_eq_norm_vsub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
⊢ dist c (inversion c R x) = HPow.hPow (β := ℕ) R 2 / dist c x
have rw : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist c x
Tactic: rw [dist_comm c, dist_comm c, dist_inversion_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
rw : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist c x
⊢ dist c (inversion c R x) = HPow.hPow (β := ℕ) R 2 / dist c x
have rw₁ : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
Tactic: rw [dist_comm c, dist_comm c, dist_inversion_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c x : P
R : ℝ
rw : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist c x
rw₁ : dist (inversion c R x) c = HPow.hPow (β := ℕ) R 2 / dist x c
⊢ dist c (inversion c R x) = HPow.hPow (β := ℕ) R 2 / dist c x
have rw₂ : HPow.hPow (β := ℕ) R 2 / dist x c = HPow.hPow (β := ℕ) R 2 / dist x c
Tactic: rw [dist_comm c, dist_comm c, dist_inversion_center]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c : P
R : ℝ
hR : R ≠ 0
x : P
⊢ inversion c R (inversion c R x) = x
have inl : inversion x R (inversion x R x) = x
Tactic: rcases eq_or_ne x c with (rfl | hne)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Inversion.Basic (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
c : P
R : ℝ
hR : R ≠ 0
x : P
inl : inversion x R (inversion x R x) = x
⊢ inversion c R (inversion c R x) = x
have inr : ∀ (hne : x ≠ c), inversion c R (inversion c R x) = x
Tactic: rcases eq_or_ne x c with (rfl | hne)