awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
⊢ Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
have hx : (e : (a : PE) → PE) x = x
Tactic: have hx : e x = x := by simp [e]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
⊢ Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
have hy : (e : (a : PE) → PE) y = y
Tactic: have hy : e y = y := by simp [e]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (hypothesis)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
⊢ Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
have hm : (e : (a : PE) → PE) (midpoint ℝ x y) = midpoint ℝ x y
Tactic: have hm := e.midpoint_fixed hx hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
hm :
  (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)) : (a : PE) → PE)
      ((f.symm : (a : PF) → PE)
          (((toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                  PF ≃ᵢ PF) :
                (a : PF) → PF)
              ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
            PF) :
        PE) =
    midpoint ℝ x y
⊢ Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
have rwa : ∀
  (hm :
    Eq.{u_2 + 1} (α := PE)
      ((f.symm : (a : PF) → PE)
          (((toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                  PF ≃ᵢ PF) :
                (a : PF) → PF)
              ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
            PF) :
        PE)
      ((IsometryEquiv.symm (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y))) : (a : PE) → PE) (midpoint ℝ x y) :
        PE)),
  Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
Tactic: rwa [← eq_symm_apply, ← toIsometryEquiv_symm, pointReflection_symm, coe_toIsometryEquiv,
    coe_toIsometryEquiv, pointReflection_self, symm_apply_eq, @pointReflection_fixed_iff] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
x y : PE
e : PE ≃ᵢ PE :=
  (IsometryEquiv.trans
        (f.trans
          (toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y)))))
        f.symm).trans
    (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)))
hx : (e : (a : PE) → PE) x = x
hy : (e : (a : PE) → PE) y = y
hm :
  (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y)) : (a : PE) → PE)
      ((f.symm : (a : PF) → PE)
          (((toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                  PF ≃ᵢ PF) :
                (a : PF) → PF)
              ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
            PF) :
        PE) =
    midpoint ℝ x y
