awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
i : Fin (n + 1)
this : i.castSucc ≠ Fin.last (n + 1)
hi : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ False

Tactic:
exact hi.not_gt (h i)

Premises used: LE.le.not_gt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
simp :
  x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y) →
    ((∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x)
⊢ map' f x = y.castSucc ↔
    x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) y) ∧
      ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x

Tactic:
simp only [map', Finset.min'_eq_iff, castSucc_mem_finset_iff, and_congr_right_iff]

Premises used: SimplexCategory.II.map', and_congr_right_iff, SimplexCategory.II.castSucc_mem_finset_iff, Finset.min'_eq_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)
mp : (∀ b ∈ finset f x, y.castSucc ≤ b) → ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x
mpr : (∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x) → ∀ b ∈ finset f x, y.castSucc ≤ b
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
mp : ∀ (this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)), False
⊢ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < x

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ i.castSucc ∈ finset f x

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ y ≤ i

Tactic:
simpa using h' i.castSucc (by simpa)

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
this : x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)
⊢ False

Tactic:
exact hi.not_ge (by simpa using h' i.castSucc (by simpa))

Premises used: LT.lt.not_ge
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
mpr₁ : ∀ (hi : Fin.last (n + 1) ∈ finset f x), y.castSucc ≤ Fin.last (n + 1)
⊢ y.castSucc ≤ i

Tactic:
obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
mpr : y ≤ i
⊢ y.castSucc ≤ i.castSucc

Tactic:
simp only [Fin.castSucc_le_castSucc_iff]

Premises used: Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
mpr : ∀ (this : i < y), False
⊢ y ≤ i

Tactic:
by_contra!
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
this : i < y
⊢ x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i)

Tactic:
simpa using hi
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
this : i < y
⊢ False

Tactic:
exact (h' i this).not_ge (by simpa using hi)

Premises used: LT.lt.not_ge
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
hi : Fin.last (n + 1) ∈ finset f x
⊢ y.castSucc ≤ Fin.last (n + 1)

Tactic:
apply Fin.le_last

Premises used: Fin.le_last
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
⊢ map' f (Fin.last (m + 1)) = Fin.last (n + 1)

Tactic:
simp [map'_eq_last_iff]

Premises used: SimplexCategory.II.map'_eq_last_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
⊢ map' f 0 = 0

Tactic:
simp [← Fin.castSucc_zero, -Fin.castSucc_zero', map'_eq_castSucc_iff]

Premises used: Fin.castSucc_zero', SimplexCategory.II.map'_eq_castSucc_iff, Fin.castSucc_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
x : Fin (n + 2)
inl : ∀ (x : Fin (n + 1)), map' OrderHom.id x.castSucc = x.castSucc
inr : Eq (α := Fin (n + 2)) (map' OrderHom.id (Fin.last (n + 1))) (Fin.last (n + 1))
⊢ map' OrderHom.id x = x

Tactic:
obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
x : Fin (n + 1)
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
⊢ map' OrderHom.id x.castSucc = x.castSucc

Tactic:
rw [map'_eq_castSucc_iff]

Premises used: SimplexCategory.II.map'_eq_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
x : Fin (n + 1)
⊢ 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:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 2)) (map' OrderHom.id (Fin.last (n + 1))) (Fin.last (n + 1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
inr : map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))
⊢ map' f (map' g x) = map' (g.comp f) x

Tactic:
obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
inl₁ : ∀ (hx : map' g x.castSucc = Fin.last (m + 1)), map' f (map' g x.castSucc) = map' (g.comp f) x.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)

Premises used: SimplexCategory.II.map', Fin.eq_castSucc_or_eq_last, Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
inl : map' f y.castSucc = map' (g.comp f) x.castSucc
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
rw [hy]
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
⊢ 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

Premises used: SimplexCategory.II.map'_eq_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
inl₁ : ∀ (hz : map' f y.castSucc = Fin.last (n + 1)), map' f y.castSucc = map' (g.comp f) x.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)

Premises used: SimplexCategory.II.map', Fin.eq_castSucc_or_eq_last, Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
inl : map' (g.comp f) x.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
rw [hz, Eq.comm]

Premises used: Eq.comm
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
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
⊢ map' (g.comp f) x.castSucc = z.castSucc

Tactic:
rw [map'_eq_castSucc_iff] at hz ⊢

Premises used: SimplexCategory.II.map'_eq_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)
inl₁ : ∀ i < z, Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.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:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)

Tactic:
hy.1.trans ?_

Premises used: And.left, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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 :
  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))
