awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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: 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 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
f : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 } ≃ { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 } :=
  {
    toFun := fun (x : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) ↦
      if h :
          LT.lt (α := Fin (n + 1))
            ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1 : Fin (n + 1))
            ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2 : Fin (n + 1)) then
        Subtype.mk (p := fun (y : Fin (n + 1) × Fin (n + 1)) ↦ y.1 < y.2)
          ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1,
            (e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2)
          h
      else
        Subtype.mk (p := fun (y : Fin (n + 1) × Fin (n + 1)) ↦ y.1 < y.2)
          ((e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).2,
            (e : (a : Fin (m + 1)) → Fin (n + 1)) (↑x : Fin (m + 1) × Fin (m + 1)).1)
          ⋯,
    invFun := fun (y : { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 }) ↦
      if h :
          LT.lt (α := Fin (m + 1))
            ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1 : Fin (m + 1))
            ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2 : Fin (m + 1)) then
        Subtype.mk (p := fun (x : Fin (m + 1) × Fin (m + 1)) ↦ x.1 < x.2)
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1,
            (e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2)
          h
      else
        Subtype.mk (p := fun (x : Fin (m + 1) × Fin (m + 1)) ↦ x.1 < x.2)
          ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).2,
            (e.symm : (a : Fin (n + 1)) → Fin (m + 1)) (↑y : Fin (n + 1) × Fin (n + 1)).1)
          ⋯,
    left_inv := ⋯, right_inv := ⋯ }
⊢ (Injective (β := ℝ) fun (i : { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 }) ↦
      dist ((s.reindex e).points (↑i : Fin (n + 1) × Fin (n + 1)).1)
        ((s.reindex e).points (↑i : Fin (n + 1) × Fin (n + 1)).2)) ↔
    Injective (β := ℝ) fun (i : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) ↦
      dist (s.points (↑i : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑i : Fin (m + 1) × Fin (m + 1)).2)
