[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x✝ x : List α
⊢ x ∈ 1 ↔ x = []
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l
[PROOFSTEP]
contradiction
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 * l = l
[PROOFSTEP]
simp [mul_def, one_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l * 1 = l
[PROOFSTEP]
simp [mul_def, one_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
⊢ NatCast.natCast (Nat.zero + 1) = NatCast.natCast Nat.zero + 1
[PROOFSTEP]
simp [Nat.cast, add_def, zero_def]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
n✝ : ℕ
⊢ NatCast.natCast (Nat.succ n✝ + 1) = NatCast.natCast (Nat.succ n✝) + 1
[PROOFSTEP]
simp [Nat.cast, add_def, zero_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ ↑(map id) l = l
[PROOFSTEP]
simp [map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
g : β → γ
f : α → β
l : Language α
⊢ ↑(map g) (↑(map f) l) = ↑(map (g ∘ f)) l
[PROOFSTEP]
simp [map, image_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ = {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ → x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
[PROOFSTEP]
rintro ⟨S, rfl, h⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
⊢ join S ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []}
[PROOFSTEP]
refine'
  ⟨S.filter fun l ↦ ¬List.isEmpty l, by simp, fun y hy ↦ _⟩
    -- Porting note: The previous code was:
        -- rw [mem_filter, empty_iff_eq_nil] at hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
⊢ join S = join (filter (fun l => decide ¬isEmpty l = true) S)
[PROOFSTEP]
simp
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ filter (fun l => decide ¬isEmpty l = true) S
⊢ y ∈ l ∧ y ≠ []
[PROOFSTEP]
rw [mem_filter, decide_not, Bool.decide_coe, Bool.not_eq_true', ← Bool.bool_iff_false, isEmpty_iff_eq_nil] at hy
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
h : ∀ (y : List α), y ∈ S → y ∈ l
y : List α
hy : y ∈ S ∧ ¬y = []
⊢ y ∈ l ∧ y ≠ []
[PROOFSTEP]
exact ⟨h y hy.1, hy.2⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ {x | ∃ S, x = join S ∧ ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []} → x ∈ l∗
[PROOFSTEP]
rintro ⟨S, hx, h⟩
[GOAL]
case h.mpr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
S : List (List α)
hx : x = join S
h : ∀ (y : List α), y ∈ S → y ∈ l ∧ y ≠ []
⊢ x ∈ l∗
[PROOFSTEP]
exact ⟨S, hx, fun y hy ↦ (h y hy).1⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x : List α
l₁ l₂ m₁ m₂ : Language α
⊢ l₁ ≤ m₁ → l₂ ≤ m₂ → l₁ * l₂ ≤ m₁ * m₂
[PROOFSTEP]
intro h₁ h₂ x hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : x ∈ l₁ * l₂
⊢ x ∈ m₁ * m₂
[PROOFSTEP]
simp only [mul_def, exists_and_left, mem_image2, image_prod] at hx ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l m : Language α
a b x✝ : List α
l₁ l₂ m₁ m₂ : Language α
h₁ : l₁ ≤ m₁
h₂ : l₂ ≤ m₂
x : List α
hx : ∃ a, a ∈ l₁ ∧ ∃ x_1, x_1 ∈ l₂ ∧ a ++ x_1 = x
⊢ ∃ a, a ∈ m₁ ∧ ∃ x_1, x_1 ∈ m₂ ∧ a ++ x_1 = x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
n : ℕ
⊢ x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
induction' n with n ihn generalizing x
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ x ∈ l ^ Nat.zero ↔ ∃ S, x = join S ∧ length S = Nat.zero ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
simp only [mem_one, pow_zero, length_eq_zero]
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ x = [] ↔ ∃ S, x = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
constructor
[GOAL]
case zero.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ x = [] → ∃ S, x = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ ∃ S, [] = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
exact ⟨[], rfl, rfl, fun _ h ↦ by contradiction⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l
[PROOFSTEP]
contradiction
[GOAL]
case zero.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ x : List α
⊢ (∃ S, x = join S ∧ S = [] ∧ ∀ (y : List α), y ∈ S → y ∈ l) → x = []
[PROOFSTEP]
rintro ⟨_, rfl, rfl, _⟩
[GOAL]
case zero.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
right✝ : ∀ (y : List α), y ∈ [] → y ∈ l
⊢ join [] = []
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ x ∈ l ^ Nat.succ n ↔ ∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
simp only [pow_succ, mem_mul, ihn]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ (∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = x) ↔
    ∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
constructor
[GOAL]
case succ.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ (∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = x) →
    ∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
rintro ⟨a, b, ha, ⟨S, rfl, rfl, hS⟩, rfl⟩
[GOAL]
case succ.mp.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x a : List α
ha : a ∈ l
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
ihn : ∀ {x : List α}, x ∈ l ^ length S ↔ ∃ S_1, x = join S_1 ∧ length S_1 = length S ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
⊢ ∃ S_1, a ++ join S = join S_1 ∧ length S_1 = Nat.succ (length S) ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
[PROOFSTEP]
exact ⟨a :: S, rfl, rfl, forall_mem_cons.2 ⟨ha, hS⟩⟩
[GOAL]
case succ.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝¹ : List α
l : Language α
x✝ : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
x : List α
⊢ (∃ S, x = join S ∧ length S = Nat.succ n ∧ ∀ (y : List α), y ∈ S → y ∈ l) →
    ∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = x
[PROOFSTEP]
rintro ⟨_ | ⟨a, S⟩, rfl, hn, hS⟩
[GOAL]
case succ.mpr.intro.nil.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
hn : length [] = Nat.succ n
hS : ∀ (y : List α), y ∈ [] → y ∈ l
⊢ ∃ a b, a ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a ++ b = join []
[PROOFSTEP]
cases hn
[GOAL]
case succ.mpr.intro.cons.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x : List α
n : ℕ
ihn : ∀ {x : List α}, x ∈ l ^ n ↔ ∃ S, x = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l
a : List α
S : List (List α)
hn : length (a :: S) = Nat.succ n
hS : ∀ (y : List α), y ∈ a :: S → y ∈ l
⊢ ∃ a_1 b, a_1 ∈ l ∧ (∃ S, b = join S ∧ length S = n ∧ ∀ (y : List α), y ∈ S → y ∈ l) ∧ a_1 ++ b = join (a :: S)
[PROOFSTEP]
cases hn
[GOAL]
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x a : List α
S : List (List α)
hS : ∀ (y : List α), y ∈ a :: S → y ∈ l
ihn :
  ∀ {x : List α},
    x ∈ l ^ Nat.add (length S) 0 ↔
      ∃ S_1, x = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
⊢ ∃ a_1 b,
    a_1 ∈ l ∧
      (∃ S_1, b = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l) ∧
        a_1 ++ b = join (a :: S)
[PROOFSTEP]
rw [forall_mem_cons] at hS
[GOAL]
case succ.mpr.intro.cons.intro.intro.refl
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x✝ : List α
l : Language α
x a : List α
S : List (List α)
hS : a ∈ l ∧ ∀ (x : List α), x ∈ S → x ∈ l
ihn :
  ∀ {x : List α},
    x ∈ l ^ Nat.add (length S) 0 ↔
      ∃ S_1, x = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
⊢ ∃ a_1 b,
    a_1 ∈ l ∧
      (∃ S_1, b = join S_1 ∧ length S_1 = Nat.add (length S) 0 ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l) ∧
        a_1 ++ b = join (a :: S)
[PROOFSTEP]
exact ⟨a, _, hS.1, ⟨S, rfl, rfl, hS.2⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ = ⨆ (i : ℕ), l ^ i
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ x ∈ l∗ ↔ x ∈ ⨆ (i : ℕ), l ^ i
[PROOFSTEP]
simp only [mem_kstar, mem_iSup, mem_pow]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l) ↔ ∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l) → ∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l
[PROOFSTEP]
rintro ⟨S, rfl, hS⟩
[GOAL]
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
⊢ ∃ i S_1, join S = join S_1 ∧ length S_1 = i ∧ ∀ (y : List α), y ∈ S_1 → y ∈ l
[PROOFSTEP]
exact ⟨_, S, rfl, rfl, hS⟩
[GOAL]
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x✝ : List α
l : Language α
x : List α
⊢ (∃ i S, x = join S ∧ length S = i ∧ ∀ (y : List α), y ∈ S → y ∈ l) → ∃ L, x = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l
[PROOFSTEP]
rintro ⟨_, S, rfl, rfl, hS⟩
[GOAL]
case h.mpr.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
S : List (List α)
hS : ∀ (y : List α), y ∈ S → y ∈ l
⊢ ∃ L, join S = join L ∧ ∀ (y : List α), y ∈ L → y ∈ l
[PROOFSTEP]
exact ⟨S, rfl, hS⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
f : α → β
l : Language α
⊢ ↑(map f) l∗ = (↑(map f) l)∗
[PROOFSTEP]
rw [kstar_eq_iSup_pow, kstar_eq_iSup_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
f : α → β
l : Language α
⊢ ↑(map f) (⨆ (i : ℕ), l ^ i) = ⨆ (i : ℕ), ↑(map f) l ^ i
[PROOFSTEP]
simp_rw [← map_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
f : α → β
l : Language α
⊢ ↑(map f) (⨆ (i : ℕ), l ^ i) = ⨆ (i : ℕ), ↑(map f) (l ^ i)
[PROOFSTEP]
exact image_iUnion
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l∗ * l = l * l∗
[PROOFSTEP]
simp only [kstar_eq_iSup_pow, mul_iSup, iSup_mul, ← pow_succ, ← pow_succ']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 + l * l∗ = l∗
[PROOFSTEP]
simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ, ← pow_zero l]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ l ^ 0 + ⨆ (i : ℕ), l ^ (i + 1) = ⨆ (i : ℕ), l ^ i
[PROOFSTEP]
exact sup_iSup_nat_succ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a b x : List α
l : Language α
⊢ 1 + l∗ * l = l∗
[PROOFSTEP]
rw [mul_self_kstar_comm, one_add_self_mul_kstar_eq_kstar]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m : Language α
a✝ b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
a : Language α
l : List α
hl : l ∈ 1
⊢ ∀ (y : List α), y ∈ [] → y ∈ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
⊢ m * l∗ ≤ m
[PROOFSTEP]
rw [kstar_eq_iSup_pow, mul_iSup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
⊢ ⨆ (i : ℕ), m * l ^ i ≤ m
[PROOFSTEP]
refine' iSup_le (fun n ↦ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
n : ℕ
⊢ m * l ^ n ≤ m
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
⊢ m * l ^ Nat.zero ≤ m
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l ^ Nat.succ n ≤ m
[PROOFSTEP]
rw [pow_succ, ← mul_assoc m l (l ^ n)]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : m * l ≤ m
n : ℕ
ih : m * l ^ n ≤ m
⊢ m * l * l ^ n ≤ m
[PROOFSTEP]
exact le_trans (le_mul_congr h le_rfl) ih
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
⊢ l∗ * m ≤ m
[PROOFSTEP]
rw [kstar_eq_iSup_pow, iSup_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
⊢ ⨆ (i : ℕ), l ^ i * m ≤ m
[PROOFSTEP]
refine' iSup_le (fun n ↦ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
n : ℕ
⊢ l ^ n * m ≤ m
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
⊢ l ^ Nat.zero * m ≤ m
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ Nat.succ n * m ≤ m
[PROOFSTEP]
rw [pow_succ', mul_assoc (l ^ n) l m]
[GOAL]
case succ
α : Type u_1
β : Type u_2
γ : Type u_3
l✝ m✝ : Language α
a b x : List α
src✝¹ : Semiring (Language α) := instSemiring
src✝ : CompleteAtomicBooleanAlgebra (Set (List α)) := Set.completeAtomicBooleanAlgebra
l m : Language α
h : l * m ≤ m
n : ℕ
ih : l ^ n * m ≤ m
⊢ l ^ n * (l * m) ≤ m
[PROOFSTEP]
exact le_trans (le_mul_congr le_rfl h) ih


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X✝ Y✝ : SimplexCategoryᵒᵖ
g : X✝ ⟶ Y✝
⊢ ∀ (j : Fin (SimplexCategory.len Y✝.unop + 1)),
    (fun i => WidePullback.π (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g.unop) i)) j ≫ f.hom =
      WidePullback.base fun x => f.hom
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePullback f✝.right (fun x => f✝.left) fun x => f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePullback f.right (fun x => f.left) fun x => f.hom
inst✝ : ∀ (n : ℕ), HasWidePullback g.right (fun x => g.left) fun x => g.hom
F : f ⟶ g
n : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len n.unop + 1)
⊢ (fun i => WidePullback.π (fun x => f.hom) i ≫ F.left) j ≫ g.hom = (WidePullback.base fun x => f.hom) ≫ F.right
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : X ⟶ Arrow.augmentedCechNerve F
⊢ (𝟭 C).map (NatTrans.app G.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
[PROOFSTEP]
have := G.w
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : X ⟶ Arrow.augmentedCechNerve F
this : (𝟭 (SimplicialObject C)).map G.left ≫ (Arrow.augmentedCechNerve F).hom = X.hom ≫ (const C).map G.right
⊢ (𝟭 C).map (NatTrans.app G.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
[PROOFSTEP]
apply_fun fun e => e.app (Opposite.op <| SimplexCategory.mk 0) at this
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : X ⟶ Arrow.augmentedCechNerve F
this :
  NatTrans.app ((𝟭 (SimplicialObject C)).map G.left ≫ (Arrow.augmentedCechNerve F).hom)
      (Opposite.op (SimplexCategory.mk 0)) =
    NatTrans.app (X.hom ≫ (const C).map G.right) (Opposite.op (SimplexCategory.mk 0))
⊢ (𝟭 C).map (NatTrans.app G.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right
[PROOFSTEP]
simpa using this
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin (SimplexCategory.len x.unop + 1)
⊢ (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom = NatTrans.app X.hom x ≫ G.right
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin (SimplexCategory.len x.unop + 1)
⊢ (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right
[PROOFSTEP]
erw [Category.assoc, Arrow.w, Augmented.toArrow_obj_hom, NatTrans.naturality_assoc, Functor.const_obj_map,
  Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f : X_1 ⟶ Y),
    X.left.map f ≫
        (fun x =>
            WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
              (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
              (_ :
                ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                  (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                    NatTrans.app X.hom x ≫ G.right))
          Y =
      (fun x =>
            WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
              (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
              (_ :
                ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                  (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                    NatTrans.app X.hom x ≫ G.right))
          X_1 ≫
        (Arrow.augmentedCechNerve F).left.map f
[PROOFSTEP]
intro x y f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      (fun x =>
          WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
            (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
            (_ :
              ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                  NatTrans.app X.hom x ≫ G.right))
        y =
    (fun x =>
          WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
            (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
            (_ :
              ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
                (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) i ≫ F.hom =
                  NatTrans.app X.hom x ≫ G.right))
        x ≫
      (Arrow.augmentedCechNerve F).left.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ X.left.map f ≫
      WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
        (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
        (_ :
          ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
            (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right) =
    WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
        (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
        (_ :
          ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
            (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
      WidePullback.lift (WidePullback.base fun x => F.hom)
        (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
            WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
              WidePullback.base fun x => F.hom)
[PROOFSTEP]
ext
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin (SimplexCategory.len y.unop + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.π (fun x => F.hom) j✝ =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.π (fun x => F.hom) j✝
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin (SimplexCategory.len y.unop + 1)
⊢ (X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.π (fun x => F.hom) j✝ =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.π (fun x => F.hom) j✝
[PROOFSTEP]
simp only [WidePullback.lift_π, Category.assoc, ← X.left.map_comp_assoc]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
j✝ : Fin (SimplexCategory.len y.unop + 1)
⊢ X.left.map (f ≫ (SimplexCategory.const y.unop j✝).op) ≫ G.left =
    X.left.map (SimplexCategory.const x.unop (↑(SimplexCategory.Hom.toOrderHom f.unop) j✝)).op ≫ G.left
[PROOFSTEP]
rfl
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.base fun x => F.hom) =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.base fun x => F.hom
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x y : SimplexCategoryᵒᵖ
f : x ⟶ y
⊢ ((X.left.map f ≫
        WidePullback.lift (NatTrans.app X.hom y ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const y.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len y.unop + 1)),
              (X.left.map (SimplexCategory.const y.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom y ≫ G.right)) ≫
      WidePullback.base fun x => F.hom) =
    (WidePullback.lift (NatTrans.app X.hom x ≫ G.right)
          (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ G.left)
          (_ :
            ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
              (X.left.map (SimplexCategory.const x.unop i).op ≫ G.left) ≫ F.hom = NatTrans.app X.hom x ≫ G.right) ≫
        WidePullback.lift (WidePullback.base fun x => F.hom)
          (fun i => WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y.unop + 1)),
              WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫ F.hom =
                WidePullback.base fun x => F.hom)) ≫
      WidePullback.base fun x => F.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
⊢ Function.LeftInverse (equivalenceRightToLeft X F) (equivalenceLeftToRight X F)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)).left = A.left
[PROOFSTEP]
dsimp
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ WidePullback.lift (NatTrans.app X.hom (Opposite.op (SimplexCategory.mk 0)) ≫ A.right)
        (fun i => X.left.map (SimplexCategory.const (SimplexCategory.mk 0) i).op ≫ A.left)
        (_ :
          ∀ (i : Fin (SimplexCategory.len (Opposite.op (SimplexCategory.mk 0)).unop + 1)),
            (fun i => X.left.map (SimplexCategory.const (Opposite.op (SimplexCategory.mk 0)).unop i).op ≫ A.left) i ≫
                F.hom =
              NatTrans.app X.hom (Opposite.op (SimplexCategory.mk 0)) ≫ A.right) ≫
      WidePullback.π (fun x => F.hom) 0 =
    A.left
[PROOFSTEP]
erw [WidePullback.lift_π]
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ X.left.map (SimplexCategory.const (SimplexCategory.mk 0) 0).op ≫ A.left = A.left
[PROOFSTEP]
nth_rw 2 [← Category.id_comp A.left]
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ X.left.map (SimplexCategory.const (SimplexCategory.mk 0) 0).op ≫ A.left = 𝟙 (Augmented.toArrow.obj X).left ≫ A.left
[PROOFSTEP]
congr 1
[GOAL]
case h₁.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ X.left.map (SimplexCategory.const (SimplexCategory.mk 0) 0).op = 𝟙 (Augmented.toArrow.obj X).left
[PROOFSTEP]
convert X.left.map_id _
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (SimplexCategory.const (SimplexCategory.mk 0) 0).op = 𝟙 (Opposite.op (SimplexCategory.mk 0))
[PROOFSTEP]
rw [← op_id]
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (SimplexCategory.const (SimplexCategory.mk 0) 0).op = (𝟙 (SimplexCategory.mk 0)).op
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_2.h.h.e'_8.e_f
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ SimplexCategory.const (SimplexCategory.mk 0) 0 = 𝟙 (SimplexCategory.mk 0)
[PROOFSTEP]
ext ⟨a, ha⟩
[GOAL]
case h.e'_2.h.h.e'_8.e_f.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
a : ℕ
ha : a < SimplexCategory.len (SimplexCategory.mk 0) + 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change a < 1 at ha
[GOAL]
case h.e'_2.h.h.e'_8.e_f.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
a : ℕ
ha : a < 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change 0 = a
[GOAL]
case h.e'_2.h.h.e'_8.e_f.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
a : ℕ
ha : a < 1
⊢ 0 = a
[PROOFSTEP]
linarith
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ (equivalenceRightToLeft X F (equivalenceLeftToRight X F A)).right = A.right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
⊢ Function.RightInverse (equivalenceRightToLeft X F) (equivalenceLeftToRight X F)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
⊢ equivalenceLeftToRight X F (equivalenceRightToLeft X F A) = A
[PROOFSTEP]
ext x : 2
[GOAL]
case h₁.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
⊢ NatTrans.app (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left x = NatTrans.app A.left x
[PROOFSTEP]
refine' WidePullback.hom_ext _ _ _ (fun j => _) _
[GOAL]
case h₁.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len x.unop + 1)
⊢ NatTrans.app (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left x ≫ WidePullback.π (fun x => F.hom) j =
    NatTrans.app A.left x ≫ WidePullback.π (fun x => F.hom) j
[PROOFSTEP]
dsimp
[GOAL]
case h₁.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len x.unop + 1)
⊢ WidePullback.lift (NatTrans.app X.hom x ≫ A.right)
        (fun i =>
          X.left.map (SimplexCategory.const x.unop i).op ≫
            NatTrans.app A.left (Opposite.op (SimplexCategory.mk 0)) ≫ WidePullback.π (fun x => F.hom) 0)
        (_ :
          ∀ (i : Fin (SimplexCategory.len x.unop + 1)),
            (fun i => X.left.map (SimplexCategory.const x.unop i).op ≫ (equivalenceRightToLeft X F A).left) i ≫ F.hom =
              NatTrans.app X.hom x ≫ (equivalenceRightToLeft X F A).right) ≫
      WidePullback.π (fun x => F.hom) j =
    NatTrans.app A.left x ≫ WidePullback.π (fun x => F.hom) j
[PROOFSTEP]
simp
[GOAL]
case h₁.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
j : Fin (SimplexCategory.len x.unop + 1)
⊢ NatTrans.app A.left x ≫
      WidePullback.π (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const x.unop j)) 0) =
    NatTrans.app A.left x ≫ WidePullback.π (fun x => F.hom) j
[PROOFSTEP]
rfl
[GOAL]
case h₁.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
x : SimplexCategoryᵒᵖ
⊢ (NatTrans.app (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).left x ≫ WidePullback.base fun x => F.hom) =
    NatTrans.app A.left x ≫ WidePullback.base fun x => F.hom
[PROOFSTEP]
simpa using congr_app A.w.symm x
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
X : Augmented C
F : Arrow C
A : X ⟶ Arrow.augmentedCechNerve F
⊢ (equivalenceLeftToRight X F (equivalenceRightToLeft X F A)).right = A.right
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    ↑(cechNerveEquiv X' Y).symm (f ≫ g) = Augmented.toArrow.map f ≫ ↑(cechNerveEquiv X Y).symm g
[PROOFSTEP]
dsimp [cechNerveEquiv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    equivalenceRightToLeft X' Y (f ≫ g) = Augmented.toArrow.map f ≫ equivalenceRightToLeft X Y g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    ↑(cechNerveEquiv X Y') (f ≫ g) = ↑(cechNerveEquiv X Y) f ≫ augmentedCechNerve.map g
[PROOFSTEP]
dsimp [cechNerveEquiv]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x => f.left) fun x => f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    equivalenceLeftToRight X Y' (f ≫ g) = equivalenceLeftToRight X Y f ≫ augmentedCechNerve.map g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
x y : SimplexCategory
g : x ⟶ y
⊢ (fun n => widePushout f.left (fun x => f.right) fun x => f.hom) x ⟶
    (fun n => widePushout f.left (fun x => f.right) fun x => f.hom) y
[PROOFSTEP]
refine'
  WidePushout.desc (WidePushout.head _) (fun i => (@WidePushout.ι _ _ _ _ _ (fun _ => f.hom) ?_ (g.toOrderHom i)))
    (fun j => _)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
x y : SimplexCategory
g : x ⟶ y
j : Fin (SimplexCategory.len x + 1)
⊢ f.hom ≫ (fun i => WidePushout.ι (fun x => f.hom) (↑(SimplexCategory.Hom.toOrderHom g) i)) j =
    WidePushout.head fun x => f.hom
[PROOFSTEP]
erw [← WidePushout.arrow_ι]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x => f✝.right) fun x => f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x => g.right) fun x => g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (SimplexCategory.len n + 1)
⊢ g.right ⟶ (cechConerve g).obj n
[PROOFSTEP]
apply WidePushout.ι _ i
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x => f✝.right) fun x => f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x => g.right) fun x => g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (SimplexCategory.len n + 1)
⊢ f.hom ≫ (fun i => F.right ≫ WidePushout.ι (fun x => g.hom) i) i = F.left ≫ WidePushout.head fun x => g.hom
[PROOFSTEP]
rw [← Arrow.w_assoc F, ← WidePushout.arrow_ι]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ (𝟭 C).map G.left ≫ (Augmented.toArrow.obj X).hom =
    F.hom ≫ (𝟭 C).map (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app G.right (SimplexCategory.mk 0))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) =
    F.hom ≫ WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app G.right (SimplexCategory.mk 0)
[PROOFSTEP]
rw [@WidePushout.arrow_ι_assoc _ _ _ _ _ (fun (_ : Fin 1) => F.hom) (by dsimp; infer_instance)]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ HasWidePushout ((𝟭 C).obj F.left) (fun x => (𝟭 C).obj F.right) fun x => F.hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ HasWidePushout F.left (fun x => F.right) fun x => F.hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : Arrow.augmentedCechConerve F ⟶ X
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app G.right (SimplexCategory.mk 0)
[PROOFSTEP]
exact congr_app G.w (SimplexCategory.mk 0)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
⊢ ∀ (j : Fin (SimplexCategory.len x + 1)),
    F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
rintro j
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
rw [← Arrow.w_assoc G]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ G.left ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
have t := X.hom.naturality (x.const j)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
t :
  ((const C).obj X.left).map (SimplexCategory.const x j) ≫ NatTrans.app X.hom x =
    NatTrans.app X.hom (SimplexCategory.mk 0) ≫ ((𝟭 (CosimplicialObject C)).obj X.right).map (SimplexCategory.const x j)
⊢ G.left ≫ (Augmented.toArrow.obj X).hom ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
dsimp at t ⊢
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
t :
  𝟙 X.left ≫ NatTrans.app X.hom x = NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j)
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j) =
    G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
simp only [Category.id_comp] at t
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
t : NatTrans.app X.hom x = NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j)
⊢ G.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0) ≫ X.right.map (SimplexCategory.const x j) =
    G.left ≫ NatTrans.app X.hom x
[PROOFSTEP]
rw [← t]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
⊢ ∀ ⦃X_1 Y : SimplexCategory⦄ (f : X_1 ⟶ Y),
    (Arrow.augmentedCechConerve F).right.map f ≫
        (fun x =>
            WidePushout.desc (G.left ≫ NatTrans.app X.hom x)
              (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
              (_ :
                ∀ (j : Fin (SimplexCategory.len x + 1)),
                  F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j =
                    G.left ≫ NatTrans.app X.hom x))
          Y =
      (fun x =>
            WidePushout.desc (G.left ≫ NatTrans.app X.hom x)
              (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
              (_ :
                ∀ (j : Fin (SimplexCategory.len x + 1)),
                  F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j =
                    G.left ≫ NatTrans.app X.hom x))
          X_1 ≫
        X.right.map f
[PROOFSTEP]
intro x y f
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (Arrow.augmentedCechConerve F).right.map f ≫
      (fun x =>
          WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
            (_ :
              ∀ (j : Fin (SimplexCategory.len x + 1)),
                F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x))
        y =
    (fun x =>
          WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
            (_ :
              ∀ (j : Fin (SimplexCategory.len x + 1)),
                F.hom ≫ (fun i => G.right ≫ X.right.map (SimplexCategory.const x i)) j = G.left ≫ NatTrans.app X.hom x))
        x ≫
      X.right.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ WidePushout.desc (WidePushout.head fun x => F.hom)
        (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
              WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len y + 1)),
            F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
      X.right.map f
[PROOFSTEP]
ext
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    WidePushout.ι (fun x => F.hom) j✝ ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ G.right ≫ X.right.map (SimplexCategory.const y (↑(SimplexCategory.Hom.toOrderHom f) j✝)) =
    (G.right ≫ X.right.map (SimplexCategory.const x j✝)) ≫ X.right.map f
[PROOFSTEP]
rw [Category.assoc, ← X.right.map_comp]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (SimplexCategory.len x + 1)
⊢ G.right ≫ X.right.map (SimplexCategory.const y (↑(SimplexCategory.Hom.toOrderHom f) j✝)) =
    G.right ≫ X.right.map (SimplexCategory.const x j✝ ≫ f)
[PROOFSTEP]
rfl
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
dsimp
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (WidePushout.head fun x => F.hom)
          (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom f) i)) j =
                WidePushout.head fun x => F.hom) ≫
        WidePushout.desc (G.left ≫ NatTrans.app X.hom y) (fun i => G.right ≫ X.right.map (SimplexCategory.const y i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len y + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const y j) = G.left ≫ NatTrans.app X.hom y) =
    (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (G.left ≫ NatTrans.app X.hom x) (fun i => G.right ≫ X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ G.right ≫ X.right.map (SimplexCategory.const x j) = G.left ≫ NatTrans.app X.hom x) ≫
        X.right.map f
[PROOFSTEP]
simp only [Functor.const_obj_map, ← NatTrans.naturality, WidePushout.head_desc_assoc, WidePushout.head_desc,
  Category.assoc]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
⊢ G.left ≫ NatTrans.app X.hom y = G.left ≫ 𝟙 X.left ≫ NatTrans.app X.hom y
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
⊢ Function.LeftInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
⊢ equivalenceRightToLeft F X (equivalenceLeftToRight F X A) = A
[PROOFSTEP]
ext x : 2
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
⊢ (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).left = A.left
[PROOFSTEP]
rfl
[GOAL]
case h₂.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ NatTrans.app (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right x = NatTrans.app A.right x
[PROOFSTEP]
refine' WidePushout.hom_ext _ _ _ (fun j => _) _
[GOAL]
case h₂.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right x =
    WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app A.right x
[PROOFSTEP]
dsimp
[GOAL]
case h₂.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) j ≫
      WidePushout.desc (A.left ≫ NatTrans.app X.hom x)
        (fun i =>
          (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app A.right (SimplexCategory.mk 0)) ≫
            X.right.map (SimplexCategory.const x i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ (fun i => (equivalenceLeftToRight F X A).right ≫ X.right.map (SimplexCategory.const x i)) j =
              (equivalenceLeftToRight F X A).left ≫ NatTrans.app X.hom x) =
    WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app A.right x
[PROOFSTEP]
simp only [Category.assoc, ← NatTrans.naturality A.right, Arrow.augmentedCechConerve_right, SimplexCategory.len_mk,
  Arrow.cechConerve_map, colimit.ι_desc, WidePushoutShape.mkCocone_ι_app, colimit.ι_desc_assoc]
[GOAL]
case h₂.h.refine'_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
j : Fin (SimplexCategory.len x + 1)
⊢ WidePushout.ι (fun x => F.hom) (↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const x j)) 0) ≫
      NatTrans.app A.right x =
    WidePushout.ι (fun x => F.hom) j ≫ NatTrans.app A.right x
[PROOFSTEP]
rfl
[GOAL]
case h₂.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x => F.hom) ≫ NatTrans.app (equivalenceRightToLeft F X (equivalenceLeftToRight F X A)).right x =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app A.right x
[PROOFSTEP]
dsimp
[GOAL]
case h₂.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ (WidePushout.head fun x => F.hom) ≫
      WidePushout.desc (A.left ≫ NatTrans.app X.hom x)
        (fun i =>
          (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app A.right (SimplexCategory.mk 0)) ≫
            X.right.map (SimplexCategory.const x i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len x + 1)),
            F.hom ≫ (fun i => (equivalenceLeftToRight F X A).right ≫ X.right.map (SimplexCategory.const x i)) j =
              (equivalenceLeftToRight F X A).left ≫ NatTrans.app X.hom x) =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app A.right x
[PROOFSTEP]
rw [colimit.ι_desc]
[GOAL]
case h₂.h.refine'_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : Arrow.augmentedCechConerve F ⟶ X
x : SimplexCategory
⊢ NatTrans.app
      (WidePushoutShape.mkCocone (A.left ≫ NatTrans.app X.hom x)
          (fun i =>
            (WidePushout.ι (fun x => F.hom) 0 ≫ NatTrans.app A.right (SimplexCategory.mk 0)) ≫
              X.right.map (SimplexCategory.const x i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len x + 1)),
              F.hom ≫ (fun i => (equivalenceLeftToRight F X A).right ≫ X.right.map (SimplexCategory.const x i)) j =
                (equivalenceLeftToRight F X A).left ≫ NatTrans.app X.hom x)).ι
      none =
    (WidePushout.head fun x => F.hom) ≫ NatTrans.app A.right x
[PROOFSTEP]
exact congr_app A.w x
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
⊢ Function.RightInverse (equivalenceRightToLeft F X) (equivalenceLeftToRight F X)
[PROOFSTEP]
intro A
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ equivalenceLeftToRight F X (equivalenceRightToLeft F X A) = A
[PROOFSTEP]
ext
[GOAL]
case h₁
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)).left = A.left
[PROOFSTEP]
rfl
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ (equivalenceLeftToRight F X (equivalenceRightToLeft F X A)).right = A.right
[PROOFSTEP]
dsimp
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ WidePushout.ι (fun x => F.hom) 0 ≫
      WidePushout.desc (A.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0))
        (fun i => A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len (SimplexCategory.mk 0) + 1)),
            F.hom ≫ (fun i => A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) i)) j =
              A.left ≫ NatTrans.app X.hom (SimplexCategory.mk 0)) =
    A.right
