awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
hy : True
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) ∧
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
hy : True
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) ∧
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
hy : True
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩) ∧
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
hy : True
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) ∧
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
hy : True
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩) ∧
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
h :
  dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2) ∧
    dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2) ∧
      dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
h₁ : dist (t.points 0) (t.points 1) ≠ dist (t.points 0) (t.points 2)
h₂ : dist (t.points 0) (t.points 1) ≠ dist (t.points 1) (t.points 2)
h₃ : dist (t.points 0) (t.points 2) ≠ dist (t.points 1) (t.points 2)
hx : True
hxy :
  dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) =
    dist (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
hy : True
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩) ∧
    Eq (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
      ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)

Tactic:
simp [h₁, h₂, h₃, h₁.symm, h₂.symm, h₃.symm] at hxy ⊢

Premises used: Ne.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.Equilateral t ↔
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Tactic:
⟨fun ⟨r, hr⟩ ↦ ?_, fun h ↦ ?_⟩

Premises used: Affine.Simplex.points, And, Iff.intro, Dist.dist, _private.0.Affine.Triangle.equilateral_iff_dist_eq_and_dist_eq.match_1, Eq
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
refine_1 :
  Simplex.Equilateral t →
    ∀ (r : ℝ) (hr : ∀ (i j : Fin (HAdd.hAdd (α := ℕ) 2 1)), i ≠ j → dist (t.points i) (t.points j) = r),
      dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
        dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀
    (h :
      dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
        dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)),
    Simplex.Equilateral t
⊢ Simplex.Equilateral t ↔
    dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
      dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : Simplex.Equilateral t
r : ℝ
hr : ∀ (i j : Fin (HAdd.hAdd (α := ℕ) 2 1)), i ≠ j → dist (t.points i) (t.points j) = r
⊢ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Tactic:
simp [hr _ _ h₁₂, hr _ _ h₁₃, hr _ _ h₂₃]
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ Simplex.Equilateral t

Tactic:
⟨dist (t.points i₁) (t.points i₂), ?_⟩

Premises used: Affine.Simplex.points, Affine.Simplex.Equilateral, Exists.intro, Dist.dist
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (i j : Fin (HAdd.hAdd (α := ℕ) 2 1)), i ≠ j → dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)
⊢ Simplex.Equilateral t

Tactic:
refine ⟨dist (t.points i₁) (t.points i₂), ?_⟩
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
⊢ i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂

Tactic:
decide +revert
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
⊢ i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂

Tactic:
have hi : (i = i₁ ∧ j = i₂) ∨ (i = i₂ ∧ j = i₁) ∨ (i = i₁ ∧ j = i₃) ∨
      (i = i₃ ∧ j = i₁) ∨ (i = i₂ ∧ j = i₃) ∨ (i = i₃ ∧ j = i₂) := by
      clear h
      decide +revert
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
⊢ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)

Tactic:
rcases h with ⟨h₁, h₂⟩
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
⊢ dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

Tactic:
rcases h with ⟨h₁, h₂⟩
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
hi : i = i₁ ∧ j = i₂ ∨ i = i₂ ∧ j = i₁ ∨ i = i₁ ∧ j = i₃ ∨ i = i₃ ∧ j = i₁ ∨ i = i₂ ∧ j = i₃ ∨ i = i₃ ∧ j = i₂
h₁ : dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃)
h₂ : dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
refine_2 :
  ∀ (h₁₃ : i ≠ i₃) (h₂₃ : j ≠ i₃) (h₁₂ : i ≠ j) (h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃))
    (h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
refine_2₁ :
  ∀ (h₂₃ : i ≠ i₃) (h₁₃ : j ≠ i₃) (h₁₂ : j ≠ i) (h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃))
    (h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
refine_2₂ :
  ∀ (h₁₂ : i ≠ i₂) (h₂₃ : i₂ ≠ j) (h₁₃ : i ≠ j) (h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j))
    (h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)),
    dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)
refine_2₃ :
  ∀ (h₂₃ : i₂ ≠ i) (h₁₂ : j ≠ i₂) (h₁₃ : j ≠ i) (h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i))
    (h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)),
    dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)
refine_2₄ :
  ∀ (h₁₂ : i₁ ≠ i) (h₁₃ : i₁ ≠ j) (h₂₃ : i ≠ j) (h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j))
    (h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)),
    dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)
refine_2₅ :
  ∀ (h₁₃ : i₁ ≠ i) (h₁₂ : i₁ ≠ j) (h₂₃ : j ≠ i) (h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i))
    (h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)),
    dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i₂)

