awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
rw : (↑(g n₀) : A.N).dim = (↑(g (n₀ + n)) : A.N).dim
⊢ (↑(g (n₀ + n + 1)) : A.N).dim = (↑(g (n₀ + n)) : A.N).dim
have rw₁ : (↑(g n₀) : A.N).dim = (↑(g n₀) : A.N).dim
Tactic: rw [← hn₀ (n₀ + n + 1) (by lia), ← hn₀ (n₀ + n) (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
f : h.RankFunction α
x y : (↑h.pairing.II : Type u)
hxy : h.pairing.AncestralRel x y
⊢ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) x) <
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)
have obtain : ∀ (x : h.ι) (hxy : h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) y),
  f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)
Tactic: obtain ⟨x, rfl⟩ := h.equivII.surjective x
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
f : h.RankFunction α
y : (↑h.pairing.II : Type u)
x : h.ι
hxy : h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) y
⊢ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)
have obtain : ∀ (y : h.ι)
  (hxy :
    h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)
      ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)),
  f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y))
Tactic: obtain ⟨y, rfl⟩ := h.equivII.surjective y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (hypothesis)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
f : h.RankFunction α
x y : h.ι
hxy :
  h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
⊢ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y))
have hxy₁ : h.AncestralRel x y
Tactic: rw [← ancestralRel_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (hypothesis)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
g : h.pairing.RankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) < g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
have hxy₁ : h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
Tactic: rw [ancestralRel_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
f : h.WeakRankFunction α
x y : (↑h.pairing.II : Type u)
hxy : h.pairing.AncestralRel x y
⊢ (↑x : A.N).dim = (↑y : A.N).dim →
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) x) <
      f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)
have obtain : ∀ (x : h.ι) (hxy : h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) y),
  S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) : A.N))) = (↑y : A.N).dim →
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
      f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)
Tactic: obtain ⟨x, rfl⟩ := h.equivII.surjective x
Cleared hypotheses: x, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
f : h.WeakRankFunction α
y : (↑h.pairing.II : Type u)
x : h.ι
hxy : h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) y
⊢ S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) : A.N))) = (↑y : A.N).dim →
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
      f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)
have obtain : ∀ (y : h.ι)
  (hxy :
    h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)
      ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)),
  S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) : A.N))) =
      S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) y) : A.N))) →
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
      f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y))
Tactic: obtain ⟨y, rfl⟩ := h.equivII.surjective y
Cleared hypotheses: y, hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (hypothesis)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
f : h.WeakRankFunction α
x y : h.ι
hxy :
  h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
⊢ S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) : A.N))) =
      S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) y) : A.N))) →
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) <
      f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y))
have hxy₁ : h.AncestralRel x y
Tactic: rw [← ancestralRel_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (hypothesis)
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
g : h.pairing.WeakRankFunction α
x y : h.ι
hxy : h.AncestralRel x y
⊢ h.dim x = h.dim y →
    g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) < g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
have hxy₁ : h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
Tactic: rw [ancestralRel_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : h.IsProper
f : h.RankFunction α
⊢ h.IsRegular
have rw : h.pairing.IsRegular
Tactic: rw [← isRegular_pairing_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank (goal)
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
inst_2 : h.IsProper
f : h.WeakRankFunction α
⊢ h.IsRegular
have rw : h.pairing.IsRegular
Tactic: rw [← isRegular_pairing_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
t : T
⊢ ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
have obtain : ∀
  (f :
    ⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌),
  CategoryTheory.Mono f →
    ∀
      (hf :
        (CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌))
            (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))) =
          (↑(↑t : (↑P.II : Type u)) : A.N).simplex),
      ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
Tactic: obtain ⟨f, _, hf⟩ := N.le_iff_exists_mono.1 t.2.2.le
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
t : T
f :
  ⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌ ⟶
    ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌
w : CategoryTheory.Mono f
hf :
  (CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))) =
    (↑(↑t : (↑P.II : Type u)) : A.N).simplex