[PROOFSTEP]
erw [WidePushout.ι_desc]
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) 0) = A.right
[PROOFSTEP]
nth_rw 2 [← Category.comp_id A.right]
[GOAL]
case h₂
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ A.right ≫ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) 0) = A.right ≫ 𝟙 (Augmented.toArrow.obj X).right
[PROOFSTEP]
congr 1
[GOAL]
case h₂.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ X.right.map (SimplexCategory.const (SimplexCategory.mk 0) 0) = 𝟙 (Augmented.toArrow.obj X).right
[PROOFSTEP]
convert X.right.map_id _
[GOAL]
case h.e'_2.h.h.e'_8
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
⊢ SimplexCategory.const (SimplexCategory.mk 0) 0 = 𝟙 (SimplexCategory.mk 0)
[PROOFSTEP]
ext ⟨a, ha⟩
[GOAL]
case h.e'_2.h.h.e'_8.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < SimplexCategory.len (SimplexCategory.mk 0) + 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change a < 1 at ha
[GOAL]
case h.e'_2.h.h.e'_8.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < 1
⊢ ↑(↑(SimplexCategory.Hom.toOrderHom (SimplexCategory.const (SimplexCategory.mk 0) 0)) { val := a, isLt := ha }) =
    ↑(↑(SimplexCategory.Hom.toOrderHom (𝟙 (SimplexCategory.mk 0))) { val := a, isLt := ha })