have h : ∀ (x : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }),
  dist (s.points (↑x : Fin (m + 1) × Fin (m + 1)).1) (s.points (↑x : Fin (m + 1) × Fin (m + 1)).2) =
    ((fun (i : { x : Fin (n + 1) × Fin (n + 1) // x.1 < x.2 }) ↦
          dist ((s.reindex e).points (↑i : Fin (n + 1) × Fin (n + 1)).1)
            ((s.reindex e).points (↑i : Fin (n + 1) × Fin (n + 1)).2)) ∘
        (⇑f : (a : { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.2 }) → { y : Fin (n + 1) × Fin (n + 1) // y.1 < y.2 }))
      x
Tactic: convert! (Injective.of_comp_iff' _ (Equiv.bijective f)).symm
-- 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
he : s.Equilateral
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)
have rcases : ∀ (r : ℝ) (hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r),
  dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)
Tactic: rcases he with ⟨r, hr⟩
Cleared hypotheses: he
-- 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
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)
have rw : r = dist (s.points i₃) (s.points i₄)
Tactic: rw [hr _ _ h₁₂, hr _ _ 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
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = r
rw : r = dist (s.points i₃) (s.points i₄)
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)
have rw₁ : r = r
Tactic: rw [hr _ _ h₁₂, hr _ _ 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Equilateral ↔ s.Equilateral
have refine_1 : (s.reindex e).Equilateral →
  ∀ (r : ℝ) (hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r)
    (i j : Fin (m + 1)) (hij : i ≠ j), dist (s.points i) (s.points j) = r
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩⟩
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_1 :
  (s.reindex e).Equilateral →
    ∀ (r : ℝ) (hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r)
      (i j : Fin (m + 1)) (hij : i ≠ j), dist (s.points i) (s.points j) = r
⊢ (s.reindex e).Equilateral ↔ s.Equilateral
have refine_2 : s.Equilateral →
  ∀ (r : ℝ) (hr : ∀ (i j : Fin (m + 1)), i ≠ j → dist (s.points i) (s.points j) = r) (i j : Fin (n + 1)) (hij : i ≠ j),
    dist ((s.reindex e).points i) ((s.reindex e).points j) = r
Tactic: refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩⟩
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
⊢ dist (s.points i) (s.points j) = r
have h : s.points i = (s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i)
Tactic: convert! hr (e i) (e j) (e.injective.ne hij) using 2
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h_1 : (s.reindex e).Equilateral
r : ℝ
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist ((s.reindex e).points i) ((s.reindex e).points j) = r
i j : Fin (m + 1)
hij : i ≠ j
h : s.points i = (s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i)
⊢ dist (s.points i) (s.points j) = r
have h₁ : s.points j = (s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) j)
Tactic: convert! hr (e i) (e j) (e.injective.ne hij) using 2
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Regular ↔ s.Regular
have refine_1 : ∀ (h : (s.reindex e).Regular) (σ : Equiv.Perm (Fin (m + 1))),
  ∃ (x : P ≃ᵢ P), s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
Tactic: refine ⟨fun h σ ↦ ?_, fun 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_1 :
  ∀ (h : (s.reindex e).Regular) (σ : Equiv.Perm (Fin (m + 1))),
    ∃ (x : P ≃ᵢ P), s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ (s.reindex e).Regular ↔ s.Regular
have refine_2 : ∀ (h : s.Regular) (σ : Equiv.Perm (Fin (n + 1))),
  ∃ (x : P ≃ᵢ P),
    (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
Tactic: refine ⟨fun h σ ↦ ?_, fun 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Regular
σ : Equiv.Perm (Fin (m + 1))
⊢ ∃ (x : P ≃ᵢ P), s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
have refine_1 : ∀ (x : P ≃ᵢ P)
  (hx :
    (s.reindex e).points ∘ (⇑((e.symm.trans σ).trans e) : (a : Fin (n + 1)) → Fin (n + 1)) =
      (⇑x : (a : P) → P) ∘ (s.reindex e).points),
  ∃ (x : P ≃ᵢ P), s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
Tactic: rcases h ((e.symm.trans σ).trans e) with ⟨x, hx⟩
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Regular
σ : Equiv.Perm (Fin (m + 1))
x : P ≃ᵢ P
hx :
  (s.reindex e).points ∘ (⇑((e.symm.trans σ).trans e) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ (s.reindex e).points
⊢ ∃ (x : P ≃ᵢ P), s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
have refine_1 : s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
Tactic: refine ⟨x, ?_⟩
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Regular
σ : Equiv.Perm (Fin (m + 1))
x : P ≃ᵢ P
hx :
  (s.reindex e).points ∘ (⇑((e.symm.trans σ).trans e) : (a : Fin (n + 1)) → Fin (n + 1)) =
    (⇑x : (a : P) → P) ∘ (s.reindex e).points
⊢ s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
have refine_1 : ∀ (i : Fin (m + 1)), (s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1))) i = ((⇑x : (a : P) → P) ∘ s.points) i
Tactic: ext i
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
⊢ ∃ (x : P ≃ᵢ P),
    (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
have refine_2 : ∀ (x : P ≃ᵢ P)
  (hx : s.points ∘ (⇑((e.trans σ).trans e.symm) : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points),
  ∃ (x : P ≃ᵢ P),
    (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
Tactic: rcases h ((e.trans σ).trans e.symm) with ⟨x, hx⟩
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
x : P ≃ᵢ P
hx : s.points ∘ (⇑((e.trans σ).trans e.symm) : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ ∃ (x : P ≃ᵢ P),
    (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
have refine_2 : (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
Tactic: refine ⟨x, ?_⟩
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
x : P ≃ᵢ P
hx : s.points ∘ (⇑((e.trans σ).trans e.symm) : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
have refine_2 : ∀ (i : Fin (n + 1)),
  ((s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1))) i = ((⇑x : (a : P) → P) ∘ (s.reindex e).points) i
Tactic: ext i
-- 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
hr : s.Regular
⊢ s.Equilateral
have refine : ∀ (i j : Fin (n + 1)) (hij : i ≠ j), dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
Tactic: refine ⟨dist (s.points 0) (s.points 1), fun i j hij ↦ ?_⟩
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
have hn : n ≠ 0
Tactic: have hn : n ≠ 0 := by lia
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
have pos : ∀ (hi : i = 1), dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
Tactic: by_cases hi : i = 1
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
pos : ∀ (hi : i = 1), dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
have neg : ∀ (hi : ¬i = 1), dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
Tactic: by_cases hi : i = 1
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
have pos : dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
Tactic: rw [hi, 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
have pos : ∀ (x : P ≃ᵢ P) (hx : s.points ∘ (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points),
  dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
Tactic: rcases hr (Equiv.swap 0 j) with ⟨x, hx⟩
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
have pos : dist (s.points j) (s.points 1) = dist (α := P) ((x : (a : P) → P) (s.points 0) : P) ((x : (a : P) → P) (s.points 1) : P)
Tactic: nth_rw 2 [← x.dist_eq]
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points j) (s.points 1) =
    dist (α := P) ((x : (a : P) → P) (s.points 0) : P) ((x : (a : P) → P) (s.points 1) : P)
have pos : dist (s.points j) (s.points 1) =
  dist (comp (α := Fin (n + 1)) s.points (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) 0)
    (comp (α := Fin (n + 1)) s.points (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) 1)
Tactic: simp_rw [← Function.comp_apply (f := x), ← hx]
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points j) (s.points 1) =
    dist (comp (α := Fin (n + 1)) s.points (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) 0)
      (comp (α := Fin (n + 1)) s.points (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) 1)
have pos : dist (s.points j) (s.points 1) = dist (s.points j) (s.points ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1))
Tactic: simp only [comp_apply, Equiv.swap_apply_left]
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ dist (s.points j) (s.points 1) = dist (s.points j) (s.points ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1))
have h : Eq (α := Fin (n + 1)) ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1) 1
Tactic: convert! rfl
-- 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
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
x : P ≃ᵢ P
hx : s.points ∘ (⇑(Equiv.swap 0 j) : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ Eq (α := Fin (n + 1)) ((Equiv.swap 0 j : (a : Fin (n + 1)) → Fin (n + 1)) 1) 1
have h : Eq (α := Fin (n + 1)) 1 1
Tactic: rw [Equiv.swap_apply_of_ne_of_ne (by simp [hn]) (by lia)]