awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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
f :
  ⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌ ⟶
    ⦋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)))⦌
w : CategoryTheory.Mono f
hf :
  (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 _⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))) =
    (↑(↑t : (↑P.II : Type u)) : A.N).simplex
⊢ (↑(↑t : (↑P.II : Type u)) : A.N).dim <
    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)))

Tactic:
simpa using SSet.N.dim_lt_of_lt t.2.2

Premises used: SSet.N.dim_lt_of_lt, And.right, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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 : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS

Tactic:
have h (t : T) : ∃ u, ψ u = t.1.1.toS := by
    obtain ⟨f, _, hf⟩ := N.le_iff_exists_mono.1 t.2.2.le
    refine ⟨⟨⟨t.1.1.dim, ?_⟩, f⟩, ?_⟩
    · simpa using SSet.N.dim_lt_of_lt t.2.2
    · rwa [SSet.S.ext_iff]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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)))))
h : ∀ (t : T), ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
choose :
  ∀ (φ : (t : T) → U) (hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS),
    Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }
⊢ Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }

Tactic:
choose φ hφ using h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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
apply : Function.Injective φ
⊢ Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }

Tactic:
apply Finite.of_injective φ

Premises used: Finite.of_injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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₂)
rw₆ rw₇ : ψ (φ t₂) = ψ (φ t₂)
⊢ t₁ = t₂

Tactic:
rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff, Subtype.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
hy : Acc P.AncestralRel y
⊢ P.rank' ⋯ = ⨆ (x : { x : (↑P.II : Type u) // P.AncestralRel x y }), P.rank' ⋯ + 1

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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
rw : P.rank' ⋯ + 1 ≤ ⨆ (x : { x : (↑P.II : Type u) // P.AncestralRel x y }), P.rank' ⋯ + 1
⊢ P.rank' ⋯ < P.rank' hy

Tactic:
rw [P.rank'_eq hy, ← Nat.add_one_le_iff]

Premises used: Nat.add_one_le_iff, SSet.Subcomplex.Pairing.rank'_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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' ⋯ + 1 ≤ ⨆ (x : { x : (↑P.II : Type u) // P.AncestralRel x y }), P.rank' ⋯ + 1

Tactic:
le_csSup (Finite.bddAbove_range _) ⟨⟨x, r⟩, rfl⟩

Premises used: iSup, Subtype.mk, Finite.bddAbove_range, Exists.intro, le_csSup, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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' ⋯ + 1 ≤ ⨆ (x : { x : (↑P.II : Type u) // P.AncestralRel x y }), P.rank' ⋯ + 1

Tactic:
exact le_csSup (Finite.bddAbove_range _) ⟨⟨x, r⟩, rfl⟩

Premises used: Finite.bddAbove_range, Exists.intro, le_csSup, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
x y : (↑P.II : Type u)
h : P.AncestralRel x y
⊢ P.rank x < P.rank y

Tactic:
P.rank'_lt _ h

Premises used: SSet.Subcomplex.Pairing.rank, SSet.Subcomplex.Pairing.rank'_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
⊢ Nonempty.{max (u + 1) 1} (P.RankFunction ℕ)

Tactic:
⟨P.rankFunction⟩

Premises used: SSet.Subcomplex.Pairing.rankFunction, Nonempty.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
⊢ Nonempty.{max (u + 1) 1} (P.WeakRankFunction ℕ)

Tactic:
⟨P.rankFunction.toWeakRankFunction⟩

Premises used: SSet.Subcomplex.Pairing.rankFunction, SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction, Nonempty.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
⊢ P.IsRegular ↔ Nonempty.{max (u + 1) 1} (P.RankFunction ℕ)

Tactic:
⟨fun _ ↦ inferInstance, fun ⟨h⟩ ↦ h.isRegular⟩

Premises used: _private.0.SSet.Subcomplex.Pairing.isRegular_iff_nonempty_rankFunction.match_1, SSet.Subcomplex.Pairing.RankFunction.isRegular, inferInstance, Iff.intro, SSet.Subcomplex.Pairing.IsRegular
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
⊢ P.IsRegular ↔ Nonempty.{max (u + 1) 1} (P.WeakRankFunction ℕ)

Tactic:
⟨fun _ ↦ inferInstance, fun ⟨h⟩ ↦ h.isRegular⟩

Premises used: inferInstance, _private.0.SSet.Subcomplex.Pairing.isRegular_iff_nonempty_weakRankFunction.match_1, SSet.Subcomplex.Pairing.WeakRankFunction.isRegular, Iff.intro, SSet.Subcomplex.Pairing.IsRegular
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
rw : Nonempty.{u + 1} (P.pairing.RankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.RankFunction ℕ)
⊢ P.IsRegular ↔ Nonempty.{u_1 + 1} (P.RankFunction ℕ)

Tactic:
rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_rankFunction]

Premises used: SSet.Subcomplex.Pairing.isRegular_iff_nonempty_rankFunction, SSet.Subcomplex.PairingCore.isRegular_pairing_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
⊢ Nonempty.{u + 1} (P.pairing.RankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.RankFunction ℕ)

Tactic:
(P.rankFunctionEquiv ℕ).symm.nonempty_congr

Premises used: SSet.Subcomplex.PairingCore.rankFunctionEquiv, Nat, Equiv.nonempty_congr, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
⊢ Nonempty.{u + 1} (P.pairing.RankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.RankFunction ℕ)

Tactic:
exact (P.rankFunctionEquiv ℕ).symm.nonempty_congr

Premises used: SSet.Subcomplex.PairingCore.rankFunctionEquiv, Nat, Equiv.nonempty_congr, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
rw : Nonempty.{u + 1} (P.pairing.WeakRankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.WeakRankFunction ℕ)
⊢ P.IsRegular ↔ Nonempty.{u_1 + 1} (P.WeakRankFunction ℕ)

Tactic:
rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_weakRankFunction]

Premises used: SSet.Subcomplex.Pairing.isRegular_iff_nonempty_weakRankFunction, SSet.Subcomplex.PairingCore.isRegular_pairing_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
⊢ Nonempty.{u + 1} (P.pairing.WeakRankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.WeakRankFunction ℕ)

Tactic:
(P.weakRankFunctionEquiv ℕ).symm.nonempty_congr

Premises used: SSet.Subcomplex.PairingCore.weakRankFunctionEquiv, Nat, Equiv.nonempty_congr, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
Goal:
X : SSet
A : X.Subcomplex
P : PairingCore.{u_1, u} A
inst : P.IsProper
⊢ Nonempty.{u + 1} (P.pairing.WeakRankFunction ℕ) ↔ Nonempty.{u_1 + 1} (P.WeakRankFunction ℕ)

Tactic:
exact (P.weakRankFunctionEquiv ℕ).symm.nonempty_congr

Premises used: SSet.Subcomplex.PairingCore.weakRankFunctionEquiv, Nat, Equiv.nonempty_congr, Equiv.symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
rw :
  { dim := c.dim + 1, simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).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))) ⋯).subcomplex
