awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) x)
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) y)
have obtain : ∀ (d : ℕ) (x : X _⦋d⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y),
  IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) y)
Tactic: obtain ⟨d, x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
y : X.S
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) y)
have obtain : ∀ (d' : ℕ) (y : X _⦋d'⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }),
  IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d', simplex := y : X.S })
Tactic: obtain ⟨d', y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d', simplex := y : X.S })
have obtain : ∀ (y : X _⦋d + 1⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }),
  IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d + 1, simplex := y : X.S })
Tactic: obtain rfl : d' = d + 1 := hxy.dim_eq
Cleared hypotheses: d', y, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ IsUniquelyCodimOneFace.{u} (X := X.op) ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d, simplex := x : X.S })
    ((Equiv.symm opEquiv : (a : X.S) → X.op.S) { dim := d + 1, simplex := y : X.S })
have simp : ∃! i : Fin (d + 2),
  Eq (α := X.op _⦋d⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
      X.op _⦋d⦌)
    ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)
Tactic: simp only [opEquiv_symm_apply, iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ ∃! i : Fin (d + 2),
    Eq (α := X.op _⦋d⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
          ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
        X.op _⦋d⦌)
      ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)
have refine : ∀ (i : Fin (d + 2))
  (hi :
    (fun (i : Fin (d + 2)) ↦
        Eq (α := X.op _⦋d⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
              ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
            X.op _⦋d⦌)
          ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌))
      i),
  i = (hxy.index sorry).rev
Tactic: refine ⟨(hxy.index rfl).rev, by simpa using hxy.δ_index rfl, fun i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
i : Fin (d + 2)
hi :
  (fun (i : Fin (d + 2)) ↦
      Eq (α := X.op _⦋d⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
            ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
          X.op _⦋d⦌)
        ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌))
    i
⊢ i = (hxy.index ⋯).rev
have obtain : ∀ (i : Fin (d + 2))
  (hi :
    Eq (α := X.op _⦋d⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X.op i.rev) : (a : X.op _⦋d + 1⦌) → X.op _⦋d⦌)
          ((Equiv.symm opObjEquiv : (a : X _⦋d + 1⦌) → X.op _⦋d + 1⦌) y : X.op _⦋d + 1⦌) :
        X.op _⦋d⦌)
      ((Equiv.symm opObjEquiv : (a : X _⦋d⦌) → X.op _⦋d⦌) x : X.op _⦋d⦌)),
  i.rev = (hxy.index sorry).rev
Tactic: obtain ⟨i, rfl⟩ := i.rev_surjective
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := x.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
        x.simplex))
    (mk (dim := y.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
        y.simplex))
have obtain : ∀ (d : ℕ) (x : X _⦋d⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y),
  IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := y.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
        y.simplex))
Tactic: obtain ⟨d, x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X : SSet
y : X.S
Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace y
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := y.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌))
        y.simplex))
have obtain : ∀ (d' : ℕ) (y : X _⦋d'⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }),
  IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := { dim := d', simplex := y : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d', simplex := y : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d', simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d', simplex := y }.dim⦌))
        { dim := d', simplex := y : X.S }.simplex))
Tactic: obtain ⟨d', y, rfl⟩ := y.mk_surjective
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
d' : ℕ
y : X _⦋d'⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d', simplex := y }
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := { dim := d', simplex := y : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d', simplex := y : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d', simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d', simplex := y }.dim⦌))
        { dim := d', simplex := y : X.S }.simplex))
have obtain : ∀ (y : X _⦋d + 1⦌) (hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }),
  IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := { dim := d + 1, simplex := y : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex))
Tactic: obtain rfl : d' = d + 1 := hxy.dim_eq
Cleared hypotheses: d', y, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace (goal)
Goal:
X Y : SSet
e : X ≅ Y
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
hxy : { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }
⊢ IsUniquelyCodimOneFace.{u} (X := Y)
    (mk (dim := { dim := d, simplex := x : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d, simplex := x : X.S }.simplex))
    (mk (dim := { dim := d + 1, simplex := y : X.S }.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex))
have rw : ∀
  (hxy :
    ∃! i : Fin (d + 2),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
            (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
          y =
        x),
  ∃! i : Fin ({ dim := d, simplex := x : X.S }.dim + 2),
    Eq (α := (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ Y i) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim + 1⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (e.hom.app (Opposite.op ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
                (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                  (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y }.dim⦌))
              { dim := d + 1, simplex := y : X.S }.simplex :
            (fun (X : Type u) ↦ X) (Y _⦋{ dim := d + 1, simplex := y : X.S }.dim⦌)) :
        (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋{ dim := d, simplex := x : X.S }.dim⦌)) :
            (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌)) →
              (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x }.dim⦌))
          { dim := d, simplex := x : X.S }.simplex :
        (fun (X : Type u) ↦ X) (Y _⦋{ dim := d, simplex := x : X.S }.dim⦌))
