awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
this :
  Nonempty.{u + 1} { f : ℕ → (↑(P.ofIso e hA).II : Type u) // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }
obtain :
  ∀ (f : ℕ → (↑(P.ofIso e hA).II : Type u)) (hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)), False
⊢ False

Tactic:
obtain ⟨f, hf⟩ := this
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → (↑(P.ofIso e hA).II : Type u)
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
⊢ False

Tactic:
hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩

Premises used: Subtype.mk, IsEmpty.false, Subtype.val, SSet.Subcomplex.N.orderIsoOfIso, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → (↑(P.ofIso e hA).II : Type u)
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
refine :
  ∀ (n : ℕ),
    P.AncestralRel
      ((fun (n : ℕ) ↦
          (Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) ((N.orderIsoOfIso e hA : (a : B.N) → A.N) (↑(f n) : B.N)) ⋯ :
            { x : A.N // x ∈ P.II }))
        (n + 1))
      ((fun (n : ℕ) ↦
          (Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) ((N.orderIsoOfIso e hA : (a : B.N) → A.N) (↑(f n) : B.N)) ⋯ :
            { x : A.N // x ∈ P.II }))
        n)
⊢ False

Tactic:
refine hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩

Premises used: Subtype.mk, IsEmpty.false, Subtype.val, SSet.Subcomplex.N.orderIsoOfIso, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → (↑(P.ofIso e hA).II : Type u)
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ P.AncestralRel
    ((fun (n : ℕ) ↦
        (Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) ((N.orderIsoOfIso e hA : (a : B.N) → A.N) (↑(f n) : B.N)) ⋯ :
          { x : A.N // x ∈ P.II }))
      (n + 1))
    ((fun (n : ℕ) ↦
        (Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) ((N.orderIsoOfIso e hA : (a : B.N) → A.N) (↑(f n) : B.N)) ⋯ :
          { x : A.N // x ∈ P.II }))
      n)

Tactic:
simpa [← P.ofIso_ancestralRel_iff e hA] using hf n

Premises used: SSet.Subcomplex.Pairing.ofIso_ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
rw : Membership.mem (γ := Set (X _⦋(↑s : A.N).dim⦌)) (X.nonDegenerate (↑s : A.N).dim) ((↑s : A.N).cast ⋯).simplex
⊢ Membership.mem (α := (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌)) (γ := Set (X _⦋(↑s : A.N).dim⦌))
    (X.nonDegenerate (↑s : A.N).dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex :
      (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl]

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.δ_index, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ Membership.mem (γ := Set (X _⦋(↑s : A.N).dim⦌)) (X.nonDegenerate (↑s : A.N).dim) ((↑s : A.N).cast ⋯).simplex

Tactic:
s.val.nonDegenerate

Premises used: Set.Mem, cast, SSet.Subcomplex.N.toN, SSet.N.nonDegenerate, Subtype.val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ Membership.mem (γ := Set (X _⦋(↑s : A.N).dim⦌)) (X.nonDegenerate (↑s : A.N).dim) ((↑s : A.N).cast ⋯).simplex

Tactic:
exact s.val.nonDegenerate

Premises used: SSet.Subcomplex.N.toN, SSet.N.nonDegenerate, Subtype.val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
rw : ((↑s : A.N).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s : A.N).dim⦌)
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex :
      (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌)) ∉
    A.obj (Opposite.op ⦋(↑s : A.N).dim⦌)

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl]

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.δ_index, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ ((↑s : A.N).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s : A.N).dim⦌)

Tactic:
s.val.notMem

Premises used: Set.Mem, cast, Subtype.val, SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ ((↑s : A.N).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s : A.N).dim⦌)

Tactic:
exact s.val.notMem

Premises used: Subtype.val, SSet.Subcomplex.N.notMem
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s t : (↑P.II : Type u)
h :
  { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S } =
    { dim := (↑t : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N) ⋯).simplex }
a :
  Eq (α := (↑P.I : Type u)) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t : (↑P.I : Type u))
⊢ s = t

Tactic:
apply P.p.injective

Premises used: SSet.Subcomplex.Pairing.p, Equiv.injective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s t : (↑P.II : Type u)
h :
  { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S } =
    { dim := (↑t : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N) ⋯).simplex }
a :
  Eq.{u + 1} (α := A.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)
    (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)
a₁ :
  Eq.{u + 1} (α := X.N) (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N))
    (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))
a₂ :
  Eq.{u + 1} (α := X.S) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)))
    (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N)))
a₃ :
  (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).toS =
    N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))