[PROOFSTEP]
change 0 = a
[GOAL]
case h.e'_2.h.h.e'_8.a.h.h.mk.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x => f.right) fun x => f.hom
F : Arrow C
X : Augmented C
A : F ⟶ Augmented.toArrow.obj X
a : ℕ
ha : a < 1
⊢ 0 = a
[PROOFSTEP]
linarith
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ (wideCospan ι X).obj none)
[PROOFSTEP]
dsimp [wideCospan]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasTerminal C
ι : Type w
X Y : C
⊢ Unique (Y ⟶ ⊤_ C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i j : WidePullbackShape ι
f : i ⟶ j
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map f ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        j =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        i ≫
      (wideCospan ι X).map f
[PROOFSTEP]
cases f
[GOAL]
case id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
i : WidePullbackShape ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id i) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        i =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        i ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id i)
[PROOFSTEP]
cases i
[GOAL]
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id none) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id none)
case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id (some val✝)) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id (some val✝))
[PROOFSTEP]
all_goals dsimp; simp
[GOAL]
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id none) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id none)
[PROOFSTEP]
dsimp
[GOAL]
case id.none
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ 𝟙 (∏ fun x => X) ≫ terminal.from (∏ fun x => X) = terminal.from (∏ fun x => X) ≫ (wideCospan ι X).map (𝟙 none)
[PROOFSTEP]
simp
[GOAL]
case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.id (some val✝)) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some val✝) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.id (some val✝))
[PROOFSTEP]
dsimp
[GOAL]
case id.some
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : ι
⊢ 𝟙 (∏ fun x => X) ≫ limit.π (Discrete.functor fun x => X) { as := val✝ } =
    limit.π (Discrete.functor fun x => X) { as := val✝ } ≫ (wideCospan ι X).map (𝟙 (some val✝))
