awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ Mono g

Tactic:
rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply] at hs

Premises used: Equiv.apply_symm_apply, SSet.nonDegenerate_iff_of_mono, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hs₁ : Mono g
⊢ ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)

Tactic:
rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply] at hs

Premises used: Equiv.apply_symm_apply, SSet.nonDegenerate_iff_of_mono, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hs₁ : Mono g
hs'₁ :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
⊢ ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)

Tactic:
rw [nonDegenerate_iff_of_mono, stdSimplex.mem_nonDegenerate_iff_mono,
    Equiv.apply_symm_apply] at hs

Premises used: Equiv.apply_symm_apply, SSet.nonDegenerate_iff_of_mono, SSet.stdSimplex.mem_nonDegenerate_iff_mono
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs : Mono g
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd : d < x.dim + 1
⊢ d ≤ x.dim

Tactic:
rw [Nat.lt_succ_iff] at hd

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs : Mono g
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd_1 : d ≤ x.dim
hd : d < x.dim
⊢ d + 1 < x.dim + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs : Mono g
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd_1 : d ≤ x.dim
hd : d < x.dim
⊢ Membership.mem (α := Δ[x.dim + 1] _⦋d⦌) (γ := Set (Δ[x.dim + 1] _⦋d⦌)) (Λ[x.dim + 1, x.index].obj (op ⦋d⦌))
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌)

Tactic:
simp [horn_obj_eq_univ x.index d (by lia)]

Premises used: SSet.horn_obj_eq_univ, SSet.Subcomplex.Pairing.RankFunction.Cell.index
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs : Mono g
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
          Δ[x.dim + 1] _⦋d⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
hd_1 : d ≤ x.dim
hd : d < x.dim
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c

Tactic:
exact (hs' (by simp [horn_obj_eq_univ x.index d (by lia)])).elim

Premises used: False.elim
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
x : f.Cell j
hd : x.dim ≤ x.dim
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋x.dim⦌) (γ := Set (f.sigmaStdSimplex j _⦋x.dim⦌))
    ((f.sigmaStdSimplex j).nonDegenerate x.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
            (SimplexCategory.δ x.index) :
          Δ[x.dim + 1] _⦋x.dim⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
hs : Mono (SimplexCategory.δ x.index)
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
            (SimplexCategory.δ x.index) :
          Δ[x.dim + 1] _⦋x.dim⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋x.dim⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
        (SimplexCategory.δ x.index) :
      Δ[x.dim + 1] _⦋x.dim⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
                (SimplexCategory.δ x.index) :
              Δ[x.dim + 1] _⦋x.dim⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
                (SimplexCategory.δ x.index) :
              Δ[x.dim + 1] _⦋x.dim⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c

Tactic:
⟨x, Or.inr rfl⟩

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
x : f.Cell j
hd : x.dim ≤ x.dim
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋x.dim⦌) (γ := Set (f.sigmaStdSimplex j _⦋x.dim⦌))
    ((f.sigmaStdSimplex j).nonDegenerate x.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
            (SimplexCategory.δ x.index) :
          Δ[x.dim + 1] _⦋x.dim⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
hs : Mono (SimplexCategory.δ x.index)
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
            (SimplexCategory.δ x.index) :
          Δ[x.dim + 1] _⦋x.dim⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋x.dim⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
        (SimplexCategory.δ x.index) :
      Δ[x.dim + 1] _⦋x.dim⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋x.dim⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
                (SimplexCategory.δ x.index) :
              Δ[x.dim + 1] _⦋x.dim⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim⦌)
                (SimplexCategory.δ x.index) :
              Δ[x.dim + 1] _⦋x.dim⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c

Tactic:
exact ⟨x, Or.inr rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
x : f.Cell j
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋x.dim + 1⦌) (γ := Set (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
    ((f.sigmaStdSimplex j).nonDegenerate (x.dim + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
            (𝟙 (unop (op ⦋x.dim + 1⦌))) :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
hs : Mono (𝟙 (unop (op ⦋x.dim + 1⦌)))
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
            (𝟙 (unop (op ⦋x.dim + 1⦌))) :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
        (𝟙 (unop (op ⦋x.dim + 1⦌))) :
      Δ[x.dim + 1] _⦋x.dim + 1⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                (𝟙 (unop (op ⦋x.dim + 1⦌))) :
              Δ[x.dim + 1] _⦋x.dim + 1⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                (𝟙 (unop (op ⦋x.dim + 1⦌))) :
              Δ[x.dim + 1] _⦋x.dim + 1⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c

Tactic:
⟨x, Or.inl rfl⟩

Premises used: Exists.intro, Or.inl, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
x : f.Cell j
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋x.dim + 1⦌) (γ := Set (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
    ((f.sigmaStdSimplex j).nonDegenerate (x.dim + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
            (𝟙 (unop (op ⦋x.dim + 1⦌))) :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
hs : Mono (𝟙 (unop (op ⦋x.dim + 1⦌)))
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
            (𝟙 (unop (op ⦋x.dim + 1⦌))) :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
        (𝟙 (unop (op ⦋x.dim + 1⦌))) :
      Δ[x.dim + 1] _⦋x.dim + 1⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                (𝟙 (unop (op ⦋x.dim + 1⦌))) :
              Δ[x.dim + 1] _⦋x.dim + 1⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                (𝟙 (unop (op ⦋x.dim + 1⦌))) :
              Δ[x.dim + 1] _⦋x.dim + 1⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c

Tactic:
exact ⟨x, Or.inl rfl⟩