awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
rw₁ : (↑(↑t₁ : (↑P.II : Type u)) : A.N) = (↑(↑t₂ : (↑P.II : Type u)) : A.N)
rw₂ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toN = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toN
rw₃ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toS = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
⊢ t₁ = t₂
have rw₄ : ψ (φ t₁) = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
rw₁ : (↑(↑t₁ : (↑P.II : Type u)) : A.N) = (↑(↑t₂ : (↑P.II : Type u)) : A.N)
rw₂ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toN = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toN
rw₃ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toS = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
rw₄ : ψ (φ t₁) = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
⊢ t₁ = t₂
have rw₅ : ψ (φ t₁) = ψ (φ t₂)
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
rw₁ : (↑(↑t₁ : (↑P.II : Type u)) : A.N) = (↑(↑t₂ : (↑P.II : Type u)) : A.N)
rw₂ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toN = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toN
rw₃ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toS = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
rw₄ : ψ (φ t₁) = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
rw₅ : ψ (φ t₁) = ψ (φ t₂)
⊢ t₁ = t₂
have rw₆ : ψ (φ t₂) = ψ (φ t₂)
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
hy : Acc P.AncestralRel y
x : (↑P.II : Type u)
r : P.AncestralRel x y
⊢ P.rank' ⋯ < P.rank' hy
have rw : P.rank' sorry + 1 ≤ ⨆ (x : { x : (↑P.II : Type u) // P.AncestralRel x y }), P.rank' sorry + 1
Tactic: rw [P.rank'_eq hy, ← Nat.add_one_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
⊢ P.IsRegular ↔ Nonempty.{u_1 + 1} (P.RankFunction ℕ)
have rw : Nonempty.{u + 1} (P.pairing.RankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.RankFunction ℕ)
Tactic: rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_rankFunction]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
⊢ P.IsRegular ↔ Nonempty.{u_1 + 1} (P.WeakRankFunction ℕ)
have rw : Nonempty.{u + 1} (P.pairing.WeakRankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.WeakRankFunction ℕ)
Tactic: rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_weakRankFunction]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ range c.map = S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
have rw : { dim := c.dim + 1, simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) sorry).simplex :
      X.S }.subcomplex =
  (S.cast (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) sorry).subcomplex
Tactic: rw [range_eq_ofSimplex, Equiv.apply_symm_apply, S.ofSimplex_eq_subcomplex_mk,
    ← S.cast_eq_self _ (P.dim_p c.s)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h : (↑c.s : A.N).subcomplex ≤ c.horn.image c.map
⊢ False
have h₁ : ∃ (x : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌),
  Membership.mem (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)) (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌)) x ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋(↑c.s : A.N).dim⦌)) :
          (a : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) → X _⦋(↑c.s : A.N).dim⦌)
        x =
      (↑c.s : A.N).simplex
Tactic: simp only [Subfunctor.ofSection_le_iff, image_obj, Set.mem_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h :
  ∃ (x : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌),
    Membership.mem (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)) (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌)) x ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋(↑c.s : A.N).dim⦌)) :
            (a : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) → X _⦋(↑c.s : A.N).dim⦌)
          x =
        (↑c.s : A.N).simplex
⊢ False
have obtain : ∀ (x : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
  (h₁ : Membership.mem (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)) (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌)) x)
  (h₂ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋(↑c.s : A.N).dim⦌)) :
          (a : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) → X _⦋(↑c.s : A.N).dim⦌)
        x =
      (↑c.s : A.N).simplex),
  False
Tactic: obtain ⟨x, h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
x : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌
h₁ : Membership.mem (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)) (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌)) x
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋(↑c.s : A.N).dim⦌)) :
        (a : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) → X _⦋(↑c.s : A.N).dim⦌)
      x =
    (↑c.s : A.N).simplex
