awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
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.IsProper
x : B.N
hx : x ∈ (P.ofIso e hA).II
⊢ (↑(Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II) x hx) : B.N).IsUniquelyCodimOneFace
    (N.toS
      (N.toN (A := B)
        (↑(((P.ofIso e hA).p : (a : (↑(P.ofIso e hA).II : Type u)) → (↑(P.ofIso e hA).I : Type u))
              (Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II) x hx)) :
          B.N)))
have obtain : ∀ (x : A.N)
  (hx : Membership.mem (α := B.N) (P.ofIso e hA).II (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x : B.N)),
  S.IsUniquelyCodimOneFace.{u} (X := Y)
    (N.toS
      (N.toN (A := B)
        (↑(Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II) (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x)
              hx) :
          B.N)))
    (N.toS
      (N.toN (A := B)
        (↑(((P.ofIso e hA).p : (a : (↑(P.ofIso e hA).II : Type u)) → (↑(P.ofIso e hA).I : Type u))
              (Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II)
                (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x) hx)) :
          B.N)))
Tactic: obtain ⟨x, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (hypothesis)
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.IsProper
x : A.N
hx : Membership.mem (α := B.N) (P.ofIso e hA).II (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x : B.N)
⊢ S.IsUniquelyCodimOneFace.{u} (X := Y)
    (N.toS
      (N.toN (A := B)
        (↑(Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II) (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x)
              hx) :
          B.N)))
    (N.toS
      (N.toN (A := B)
        (↑(((P.ofIso e hA).p : (a : (↑(P.ofIso e hA).II : Type u)) → (↑(P.ofIso e hA).I : Type u))
              (Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II)
                (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x) hx)) :
          B.N)))
have hx₁ : x ∈ P.II
Tactic: simp only [ofIso_II, Set.mem_preimage, OrderIso.apply_symm_apply] at hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
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.IsProper
x : A.N
hx_1 : Membership.mem (α := B.N) (P.ofIso e hA).II (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x : B.N)
hx : x ∈ P.II
⊢ S.IsUniquelyCodimOneFace.{u} (X := Y)
    (N.toS
      (N.toN (A := B)
        (↑(Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II) (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x)
              hx_1) :
          B.N)))
    (N.toS
      (N.toN (A := B)
        (↑(((P.ofIso e hA).p : (a : (↑(P.ofIso e hA).II : Type u)) → (↑(P.ofIso e hA).I : Type u))
              (Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II)
                (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x) hx_1)) :
          B.N)))
have simp : S.IsUniquelyCodimOneFace (X := Y) (N.toS (N.toN (A := B) (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) x)))
  (N.toS
    (N.toN (A := B)
      (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N)
        (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) (Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) x hx)) : A.N))))
Tactic: simp only [ofIso_II, ofIso_I, dsimp% P.ofIso_p e hA ⟨x, hx⟩]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (hypothesis)
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
⊢ WellFounded (P.ofIso e hA).AncestralRel
have hP : WellFounded P.AncestralRel
Tactic: have hP := P.wf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
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 : WellFounded P.AncestralRel
⊢ WellFounded (P.ofIso e hA).AncestralRel
have rw : ∀ (hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }),
  IsEmpty.{max 1 (u + 1)}
    { f : ℕ → (↑(P.ofIso e hA).II : Type u) // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }
Tactic: rw [wellFounded_iff_isEmpty_descending_chain] at hP ⊢
Cleared hypotheses: hP
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
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) }
⊢ IsEmpty.{max 1 (u + 1)}
    { f : ℕ → (↑(P.ofIso e hA).II : Type u) // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }
have by_contra! : ∀
  (this :
    Nonempty.{u + 1}
      { f : ℕ → (↑(P.ofIso e hA).II : Type u) // ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n) }),
  False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
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) }
⊢ False
have obtain : ∀ (f : ℕ → (↑(P.ofIso e hA).II : Type u)) (hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)), False
Tactic: obtain ⟨f, hf⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
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
have 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)) sorry :
          { 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)) sorry :
          { x : A.N // x ∈ P.II }))
      n)
Tactic: refine hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ 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⦌))
have rw : Membership.mem (γ := Set (X _⦋(↑s : A.N).dim⦌)) (X.nonDegenerate (↑s : A.N).dim) ((↑s : A.N).cast sorry).simplex
Tactic: rw [(P.isUniquelyCodimOneFace s).δ_index rfl]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
s : (↑P.II : Type u)
⊢ ((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⦌)
have rw : ((↑s : A.N).cast sorry).simplex ∉ A.obj (Opposite.op ⦋(↑s : A.N).dim⦌)
Tactic: rw [(P.isUniquelyCodimOneFace s).δ_index rfl]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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 }
⊢ s = t
have 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))
Tactic: apply P.p.injective
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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 }
⊢ 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))
have 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)
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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)
⊢ 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))
have 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))
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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))
⊢ 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))
have 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)))
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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)))
⊢ 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))
have a₃ : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry).toS =
  N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N))
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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))
⊢ 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))
have a₄ : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry).toS =
  (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) t) : A.N) sorry).toS
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]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (hypothesis)
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))
⊢ s = t
have h₁ : { dim := (↑s : A.N).dim, simplex := ((↑s : A.N).cast sorry).simplex : X.S } =
  { dim := (↑t : A.N).dim, simplex := ((↑t : A.N).cast sorry).simplex }
Tactic: rw [(P.isUniquelyCodimOneFace s).δ_index rfl,
      (P.isUniquelyCodimOneFace t).δ_index rfl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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 }
⊢ s = t
have rwa : (↑s : A.N) = (↑t : A.N)
Tactic: rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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)
⊢ s = t
have rwa₁ : (↑s : A.N).toN = (↑t : A.N).toN
Tactic: rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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
⊢ s = t
have rwa₂ : (↑s : A.N).toS = (↑t : A.N).toS
Tactic: rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (hypothesis)
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)
⊢ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) = (↑t : A.N)
have h₁ : { dim := (↑s : A.N).dim + 1,
    simplex := (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry).simplex : X.S } =
  { dim := (↑t : A.N).dim, simplex := ((↑t : A.N).cast sorry).simplex }
Tactic: rw [(P.isUniquelyCodimOneFace t).δ_index rfl] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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 }
⊢ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) = (↑t : A.N)
have rwa : N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry = (↑t : A.N)
Tactic: rwa [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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)
⊢ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) = (↑t : A.N)
have rwa₁ : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry).toN = (↑t : A.N).toN
Tactic: rwa [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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
⊢ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) = (↑t : A.N)
have rwa₂ : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry).toS = (↑t : A.N).toS
Tactic: rwa [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x : A.N
⊢ ∃ (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)
have 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) sorry).simplex } ∨
      (↑s : A.N).toS =
        S.mk (dim := (↑s_1 : A.N).dim)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (sorry.index sorry)) :
              (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) sorry).simplex)
Tactic: obtain ⟨s, rfl | rfl⟩ := P.exists_or x
Cleared hypotheses: x