[PROOFSTEP]
simp
[GOAL]
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ ((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).map (WidePullbackShape.Hom.term j✝) ≫
      (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        none =
    (fun X_1 =>
          Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
            fun i => limit.π (Discrete.functor fun x => X) { as := i })
        (some j✝) ≫
      (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
[PROOFSTEP]
dsimp
[GOAL]
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ 𝟙 (∏ fun x => X) ≫ terminal.from (∏ fun x => X) =
    limit.π (Discrete.functor fun x => X) { as := j✝ } ≫ (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
[PROOFSTEP]
simp only [terminal.comp_from]
[GOAL]
case term
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j✝ : ι
⊢ terminal.from (∏ fun x => X) =
    limit.π (Discrete.functor fun x => X) { as := j✝ } ≫ (wideCospan ι X).map (WidePullbackShape.Hom.term j✝)
[PROOFSTEP]
exact Subsingleton.elim _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
⊢ f = (fun s => Pi.lift fun j => NatTrans.app s.π (some j)) s
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
⊢ f = Pi.lift fun j => NatTrans.app s.π (some j)
[PROOFSTEP]
ext j
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j = (Pi.lift fun j => NatTrans.app s.π (some j)) ≫ Pi.π (fun x => X) j
[PROOFSTEP]
dsimp only [Limits.Pi.lift]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j =
    limit.lift (Discrete.functor fun b => X) (Fan.mk s.pt fun j => NatTrans.app s.π (some j)) ≫ Pi.π (fun x => X) j
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j = NatTrans.app (Fan.mk s.pt fun j => NatTrans.app s.π (some j)).π { as := j }
[PROOFSTEP]
dsimp
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
f :
  s.pt ⟶
    { pt := ∏ fun x => X,
        π :=
          NatTrans.mk fun X_1 =>
            Option.casesOn X_1 (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none))
              fun i => limit.π (Discrete.functor fun x => X) { as := i } }.pt
h :
  ∀ (j : WidePullbackShape ι),
    f ≫
        NatTrans.app
          { pt := ∏ fun x => X,
              π :=
                NatTrans.mk fun X_1 =>
                  Option.casesOn X_1
                    (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ fun x => X)).obj none)) fun i =>
                    limit.π (Discrete.functor fun x => X) { as := i } }.π
          j =
      NatTrans.app s.π j