a₄ a₅ a₆ a₇ :
  (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).toS =
    (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N) ⋯).toS
⊢ Eq (α := (↑P.I : Type u)) ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s : (↑P.I : Type u))
    ((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t : (↑P.I : Type u))

Tactic:
rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff,
      ← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      ← (P.p t).val.cast_eq_self (P.isUniquelyCodimOneFace t).dim_eq]

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.p, SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff, SSet.S.IsUniquelyCodimOneFace.dim_eq, Subtype.ext_iff, SSet.Subcomplex.N.cast_eq_self, Subtype.val, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s t : (↑P.II : Type u)
h :
  Eq.{u + 1} (α := X.S)
    (S.mk (dim := (↑s : A.N).dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex))
    (S.mk (dim := (↑t : A.N).dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑t : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑t : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N) ⋯).simplex))
⊢ { dim := (↑s : A.N).dim, simplex := ((↑s : A.N).cast ⋯).simplex : X.S } =
    { dim := (↑t : A.N).dim, simplex := ((↑t : A.N).cast ⋯).simplex }

Tactic:
rw [(P.isUniquelyCodimOneFace s).δ_index rfl,
      (P.isUniquelyCodimOneFace t).δ_index rfl] at h

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.δ_index, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s t : (↑P.II : Type u)
h :
  { dim := (↑s : A.N).dim, simplex := ((↑s : A.N).cast ⋯).simplex : X.S } =
    { dim := (↑t : A.N).dim, simplex := ((↑t : A.N).cast ⋯).simplex }
rwa : (↑s : A.N) = (↑t : A.N)
rwa₁ : (↑s : A.N).toN = (↑t : A.N).toN
rwa₂ rwa₃ rwa₄ rwa₅ : (↑s : A.N).toS = (↑t : A.N).toS
⊢ s = t

Tactic:
rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff]

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff, Subtype.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s t : (↑P.II : Type u)
h :
  { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S } =
    S.mk (dim := (↑t : A.N).dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑t : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑t : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N) ⋯).simplex)
⊢ { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S } =
    { dim := (↑t : A.N).dim, simplex := ((↑t : A.N).cast ⋯).simplex }

Tactic:
rw [(P.isUniquelyCodimOneFace t).δ_index rfl] at h

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.δ_index, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s t : (↑P.II : Type u)
h :
  { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S } =
    { dim := (↑t : A.N).dim, simplex := ((↑t : A.N).cast ⋯).simplex }
rwa : N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯ = (↑t : A.N)
rwa₁ : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).toN = (↑t : A.N).toN
rwa₂ rwa₃ rwa₄ rwa₅ : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).toS = (↑t : A.N).toS
⊢ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) = (↑t : A.N)

Tactic:
rwa [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      N.ext_iff, SSet.N.ext_iff]

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.p, SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff, SSet.S.IsUniquelyCodimOneFace.dim_eq, SSet.Subcomplex.N.cast_eq_self, Subtype.val, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x : A.N
inl :
  ∀ (s : (↑P.II : Type u)),
    ∃ (s_1 : (↑P.II : Type u)),
      (↑s : A.N).toS =
          { dim := (↑s_1 : A.N).dim + 1,
            simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex } ∨
        (↑s : A.N).toS =
          S.mk (dim := (↑s_1 : A.N).dim)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim + 1⦌)) →
                  (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim⦌))
              (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex)
inr :
  ∀ (s : (↑P.II : Type u)),
    ∃ (s_1 : (↑P.II : Type u)),
      N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)) =
          { dim := (↑s_1 : A.N).dim + 1,
            simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex : X.S } ∨
        Eq.{u + 1} (α := X.S) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)))
          (S.mk (dim := (↑s_1 : A.N).dim)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim + 1⦌)) →
                  (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim⦌))
              (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex))
⊢ ∃ (s : (↑P.II : Type u)),
    x.toS =
        { dim := (↑s : A.N).dim + 1,
          simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex } ∨
      x.toS =
        S.mk (dim := (↑s : A.N).dim)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))
            (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex)

Tactic:
obtain ⟨s, rfl | rfl⟩ := P.exists_or x

Premises used: SSet.Subcomplex.Pairing.exists_or, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ ∃ (s_1 : (↑P.II : Type u)),
    (↑s : A.N).toS =
        { dim := (↑s_1 : A.N).dim + 1,
          simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex } ∨
      (↑s : A.N).toS =
        S.mk (dim := (↑s_1 : A.N).dim)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim⦌))
            (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex)

