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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} j) : SignType) (1 : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights {i} i j) : SignType) (1 : SignType)
have rw₁ : Eq (α := SignType) 1 1
Tactic: rw [(s.excenterExists_singleton i).sign_touchpointWeights hne,
    s.sign_excenterWeights_singleton_pos hne]
-- 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ s.touchpoint {i} i ∈ (s.faceOpposite i).interior
have rw : (∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 → 0 < s.touchpointWeights {i} i i_1) ∧
  ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights {i} i i_1 = 0
Tactic: rw [faceOpposite, ← affineCombination_touchpointWeights,
    s.affineCombination_mem_interior_face_iff_pos _ (s.sum_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
⊢ (∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 → 0 < s.touchpointWeights {i} i i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights {i} i i_1 = 0
have simp : ∀ (i_1 : Fin (n + 1)), ¬i_1 = i → 0 < s.touchpointWeights {i} i i_1
Tactic: simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights {i} j i) : SignType) (-1 : SignType)
have rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
Tactic: rw [(s.excenterExists_singleton i).sign_touchpointWeights hne.symm,
    s.sign_excenterWeights_singleton_neg]
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights {i} j i) : SignType) (-1 : SignType)
have rw₁ : Eq (α := SignType) (-1) (-1)
Tactic: rw [(s.excenterExists_singleton i).sign_touchpointWeights hne.symm,
    s.sign_excenterWeights_singleton_neg]
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : s.touchpoint signs i = s.points j
⊢ False
have he₁ : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
Tactic: rw [eq_comm, ← Finset.univ.affineCombination_piSingle ℝ s.points (Finset.mem_univ _),
    affineCombination_eq_touchpoint_iff (Fintype.sum_pi_single' _ _)] at he
Cleared hypotheses: he
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
⊢ False
have this : 1 < n
Tactic: have : 1 < n := Nat.AtLeastTwo.one_lt
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
⊢ False
have obtain : ∀ (k : Fin (n + 1)) (hki : k ≠ i) (hkj : k ≠ j), False
Tactic: obtain ⟨k, hki, hkj⟩ : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j (by lia)
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ False
have he' : Eq (α := SignType)
  ((SignType.sign : (a : ℝ) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 k : ℝ) : SignType)
  ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i k) : SignType)
Tactic: have he' := congr(SignType.sign ($he k))
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 k : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i k) : SignType)
⊢ False
have he'₁ : HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k = 0
Tactic: rw [Pi.single_eq_of_ne hkj, sign_zero, eq_comm, h.sign_touchpointWeights hki.symm,
    sign_eq_zero_iff, excenterWeights] at he'
Cleared hypotheses: he'
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k = 0
⊢ False
have rw : ∀ (h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0) (i j : Fin (n + 1))
  (he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i) (this : 1 < n) (k : Fin (n + 1))
  (hki : k ≠ i) (hkj : k ≠ j)
  (he' :
    HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k = 0),
  False
Tactic: rw [ExcenterExists] at h
Cleared hypotheses: h, i, j, he, this, k, hki, hkj, he'
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k = 0
⊢ False
have he'₁ : s.excenterWeightsUnnorm signs k = 0
Tactic: simp only [Pi.smul_apply, smul_eq_mul, mul_eq_zero, inv_eq_zero, h, false_or] at he'
Cleared hypotheses: he'
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : s.excenterWeightsUnnorm signs k = 0
⊢ False
have he'₁ : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
Tactic: rw [excenterWeightsUnnorm] at he'
Cleared hypotheses: he'
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
⊢ False
have pos : ∀ (hk : k ∈ signs), False
Tactic: by_cases hk : k ∈ signs
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
pos : ∀ (hk : k ∈ signs), False
⊢ False
have neg : ∀ (hk : k ∉ signs), False
Tactic: by_cases hk : k ∈ signs
-- 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
signs : Finset (Fin 3)
⊢ Simplex.ExcenterExists t signs
have h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
Tactic: have h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ i, signs = {i} ∨ signs = {i}ᶜ := by 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
⊢ Simplex.ExcenterExists t signs
have inl : Simplex.ExcenterExists t ∅
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
inl : Simplex.ExcenterExists t ∅
⊢ Simplex.ExcenterExists t signs
have inr : Simplex.ExcenterExists t ∅ᶜ
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
inl : Simplex.ExcenterExists t ∅
inr : Simplex.ExcenterExists t ∅ᶜ
⊢ Simplex.ExcenterExists t signs
have inr₁ : ∀ (i : Fin 3), Simplex.ExcenterExists t {i}
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
inl : Simplex.ExcenterExists t ∅
inr : Simplex.ExcenterExists t ∅ᶜ
inr₁ : ∀ (i : Fin 3), Simplex.ExcenterExists t {i}
⊢ Simplex.ExcenterExists t signs
have inr₂ : ∀ (i : Fin 3), Simplex.ExcenterExists t {i}ᶜ
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
⊢ Simplex.ExcenterExists t ∅ᶜ
have inr : Simplex.ExcenterExists t ∅
Tactic: rw [Simplex.excenterExists_compl]
-- 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 : Fin 3
⊢ Simplex.ExcenterExists t {i}ᶜ
have inr : Simplex.ExcenterExists t {i}
Tactic: rw [Simplex.excenterExists_compl]
-- 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
signs : Finset (Fin 3)
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t signs = Simplex.excenter t {i}
have h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
Tactic: have h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ i, signs = {i} ∨ signs = {i}ᶜ := by 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t signs = Simplex.excenter t {i}
have inl : Simplex.excenter t ∅ = Simplex.incenter t ∨
  ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t ∅ = Simplex.excenter t {i}
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
inl :
  Simplex.excenter t ∅ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t ∅ = Simplex.excenter t {i}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t signs = Simplex.excenter t {i}