⊢ ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
have refine_1 : (↑(↑t : (↑P.II : Type u)) : A.N).dim <
  S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))
Tactic: refine ⟨⟨⟨t.1.1.dim, ?_⟩, f⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
t : T
f :
  ⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌ ⟶
    ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌
w : CategoryTheory.Mono f
hf :
  (CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(↑(↑t : (↑P.II : Type u)) : A.N).dim⦌))
      (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))) =
    (↑(↑t : (↑P.II : Type u)) : A.N).simplex
refine_1 :
  (↑(↑t : (↑P.II : Type u)) : A.N).dim <
    S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))
⊢ ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
have refine_2 : ψ
    (Sigma.mk (β :=
      fun
        (d :
          Fin
            (S.dim.{u} (X := X)
              (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ↦
      ⦋(↑d : ℕ)⦌ ⟶
        ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
      (⟨(↑(↑t : (↑P.II : Type u)) : A.N).dim, sorry⟩ :
        Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
      f) =
  (↑(↑t : (↑P.II : Type u)) : A.N).toS
Tactic: refine ⟨⟨⟨t.1.1.dim, ?_⟩, f⟩, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
⊢ Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }
have h : ∀ (t : T), ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
Tactic: have h (t : T) : ∃ u, ψ u = t.1.1.toS := by
    obtain ⟨f, _, hf⟩ := N.le_iff_exists_mono.1 t.2.2.le
    refine ⟨⟨⟨t.1.1.dim, ?_⟩, f⟩, ?_⟩
    · simpa using SSet.N.dim_lt_of_lt t.2.2
    · rwa [SSet.S.ext_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
h : ∀ (t : T), ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS
⊢ Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }
have choose : ∀ (φ : (t : T) → U) (hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS),
  Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }
Tactic: choose φ hφ using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
⊢ Finite.{max 1 (u + 1)} { x : (↑P.II : Type u) // P.AncestralRel x y }
have apply : Function.Injective φ
Tactic: apply Finite.of_injective φ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ t₁ = t₂
have rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
⊢ t₁ = t₂
have rw₁ : (↑(↑t₁ : (↑P.II : Type u)) : A.N) = (↑(↑t₂ : (↑P.II : Type u)) : A.N)
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
rw₁ : (↑(↑t₁ : (↑P.II : Type u)) : A.N) = (↑(↑t₂ : (↑P.II : Type u)) : A.N)
⊢ t₁ = t₂
have rw₂ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toN = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toN
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : (↑P.II : Type u)
T : Type (max 0 u) := { x : (↑P.II : Type u) // P.AncestralRel x y }
U : Type :=
  (d :
    Fin (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N))))) ×
    (⦋(↑d : ℕ)⦌ ⟶
      ⦋S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))⦌)
ψ : U → X.S :=
  fun (x : U) ↦
    match (motive := U → X.S) x with
    | ⟨d, f⟩ =>
      S.mk (dim := (↑d : ℕ))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : (fun (X : Type u) ↦ X) (X _⦋(↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N).dim⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋(↑d : ℕ)⦌))
          (S.simplex (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) y) : A.N)))))
φ : (t : T) → U
hφ : ∀ (t : T), ψ (φ t) = (↑(↑t : (↑P.II : Type u)) : A.N).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
rw : (↑t₁ : (↑P.II : Type u)) = (↑t₂ : (↑P.II : Type u))
rw₁ : (↑(↑t₁ : (↑P.II : Type u)) : A.N) = (↑(↑t₂ : (↑P.II : Type u)) : A.N)
rw₂ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toN = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toN
⊢ t₁ = t₂
have rw₃ : (↑(↑t₁ : (↑P.II : Type u)) : A.N).toS = (↑(↑t₂ : (↑P.II : Type u)) : A.N).toS
Tactic: rw [Subtype.ext_iff, Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff, ← hφ, ← hφ, h]