awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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
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
⊢ ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s

Tactic:
obtain ⟨s, _ | _⟩ := h.surjective' x

Premises used: SSet.Subcomplex.PairingCore.surjective'
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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
rwa₁ rwa₂ rwa₃ rwa₄ : x.toS = (h.type₁ s).toS
⊢ x = h.type₁ s

Tactic:
rwa [N.ext_iff, SSet.N.ext_iff]

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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 }
⊢ ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s

Tactic:
exact ⟨s, Or.inl (by rwa [N.ext_iff, SSet.N.ext_iff])⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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
rwa₁ rwa₂ rwa₃ rwa₄ : x.toS = (h.type₂ s).toS
⊢ x = h.type₂ s

Tactic:
rwa [N.ext_iff, SSet.N.ext_iff]

Premises used: SSet.N.ext_iff, SSet.Subcomplex.N.ext_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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))
⊢ ∃ (s : h.ι), x = h.type₁ s ∨ x = h.type₂ s

Tactic:
exact ⟨s, Or.inr (by rwa [N.ext_iff, SSet.N.ext_iff])⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h₁ : ∀ (s : A.N), s ∈ h.I ∩ h.II ↔ Membership.mem (γ := Set A.N) ∅ s
⊢ h.I ∩ h.II = ∅

Tactic:
ext s
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s : A.N
h₁ : ∀ (x : h.ι) (h_1 : h.type₁ x = s) (x : h.ι), ¬h.type₂ x = s
⊢ s ∈ h.I ∩ h.II ↔ Membership.mem (γ := Set A.N) ∅ 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]

Premises used: SSet.Subcomplex.PairingCore.II, Set.mem_range, iff_false, Set.mem_inter_iff, forall_exists_index, not_exists, SSet.Subcomplex.PairingCore.I, Set.mem_empty_iff_false, not_and
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
t s : h.ι
⊢ ¬h.type₂ s = h.type₁ t

Tactic:
(h.type₁_ne_type₂ t s).symm

Premises used: Ne.symm, SSet.Subcomplex.PairingCore.type₁_ne_type₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
t s : h.ι
⊢ ¬h.type₂ s = h.type₁ t

Tactic:
exact (h.type₁_ne_type₂ t s).symm

Premises used: Ne.symm, SSet.Subcomplex.PairingCore.type₁_ne_type₂
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h₁ : ∀ (s : A.N), s ∈ h.I ∪ h.II ↔ Membership.mem (γ := Set A.N) Set.univ s
⊢ h.I ∪ h.II = Set.univ

Tactic:
ext s
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s : A.N
⊢ ∃ (s_1 : h.ι), s = h.type₁ s_1 ∨ s = h.type₂ s_1

Tactic:
have := h.surjective s
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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
h₁ : (∃ (y : h.ι), h.type₁ y = s) ∨ ∃ (y : h.ι), h.type₂ y = s
⊢ s ∈ h.I ∪ h.II ↔ Membership.mem (γ := Set A.N) Set.univ s

Tactic:
simp only [I, II, Set.mem_union, Set.mem_range, Set.mem_univ, iff_true]

Premises used: Set.mem_union, SSet.Subcomplex.PairingCore.II, Set.mem_range, iff_true, SSet.Subcomplex.PairingCore.I, Set.mem_univ
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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
⊢ (∃ (y : h.ι), h.type₁ y = s) ∨ ∃ (y : h.ι), h.type₂ y = s

Tactic:
aesop
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : h.ι
⊢ Eq (α := (↑h.I : Type u))
    ((h.pairing.p : (a : (↑h.II : Type u)) → (↑h.I : Type u)) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x) :
      (↑h.I : Type u))
    ((h.equivI : (a : h.ι) → (↑h.I : Type u)) x : (↑h.I : Type u))

Tactic:
simp [pairing]

Premises used: SSet.Subcomplex.PairingCore.pairing
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : h.ι
⊢ Eq (α := (↑h.II : Type u))
    ((h.pairing.p.symm : (a : (↑h.I : Type u)) → (↑h.II : Type u)) ((h.equivI : (a : h.ι) → (↑h.I : Type u)) x) :
      (↑h.II : Type u))
    ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x : (↑h.II : Type u))

Tactic:
simp [pairing]

Premises used: SSet.Subcomplex.PairingCore.pairing
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
x : h.ι
⊢ h.type₁ x =
    (↑((h.pairing.p : (a : (↑h.pairing.II : Type u)) → (↑h.pairing.I : Type u))
          ((h.equivII : (a : h.ι) → (↑h.II : Type u)) x)) :
      A.N)

Tactic:
simp +instances
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
⊢ (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS

Tactic:
IsProper.isUniquelyCodimOneFace _

Premises used: SSet.Subcomplex.PairingCore.IsProper.isUniquelyCodimOneFace
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
x : (↑h.pairing.II : Type u)
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)))
⊢ (↑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)))

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

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
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:
simpa using h.isUniquelyCodimOneFace s

Premises used: SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
⊢ h.pairing.IsProper ↔ h.IsProper

Tactic:
⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩

