awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ∃ (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 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) sorry).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 (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
-- 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)
⊢ ∃ (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)
have inl : (↑s : A.N).toS =
  S.mk (dim := (↑s : A.N).dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (sorry.index sorry)) :
        (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) sorry).simplex)
Tactic: refine ⟨s, Or.inr ?_⟩
-- 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)
⊢ ∃ (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))
have 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) sorry).simplex : X.S }
Tactic: refine ⟨s, Or.inl ?_⟩
-- 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)
⊢ 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 }
have inr : (N.cast (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) s) : A.N) sorry).toS =
  { 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 }
Tactic: nth_rw 1 [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x x_1 : h.ι
hst : h.type₁ x = h.type₁ x_1
⊢ { dim := h.dim x + 1, simplex := h.simplex x : X.S } = { dim := h.dim x_1 + 1, simplex := h.simplex x_1 }
have 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 }
Tactic: rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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 }
⊢ { dim := h.dim x + 1, simplex := h.simplex x : X.S } = { dim := h.dim x_1 + 1, simplex := h.simplex x_1 }
have 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 }
Tactic: rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s t : h.ι
hst : h.type₂ s = h.type₂ 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)))
have 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)))
Tactic: rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : A.N
⊢ ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s
have inl : ∀ (s : h.ι), x.toS = { dim := h.dim s + 1, simplex := h.simplex s } → ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s
Tactic: obtain ⟨s, _ | _⟩ := h.surjective' x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : A.N
inl : ∀ (s : h.ι), x.toS = { dim := h.dim s + 1, simplex := h.simplex s } → ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s
⊢ ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s
have inr : ∀ (s : h.ι),
  x.toS =
      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 : h.ι), x = h.type₁ s ∨ x = h.type₂ s
Tactic: obtain ⟨s, _ | _⟩ := h.surjective' x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : A.N
s : h.ι
h_1 : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
⊢ x = h.type₁ s
have rwa : x.toN = (h.type₁ s).toN
Tactic: rwa [N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : A.N
s : h.ι
h_1 : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
rwa : x.toN = (h.type₁ s).toN
⊢ x = h.type₁ s
have rwa₁ : x.toS = (h.type₁ s).toS
Tactic: rwa [N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : A.N
s : h.ι
h_1 :
  x.toS =
    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))
⊢ x = h.type₂ s
have rwa : x.toN = (h.type₂ s).toN
Tactic: rwa [N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : A.N
s : h.ι
h_1 :
  x.toS =
    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))
rwa : x.toN = (h.type₂ s).toN
⊢ x = h.type₂ s
have rwa₁ : x.toS = (h.type₂ s).toS
Tactic: rwa [N.ext_iff, SSet.N.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
⊢ h.I ∩ h.II = ∅
have h₁ : ∀ (s : A.N), s ∈ h.I ∩ h.II ↔ Membership.mem (γ := Set A.N) ∅ s
Tactic: ext s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s : A.N
⊢ s ∈ h.I ∩ h.II ↔ Membership.mem (γ := Set A.N) ∅ s
have h₁ : ∀ (x : h.ι) (h_1 : h.type₁ x = s) (x : h.ι), ¬h.type₂ x = s
Tactic: simp only [I, II, Set.mem_inter_iff, Set.mem_range, Set.mem_empty_iff_false,
      iff_false, not_and, not_exists, forall_exists_index]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
⊢ h.I ∪ h.II = Set.univ
have h₁ : ∀ (s : A.N), s ∈ h.I ∪ h.II ↔ Membership.mem (γ := Set A.N) Set.univ s
Tactic: ext s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s : A.N
⊢ s ∈ h.I ∪ h.II ↔ Membership.mem (γ := Set A.N) Set.univ s
have this : ∃ (s_1 : h.ι), s = h.type₁ s_1 ∨ s = h.type₂ s_1
Tactic: have := h.surjective s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s : A.N
this : ∃ (s_1 : h.ι), s = h.type₁ s_1 ∨ s = h.type₂ s_1
⊢ s ∈ h.I ∪ h.II ↔ Membership.mem (γ := Set A.N) Set.univ s
have h₁ : (∃ (y : h.ι), h.type₁ y = s) ∨ ∃ (y : h.ι), h.type₂ y = s
Tactic: simp only [I, II, Set.mem_union, Set.mem_range, Set.mem_univ, iff_true]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
x : (↑h.pairing.II : Type u)
⊢ (↑x : A.N).IsUniquelyCodimOneFace
    (N.toS (N.toN (A := A) (↑((h.pairing.p : (a : (↑h.pairing.II : Type u)) → (↑h.pairing.I : Type u)) x) : A.N)))
have obtain : ∀ (s : h.ι),
  S.IsUniquelyCodimOneFace.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) s) : A.N)))
    (N.toS
      (N.toN (A := A)
        (↑((h.pairing.p : (a : (↑h.pairing.II : Type u)) → (↑h.pairing.I : Type u))
              ((h.equivII : (a : h.ι) → (↑h.II : Type u)) s)) :
          A.N)))
Tactic: obtain ⟨s, rfl⟩ := h.equivII.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
⊢ h.pairing.IsProper ↔ h.IsProper
have refine : h.pairing.IsProper → ∀ (s : h.ι), (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
Tactic: refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ = h.index s
have symm : h.index s = sorry.index sorry
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
d : ℕ
hd : h.dim s = d
⊢ (↑(⋯.index hd) : ℕ) = (↑(h.index s) : ℕ)
have subst : (↑(sorry.index sorry) : ℕ) = (↑(h.index s) : ℕ)
Tactic: subst hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsInner
inst_1 : h.IsProper
x : (↑h.pairing.II : Type u)
⊢ ∀ {d : ℕ} (hd : (↑x : A.N).dim = d), ⋯.index hd ≠ 0
have obtain : ∀ (s : h.ι) {d : ℕ}
  (hd : S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) s) : A.N))) = d),
  S.IsUniquelyCodimOneFace.index sorry hd ≠ 0