rwa :
  ∀
    (hm :
      Eq.{u_2 + 1} (α := PE)
        ((f.symm : (a : PF) → PE)
            (((toIsometryEquiv (𝕜 := ℝ)
                      (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                    PF ≃ᵢ PF) :
                  (a : PF) → PF)
                ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
              PF) :
          PE)
        ((IsometryEquiv.symm (toIsometryEquiv (pointReflection ℝ (midpoint ℝ x y))) : (a : PE) → PE) (midpoint ℝ x y) :
          PE)),
    Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
      (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
⊢ Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
have rwa₁ : ∀
  (hm :
    Eq.{u_2 + 1} (α := PE)
      ((f.symm : (a : PF) → PE)
          (((toIsometryEquiv (𝕜 := ℝ) (pointReflection ℝ (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y))) :
                  PF ≃ᵢ PF) :
                (a : PF) → PF)
              ((f : (a : PE) → PF) (midpoint ℝ x y) : PF) :
            PF) :
        PE)
      ((toIsometryEquiv (AffineIsometryEquiv.symm (pointReflection ℝ (midpoint ℝ x y))) : (a : PE) → PE)
          (midpoint ℝ x y) :
        PE)),
  Eq.{u_4 + 1} (α := PF) ((f : (a : PE) → PF) (midpoint ℝ x y) : PF)
    (midpoint ℝ ((f : (a : PE) → PF) x) ((f : (a : PE) → PF) y) : PF)
Tactic: rwa [← eq_symm_apply, ← toIsometryEquiv_symm, pointReflection_symm, coe_toIsometryEquiv,
    coe_toIsometryEquiv, pointReflection_self, symm_apply_eq, @pointReflection_fixed_iff] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.MazurUlam (goal)
Goal:
E : Type u_1
PE : Type u_2
F : Type u_3
PF : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MetricSpace PE
inst_3 : NormedAddTorsor E PE
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ F
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor F PF
f : PE ≃ᵢ PF
⊢ toIsometryEquiv f.toRealAffineIsometryEquiv = f
have H : ∀ (x : PE),
  Eq.{u_4 + 1} (α := PF) ((toIsometryEquiv f.toRealAffineIsometryEquiv : (a : PE) → PF) x : PF)
    ((f : (a : PE) → PF) x : PF)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (hypothesis)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬(i₁ = i₃ ∧ i₂ = i₄)
h₁₂₄₃ : ¬(i₁ = i₄ ∧ i₂ = i₃)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have h₁₂₃₅ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
Tactic: rw [Classical.not_and_iff_not_or_not] at h₁₂₃₄ h₁₂₄₃
Cleared hypotheses: h₁₂₃₄, h₁₂₄₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (hypothesis)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬(i₁ = i₃ ∧ i₂ = i₄)
h₁₂₄₃ : ¬(i₁ = i₄ ∧ i₂ = i₃)
h₁₂₃₅ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have h₁₂₄₄ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
Tactic: rw [Classical.not_and_iff_not_or_not] at h₁₂₃₄ h₁₂₄₃
Cleared hypotheses: h₁₂₃₄, h₁₂₄₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inl : ∀ (h₁₂lt : i₁ < i₂), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rcases h₁₂.lt_or_gt with h₁₂lt | h₂₁lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
inl : ∀ (h₁₂lt : i₁ < i₂), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inr : ∀ (h₂₁lt : i₂ < i₁), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rcases h₁₂.lt_or_gt with h₁₂lt | h₂₁lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inl : ∀ (h₃₄lt : i₃ < i₄), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
inl : ∀ (h₃₄lt : i₃ < i₄), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inl₁ : ∀ (h₄₃lt : i₄ < i₃), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inr : ∀ (h₃₄lt : i₃ < i₄), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
inr : ∀ (h₃₄lt : i₃ < i₄), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inr₁ : ∀ (h₄₃lt : i₄ < i₃), dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rcases h₃₄.lt_or_gt with h₃₄lt | h₄₃lt
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inl : Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
  (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
  (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
Tactic: apply hs.ne (a₁ := ⟨(i₁, i₂), h₁₂lt⟩) (a₂ := ⟨(i₃, i₄), h₃₄lt⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
have inl : ¬i₁ = i₃ →
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
Tactic: cases h₁₂₃₄
Cleared hypotheses: h₁₂₃₄
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₃₄lt : i₃ < i₄
inl :
  ¬i₁ = i₃ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
have inl₁ : ¬i₂ = i₄ →
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
Tactic: cases h₁₂₃₄
Cleared hypotheses: h₁₂₃₄
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inl : dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)
Tactic: nth_rw 2 [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)
have inl : Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
  (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
  (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
Tactic: apply hs.ne (a₁ := ⟨(i₁, i₂), h₁₂lt⟩) (a₂ := ⟨(i₄, i₃), h₄₃lt⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
have inl : ¬i₁ = i₄ →
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
Tactic: cases h₁₂₄₃
Cleared hypotheses: h₁₂₄₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
inl :
  ¬i₁ = i₄ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
have inl₁ : ¬i₂ = i₃ →
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₁, i₂) h₁₂lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₄, i₃) h₄₃lt)
Tactic: cases h₁₂₄₃
Cleared hypotheses: h₁₂₄₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inr : dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
have inr : Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
  (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
  (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
Tactic: apply hs.ne (a₁ := ⟨(i₂, i₁), h₂₁lt⟩) (a₂ := ⟨(i₃, i₄), h₃₄lt⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
have inr : ¬i₁ = i₄ →
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
Tactic: cases h₁₂₄₃
Cleared hypotheses: h₁₂₄₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₃₄lt : i₃ < i₄
inr :
  ¬i₁ = i₄ →
    Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
      (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
⊢ Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
have inr₁ : ¬i₂ = i₃ →
  Ne (α := { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 })
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₂, i₁) h₂₁lt)
    (Subtype.mk (p := fun (x : Fin (n + 1) × Fin (n + 1)) ↦ x.1 < x.2) (i₃, i₄) h₃₄lt)
Tactic: cases h₁₂₄₃
Cleared hypotheses: h₁₂₄₃
-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Simplex (goal)
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
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)
have inr : dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)
Tactic: rw [dist_comm]