Premises used: SSet.Subcomplex.PairingCore.IsProper.mk, inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
refine : h.pairing.IsProper → ∀ (s : h.ι), (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS
⊢ h.pairing.IsProper ↔ h.IsProper

Tactic:
refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsProper
s : h.ι
⊢ (h.type₂ s).IsUniquelyCodimOneFace (h.type₁ s).toS

Tactic:
simpa [type₁_pairing] using h.pairing.isUniquelyCodimOneFace (h.equivII s)

Premises used: SSet.Subcomplex.PairingCore.equivII, SSet.Subcomplex.Pairing.isUniquelyCodimOneFace, SSet.Subcomplex.PairingCore.type₁_pairing, SSet.Subcomplex.PairingCore.pairing, DFunLike.coe
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
symm : h.index s = ⋯.index ⋯
⊢ ⋯.index ⋯ = h.index s

Tactic:
symm
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
⊢ h.index s = ⋯.index ⋯

Tactic:
simp [← (h.isUniquelyCodimOneFace s).δ_eq_iff]

Premises used: SSet.Subcomplex.PairingCore.isUniquelyCodimOneFace, SSet.S.IsUniquelyCodimOneFace.δ_eq_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
d : ℕ
hd : h.dim s = d
subst : (↑(⋯.index ⋯) : ℕ) = (↑(h.index s) : ℕ)
⊢ (↑(⋯.index hd) : ℕ) = (↑(h.index s) : ℕ)

Tactic:
subst hd
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsProper
s : h.ι
⊢ (↑(⋯.index ⋯) : ℕ) = (↑(h.index s) : ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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)
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 ⋯ hd ≠ 0
⊢ ∀ {d : ℕ} (hd : (↑x : A.N).dim = d), ⋯.index hd ≠ 0

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

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsInner
inst_1 : h.IsProper
s : h.ι
⊢ S.IsUniquelyCodimOneFace.index ⋯ ⋯ ≠ 0

Tactic:
simpa using IsInner.ne_zero s

Premises used: SSet.Subcomplex.PairingCore.IsInner.ne_zero
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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)
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 ⋯ hd ≠ Fin.last (d + 1)
⊢ ∀ {d : ℕ} (hd : (↑x : A.N).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

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

Premises used: SSet.Subcomplex.PairingCore.equivII, Equiv.surjective, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsInner
inst_1 : h.IsProper
s : h.ι
⊢ S.IsUniquelyCodimOneFace.index ⋯ ⋯ ≠
    Fin.last (S.dim.{u} (X := X) (N.toS (N.toN (A := A) (↑((h.equivII : (a : h.ι) → (↑h.II : Type u)) s) : A.N))) + 1)

Tactic:
simpa using IsInner.ne_last s

Premises used: SSet.Subcomplex.PairingCore.IsInner.ne_last
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
s t : h.ι
⊢ h.AncestralRel s t ↔
    h.pairing.AncestralRel ((h.equivII : (a : h.ι) → (↑h.II : Type u)) s) ((h.equivII : (a : h.ι) → (↑h.II : Type u)) t)

Tactic:
simp [AncestralRel, Pairing.AncestralRel]

Premises used: SSet.Subcomplex.Pairing.AncestralRel, SSet.Subcomplex.PairingCore.AncestralRel
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsRegular
⊢ WellFounded h.AncestralRel

Tactic:
have := IsRegular.wf h
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsRegular
this : WellFounded h.AncestralRel
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) }
⊢ WellFounded h.pairing.AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain] at this ⊢

Premises used: wellFounded_iff_isEmpty_descending_chain
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsRegular
this : IsEmpty.{max 1 (u_1 + 1)} { f : ℕ → h.ι // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
x : { f : ℕ → (↑h.pairing.II : Type u) // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
f : ℕ → (↑h.pairing.II : Type u)
hf : ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.AncestralRel ((fun (n : ℕ) ↦ ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) (f n) : h.ι)) (n + 1))
    ((fun (n : ℕ) ↦ ((h.equivII.symm : (a : (↑h.II : Type u)) → h.ι) (f n) : h.ι)) n)

Tactic:
simpa [ancestralRel_iff] using hf n

Premises used: SSet.Subcomplex.PairingCore.ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
inst : h.IsRegular
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:
exact ⟨fun ⟨f, hf⟩ ↦ this.false
      ⟨fun n ↦ h.equivII.symm (f n), fun n ↦ by simpa [ancestralRel_iff] using hf n⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
⊢ h.pairing.IsRegular ↔ h.IsRegular

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
refine : h.pairing.IsRegular → h.IsRegular
⊢ h.pairing.IsRegular ↔ h.IsRegular

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
rw : h.pairing.IsProper
⊢ h.IsProper

Tactic:
rw [← isProper_pairing_iff]

Premises used: SSet.Subcomplex.PairingCore.isProper_pairing_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
⊢ h.pairing.IsProper

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
⊢ h.IsProper

Tactic:
have : h.IsProper := by
    rw [← isProper_pairing_iff]
    infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this : h.IsProper
wf : WellFounded h.AncestralRel
⊢ h.IsRegular

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this : h.IsProper
⊢ WellFounded h.pairing.AncestralRel

