-- Mathlib/Analysis/Normed/Affine/Simplex.lean
@[simp] lemma regular_reindex_iff {s : Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).Regular ↔ s.Regular

Proof state:
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex R P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).Regular ↔ s.Regular

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

Result:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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, s.points ∘ ⇑σ = ⇑x ∘ s.points

case refine_2
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Proof state:
case refine_2.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ s.points
⊢ ∃ x, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Tactic:
refine ⟨x, ?_⟩

Result:
case refine_2.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ s.points
⊢ (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Proof state:
case refine_1.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ (s.reindex e).points
⊢ s.points ∘ ⇑σ = ⇑x ∘ s.points

Tactic:
ext i

Result:
case refine_1.intro.h
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ (s.reindex e).points
i : Fin (m + 1)
⊢ (s.points ∘ ⇑σ) i = (⇑x ∘ s.points) i

Proof state:
case refine_1.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ (s.reindex e).points
⊢ ∃ x, s.points ∘ ⇑σ = ⇑x ∘ s.points

Tactic:
refine ⟨x, ?_⟩

Result:
case refine_1.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ (s.reindex e).points
⊢ s.points ∘ ⇑σ = ⇑x ∘ s.points

Proof state:
case refine_2
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Tactic:
rcases h ((e.trans σ).trans e.symm) with ⟨x, hx⟩

Result:
case refine_2.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ s.points
⊢ ∃ x, (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Proof state:
case refine_1
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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, s.points ∘ ⇑σ = ⇑x ∘ s.points

Tactic:
rcases h ((e.symm.trans σ).trans e) with ⟨x, hx⟩

Result:
case refine_1.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ (s.reindex e).points
⊢ ∃ x, s.points ∘ ⇑σ = ⇑x ∘ s.points

Proof state:
case refine_2.intro.h
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ s.points
i : Fin (n + 1)
⊢ ((s.reindex e).points ∘ ⇑σ) i = (⇑x ∘ (s.reindex e).points) i

Tactic:
simpa using congrFun hx (e.symm i)

Result:
no goals

Proof state:
case refine_1.intro.h
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ (s.reindex e).points
i : Fin (m + 1)
⊢ (s.points ∘ ⇑σ) i = (⇑x ∘ s.points) i

Tactic:
simpa using congrFun hx (e i)

Result:
no goals

Proof state:
case refine_2.intro
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ s.points
⊢ (s.reindex e).points ∘ ⇑σ = ⇑x ∘ (s.reindex e).points

Tactic:
ext i

Result:
case refine_2.intro.h
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : 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) = ⇑x ∘ s.points
i : Fin (n + 1)
⊢ ((s.reindex e).points ∘ ⇑σ) i = (⇑x ∘ (s.reindex e).points) i