-- Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean
lemma Truncated.morphismProperty_eq_top
    {d : ℕ} (W : MorphismProperty (Truncated d)) [W.IsMultiplicative]
    (δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)),
    W (SimplexCategory.δ (n := n) i : ⟨.mk n, by dsimp; omega⟩ ⟶
      ⟨.mk (n + 1), by dsimp; omega⟩))
    (σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)),
    W (SimplexCategory.σ (n := n) i : ⟨.mk (n + 1), by dsimp; omega⟩ ⟶
      ⟨.mk n, by dsimp; omega⟩)) :
    W = ⊤

Proof state:
case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
f' : mk a ⟶ mk b := f
h₁ : Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

case neg
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
f' : mk a ⟶ mk b := f
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

Tactic:
swap

Result:
case neg
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
f' : mk a ⟶ mk b := f
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

case pos
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
f' : mk a ⟶ mk b := f
h₁ : Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

Proof state:
case h.mk.mk.h.h.zero
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
ha hb : 0 ≤ d
h : 0 + 0 = 0
⊢ W (𝟙 { obj := mk 0, property := ha })

Tactic:
apply MorphismProperty.id_mem

Result:
no goals

Proof state:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := mk (a + 1), property := ha } ⟶ { obj := mk b, property := hb }
h : a + 1 + b = c + 1
f' : mk (a + 1) ⟶ mk b := f
h₁ : Function.Surjective ⇑(Hom.toOrderHom f')
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f')
i : Fin (a + 1)
g' : mk a ⟶ mk b
hf' : f' = σ i ≫ g'
⊢ { obj := mk (a + 1), property := ha } ⟶ { obj := mk a, property := ?m.4387 }

Tactic:
exact σ i

Result:
no goals

Proof state:
case h.mk.mk.h.h.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
⊢ W f

Tactic:
let f' : mk a ⟶ mk b := f

Result:
case h.mk.mk.h.h.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
f' : mk a ⟶ mk b := f
⊢ W f

Proof state:
case neg
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }
h : a + b = c + 1
f' : mk a ⟶ mk b := f
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

Tactic:
obtain _ | b := b

Result:
case neg.zero
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
hb : 0 ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk 0, property := hb }
h : a + 0 = c + 1
f' : mk a ⟶ mk 0 := f
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

case neg.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b + 1 ≤ d
f : { obj := mk a, property := ha } ⟶ { obj := mk (b + 1), property := hb }
h : a + (b + 1) = c + 1
f' : mk a ⟶ mk (b + 1) := f
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f')
⊢ W f

Proof state:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
h : a + 1 + b = c + 1
i : Fin (a + 1)
g' : mk a ⟶ mk b
f' : mk (a + 1) ⟶ mk b := σ i ≫ g'
h₁ : Function.Surjective ⇑(Hom.toOrderHom f')
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f')
hf' : f' = σ i ≫ g'
⊢ a < d

Tactic:
omega

Result:
no goals

Proof state:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ i)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d) (f : { obj := mk a, property := ha } ⟶ { obj := mk b, property := hb }),
    a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b + 1 ≤ d
h : a + (b + 1) = c + 1
i : Fin (b + 2)
g' : mk a ⟶ mk b
f' : mk a ⟶ mk (b + 1) := g' ≫ δ i
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f')
⊢ a + b = c

Tactic:
omega

Result:
no goals