⊢ False
have obtain : ∀ (g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌)
  (h₁ :
    Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
      (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
      ((Equiv.symm stdSimplex.objEquiv :
            (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
          g :
        Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
  (h₂ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋(↑c.s : A.N).dim⦌)) :
          (a : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) → X _⦋(↑c.s : A.N).dim⦌)
        ((Equiv.symm stdSimplex.objEquiv :
              (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
            g :
          Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) =
      (↑c.s : A.N).simplex),
  False
Tactic: obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective x
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋(↑c.s : A.N).dim⦌)) :
        (a : Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) → X _⦋(↑c.s : A.N).dim⦌)
      ((Equiv.symm stdSimplex.objEquiv :
            (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
          g :
        Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) =
    (↑c.s : A.N).simplex
⊢ False
have h₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
    (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) sorry).simplex =
  (↑c.s : A.N).simplex
Tactic: rw [← stdSimplex.map_objEquiv_op_apply, Equiv.apply_symm_apply] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
⊢ False
have this : Mono g
Tactic: have := mono_of_nonDegenerate (x := ⟨_, c.s.val.nonDegenerate⟩) _ _ _ h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono g
⊢ False
have h₃ : Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
  (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
  ((Equiv.symm stdSimplex.objEquiv :
        (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
      (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index sorry sorry)) :
    Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
Tactic: obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂
Cleared hypotheses: g, h₁, h₂, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono g
h₃ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
⊢ False
have h₄ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index sorry sorry)))) :
      (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
    (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) sorry).simplex =
  (↑c.s : A.N).simplex
Tactic: obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂
Cleared hypotheses: g, h₁, h₂, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
g : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        g :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map g.op) : (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono g
h₃ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
⊢ False
have this₁ : Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index sorry sorry))
Tactic: obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂
Cleared hypotheses: g, h₁, h₂, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
h₁ :
  Membership.mem (α := Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌) (γ := Set (Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌))
    (c.horn.obj (op ⦋(↑c.s : A.N).dim⦌))
    ((Equiv.symm stdSimplex.objEquiv :
          (a : unop (op ⦋(↑c.s : A.N).dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
        (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)) :
      Δ[c.dim + 1] _⦋(↑c.s : A.N).dim⦌)
h₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (X.map (Quiver.Hom.op (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯)))) :
        (a : X _⦋c.dim + 1⦌) → X _⦋(↑c.s : A.N).dim⦌)
      (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).simplex =
    (↑c.s : A.N).simplex
this : Mono (X := ⦋(↑c.s : A.N).dim⦌) (SimplexCategory.δ (S.IsUniquelyCodimOneFace.index ⋯ ⋯))
⊢ False
have h₃ : ¬LE.le.{u} (α := Δ[c.dim + 1].Subcomplex) (stdSimplex.face {c.index}ᶜ)
    (stdSimplex.face {S.IsUniquelyCodimOneFace.index sorry sorry}ᶜ)
Tactic: rw [← ofSimplex_le_iff, subcomplex_le_horn_iff, ← stdSimplex.face_singleton_compl] at h₁
Cleared hypotheses: h₁, h₂, this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ c.horn.image c.map <
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
have rw : c.horn.image c.map ≤
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ∧
  c.horn.image c.map ≠
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N)))
Tactic: rw [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ image (stdSimplex.face {c.index}ᶜ) c.map = (↑c.s : A.N).subcomplex
have rw : ofSimplex (n := c.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
        (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
          (SimplexCategory.δ c.index) :
        Δ[c.dim + 1] _⦋c.dim⦌)) =
  (↑c.s : A.N).subcomplex
Tactic: rw [stdSimplex.face_singleton_compl, image_ofSimplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst_1 : P.IsProper
⊢ ofSimplex (n := c.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
            (SimplexCategory.δ c.index) :
          Δ[c.dim + 1] _⦋c.dim⦌)) =
    (↑c.s : A.N).subcomplex
have e_x : (ConcreteCategory.hom (FC := TypeCat.Fun) (c.map.app (op ⦋c.dim⦌)) :
      (a : (fun (X : Type u) ↦ X) (Δ[c.dim + 1] _⦋c.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋c.dim⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋c.dim⦌) ⟶ ⦋c.dim + 1⦌) → Δ[c.dim + 1] _⦋c.dim⦌)
        (SimplexCategory.δ c.index) :
      Δ[c.dim + 1] _⦋c.dim⦌) =
  (↑c.s : A.N).simplex
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤ f.filtration i
have refine : LE.le.{u} (α := X.Subcomplex)
  (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
  (⨆ (j : ι),
    ⨆ (_ : j < i),
      ⨆ (c : f.Cell j),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
Tactic: refine le_trans ?_ le_sup_right
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (⨆ (j : ι),
      ⨆ (_ : j < i),
        ⨆ (c : f.Cell j),
          S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
have refine : LE.le.{u} (α := X.Subcomplex)
  (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
  (⨆ (_ : j < i),
    ⨆ (c : f.Cell j),
      S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
Tactic: refine le_trans ?_ (le_iSup _ j)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
h : j < i
⊢ LE.le.{u} (α := X.Subcomplex)
    (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
    (⨆ (_ : j < i),
      ⨆ (c : f.Cell j),
        S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
have refine : LE.le.{u} (α := X.Subcomplex)
  (S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
  (⨆ (c : f.Cell j),
    S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))))
Tactic: refine le_trans ?_ (le_iSup _ h)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
i₁ i₂ : ι
h : i₁ ≤ i₂
⊢ A ⊔
      ⨆ (j : ι),
        ⨆ (_ : j < i₁),
          ⨆ (c : f.Cell j),
            S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N))) ≤
    f.filtration i₂
have simp : ∀ (i : ι) (i_1 : i < i₁) (i_2 : f.Cell i),
  S.subcomplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_2.s) : A.N))) ≤
    f.filtration i₂
Tactic: simp only [sup_le_iff, iSup_le_iff, le_filtration, true_and]