awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
⊢ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
have mp : ∀ (this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
h' : ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 2)
hi : i ∈ finset f x
⊢ y.castSucc ≤ i
have mpr : ∀ (i : Fin (n + 1)) (hi : i.castSucc ∈ finset f x), y.castSucc ≤ i.castSucc
Tactic: obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
h' : ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 2)
hi : i ∈ finset f x
mpr : ∀ (i : Fin (n + 1)) (hi : i.castSucc ∈ finset f x), y.castSucc ≤ i.castSucc
⊢ y.castSucc ≤ i
have mpr₁ : ∀ (hi : Fin.last (n + 1) ∈ finset f x), y.castSucc ≤ Fin.last (n + 1)
Tactic: obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
h' : ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
⊢ y.castSucc ≤ i.castSucc
have mpr : y ≤ i
Tactic: simp only [Fin.castSucc_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y)
h' : ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
⊢ y ≤ i
have mpr : ∀ (this : i < y), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
x : Fin (n + 2)
⊢ map' OrderHom.id x = x
have inl : ∀ (x : Fin (n + 1)), map' OrderHom.id x.castSucc = x.castSucc
Tactic: obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
x : Fin (n + 2)
inl : ∀ (x : Fin (n + 1)), map' OrderHom.id x.castSucc = x.castSucc
⊢ map' OrderHom.id x = x
have inr : Eq (α := Fin (n + 2)) (map' OrderHom.id (Fin.last (n + 1))) (Fin.last (n + 1))
Tactic: obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
x : Fin (n + 1)
⊢ map' OrderHom.id x.castSucc = x.castSucc
have inl : x.castSucc ≤ Fin.castSucc ((OrderHom.id : (a : Fin (n + 1)) → Fin (n + 1)) x) ∧
  ∀ i < x, Fin.castSucc ((OrderHom.id : (a : Fin (n + 1)) → Fin (n + 1)) i) < x.castSucc
Tactic: rw [map'_eq_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 2)
⊢ map' f (map' g x) = map' (g.comp f) x
have inl : ∀ (x : Fin (p + 1)), map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
Tactic: obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 2)
inl : ∀ (x : Fin (p + 1)), map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
⊢ map' f (map' g x) = map' (g.comp f) x
have inr : map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))
Tactic: obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
have inl : ∀ (y : Fin (m + 1)) (hy : map' g x.castSucc = y.castSucc), map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
Tactic: obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
inl : ∀ (y : Fin (m + 1)) (hy : map' g x.castSucc = y.castSucc), map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
have inl₁ : ∀ (hx : map' g x.castSucc = Fin.last (m + 1)), map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
Tactic: obtain ⟨y, hy⟩ | hx := Fin.eq_castSucc_or_eq_last (map' g x.castSucc)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
have inl : map' f y.castSucc = map' (g.comp f) x.castSucc
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (hypothesis)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : map' g x.castSucc = y.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
have hy₁ : x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
  ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
Tactic: rw [map'_eq_castSucc_iff] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
have inl : ∀ (z : Fin (n + 1)) (hz : map' f y.castSucc = z.castSucc), map' f y.castSucc = map' (g.comp f) x.castSucc
Tactic: obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
inl : ∀ (z : Fin (n + 1)) (hz : map' f y.castSucc = z.castSucc), map' f y.castSucc = map' (g.comp f) x.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
have inl₁ : ∀ (hz : map' f y.castSucc = Fin.last (n + 1)), map' f y.castSucc = map' (g.comp f) x.castSucc
Tactic: obtain ⟨z, hz⟩ | hz := Fin.eq_castSucc_or_eq_last (map' f y.castSucc)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
have inl : map' (g.comp f) x.castSucc = z.castSucc
Tactic: rw [hz, Eq.comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' (g.comp f) x.castSucc = z.castSucc
have inl : ∀
  (hz :
    y.castSucc ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z) ∧
      ∀ i < z, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc),
  x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc
Tactic: rw [map'_eq_castSucc_iff] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
z : Fin (n + 1)
hz :
  y.castSucc ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc
⊢ x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc
have inl : x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
z : Fin (n + 1)
hz :
  y.castSucc ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc
inl : x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z)
⊢ x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc
have inl₁ : ∀ i < z, Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
z : Fin (n + 1)
hz :
  y.castSucc ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc
⊢ x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z)
have inl : LE.le (α := Fin (p + 2)) (Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y))
  (Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z))
Tactic: refine hy.1.trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
z : Fin (n + 1)
hz :
  y.castSucc ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z) ∧
    ∀ i < z, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc
⊢ LE.le (α := Fin (p + 2)) (Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y))
    (Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z))
have inl : LE.le (α := Fin (p + 1)) ((g : (a : Fin (m + 1)) → Fin (p + 1)) y : Fin (p + 1))
  ((g : (a : Fin (m + 1)) → Fin (p + 1)) ((f : (a : Fin (n + 1)) → Fin (m + 1)) z) : Fin (p + 1))
Tactic: simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc
have inl : map' (g.comp f) x.castSucc = Fin.last (n + 1)
Tactic: rw [hz, Eq.comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy :
  x.castSucc ≤ Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) y) ∧
    ∀ i < y, Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)
have inl : ∀ (hz : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc) (i : Fin (n + 1)),
  Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc
Tactic: rw [map'_eq_last_iff] at hz ⊢
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc
have inl : map' (g.comp f) x.castSucc = Fin.last (n + 1)
Tactic: rw [Eq.comm, hx, map'_last]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)
have inl : ∀ (hx : ∀ (i : Fin (m + 1)), Fin.castSucc ((g : (a : Fin (m + 1)) → Fin (p + 1)) i) < x.castSucc) (i : Fin (n + 1)),
  Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc
Tactic: rw [map'_eq_last_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 3)
⊢ map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x
have inl : ∀ (x : Fin (n + 2)), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Tactic: obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 3)
inl : ∀ (x : Fin (n + 2)), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x
have inr : map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))
Tactic: obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
have pos : ∀ (hx : x ≤ i), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Tactic: by_cases! hx : x ≤ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 2)
pos : ∀ (hx : x ≤ i), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
have neg : ∀ (hx : i < x), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Tactic: by_cases! hx : x ≤ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
have pos : map' i.succAboveOrderEmb.toOrderHom x.castSucc = x
Tactic: rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = x
have pos : ∀ (x : Fin (n + 1)) (hx : x.castSucc ≤ i), map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = x.castSucc
Tactic: obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
pos : ∀ (x : Fin (n + 1)) (hx : x.castSucc ≤ i), map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = x.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = x
have pos₁ : ∀ (hx : Fin.last (n + 1) ≤ i), map' i.succAboveOrderEmb.toOrderHom (Fin.castSucc (Fin.last (n + 1))) = Fin.last (n + 1)
Tactic: obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = x.castSucc
have pos : x.castSucc ≤ i.succAbove x ∧ ∀ i_1 < x, i.succAbove i_1 < x.castSucc
Tactic: simp only [map'_eq_castSucc_iff, OrderEmbedding.toOrderHom_coe,
          Fin.succAboveOrderEmb_apply, Fin.castSucc_le_castSucc_iff,
          Fin.castSucc_lt_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x ∧ ∀ i_1 < x, i.succAbove i_1 < x.castSucc
have pos : x.castSucc ≤ i.succAbove x
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
pos : x.castSucc ≤ i.succAbove x
⊢ x.castSucc ≤ i.succAbove x ∧ ∀ i_1 < x, i.succAbove i_1 < x.castSucc
have pos₁ : ∀ i_1 < x, i.succAbove i_1 < x.castSucc
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ x.castSucc ≤ i.succAbove x
have pos : ∀ (hx : x.castSucc < i), x.castSucc ≤ i.succAbove x
Tactic: obtain hx | rfl := hx.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
pos : ∀ (hx : x.castSucc < i), x.castSucc ≤ i.succAbove x
⊢ x.castSucc ≤ i.succAbove x
have pos₁ : ∀ (hx : x.castSucc ≤ x.castSucc), x.castSucc ≤ x.castSucc.succAbove x
Tactic: obtain hx | rfl := hx.lt_or_eq
Cleared hypotheses: i, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx_1 : x.castSucc ≤ i
hx : x.castSucc < i
⊢ x.castSucc ≤ i.succAbove x
have pos : x.castSucc ≤ x.castSucc
Tactic: rwa [Fin.succAbove_of_castSucc_lt]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.castSucc
have pos : j.castSucc < x.castSucc
Tactic: rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.castSucc (Fin.last (n + 1))) = Fin.last (n + 1)
have pos : ∀ (hx : LE.le (α := Fin (n + 2)) (Fin.last (n + 1)) (Fin.last (n + 1))),
  Eq (α := Fin (n + 2))
    (map' (OrderEmbedding.toOrderHom (Fin.succAboveOrderEmb (Fin.last (n + 1)))) (Fin.castSucc (Fin.last (n + 1))))
    (Fin.last (n + 1))
Tactic: obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx
Cleared hypotheses: i, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
have neg : ∀ (x : Fin (n + 1)) (hx : i < x.succ), map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = i.predAbove x.succ.castSucc
Tactic: obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = i.predAbove x.succ.castSucc
have neg : x.succ.castSucc ≤ Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) x) ∧
  ∀ i_1 < x, Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i_1) < x.succ.castSucc
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ x.succ.castSucc ≤ Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) x) ∧
    ∀ i_1 < x,
      Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i_1) < x.succ.castSucc
