awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left : { dim := d + 1, simplex := y : X.S }.dim = { dim := d, simplex := x : X.S }.dim + 1
f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
    (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
          Mono f ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                    (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                { dim := d + 1, simplex := y : X.S }.simplex =
              { dim := d, simplex := x : X.S }.simplex)
        y_1 →
      y_1 = f
left_1 : Mono f
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
mp :
  ∀ (i : Fin ({ dim := d, simplex := x : X.S }.dim + 2))
    (h₂ :
      ∀ (y_1 : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
        (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
              Mono f ∧
                (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                        (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                    { dim := d + 1, simplex := y : X.S }.simplex =
                  { dim := d, simplex := x : X.S }.simplex)
            y_1 →
          y_1 = SimplexCategory.δ i),
    Mono (SimplexCategory.δ i) →
      ∀
        (h₁ :
          (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ i).op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                  (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
              { dim := d + 1, simplex := y : X.S }.simplex =
            { dim := d, simplex := x : X.S }.simplex),
        ∃! i : Fin (d + 2),
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x
⊢ ∃! i : Fin (d + 2),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        y =
      x

Tactic:
obtain ⟨i, rfl⟩ := SimplexCategory.eq_δ_of_mono f

Premises used: SimplexCategory.eq_δ_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left : { dim := d + 1, simplex := y : X.S }.dim = { dim := d, simplex := x : X.S }.dim + 1
i : Fin ({ dim := d, simplex := x : X.S }.dim + 2)
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
    (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
          Mono f ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                    (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                { dim := d + 1, simplex := y : X.S }.simplex =
              { dim := d, simplex := x : X.S }.simplex)
        y_1 →
      y_1 = SimplexCategory.δ i
left_1 : Mono (SimplexCategory.δ i)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ i).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
⊢ ∃! i : Fin (d + 2),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        y =
      x

Tactic:
⟨i, h₁, fun j hj ↦ SimplexCategory.δ_injective (h₂ _ ⟨inferInstance, hj⟩)⟩

Premises used: inferInstance, SimplexCategory.δ, SimplexCategory.δ_injective, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
left : { dim := d + 1, simplex := y : X.S }.dim = { dim := d, simplex := x : X.S }.dim + 1
i : Fin ({ dim := d, simplex := x : X.S }.dim + 2)
h₂ :
  ∀ (y_1 : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
    (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
          Mono f ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                    (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                { dim := d + 1, simplex := y : X.S }.simplex =
              { dim := d, simplex := x : X.S }.simplex)
        y_1 →
      y_1 = SimplexCategory.δ i
left_1 : Mono (SimplexCategory.δ i)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ i).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
⊢ ∃! i : Fin (d + 2),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        y =
      x

Tactic:
exact ⟨i, h₁, fun j hj ↦ SimplexCategory.δ_injective (h₂ _ ⟨inferInstance, hj⟩)⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      y =
    x
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (i : Fin (d + 2)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x)
        y_1 →
      y_1 = i
⊢ { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩

Premises used: inferInstance, SimplexCategory.δ, _private.0.SSet.S.IsUniquelyCodimOneFace.iff.match_1, And.intro, Exists.intro, Eq, SSet.S.IsUniquelyCodimOneFace, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      y =
    x
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (i : Fin (d + 2)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x)
        y_1 →
      y_1 = i
mpr :
  ∀ (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌),
    (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
          Mono f ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                  (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                    (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
                { dim := d + 1, simplex := y : X.S }.simplex =
              { dim := d, simplex := x : X.S }.simplex)
        f →
      ∀ (h₃ : Mono f)
        (h₄ :
          (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                  (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
              { dim := d + 1, simplex := y : X.S }.simplex =
            { dim := d, simplex := x : X.S }.simplex),
        f = SimplexCategory.δ i
⊢ { dim := d, simplex := x : X.S }.IsUniquelyCodimOneFace { dim := d + 1, simplex := y }

Tactic:
refine ⟨rfl, SimplexCategory.δ i, ⟨inferInstance, h₁⟩, fun f ⟨h₃, h₄⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      y =
    x
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (i : Fin (d + 2)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x)
        y_1 →
      y_1 = i
f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌
h :
  (fun (f : ⦋{ dim := d, simplex := x : X.S }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y : X.S }.dim⦌) ↦
      Mono f ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d + 1, simplex := y : X.S }.simplex =
          { dim := d, simplex := x : X.S }.simplex)
    f
h₃ : Mono f
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
mpr :
  ∀ (j : Fin ({ dim := d, simplex := x : X.S }.dim + 2)),
    Mono (SimplexCategory.δ j) ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
              (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
            { dim := d + 1, simplex := y : X.S }.simplex =
          { dim := d, simplex := x : X.S }.simplex →
      ∀ (h₃ : Mono (SimplexCategory.δ j))
        (h₄ :
          (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
                (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
                  (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
              { dim := d + 1, simplex := y : X.S }.simplex =
            { dim := d, simplex := x : X.S }.simplex),
        SimplexCategory.δ j = SimplexCategory.δ i
⊢ f = SimplexCategory.δ i

Tactic:
obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f

Premises used: SimplexCategory.eq_δ_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      y =
    x
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (i : Fin (d + 2)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x)
        y_1 →
      y_1 = i
j : Fin ({ dim := d, simplex := x : X.S }.dim + 2)
h :
  Mono (SimplexCategory.δ j) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex =
      { dim := d, simplex := x : X.S }.simplex
h₃ : Mono (SimplexCategory.δ j)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
⊢ j = i

Tactic:
h₂ _ h₄
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      y =
    x
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (i : Fin (d + 2)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x)
        y_1 →
      y_1 = i
j : Fin ({ dim := d, simplex := x : X.S }.dim + 2)
h :
  Mono (SimplexCategory.δ j) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex =
      { dim := d, simplex := x : X.S }.simplex
h₃ : Mono (SimplexCategory.δ j)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
mpr :
  ∀
    (h₁ :
      (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
            (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
          y =
        x)
    (h₂ :
      ∀ (y_1 : Fin (d + 2)),
        (fun (i : Fin (d + 2)) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                    (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
                  y =
                x)
            y_1 →
          y_1 = j),
    SimplexCategory.δ j = SimplexCategory.δ j
⊢ SimplexCategory.δ j = SimplexCategory.δ i

Tactic:
obtain rfl : j = i := h₂ _ h₄

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
j : Fin ({ dim := d, simplex := x : X.S }.dim + 2)
h :
  Mono (SimplexCategory.δ j) ∧
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
          (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
        { dim := d + 1, simplex := y : X.S }.simplex =
      { dim := d, simplex := x : X.S }.simplex
h₃ : Mono (SimplexCategory.δ j)
h₄ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (SimplexCategory.δ j).op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋{ dim := d + 1, simplex := y }.dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋{ dim := d, simplex := x }.dim⦌))
      { dim := d + 1, simplex := y : X.S }.simplex =
    { dim := d, simplex := x : X.S }.simplex
h₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      y =
    x
h₂ :
  ∀ (y_1 : Fin (d + 2)),
    (fun (i : Fin (d + 2)) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
                (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
              y =
            x)
        y_1 →
      y_1 = j
⊢ SimplexCategory.δ j = SimplexCategory.δ j

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ y.dim = x.dim + 1

Tactic:
hxy.1

Premises used: And.left
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
rw : x.dim + 1 = d + 1
rw₁ rw₂ : d + 1 = d + 1
⊢ y.dim = d + 1

Tactic:
rw [hxy.dim_eq, hd]

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (x.cast hd).IsUniquelyCodimOneFace (y.cast ⋯)

Tactic:
simpa only [cast_eq_self]

Premises used: SSet.S.cast_eq_self
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
rw : x.dim + 1 = d + 1
rw₁ rw₂ : d + 1 = d + 1
⊢ y.dim = d + 1

Tactic:
rw [hxy.dim_eq, hd]

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ ∃! i : Fin (d + 2),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X i) :
          (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
        (y.cast ⋯).simplex =
      (x.cast hd).simplex

Tactic:
simpa only [S.cast, iff] using hxy.cast hd

Premises used: SSet.S.cast, SSet.S.IsUniquelyCodimOneFace.cast, SSet.S.IsUniquelyCodimOneFace.iff
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index hd)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex

Tactic:
(hxy.existsUnique_δ_cast_simplex hd).exists.choose_spec

Premises used: Exists.choose_spec, ExistsUnique.exists, SSet.S.IsUniquelyCodimOneFace.index, SSet.S.IsUniquelyCodimOneFace.existsUnique_δ_cast_simplex
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index hd)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex

Tactic:
apply δ_index

Premises used: SSet.S.IsUniquelyCodimOneFace.δ_index
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋x.dim + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋x.dim⦌))
      (y.cast ⋯).simplex =
    (x.cast ⋯).simplex

Tactic:
have := hxy.δ_index rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
      (y.cast ⋯).simplex =
    x.simplex
rw :
  Membership.mem (α := X _⦋x.dim⦌) (γ := Set (X _⦋x.dim⦌)) ((y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
        (y.cast ⋯).simplex :
      X _⦋x.dim⦌)
⊢ x ≤ y

Tactic:
rw [S.le_def, ← y.subcomplex_cast hxy.dim_eq, Subfunctor.ofSection_le_iff,
    ← this]

Premises used: SSet.S.subcomplex_cast, SSet.S.IsUniquelyCodimOneFace.dim_eq, CategoryTheory.Subfunctor.ofSection_le_iff, SSet.S.le_def
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
      (y.cast ⋯).simplex =
    x.simplex
⊢ Membership.mem (α := X _⦋x.dim⦌) (γ := Set (X _⦋x.dim⦌)) ((y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
        (y.cast ⋯).simplex :
      X _⦋x.dim⦌)

Tactic:
⟨(SimplexCategory.δ _).op, rfl⟩

Premises used: Set.Mem, Quiver.Hom.op, setOf, SimplexCategory.δ, Exists.intro, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
this :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
      (y.cast ⋯).simplex =
    x.simplex
⊢ Membership.mem (α := X _⦋x.dim⦌) (γ := Set (X _⦋x.dim⦌)) ((y.cast ⋯).subcomplex.obj (Opposite.op ⦋x.dim⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X (hxy.index ⋯)) : (a : X _⦋x.dim + 1⦌) → X _⦋x.dim⦌)
        (y.cast ⋯).simplex :
      X _⦋x.dim⦌)

Tactic:
exact ⟨(SimplexCategory.δ _).op, rfl⟩
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
rw : x.dim + 1 = d + 1
rw₁ rw₂ : d + 1 = d + 1
⊢ y.dim = d + 1

Tactic:
rw [hxy.dim_eq, hd]

Premises used: SSet.S.IsUniquelyCodimOneFace.dim_eq
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex
dsimp : Mono f
⊢ Mono f

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex
⊢ Mono f

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex
dsimp : Mono (SimplexCategory.δ (hxy.index hd))
⊢ Mono (SimplexCategory.δ (hxy.index hd))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
Goal:
X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst : Mono f
hf :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋d + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋d⦌))
      (y.cast ⋯).simplex =
    (x.cast hd).simplex
⊢ Mono (SimplexCategory.δ (hxy.index hd))

Tactic:
infer_instance