awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
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

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

Premises used: SSet.Subcomplex.N.opEquiv, Subtype.mk, IsEmpty.false, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
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)
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)) ⋯ :
            { 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)) ⋯ :
            { x : A.N // x ∈ P.II }))
        n)
⊢ False

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

Premises used: SSet.Subcomplex.N.opEquiv, Subtype.mk, IsEmpty.false, Subtype.val, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op
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)
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)) ⋯ :
          { 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)) ⋯ :
          { x : A.N // x ∈ P.II }))
      n)

Tactic:
simpa [← P.op_ancestralRel_iff] using hf n

Premises used: SSet.Subcomplex.Pairing.op_ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x : (↑P.II : Type u)
⊢ (↑x : A.N).IsUniquelyCodimOneFace
    (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N)))

Tactic:
IsProper.isUniquelyCodimOneFace x

Premises used: SSet.Subcomplex.Pairing.IsProper.isUniquelyCodimOneFace
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x : (↑P.II : Type u)
⊢ S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N))) =
    (↑x : A.N).dim + 1

Tactic:
(P.isUniquelyCodimOneFace x).dim_eq

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.dim_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x y : (↑P.II : Type u)
hxy : P.AncestralRel x y
⊢ (↑x : A.N).dim ≤ (↑y : A.N).dim

Tactic:
simpa only [(P.isUniquelyCodimOneFace y).dim_eq, Nat.lt_succ_iff] using
    SSet.N.dim_lt_of_lt hxy.2

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.dim_eq, SSet.N.dim_lt_of_lt, And.right, Nat.lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsRegular
⊢ WellFounded P.AncestralRel

Tactic:
IsRegular.wf

Premises used: SSet.Subcomplex.Pairing.IsRegular.wf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
⊢ Membership.mem (γ := Set A.N) Set.univ x

Tactic:
have := Set.mem_univ x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
this : Membership.mem (γ := Set A.N) Set.univ x
⊢ x ∈ P.I ∨ x ∈ P.II

Tactic:
rw [← P.union, Set.mem_union] at this

Premises used: Set.mem_union, SSet.Subcomplex.Pairing.union
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
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)
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)
⊢ ∃ (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
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.I
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)
⊢ ∃ (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⟩

Premises used: SSet.Subcomplex.Pairing.p, Subtype.mk, Equiv.surjective
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
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
rw rw₁ : x = (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x h) : A.N)
⊢ x = (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)

Tactic:
rw [hy]
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
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
⊢ ∃ (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:
exact ⟨y, Or.inr (by rw [hy])⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
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:
⟨⟨_, h⟩, Or.inl rfl⟩

Premises used: Subtype.mk, Exists.intro, Or.inl, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
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:
exact ⟨⟨_, h⟩, Or.inl rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : (↑P.I : Type u)
y : (↑P.II : Type u)
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)
⊢ (↑x : A.N) ≠ (↑y : A.N)

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
x : A.N
hx : x ∈ P.I
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)
⊢ (↑(Subtype.mk (p := fun (x : A.N) ↦ x ∈ P.I) x hx) : A.N) ≠ (↑y : A.N)

Tactic:
obtain ⟨y, hy⟩ := y
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
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
⊢ x ∈ P.I ∩ P.II

Tactic:
have : x ∈ P.I ∩ P.II := ⟨hx, hy⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
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
this : x ∈ P.I ∩ P.II
⊢ False

Tactic:
simp [P.inter] at this

Premises used: SSet.Subcomplex.Pairing.inter
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x : (↑P.II : Type u)
⊢ (↑x : A.N) ≤ (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N)

Tactic:
(P.isUniquelyCodimOneFace x).le

Premises used: SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.le
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst : P.IsProper
x : (↑P.II : Type u)
⊢ (↑x : A.N) < (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N)

Tactic:
lt_of_le_of_ne' (P.le x) (P.ne _ _)

Premises used: SSet.Subcomplex.Pairing.ne, lt_of_le_of_ne', SSet.Subcomplex.Pairing.le
-- 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
⊢ Eq (α := Set B.N)
    ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I ∩ (⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) ∅

Tactic:
simp [← Set.preimage_inter, P.inter]

Premises used: Set.preimage_inter, SSet.Subcomplex.Pairing.inter
-- 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
⊢ Eq (α := Set B.N)
    ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I ∪ (⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II)
    Set.univ

Tactic:
simp [← Set.preimage_union, P.union]

Premises used: Set.preimage_union, SSet.Subcomplex.Pairing.union
-- 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
⊢ ∀ (a : B.N),
    Membership.mem (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.II) a ↔
      Membership.mem (α := A.N) P.II
        (((N.orderIsoOfIso e hA).toEquiv (r := fun (x1 x2 : B.N) ↦ x1 ≤ x2) (s := fun (x1 x2 : A.N) ↦ x1 ≤ x2) :
              (a : B.N) → A.N)
            a :
          A.N)