Tactic: obtain ⟨s, rfl⟩ := h.equivII.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsInner
inst_1 : h.IsProper
x : (↑h.pairing.II : Type u)
⊢ ∀ {d : ℕ} (hd : (↑x : A.N).dim = d), ⋯.index hd ≠ Fin.last (d + 1)
have obtain : ∀ (s : h.ι) {d : ℕ}
  (hd : S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) s) : A.N))) = d),
  S.IsUniquelyCodimOneFace.index sorry hd ≠ Fin.last (d + 1)
Tactic: obtain ⟨s, rfl⟩ := h.equivII.surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsRegular
⊢ WellFounded h.pairing.AncestralRel
have this : WellFounded h.AncestralRel
Tactic: have := IsRegular.wf h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsRegular
this : WellFounded h.AncestralRel
⊢ WellFounded h.pairing.AncestralRel
have rw : ∀ (this : IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → h.ι // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }),
  IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑h.pairing.II : Type u) // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
Tactic: rw [wellFounded_iff_isEmpty_descending_chain] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
⊢ h.pairing.IsRegular ↔ h.IsRegular
have refine : h.pairing.IsRegular → h.IsRegular
Tactic: refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
⊢ h.IsProper
have rw : h.pairing.IsProper
Tactic: rw [← isProper_pairing_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
⊢ h.IsRegular
have this : h.IsProper
Tactic: have : h.IsProper := by
    rw [← isProper_pairing_iff]
    infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this : h.IsProper
⊢ h.IsRegular
have wf : WellFounded h.AncestralRel
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this : h.IsProper
⊢ WellFounded h.AncestralRel
have this₁ : WellFounded h.pairing.AncestralRel
Tactic: have := h.pairing.wf
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this_1 : h.IsProper
this : WellFounded h.pairing.AncestralRel
⊢ WellFounded h.AncestralRel
have wf : ∀
  (this :
    IsEmpty.{max 1 (u + 1)}
      { f : ℕ → (↑h.pairing.II : Type u) // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }),
  IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → h.ι // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
Tactic: rw [wellFounded_iff_isEmpty_descending_chain] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
f : P.RankFunction α
⊢ WellFounded P.AncestralRel
have rw : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
Tactic: rw [wellFounded_iff_isEmpty_descending_chain]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : P.IsProper
f : P.WeakRankFunction α
⊢ WellFounded P.AncestralRel
have rw : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
Tactic: rw [wellFounded_iff_isEmpty_descending_chain]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : P.IsProper
f : P.WeakRankFunction α
⊢ IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
have refine : ∀ (x : { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }) (g : ℕ → (↑P.II : Type u))
  (hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)), False
Tactic: refine ⟨fun ⟨g, hg⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : P.IsProper
f : P.WeakRankFunction α
x : { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → (↑P.II : Type u)
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
⊢ False
have obtain : ∀ (n₀ : ℕ)
  (hn₀ :
    ∀ (m : ℕ),
      n₀ ≤ m →
        Eq (α := ℕᵒᵈ) (({ toFun := fun (n : ℕ) ↦ (↑(g n) : A.N).dim, monotone' := sorry } : (a : ℕ) → ℕᵒᵈ) n₀ : ℕᵒᵈ)
          (({ toFun := fun (n : ℕ) ↦ (↑(g n) : A.N).dim, monotone' := sorry } : (a : ℕ) → ℕᵒᵈ) m : ℕᵒᵈ)),
  False
Tactic: obtain ⟨n₀, hn₀⟩ :=
    (wellFoundedGT_iff_monotone_chain_condition (α := ℕᵒᵈ)).1
      inferInstance ⟨fun n ↦ (g n).1.dim,
        monotone_nat_of_le_succ (fun n ↦ (hg n).dim_le)⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : P.IsProper
f : P.WeakRankFunction α
x : { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → (↑P.II : Type u)
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀) : A.N).dim = (↑(g m) : A.N).dim
⊢ False
have refine : ∀ (n : ℕ), f.rank (g (n₀ + (n + 1))) < f.rank (g (n₀ + n))
Tactic: refine not_strictAnti_of_wellFoundedLT (fun n ↦ f.rank (g (n₀ + n)))
    (strictAnti_nat_of_succ_lt (fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : P.IsProper
f : P.WeakRankFunction α
x : { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → (↑P.II : Type u)
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀) : A.N).dim = (↑(g m) : A.N).dim
n : ℕ
⊢ f.rank (g (n₀ + (n + 1))) < f.rank (g (n₀ + n))
have rw : f.rank (g (n₀ + n + 1)) < f.rank (g (n₀ + n))
Tactic: rw [← add_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : P.IsProper
f : P.WeakRankFunction α
x : { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → (↑P.II : Type u)
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀) : A.N).dim = (↑(g m) : A.N).dim
n : ℕ
⊢ (↑(g (n₀ + n + 1)) : A.N).dim = (↑(g (n₀ + n)) : A.N).dim
have rw : (↑(g n₀) : A.N).dim = (↑(g (n₀ + n)) : A.N).dim
Tactic: rw [← hn₀ (n₀ + n + 1) (by lia), ← hn₀ (n₀ + n) (by lia)]