Tactic: rw [iff] at hxy ⊢
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
⊢ WellFounded P.op.AncestralRel
have hP : WellFounded P.AncestralRel
Tactic: have hP := P.wf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
hP : WellFounded P.AncestralRel
⊢ WellFounded P.op.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.op.II : Type u) // ∀ (n : ℕ), P.op.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.Op (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
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.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
have by_contra! : ∀ (this : Nonempty.{u + 1} { f : ℕ → (↑P.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
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.op.II : Type u) // ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n) }
⊢ False
have obtain : ∀ (f : ℕ → (↑P.op.II : Type u)) (hf : ∀ (n : ℕ), P.op.AncestralRel (f (n + 1)) (f n)), False
Tactic: obtain ⟨f, hf⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
hP : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → (↑P.op.II : Type u)
hf : ∀ (n : ℕ), P.op.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.opEquiv : (a : A.op.N) → A.N) (↑(f n) : A.op.N)) sorry :
          { x : A.N // x ∈ P.II }))
      (n + 1))
    ((fun (n : ℕ) ↦
        (Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) ((N.opEquiv : (a : A.op.N) → A.N) (↑(f n) : A.op.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.Pairing (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
⊢ ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
have this : Membership.mem (γ := Set A.N) Set.univ x
Tactic: have := Set.mem_univ x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : Membership.mem (γ := Set A.N) Set.univ x
⊢ ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
have this₁ : x ∈ P.I ∨ x ∈ P.II
Tactic: rw [← P.union, Set.mem_union] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : x ∈ P.I ∨ x ∈ P.II
⊢ ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
have inl : ∀ (h : x ∈ P.I),
  ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
Tactic: obtain h | h := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : x ∈ P.I ∨ x ∈ P.II
inl :
  ∀ (h : x ∈ P.I),
    ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
⊢ ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
have inr : ∀ (h : x ∈ P.II),
  ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
Tactic: obtain h | h := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
⊢ ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
have inl : ∀ (y : (↑P.II : Type u))
  (hy : (P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y = Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x h),
  ∃ (y : (↑P.II : Type u)), x = (↑y : A.N) ∨ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
Tactic: obtain ⟨y, hy⟩ := P.p.surjective ⟨x, h⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
y : (↑P.II : Type u)
hy : (P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y = Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x h
⊢ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)
have rw : x = (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x h) : A.N)
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : (↑P.I : Type u)
y : (↑P.II : Type u)
⊢ (↑x : A.N) ≠ (↑y : A.N)
have obtain : ∀ (x : A.N) (hx : x ∈ P.I), (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x hx) : A.N) ≠ (↑y : A.N)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
x : A.N
hx : x ∈ P.I
⊢ (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x hx) : A.N) ≠ (↑y : A.N)
have obtain : ∀ (y : A.N) (hy : y ∈ P.II),
  (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x hx) : A.N) ≠ (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.II) y hy) : A.N)
Tactic: obtain ⟨y, hy⟩ := y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
hy : (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x hx) : A.N) ∈ P.II
⊢ False
have this : x ∈ P.I ∩ P.II
Tactic: have : x ∈ P.I ∩ P.II := ⟨hx, hy⟩
-- 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
x : (↑P.II : Type u)
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
⊢ ((P.ofIso e hA).p :
        (a : (↑((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) : Type u)) →
          (↑((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I) : Type u))
      (Subtype.mk (p := fun (x : B.N) ↦
        Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) x)
        (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑x : A.N)) ⋯) =
    Subtype.mk (p := fun (x : B.N) ↦
      Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I) x)
      (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N)) ⋯
have a : (↑(((P.ofIso e hA).p :
          (a : (↑((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) : Type u)) →
            (↑((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I) : Type u))
        (Subtype.mk (p := fun (x : B.N) ↦
          Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) x)
          (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑x : A.N)) sorry)) :
    B.N) =
  (↑(Subtype.mk (p := fun (x : B.N) ↦
        Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I) x)
        (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N))
        sorry) :
    B.N)
Tactic: ext
-- 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
x : (↑P.II : Type u)
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
⊢ (↑(((P.ofIso e hA).p :
            (a : (↑((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) : Type u)) →
              (↑((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I) : Type u))
          (Subtype.mk (p := fun (x : B.N) ↦
            Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) x)
            (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑x : A.N)) ⋯)) :
      B.N) =
    (↑(Subtype.mk (p := fun (x : B.N) ↦
          Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I) x)
          (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N)
            (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N))
          ⋯) :
      B.N)
have a : Eq (α := B.N)
  ((e'.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) ((e' : (a : B.N) → A.N) ((e'.symm : (a : A.N) → B.N) (↑x : A.N)))
            sorry)) :
      A.N))
  ((e'.symm : (a : A.N) → B.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N))
Tactic: change e'.symm (P.p ⟨e' (e'.symm x), _⟩) = e'.symm (P.p x)