Tactic:
have := h.pairing.wf
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
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
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) }
⊢ WellFounded h.AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain] at this ⊢

Premises used: wellFounded_iff_isEmpty_descending_chain
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this_1 : h.IsProper
this :
  IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑h.pairing.II : Type u) // ∀ (n : ℕ), h.pairing.AncestralRel (f (n + 1)) (f n) }
x : { f : ℕ → h.ι // ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n) }
f : ℕ → h.ι
hf : ∀ (n : ℕ), h.AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ h.pairing.AncestralRel ((fun (n : ℕ) ↦ ((h.equivII : (a : h.ι) → (↑h.II : Type u)) (f n) : (↑h.II : Type u))) (n + 1))
    ((fun (n : ℕ) ↦ ((h.equivII : (a : h.ι) → (↑h.II : Type u)) (f n) : (↑h.II : Type u))) n)

Tactic:
simpa [ancestralRel_iff] using hf n

Premises used: SSet.Subcomplex.PairingCore.ancestralRel_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
Goal:
X : SSet
A : X.Subcomplex
h : PairingCore.{u_1, u} A
h_1 : h.pairing.IsRegular
this_1 : h.IsProper
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:
exact ⟨fun ⟨f, hf⟩ ↦ this.false
    ⟨fun n ↦ h.equivII (f n), fun n ↦ by simpa [ancestralRel_iff] using hf n⟩⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
f : P.RankFunction α
rw : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ WellFounded P.AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain]

Premises used: wellFounded_iff_isEmpty_descending_chain
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
f : P.RankFunction α
⊢ IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }

Tactic:
⟨fun ⟨g, hg⟩ ↦ not_strictAnti_of_wellFoundedLT (f.rank ∘ g)
    (strictAnti_nat_of_succ_lt (fun n ↦ f.lt (hg n)))⟩

Premises used: SSet.Subcomplex.Pairing.RankFunction.rank, False, Function.comp, IsEmpty.mk, _private.0.SSet.Subcomplex.Pairing.RankFunction.wf_ancestralRel.match_1, SSet.Subcomplex.Pairing.RankFunction.lt, strictAnti_nat_of_succ_lt, not_strictAnti_of_wellFoundedLT
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst : PartialOrder α
inst_1 : WellFoundedLT α
f : P.RankFunction α
⊢ IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }

Tactic:
exact ⟨fun ⟨g, hg⟩ ↦ not_strictAnti_of_wellFoundedLT (f.rank ∘ g)
    (strictAnti_nat_of_succ_lt (fun n ↦ f.lt (hg n)))⟩
-- 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 α
rw : IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
⊢ WellFounded P.AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain]

Premises used: wellFounded_iff_isEmpty_descending_chain
-- 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 α
⊢ IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }

Tactic:
⟨fun ⟨g, hg⟩ ↦ ?_⟩

Premises used: False, IsEmpty.mk, _private.0.SSet.Subcomplex.Pairing.RankFunction.wf_ancestralRel.match_1
-- 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 α
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
⊢ IsEmpty.{max 1 (u + 1)} { f : ℕ → (↑P.II : Type u) // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }

Tactic:
refine ⟨fun ⟨g, hg⟩ ↦ ?_⟩
-- 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)
obtain :
  ∀ (n₀ : ℕ)
    (hn₀ :
      ∀ (m : ℕ),
        n₀ ≤ m →
          Eq (α := ℕᵒᵈ) (({ toFun := fun (n : ℕ) ↦ (↑(g n) : A.N).dim, monotone' := ⋯ } : (a : ℕ) → ℕᵒᵈ) n₀ : ℕᵒᵈ)
            (({ toFun := fun (n : ℕ) ↦ (↑(g n) : A.N).dim, monotone' := ⋯ } : (a : ℕ) → ℕᵒᵈ) m : ℕᵒᵈ)),
    False
⊢ 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)⟩

Premises used: inferInstance, SSet.Subcomplex.N.toN, wellFoundedGT_iff_monotone_chain_condition, SSet.Subcomplex.Pairing.AncestralRel.dim_le, SSet.N.toS, SSet.S.dim, Iff.mp, OrderHom.mk, Subtype.val, monotone_nat_of_le_succ
-- 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
⊢ False

Tactic:
not_strictAnti_of_wellFoundedLT (fun n ↦ f.rank (g (n₀ + n)))
    (strictAnti_nat_of_succ_lt (fun n ↦ ?_))

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.rank, HAdd.hAdd, strictAnti_nat_of_succ_lt, not_strictAnti_of_wellFoundedLT
-- 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
refine : ∀ (n : ℕ), f.rank (g (n₀ + (n + 1))) < f.rank (g (n₀ + n))
⊢ False

Tactic:
refine not_strictAnti_of_wellFoundedLT (fun n ↦ f.rank (g (n₀ + n)))
    (strictAnti_nat_of_succ_lt (fun n ↦ ?_))

Premises used: SSet.Subcomplex.Pairing.WeakRankFunction.rank, HAdd.hAdd, strictAnti_nat_of_succ_lt, not_strictAnti_of_wellFoundedLT