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
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 (α := { x : Fin (m + 1) × Fin (m + 1) // x.1 < x.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 }))

Tactic:
(Injective.of_comp_iff' _ (Equiv.bijective f)).symm

Premises used: Equiv.bijective, Function.Injective.of_comp_iff', Iff.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
n : ℕ
s : Simplex R P n
he : s.Equilateral
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
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₄)
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

Tactic:
rcases he with ⟨r, hr⟩
-- 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
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₄)
rw₁ rw₂ : r = r
⊢ dist (s.points i₁) (s.points i₂) = dist (s.points i₃) (s.points i₄)

Tactic:
rw [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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Equilateral ↔ s.Equilateral

Tactic:
⟨fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩⟩

Premises used: _private.0.Affine.Simplex.equilateral_reindex_iff.match_2, _private.0.Affine.Simplex.equilateral_reindex_iff.match_1, Affine.Simplex.reindex, Affine.Simplex.Equilateral, Iff.intro, Exists.intro
-- 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
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
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
⊢ (s.reindex e).Equilateral ↔ s.Equilateral

Tactic:
refine ⟨fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩, fun ⟨r, hr⟩ ↦ ⟨r, fun i j hij ↦ ?_⟩⟩
-- 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
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.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i))
      ((s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) j)) =
    r

Tactic:
hr (e i) (e j) (e.injective.ne hij)

Premises used: Function.Injective.ne, Equiv.injective, DFunLike.coe
-- 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
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)
h₁ : s.points j = (s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) j)
⊢ dist (s.points i) (s.points j) = r

Tactic:
convert! hr (e i) (e j) (e.injective.ne hij) using 2

Premises used: Function.Injective.ne, Equiv.injective, DFunLike.coe
-- 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
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
⊢ s.points i = (s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) i)

Tactic:
simp
-- 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
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
⊢ s.points j = (s.reindex e).points ((e : (a : Fin (m + 1)) → Fin (n + 1)) j)

Tactic:
simp
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : 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.points ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) i))
      (s.points ((e.symm : (a : Fin (n + 1)) → Fin (m + 1)) j)) =
    r

Tactic:
hr (e.symm i) (e.symm j) (e.symm.injective.ne hij)

Premises used: Function.Injective.ne, Equiv.injective, Equiv.symm, DFunLike.coe
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : 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:
convert! hr (e.symm i) (e.symm j) (e.symm.injective.ne hij) using 2

Premises used: Function.Injective.ne, Equiv.injective, Equiv.symm, DFunLike.coe
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Regular ↔ s.Regular

Tactic:
⟨fun h σ ↦ ?_, fun h σ ↦ ?_⟩

Premises used: Iff.intro
-- 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
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
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
⊢ (s.reindex e).Regular ↔ s.Regular

Tactic:
refine ⟨fun h σ ↦ ?_, 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : (s.reindex e).Regular
σ : Equiv.Perm (Fin (m + 1))
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
⊢ ∃ (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⟩

Premises used: Equiv.trans, Equiv.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
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

Tactic:
⟨x, ?_⟩

Premises used: Exists.intro
-- 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
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
refine_1 : s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points
⊢ ∃ (x : P ≃ᵢ P), s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points

Tactic:
refine ⟨x, ?_⟩
-- 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
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
refine_1 :
  ∀ (i : Fin (m + 1)), (s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1))) i = ((⇑x : (a : P) → P) ∘ s.points) i
⊢ s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1)) = (⇑x : (a : P) → P) ∘ s.points

Tactic:
ext 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
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
i : Fin (m + 1)
⊢ (s.points ∘ (⇑σ : (a : Fin (m + 1)) → Fin (m + 1))) i = ((⇑x : (a : P) → P) ∘ s.points) i

Tactic:
simpa using congrFun hx (e i)

Premises used: congrFun, DFunLike.coe
-- 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
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
h : s.Regular
σ : Equiv.Perm (Fin (n + 1))
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
⊢ ∃ (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⟩

Premises used: Equiv.trans, Equiv.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
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

Tactic:
⟨x, ?_⟩

Premises used: Exists.intro
-- 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
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
refine_2 : (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points
⊢ ∃ (x : P ≃ᵢ P),
    (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points

Tactic:
refine ⟨x, ?_⟩
-- 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
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
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
⊢ (s.reindex e).points ∘ (⇑σ : (a : Fin (n + 1)) → Fin (n + 1)) = (⇑x : (a : P) → P) ∘ (s.reindex e).points

Tactic:
ext 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
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
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:
simpa using congrFun hx (e.symm i)

Premises used: congrFun, Equiv.symm, DFunLike.coe
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
⊢ s.Equilateral

Tactic:
⟨dist (s.points 0) (s.points 1), fun i j hij ↦ ?_⟩

Premises used: Affine.Simplex.points, Affine.Simplex.Equilateral, Exists.intro, Dist.dist, OfNat.ofNat
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
refine : ∀ (i j : Fin (n + 1)) (hij : i ≠ j), dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)
⊢ s.Equilateral

Tactic:
refine ⟨dist (s.points 0) (s.points 1), fun i j hij ↦ ?_⟩
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
⊢ n ≠ 0

Tactic:
lia
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
⊢ n ≠ 0

Tactic:
have hn : n ≠ 0 := by lia
-- 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
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)
neg : ∀ (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)

Tactic:
by_cases hi : i = 1
-- 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
pos : dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)
⊢ dist (s.points i) (s.points j) = dist (s.points 0) (s.points 1)

Tactic:
rw [hi, 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
n : ℕ
s : Simplex R P n
hr : s.Regular
i j : Fin (n + 1)
hij : i ≠ j
hn : n ≠ 0
hi : i = 1
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)
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)

Tactic:
rcases hr (Equiv.swap 0 j) with ⟨x, hx⟩

Premises used: Equiv.swap, OfNat.ofNat
-- 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
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
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)
⊢ dist (s.points j) (s.points 1) = dist (s.points 0) (s.points 1)

Tactic:
nth_rw 2 [← x.dist_eq]

Premises used: IsometryEquiv.dist_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
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
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)
⊢ 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:
simp_rw [← Function.comp_apply (f := x), ← hx]

Premises used: Function.comp_apply
-- 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
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
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))
⊢ 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 only [comp_apply, Equiv.swap_apply_left]

Premises used: Function.comp_apply, Equiv.swap_apply_left
-- 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
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 1)

Tactic:
rfl

Premises used: rfl