Tactic:
⟨s, Or.inr ?_⟩

Premises used: Exists.intro, Or.inr
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
inl :
  (↑s : A.N).toS =
    S.mk (dim := (↑s : A.N).dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex)
⊢ ∃ (s_1 : (↑P.II : Type u)),
    (↑s : A.N).toS =
        { dim := (↑s_1 : A.N).dim + 1,
          simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex } ∨
      (↑s : A.N).toS =
        S.mk (dim := (↑s_1 : A.N).dim)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim⦌))
            (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex)

Tactic:
refine ⟨s, Or.inr ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ (↑s : A.N).toS =
    S.mk (dim := (↑s : A.N).dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s : A.N).dim⦌))
        (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex)

Tactic:
simp [(P.isUniquelyCodimOneFace s).δ_index]

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.δ_index
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ ∃ (s_1 : (↑P.II : Type u)),
    N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)) =
        { dim := (↑s_1 : A.N).dim + 1,
          simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex : X.S } ∨
      Eq.{u + 1} (α := X.S) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)))
        (S.mk (dim := (↑s_1 : A.N).dim)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim⦌))
            (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex))

Tactic:
⟨s, Or.inl ?_⟩

Premises used: Exists.intro, Or.inl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
inr :
  N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)) =
    { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S }
⊢ ∃ (s_1 : (↑P.II : Type u)),
    N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)) =
        { dim := (↑s_1 : A.N).dim + 1,
          simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex : X.S } ∨
      Eq.{u + 1} (α := X.S) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)))
        (S.mk (dim := (↑s_1 : A.N).dim)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (⋯.index ⋯)) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋(↑s_1 : A.N).dim⦌))
            (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s_1) : A.N) ⋯).simplex))

Tactic:
refine ⟨s, Or.inl ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
inr :
  (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).toS =
    { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex }
⊢ N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N)) =
    { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex : X.S }

Tactic:
nth_rw 1 [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq]

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.Pairing.p, SSet.S.IsUniquelyCodimOneFace.dim_eq, SSet.Subcomplex.N.cast_eq_self, Subtype.val, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).toS =
    { dim := (↑s : A.N).dim + 1,
      simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) ⋯).simplex }

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x x_1 : h.ι
hst : h.type₁ x = h.type₁ x_1
rwa :
  ∀ (hst : (h.type₁ x).toN = (h.type₁ x_1).toN),
    { dim := h.dim x + 1, simplex := h.simplex x : X.S } = { dim := h.dim x_1 + 1, simplex := h.simplex x_1 }
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hst : (h.type₁ x).toS = (h.type₁ x_1).toS),
    { dim := h.dim x + 1, simplex := h.simplex x : X.S } = { dim := h.dim x_1 + 1, simplex := h.simplex x_1 }
⊢ { dim := h.dim x + 1, simplex := h.simplex x : X.S } = { dim := h.dim x_1 + 1, simplex := h.simplex x_1 }

Tactic:
rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s t : h.ι
hst : h.type₂ s = h.type₂ t
rwa :
  ∀ (hst : (h.type₂ s).toN = (h.type₂ t).toN),
    Eq.{u + 1} (α := X.S)
      (S.mk (dim := h.dim s)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (h.index s)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋h.dim s + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋h.dim s⦌))
          (h.simplex s)))
      (S.mk (dim := h.dim t)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (h.index t)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋h.dim t + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋h.dim t⦌))
          (h.simplex t)))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (hst : (h.type₂ s).toS = (h.type₂ t).toS),
    Eq.{u + 1} (α := X.S)
      (S.mk (dim := h.dim s)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (h.index s)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋h.dim s + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋h.dim s⦌))
          (h.simplex s)))
      (S.mk (dim := h.dim t)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (h.index t)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋h.dim t + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋h.dim t⦌))
          (h.simplex t)))
⊢ Eq.{u + 1} (α := X.S)
    (S.mk (dim := h.dim s)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (h.index s)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋h.dim s + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋h.dim s⦌))
        (h.simplex s)))
    (S.mk (dim := h.dim t)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (h.index t)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋h.dim t + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋h.dim t⦌))
        (h.simplex t)))

Tactic:
rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s t : h.ι
⊢ h.type₁ s ≠ h.type₂ t

Tactic:
simpa only [ne_eq, N.ext_iff, SSet.N.ext_iff] using h.type₁_ne_type₂' s t

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff, ne_eq, SSet.Subcomplex.PairingCore.type₁_ne_type₂'