have neg : ∀ i_1 < x, i.succAbove i_1 < x.succ
Tactic: simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.succ
have pos : ∀ (h : j.castSucc < i), i.succAbove j < x.succ
Tactic: by_cases! h : j.castSucc < i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
pos : ∀ (h : j.castSucc < i), i.succAbove j < x.succ
⊢ i.succAbove j < x.succ
have neg : ∀ (h : i ≤ j.castSucc), i.succAbove j < x.succ
Tactic: by_cases! h : j.castSucc < i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
⊢ i.succAbove j < x.succ
have neg : j.succ < x.succ
Tactic: rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 1)
x : Fin (n + 2)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x = i.succ.castSucc.succAbove x
have inl : ∀ (x : Fin (n + 1)),
  map' { toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
Tactic: obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i : Fin (n + 1)
x : Fin (n + 2)
inl :
  ∀ (x : Fin (n + 1)),
    map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
      i.succ.castSucc.succAbove x.castSucc
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x = i.succ.castSucc.succAbove x
have inr : map' { toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } (Fin.last (n + 1)) =
  i.succ.castSucc.succAbove (Fin.last (n + 1))
Tactic: obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialObject.II (goal)
Goal:
n : ℕ
i x : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
have pos : ∀ (hi : i < x),
  map' { toFun := i.predAbove, monotone' := sorry : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc
Tactic: by_cases! hi : i < x