awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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 : f.rank (g (n₀ + n + 1)) < f.rank (g (n₀ + n))
⊢ f.rank (g (n₀ + (n + 1))) < f.rank (g (n₀ + n))

Tactic:
rw [← add_assoc]

Premises used: add_assoc
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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 : ℕ
⊢ n₀ ≤ n₀ + n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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 : ℕ
⊢ n₀ ≤ n₀ + n

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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
rw₁ rw₂ : (↑(g n₀) : A.N).dim = (↑(g n₀) : A.N).dim
⊢ (↑(g (n₀ + n + 1)) : A.N).dim = (↑(g (n₀ + n)) : A.N).dim

Tactic:
rw [← hn₀ (n₀ + n + 1) (by lia), ← hn₀ (n₀ + n) (by lia)]

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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))

Tactic:
exact f.lt (hg _) (by rw [← hn₀ (n₀ + n + 1) (by lia), ← hn₀ (n₀ + n) (by lia)])

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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
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)
⊢ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) x) <
    f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) y)

Tactic:
obtain ⟨x, rfl⟩ := h.equivII.surjective x

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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
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))
⊢ 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 ⟨y, rfl⟩ := h.equivII.surjective y

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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)
⊢ h.AncestralRel x y

Tactic:
rw [← ancestralRel_iff] at hxy

Premises used: SSet.Subcomplex.PairingCore.ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.AncestralRel 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.ι) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y))

Tactic:
simpa using f.lt hxy

Premises used: SSet.Subcomplex.PairingCore.RankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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
⊢ 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

Premises used: SSet.Subcomplex.PairingCore.ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
⊢ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) < g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)

Tactic:
g.lt hxy

Premises used: SSet.Subcomplex.Pairing.RankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)
⊢ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) < g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) y)

Tactic:
exact g.lt hxy

Premises used: SSet.Subcomplex.Pairing.RankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
x : h.RankFunction α
⊢ (fun (g : h.pairing.RankFunction α) ↦
        ({ rank := fun (x : h.ι) ↦ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x), lt := ⋯ } : h.RankFunction α))
      ((fun (f : h.RankFunction α) ↦
          ({ rank := fun (s : (↑h.pairing.II : Type u)) ↦ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) s),
              lt := ⋯ } :
            h.pairing.RankFunction α))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
x : h.pairing.RankFunction α
⊢ (fun (f : h.RankFunction α) ↦
        ({ rank := fun (s : (↑h.pairing.II : Type u)) ↦ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) s),
            lt := ⋯ } :
          h.pairing.RankFunction α))
      ((fun (g : h.pairing.RankFunction α) ↦
          ({ rank := fun (x : h.ι) ↦ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x), lt := ⋯ } :
            h.RankFunction α))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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
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)
⊢ (↑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)

Tactic:
obtain ⟨x, rfl⟩ := h.equivII.surjective x

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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
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))
⊢ 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 ⟨y, rfl⟩ := h.equivII.surjective y

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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)
⊢ h.AncestralRel x y

Tactic:
rw [← ancestralRel_iff] at hxy

Premises used: SSet.Subcomplex.PairingCore.ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.AncestralRel x 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:
simpa using f.lt hxy

Premises used: SSet.Subcomplex.PairingCore.WeakRankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.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

Premises used: SSet.Subcomplex.PairingCore.ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) 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)

Tactic:
g.lt hxy

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) 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)

Tactic:
exact g.lt hxy

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.lt
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
x : h.WeakRankFunction α
⊢ (fun (g : h.pairing.WeakRankFunction α) ↦
        ({ rank := fun (x : h.ι) ↦ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x), lt := ⋯ } :
          h.WeakRankFunction α))
      ((fun (f : h.WeakRankFunction α) ↦
          ({ rank := fun (s : (↑h.pairing.II : Type u)) ↦ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) s),
              lt := ⋯ } :
            h.pairing.WeakRankFunction α))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X_1 : SSet
A_1 : X_1.Subcomplex
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
α : Type v
inst : PartialOrder α
x : h.pairing.WeakRankFunction α
⊢ (fun (f : h.WeakRankFunction α) ↦
        ({ rank := fun (s : (↑h.pairing.II : Type u)) ↦ f.rank ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) s),
            lt := ⋯ } :
          h.pairing.WeakRankFunction α))
      ((fun (g : h.pairing.WeakRankFunction α) ↦
          ({ rank := fun (x : h.ι) ↦ g.rank ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x), lt := ⋯ } :
            h.WeakRankFunction α))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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 α
rw : h.pairing.IsRegular
⊢ h.IsRegular

Tactic:
rw [← isRegular_pairing_iff]

Premises used: SSet.Subcomplex.PairingCore.isRegular_pairing_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.IsRegular

Tactic:
(h.rankFunctionEquiv α f).isRegular

Premises used: SSet.Subcomplex.PairingCore.rankFunctionEquiv, SSet.Subcomplex.Pairing.RankFunction.isRegular, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.IsRegular

Tactic:
exact (h.rankFunctionEquiv α f).isRegular

Premises used: SSet.Subcomplex.PairingCore.rankFunctionEquiv, SSet.Subcomplex.Pairing.RankFunction.isRegular, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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 α
rw : h.pairing.IsRegular
⊢ h.IsRegular

Tactic:
rw [← isRegular_pairing_iff]

Premises used: SSet.Subcomplex.PairingCore.isRegular_pairing_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.IsRegular

Tactic:
(h.weakRankFunctionEquiv α f).isRegular

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.isRegular, SSet.Subcomplex.PairingCore.weakRankFunctionEquiv, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
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.pairing.IsRegular

Tactic:
exact (h.weakRankFunctionEquiv α f).isRegular

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.isRegular, SSet.Subcomplex.PairingCore.weakRankFunctionEquiv, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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
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
⊢ ∃ (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

Premises used: LT.lt.le, SSet.N.le_iff_exists_mono, And.right, Iff.mp, Subtype.property
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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

Tactic:
⟨⟨⟨t.1.1.dim, ?_⟩, f⟩, ?_⟩

Premises used: Fin.mk, SSet.Subcomplex.N.toN, SSet.N.toS, SSet.S.dim, Exists.intro, Sigma.mk, Subtype.val
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
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)))
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, ⋯⟩ :
          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
⊢ ∃ (u : U), ψ u = (↑(↑t : (↑P.II : Type u)) : A.N).toS

Tactic:
refine ⟨⟨⟨t.1.1.dim, ?_⟩, f⟩, ?_⟩