Tactic:
simp
-- 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
⊢ ∀ (a : A.N),
    a ∈ P.I ↔
      Membership.mem (α := B.N) (γ := Set B.N) ((⇑(N.orderIsoOfIso e hA) : (a : B.N) → A.N) ⁻¹' P.I)
        (((N.orderIsoOfIso e hA).symm.toEquiv (r := fun (x1 x2 : A.N) ↦ x1 ≤ x2) (s := fun (x1 x2 : B.N) ↦ x1 ≤ x2) :
              (a : A.N) → B.N)
            a :
          B.N)

Tactic:
simp
-- 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
x : (↑P.II : Type u)
⊢ Membership.mem (α := B.N) (P.ofIso e hA).II (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑x : A.N) : B.N)

Tactic:
simp
-- 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
x : (↑P.II : Type u)
⊢ ((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N) ∈
    (P.ofIso e hA).I

Tactic:
simp
-- 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
x : (↑P.II : Type u)
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
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)) ⋯)) :
      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)
⊢ ((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)) ⋯

Tactic:
ext
-- 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
x : (↑P.II : Type u)
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
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))) ⋯)) :
        A.N))
    ((e'.symm : (a : A.N) → B.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N))
⊢ (↑(((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)

Tactic:
change e'.symm (P.p ⟨e' (e'.symm x), _⟩) = e'.symm (P.p x)

Premises used: SSet.Subcomplex.Pairing.p, OrderIso.symm, Subtype.mk, Subtype.val, DFunLike.coe
-- 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
x : (↑P.II : Type u)
e' : B.N ≃o A.N := N.orderIsoOfIso e hA
⊢ 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))) ⋯)) :
        A.N))
    ((e'.symm : (a : A.N) → B.N) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) x) : A.N))

Tactic:
simp
-- 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
x y : (↑P.II : Type u)
⊢ Membership.mem (α := B.N) (P.ofIso e hA).II (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑x : A.N) : B.N)

Tactic:
simp
-- 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
x y : (↑P.II : Type u)
⊢ Membership.mem (α := B.N) (P.ofIso e hA).II (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑y : A.N) : B.N)

Tactic:
simp
-- 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
x y : (↑P.II : Type u)
⊢ Eq (α := (↑(P.ofIso e hA).II : 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 : A.N)) ⋯ :
        { x : B.N // x ∈ (P.ofIso e hA).II })
      (Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II)
          (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑y : A.N)) ⋯ :
        { x : B.N // x ∈ (P.ofIso e hA).II }) ↔
    x = y

Tactic:
aesop
-- 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
x y : (↑P.II : Type u)
⊢ LT.lt (α := B.N)
      ((↑(Subtype.mk (p := fun (x : B.N) ↦ x ∈ (P.ofIso e hA).II)
              (((N.orderIsoOfIso e hA).symm : (a : A.N) → B.N) (↑x : A.N)) ⋯) :
          B.N) :
        B.N)
      ((↑(((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) (↑y : A.N)) ⋯)) :
          B.N) :
        B.N) ↔
    (↑x : A.N) < (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)

Tactic:
simp
-- 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.IsProper
x : B.N
hx : x ∈ (P.ofIso e hA).II
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)))
⊢ (↑(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)))

Tactic:
obtain ⟨x, rfl⟩ := (N.orderIsoOfIso e hA).symm.surjective x

Premises used: OrderIso.surjective, OrderIso.symm, SSet.Subcomplex.N.orderIsoOfIso, rfl
-- 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.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)
⊢ x ∈ P.II

Tactic:
simp only [ofIso_II, Set.mem_preimage, OrderIso.apply_symm_apply] at hx

Premises used: OrderIso.apply_symm_apply, SSet.Subcomplex.Pairing.ofIso_II, Set.mem_preimage
-- 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.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
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))))
⊢ 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)))

Tactic:
simp only [ofIso_II, ofIso_I, dsimp% P.ofIso_p e hA ⟨x, hx⟩]

Premises used: SSet.Subcomplex.Pairing.ofIso_I, Subtype.mk, SSet.Subcomplex.Pairing.ofIso_p, SSet.Subcomplex.Pairing.ofIso_II
-- 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.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 (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:
(P.isUniquelyCodimOneFace ⟨x, hx⟩).of_iso e.symm

Premises used: SSet.S.IsUniquelyCodimOneFace.of_iso, SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, Subtype.mk, CategoryTheory.Iso.symm
-- 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.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 (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:
exact (P.isUniquelyCodimOneFace ⟨x, hx⟩).of_iso e.symm

Premises used: SSet.S.IsUniquelyCodimOneFace.of_iso, SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, Subtype.mk, CategoryTheory.Iso.symm
-- 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
⊢ WellFounded P.AncestralRel

Tactic:
have hP := P.wf
-- 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 : WellFounded P.AncestralRel
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) }
⊢ WellFounded (P.ofIso e hA).AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain] at hP ⊢

Premises used: wellFounded_iff_isEmpty_descending_chain
-- 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) }
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
⊢ 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:
by_contra!