⊢ x.castSucc ≤ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) z)

Tactic:
refine hy.1.trans ?_

Premises used: And.left, LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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 :
  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))
⊢ 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:
simp only [OrderHom.comp_coe, Function.comp_apply, Fin.castSucc_le_castSucc_iff]

Premises used: OrderHom.comp_coe, Fin.castSucc_le_castSucc_iff, Function.comp_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
⊢ y ≤ (f : (a : Fin (n + 1)) → Fin (m + 1)) z

Tactic:
simpa using hz.1

Premises used: And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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 + 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:
exact g.monotone (by simpa using hz.1)

Premises used: OrderHom.monotone
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
i : Fin (n + 1)
hi : i < z
⊢ (f : (a : Fin (n + 1)) → Fin (m + 1)) i < y

Tactic:
simpa using hz.2 i hi

Premises used: And.right
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
i : Fin (n + 1)
hi : i < z
⊢ Fin.castSucc ((g.comp f : (a : Fin (n + 1)) → Fin (p + 1)) i) < x.castSucc

Tactic:
exact hy.2 (f i) (by simpa using hz.2 i hi)

Premises used: And.right, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)
inl : map' (g.comp f) x.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
rw [hz, Eq.comm]

Premises used: Eq.comm
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)
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
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)

Tactic:
rw [map'_eq_last_iff] at hz ⊢

Premises used: SimplexCategory.II.map'_eq_last_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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 : ∀ (i : Fin (n + 1)), Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) i) < y.castSucc
i : Fin (n + 1)
⊢ (f : (a : Fin (n + 1)) → Fin (m + 1)) i < y

Tactic:
simpa using hz i
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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 : ∀ (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:
exact hy.2 (f i) (by simpa using hz i)

Premises used: And.right, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)
inl : map' (g.comp f) x.castSucc = Fin.last (n + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
rw [Eq.comm, hx, map'_last]

Premises used: SimplexCategory.II.map'_last, Eq.comm
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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)
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
⊢ map' (g.comp f) x.castSucc = Fin.last (n + 1)

Tactic:
rw [map'_eq_last_iff] at hx ⊢

Premises used: SimplexCategory.II.map'_eq_last_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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 : ∀ (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:
apply hx
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
⊢ map' f (map' g (Fin.last (p + 1))) = map' (g.comp f) (Fin.last (p + 1))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
inr : map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))
⊢ map' i.succAboveOrderEmb.toOrderHom x = i.predAbove x

Tactic:
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 2)
pos : ∀ (hx : x ≤ i), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
neg : ∀ (hx : i < x), map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
by_cases! hx : x ≤ i
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
pos : map' i.succAboveOrderEmb.toOrderHom x.castSucc = x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ (by simpa), Fin.castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, Fin.predAbove_of_le_castSucc, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
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
pos₁ :
  ∀ (hx : Fin.last (n + 1) ≤ i),
    map' i.succAboveOrderEmb.toOrderHom (Fin.castSucc (Fin.last (n + 1))) = Fin.last (n + 1)
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = x

Tactic:
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
pos : x.castSucc ≤ i.succAbove x ∧ ∀ i_1 < x, i.succAbove i_1 < x.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc.castSucc = 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]

Premises used: OrderEmbedding.toOrderHom_coe, Fin.castSucc_lt_castSucc_iff, SimplexCategory.II.map'_eq_castSucc_iff, Fin.castSucc_le_castSucc_iff, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
pos : x.castSucc ≤ i.succAbove x
pos₁ : ∀ i_1 < x, i.succAbove i_1 < x.castSucc
⊢ x.castSucc ≤ i.succAbove x ∧ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
constructor