Tactic:
rcases hi with ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₃ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₃ : i ≠ i₃
h₂₃ : j ≠ i₃
h₁₂ : i ≠ j
h₁ : dist (t.points i) (t.points j) = dist (t.points i) (t.points i₃)
h₂ : dist (t.points i) (t.points j) = dist (t.points j) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points j)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₃ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₂₃ : i ≠ i₃
h₁₃ : j ≠ i₃
h₁₂ : j ≠ i
h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃)
h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)

Tactic:
dist_comm _ _

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₃ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₂₃ : i ≠ i₃
h₁₃ : j ≠ i₃
h₁₂ : j ≠ i
h₁ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i₃)
h₂ : dist (t.points j) (t.points i) = dist (t.points i) (t.points i₃)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i)

Tactic:
exact dist_comm _ _

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₂ : i ≠ i₂
h₂₃ : i₂ ≠ j
h₁₃ : i ≠ j
h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j)
h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)

Tactic:
h₁.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₂ : i ≠ i₂
h₂₃ : i₂ ≠ j
h₁₃ : i ≠ j
h₁ : dist (t.points i) (t.points i₂) = dist (t.points i) (t.points j)
h₂ : dist (t.points i) (t.points i₂) = dist (t.points i₂) (t.points j)
⊢ dist (t.points i) (t.points j) = dist (t.points i) (t.points i₂)

Tactic:
exact h₁.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₂ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₂₃ : i₂ ≠ i
h₁₂ : j ≠ i₂
h₁₃ : j ≠ i
h₁ : dist (t.points j) (t.points i₂) = dist (t.points j) (t.points i)
h₂ : dist (t.points j) (t.points i₂) = dist (t.points i₂) (t.points i)
refine_2 : dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
refine_2₁ refine_2₂ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points j) (t.points i₂)

Tactic:
rw [h₁, dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₂ : i₁ ≠ i
h₁₃ : i₁ ≠ j
h₂₃ : i ≠ j
h₁ : dist (t.points i₁) (t.points i) = dist (t.points i₁) (t.points j)
h₂ : dist (t.points i₁) (t.points i) = dist (t.points i) (t.points j)
refine_2 : dist (t.points i) (t.points j) = dist (t.points i) (t.points j)
refine_2₁ refine_2₂ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points i)

Tactic:
rw [h₂, dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
i₁ : Fin 3
i j : Fin (HAdd.hAdd (α := ℕ) 2 1)
hij : i ≠ j
h₁₃ : i₁ ≠ i
h₁₂ : i₁ ≠ j
h₂₃ : j ≠ i
h₁ : dist (t.points i₁) (t.points j) = dist (t.points i₁) (t.points i)
h₂ : dist (t.points i₁) (t.points j) = dist (t.points j) (t.points i)
refine_2 : dist (t.points i) (t.points j) = dist (t.points j) (t.points i)
refine_2₁ refine_2₂ : dist (t.points j) (t.points i) = dist (t.points j) (t.points i)
⊢ dist (t.points i) (t.points j) = dist (t.points i₁) (t.points j)

Tactic:
rw [h₂, dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
⊢ Ne (α := Fin 3) 0 1

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
⊢ Ne (α := Fin 3) 0 2

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Affine.Simplex
Goal:
R : Type u_1
V : Type u_2
P : Type u_3
inst : Ring R
inst_1 : SeminormedAddCommGroup V
inst_2 : PseudoMetricSpace P
inst_3 : Module R V
inst_4 : NormedAddTorsor V P
t : Triangle R P
⊢ Ne (α := Fin 3) 1 2

Tactic:
decide
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
K : Type u_1
L : Type u_2
inst : NontriviallyNormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
F : IntermediateField K L
obtain : ∀ (k : K) (hk : 1 < ‖k‖), ∃ (x : ↥F), 1 < ‖x‖
⊢ ∃ (x : ↥F), 1 < ‖x‖

Tactic:
obtain ⟨k, hk⟩ := @NontriviallyNormedField.non_trivial K _

Premises used: NontriviallyNormedField.non_trivial
-- Module: Mathlib.Analysis.Normed.Algebra.Basic
Goal:
K : Type u_1
L : Type u_2
inst : NontriviallyNormedField K
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
F : IntermediateField K L
k : K
hk : 1 < ‖k‖
h : 1 < norm.{u_2} (E := ↥F) ((algebraMap K ↥F : (a : K) → ↥F) k : ↥F)
⊢ ∃ (x : ↥F), 1 < ‖x‖

Tactic:
use algebraMap K F k

Premises used: Algebra.algebraMap, Membership.mem, Subtype, DFunLike.coe