have inr : Simplex.excenter t Finset.univ = Simplex.incenter t ∨
  ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t Finset.univ = Simplex.excenter t {i}
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
inl :
  Simplex.excenter t ∅ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t ∅ = Simplex.excenter t {i}
inr :
  Simplex.excenter t Finset.univ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t Finset.univ = Simplex.excenter t {i}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t signs = Simplex.excenter t {i}
have inr₁ : ∀ (i : Fin 3),
  Simplex.excenter t {i} = Simplex.incenter t ∨
    ∃ (i_1 : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t {i} = Simplex.excenter t {i_1}
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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
signs : Finset (Fin 3)
h : signs = ∅ ∨ signs = Finset.univ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ
inl :
  Simplex.excenter t ∅ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t ∅ = Simplex.excenter t {i}
inr :
  Simplex.excenter t Finset.univ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t Finset.univ = Simplex.excenter t {i}
inr₁ :
  ∀ (i : Fin 3),
    Simplex.excenter t {i} = Simplex.incenter t ∨
      ∃ (i_1 : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t {i} = Simplex.excenter t {i_1}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t signs = Simplex.excenter t {i}
have inr₂ : ∀ (i : Fin 3),
  Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨
    ∃ (i_1 : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}
Tactic: rcases h with rfl | rfl | ⟨i, rfl | rfl⟩
Cleared hypotheses: signs, 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 : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨
    ∃ (i_1 : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}
have inr : Simplex.excenter t {i}ᶜ = Simplex.excenter t {i}
Tactic: refine .inr ⟨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 : Fin 3
⊢ Simplex.excenter t {i}ᶜ = Simplex.excenter t {i}
have inr : Simplex.excenter t {i} = Simplex.excenter t {i}
Tactic: rw [t.excenter_compl]
-- 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
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
have inl : ∀ (h : Simplex.excenter t signs = Simplex.incenter t),
  Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
Tactic: rcases t.excenter_eq_incenter_or_excenter_singleton signs with h | ⟨i, 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
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
inl :
  ∀ (h : Simplex.excenter t signs = Simplex.incenter t),
    Simplex.excenter t signs = Simplex.incenter t ∨
      Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
        Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
have inr : ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) (h : Simplex.excenter t signs = Simplex.excenter t {i}),
  Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
Tactic: rcases t.excenter_eq_incenter_or_excenter_singleton signs with h | ⟨i, 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
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : Simplex.excenter t signs = Simplex.excenter t {i}
⊢ Simplex.excenter t signs = Simplex.incenter t ∨
    Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
      Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
have inr : Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
  Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
Tactic: refine .inr ?_
-- 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
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : Simplex.excenter t signs = Simplex.excenter t {i}
⊢ Simplex.excenter t signs = Simplex.excenter t {i₁} ∨
    Simplex.excenter t signs = Simplex.excenter t {i₂} ∨ Simplex.excenter t signs = Simplex.excenter t {i₃}
have inr : Simplex.excenter t {i} = Simplex.excenter t {i₁} ∨
  Simplex.excenter t {i} = Simplex.excenter t {i₂} ∨ Simplex.excenter t {i} = Simplex.excenter t {i₃}
Tactic: rw [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
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : Simplex.excenter t signs = Simplex.excenter t {i}
⊢ Simplex.excenter t {i} = Simplex.excenter t {i₁} ∨
    Simplex.excenter t {i} = Simplex.excenter t {i₂} ∨ Simplex.excenter t {i} = Simplex.excenter t {i₃}
have this : i = i₁ ∨ i = i₂ ∨ i = i₃
Tactic: have : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear h; 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₃
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (Simplex.incenter t) (t.points i₁)
have h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
Tactic: convert! t.sSameSide_incenter_point i₁