j : ι
⊢ f ≫ Pi.π (fun x => X) j = NatTrans.app s.π (some j)
[PROOFSTEP]
rw [← h (some j)]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x => (Arrow.mk (terminal.from X)).left) fun x =>
    (Arrow.mk (terminal.from X)).hom
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
val✝ : Fintype ι
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x => (Arrow.mk (terminal.from X)).left) fun x =>
    (Arrow.mk (terminal.from X)).hom
[PROOFSTEP]
exact ⟨⟨wideCospan.limitCone ι X⟩⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
j : ι
⊢ (limitIsoPi ι X).hom ≫ Pi.π (fun x => X) j = WidePullback.π (fun x => terminal.from X) j
[PROOFSTEP]
rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
⊢ (Arrow.cechNerve (Arrow.mk (terminal.from X))).map f ≫
      ((fun m => wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left)
          n).hom =
    ((fun m => wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left) m).hom ≫
      (cechNerveTerminalFrom X).map f
[PROOFSTEP]
dsimp only [cechNerveTerminalFrom, Arrow.cechNerve]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
⊢ WidePullback.lift (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
        (fun i =>
          WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                (Arrow.mk (terminal.from X)).hom =
              WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom) ≫
      (wideCospan.limitIsoPi (Fin (SimplexCategory.len n.unop + 1)) (Arrow.mk (terminal.from X)).left).hom =
    (wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
      Pi.lift fun i => Pi.π (fun x => X) (↑(SimplexCategory.Hom.toOrderHom f.unop) i)
[PROOFSTEP]
ext ⟨j⟩
[GOAL]
case h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
j : ℕ
isLt✝ : j < SimplexCategory.len n.unop + 1
⊢ (WidePullback.lift (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
          (fun i =>
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
              WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                  (Arrow.mk (terminal.from X)).hom =
                WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom) ≫
        (wideCospan.limitIsoPi (Fin (SimplexCategory.len n.unop + 1)) (Arrow.mk (terminal.from X)).left).hom) ≫
      Pi.π (fun x => X) { val := j, isLt := isLt✝ } =
    ((wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
        Pi.lift fun i => Pi.π (fun x => X) (↑(SimplexCategory.Hom.toOrderHom f.unop) i)) ≫
      Pi.π (fun x => X) { val := j, isLt := isLt✝ }
[PROOFSTEP]
simp only [Category.assoc, limit.lift_π, Fan.mk_π_app]
[GOAL]
case h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
j : ℕ
isLt✝ : j < SimplexCategory.len n.unop + 1
⊢ WidePullback.lift (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
        (fun i =>
          WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
        (_ :
          ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                (Arrow.mk (terminal.from X)).hom =
              WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom) ≫
      (wideCospan.limitIsoPi (Fin (SimplexCategory.len n.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
        Pi.π (fun x => X) { val := j, isLt := isLt✝ } =
    (wideCospan.limitIsoPi (Fin (SimplexCategory.len m.unop + 1)) (Arrow.mk (terminal.from X)).left).hom ≫
      Pi.π (fun x => X) (↑(SimplexCategory.Hom.toOrderHom f.unop) { val := j, isLt := isLt✝ })
[PROOFSTEP]
erw [wideCospan.limitIsoPi_hom_comp_pi, wideCospan.limitIsoPi_hom_comp_pi, limit.lift_π]
[GOAL]
case h.mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
ι : Type w
inst✝ : HasFiniteProducts C
X : C
m n : SimplexCategoryᵒᵖ
f : m ⟶ n
j : ℕ
isLt✝ : j < SimplexCategory.len n.unop + 1
⊢ NatTrans.app
      (WidePullbackShape.mkCone (WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)
          (fun i =>
            WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) i))
          (_ :
            ∀ (j : Fin (SimplexCategory.len n.unop + 1)),
              WidePullback.π (fun x => (Arrow.mk (terminal.from X)).hom) (↑(SimplexCategory.Hom.toOrderHom f.unop) j) ≫
                  (Arrow.mk (terminal.from X)).hom =
                WidePullback.base fun x => (Arrow.mk (terminal.from X)).hom)).π
      (some { val := j, isLt := isLt✝ }) =
    WidePullback.π (fun x => terminal.from X) (↑(SimplexCategory.Hom.toOrderHom f.unop) { val := j, isLt := isLt✝ })
[PROOFSTEP]
rfl