⊢ 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)))

Tactic:
rw [range_eq_ofSimplex, Equiv.apply_symm_apply, S.ofSimplex_eq_subcomplex_mk,
    ← S.cast_eq_self _ (P.dim_p c.s)]

Premises used: Equiv.apply_symm_apply, SSet.Subcomplex.range_eq_ofSimplex, SSet.Subcomplex.Pairing.dim_p, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.S.ofSimplex_eq_subcomplex_mk, SSet.S.cast_eq_self
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ { dim := c.dim + 1, simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N) ⋯).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))) ⋯).subcomplex

Tactic:
dsimp [S.subcomplex]

Premises used: SSet.S.subcomplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ (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:
(P.isUniquelyCodimOneFace c.s).δ_index rfl

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SimplexCategory.mkHom, cast, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SimplexCategory.δ, SSet.Subcomplex.Pairing.RankFunction.Cell.index, OrderEmbedding.toOrderHom, SSet.S.IsUniquelyCodimOneFace.δ_index, rfl, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ ∃ (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

Premises used: SSet.Subcomplex.image_obj, Set.mem_image, CategoryTheory.Subfunctor.ofSection_le_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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
⊢ False

Tactic:
obtain ⟨x, h₁, h₂⟩ := h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
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
⊢ False

Tactic:
obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective x

Premises used: Equiv.surjective, Equiv.symm, SSet.stdSimplex.objEquiv, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ (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

Tactic:
rw [← stdSimplex.map_objEquiv_op_apply, Equiv.apply_symm_apply] at h₂

Premises used: Equiv.apply_symm_apply, SSet.stdSimplex.map_objEquiv_op_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ Mono g

Tactic:
have := mono_of_nonDegenerate (x := ⟨_, c.s.val.nonDegenerate⟩) _ _ _ h₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
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
⊢ 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⦌)

Tactic:
obtain rfl := (P.isUniquelyCodimOneFace c.s).unique rfl _ h₂

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.RankFunction.Cell.s, SSet.S.IsUniquelyCodimOneFace.unique, rfl