awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
⊢ 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'

Premises used: inv_eq_zero, false_or, mul_eq_zero, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
⊢ (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0

Tactic:
rw [excenterWeightsUnnorm] at he'

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
neg : ∀ (hk : k ∉ signs), False
⊢ False

Tactic:
by_cases hk : k ∈ signs
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
hk : k ∈ signs
⊢ False

Tactic:
simp [hk, (s.height_pos k).ne'] at he'

Premises used: Affine.Simplex.height_pos, LT.lt.ne'
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
hk : k ∉ signs
⊢ False

Tactic:
simp [hk, (s.height_pos k).ne'] at he'

Premises used: Affine.Simplex.height_pos, LT.lt.ne'
-- Module: Mathlib.Geometry.Euclidean.Incenter
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)
⊢ s.touchpoint ∅ i ≠ s.points j

Tactic:
s.excenterExists_empty.touchpoint_ne_point i j

Premises used: Affine.Simplex.ExcenterExists.touchpoint_ne_point, Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
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)
⊢ signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.Incenter
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)
⊢ signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ

Tactic:
have h : signs = ∅ ∨ signs = ∅ᶜ ∨ ∃ i, signs = {i} ∨ signs = {i}ᶜ := by decide +revert
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}
inr₂ : ∀ (i : Fin 3), Simplex.ExcenterExists t {i}ᶜ
⊢ Simplex.ExcenterExists t signs

Tactic:
rcases h with rfl | rfl | ⟨i, rfl | rfl⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 ∅

Tactic:
t.excenterExists_empty

Premises used: Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 ∅

Tactic:
exact t.excenterExists_empty

Premises used: Affine.Simplex.excenterExists_empty
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
inr : Simplex.ExcenterExists t ∅
⊢ Simplex.ExcenterExists t ∅ᶜ

Tactic:
rw [Simplex.excenterExists_compl]

Premises used: Affine.Simplex.excenterExists_compl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}

Tactic:
t.excenterExists_singleton _

Premises used: Affine.Simplex.excenterExists_singleton
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}

Tactic:
exact t.excenterExists_singleton _

Premises used: Affine.Simplex.excenterExists_singleton
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
inr : Simplex.ExcenterExists t {i}
⊢ Simplex.ExcenterExists t {i}ᶜ

Tactic:
rw [Simplex.excenterExists_compl]

Premises used: Affine.Simplex.excenterExists_compl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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)
⊢ signs = ∅ ∨ signs = Finset.univ ∨ ∃ (i : Fin 3), signs = {i} ∨ signs = {i}ᶜ

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.Incenter
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)
⊢ 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
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}
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}

Tactic:
rcases h with rfl | rfl | ⟨i, rfl | rfl⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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.excenter t ∅ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t ∅ = Simplex.excenter t {i}

Tactic:
.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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.excenter t ∅ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t ∅ = Simplex.excenter t {i}

Tactic:
exact .inl rfl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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.excenter t Finset.univ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t Finset.univ = Simplex.excenter t {i}

Tactic:
.inl t.excenter_univ

Premises used: Or.inl, Affine.Simplex.excenter_univ
-- Module: Mathlib.Geometry.Euclidean.Incenter
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.excenter t Finset.univ = Simplex.incenter t ∨
    ∃ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t Finset.univ = Simplex.excenter t {i}

Tactic:
exact .inl t.excenter_univ
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}

Tactic:
.inr ⟨i, rfl⟩

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}

Tactic:
exact .inr ⟨i, rfl⟩
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}

Tactic:
.inr ⟨i, ?_⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
inr : Simplex.excenter t {i}ᶜ = Simplex.excenter t {i}
⊢ Simplex.excenter t {i}ᶜ = Simplex.incenter t ∨
    ∃ (i_1 : Fin (HAdd.hAdd (α := ℕ) 2 1)), Simplex.excenter t {i}ᶜ = Simplex.excenter t {i_1}

Tactic:
refine .inr ⟨i, ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
inr inr₁ : Simplex.excenter t {i} = Simplex.excenter t {i}
⊢ Simplex.excenter t {i}ᶜ = Simplex.excenter t {i}

Tactic:
rw [t.excenter_compl]

Premises used: Affine.Simplex.excenter_compl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃}
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₃}
⊢ 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⟩

Premises used: Affine.Triangle.excenter_eq_incenter_or_excenter_singleton
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
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:
.inl h

Premises used: Or.inl
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
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:
exact .inl h
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃}

Tactic:
.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}
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₃}
⊢ 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:
refine .inr ?_
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}
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₃}
⊢ 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:
rw [h]
-- Module: Mathlib.Geometry.Euclidean.Incenter
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)
⊢ i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
decide +revert
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}
⊢ i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
have : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear h; decide +revert
-- Module: Mathlib.Geometry.Euclidean.Incenter
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}
this : i = i₁ ∨ i = i₂ ∨ i = 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₃}

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 ℝ (Set.range (Simplex.faceOpposite t i₁).points)) (Simplex.incenter t)
    (t.points i₁)

Tactic:
t.sSameSide_incenter_point i₁

Premises used: Affine.Simplex.sSameSide_incenter_point
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (Simplex.incenter t) (t.points i₁)

Tactic:
convert! t.sSameSide_incenter_point i₁

Premises used: Affine.Simplex.sSameSide_incenter_point
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
h : {t.points i₂, t.points i₃} = t.points '' {i₁}ᶜ
⊢ {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃} = t.points '' {i₁}ᶜ

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 ℝ (Set.range (Simplex.faceOpposite t i₁).points)) (t.points i₁)
    (Simplex.incenter t)

Tactic:
t.sSameSide_point_incenter i₁

Premises used: Affine.Simplex.sSameSide_point_incenter
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (t.points i₁) (Simplex.incenter t)

Tactic:
convert! t.sSameSide_point_incenter i₁

Premises used: Affine.Simplex.sSameSide_point_incenter
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 ℝ (Set.range (Simplex.faceOpposite t i₁).points)) (Simplex.excenter t {i₁})
    (t.points i₁)

Tactic:
t.sOppSide_excenter_singleton_point i₁

Premises used: Affine.Simplex.sOppSide_excenter_singleton_point
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ AffineSubspace.SOppSide (affineSpan ℝ {t.points i₂, t.points i₃}) (Simplex.excenter t {i₁}) (t.points i₁)

Tactic:
convert! t.sOppSide_excenter_singleton_point i₁

Premises used: Affine.Simplex.sOppSide_excenter_singleton_point
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 ℝ (Set.range (Simplex.faceOpposite t i₁).points)) (t.points i₁)
    (Simplex.excenter t {i₁})

Tactic:
t.sOppSide_point_excenter_singleton i₁

Premises used: Affine.Simplex.sOppSide_point_excenter_singleton
-- Module: Mathlib.Geometry.Euclidean.Incenter
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₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ AffineSubspace.SOppSide (affineSpan ℝ {t.points i₂, t.points i₃}) (t.points i₁) (Simplex.excenter t {i₁})

Tactic:
convert! t.sOppSide_point_excenter_singleton i₁

Premises used: Affine.Simplex.sOppSide_point_excenter_singleton