awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (hypothesis)
Goal:
X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h' :
  mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯ ≤
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯
f :
  ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌ ⟶
    ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯).dim⦌
hf : Mono f
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
        (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₂, hx₂⟩ : X _⦋n₁⦌) ⋯).dim⦌)) →
          (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₁, hx₁⟩ : X _⦋n₁⦌) ⋯).dim⦌))
      (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯).simplex =
    (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).simplex
hf₁ : Mono (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯).dim⦌)
⊢ mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) ⋯ =
    mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) ⋯
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun)
        (X.map
          (Quiver.Hom.op
            (𝟙 ⦋(mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).dim⦌))) :
      (a : (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₂, hx₂⟩ : X _⦋n₁⦌) sorry).dim⦌)) →
        (fun (X : Type u) ↦ X) (X _⦋(mk (↑⟨x₁, hx₁⟩ : X _⦋n₁⦌) sorry).dim⦌))
    (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₂ hx₂) : X _⦋n₁⦌) sorry).simplex =
  (mk (↑(Subtype.mk (p := fun (x : X _⦋n₁⦌) ↦ x ∈ X.nonDegenerate n₁) x₁ hx₁) : X _⦋n₁⦌) sorry).simplex
Tactic: obtain rfl := SimplexCategory.eq_id_of_mono f
Cleared hypotheses: f, hf, h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ x = y
have a : x ≤ y
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
a : x ≤ y
⊢ x = y
have a₁ : y ≤ x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ x ≤ y
have a : x.subcomplex ≤ y.subcomplex
Tactic: rw [le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
a : x.subcomplex ≤ y.subcomplex
⊢ x ≤ y
have a₁ : y.subcomplex ≤ y.subcomplex
Tactic: rw [le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
⊢ y ≤ x
have a : y.subcomplex ≤ x.subcomplex
Tactic: rw [le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.N
h : x.subcomplex = y.subcomplex
a : y.subcomplex ≤ x.subcomplex
⊢ y ≤ x
have a₁ : y.subcomplex ≤ y.subcomplex
Tactic: rw [le_iff, h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ Membership.mem (γ := Set (X _⦋(s.cast hd).dim⦌)) (X.nonDegenerate (s.cast hd).dim) (s.cast hd).simplex
have subst : Membership.mem (γ := Set (X _⦋(s.cast sorry).dim⦌)) (X.nonDegenerate (s.cast sorry).dim) (s.cast sorry).simplex
Tactic: subst hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
s : X.N
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s
have subst : s.cast sorry = s
Tactic: subst hd
Cleared hypotheses: d, hd
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
⊢ LE.le.{u} (α := X.Subcomplex) ⊤ (⨆ (s : X.N), s.subcomplex)
have rw : ∀ (i : (p : ℕ) × (↑(X.nonDegenerate p) : Type u)),
  Subcomplex.ofSimplex (↑(i.snd (β := fun (p : ℕ) ↦ (↑(X.nonDegenerate p) : Type u))) : X _⦋i.fst⦌) ≤
    ⨆ (s : X.N), s.subcomplex
Tactic: rw [← Subcomplex.iSup_ofSimplex_nonDegenerate_eq_top X, iSup_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
A B : X.Subcomplex
⊢ A ≤ B ↔ ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
have rw : (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)) ↔
  ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
Tactic: rw [Subcomplex.le_iff_contains_nonDegenerate]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
A B : X.Subcomplex
⊢ (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
have refine_1 : ∀
  (h :
    ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌))
  (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
Tactic: refine ⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
A B : X.Subcomplex
refine_1 :
  ∀
    (h :
      ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
        Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
          Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌))
    (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
⊢ (∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
      Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
        Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)) ↔
    ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B
have refine_2 : ∀ (h : ∀ (s : X.N), s.subcomplex ≤ A → s.subcomplex ≤ B) (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u))
  (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)),
  Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
Tactic: refine ⟨fun h s ↦ ?_, fun h n x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
n : ℕ
x : (↑(X.nonDegenerate n) : Type u)
hx : (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ A
⊢ (mk (↑x : X _⦋n⦌) ⋯).subcomplex ≤ B
have refine_1 : ∀ (hx : Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)),
  Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
Tactic: simp only [Subfunctor.ofSection_le_iff, mk_dim, mk_simplex] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
A B : X.Subcomplex
h :
  ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
    Membership.mem (γ := Set (X _⦋n⦌)) (A.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌) →
      Membership.mem (γ := Set (X _⦋n⦌)) (B.obj (Opposite.op ⦋n⦌)) (↑x : X _⦋n⦌)
s : X.N
⊢ s.subcomplex ≤ A → s.subcomplex ≤ B
have refine_1 : ∀ (n : ℕ) (x : (↑(X.nonDegenerate n) : Type u)),
  (mk (↑x : X _⦋n⦌) sorry).subcomplex ≤ A → (mk (↑x : X _⦋n⦌) sorry).subcomplex ≤ B
Tactic: induction s using N.induction with
    | mk n x =>
      intro hx
      simp only [Subfunctor.ofSection_le_iff, mk_dim, mk_simplex] at hx ⊢
      exact h _ _ hx
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.op.N
⊢ LE.le (α := X.N)
      (({ toFun := fun (x : X.op.N) ↦ mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯,
              invFun := fun (y : X.N) ↦ mk ((Equiv.symm opObjEquiv : (a : X _⦋y.dim⦌) → X.op _⦋y.dim⦌) y.simplex) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.op.N) → X.N)
          x :
        X.N)
      (({ toFun := fun (x : X.op.N) ↦ mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯,
              invFun := fun (y : X.N) ↦ mk ((Equiv.symm opObjEquiv : (a : X _⦋y.dim⦌) → X.op _⦋y.dim⦌) y.simplex) ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.op.N) → X.N)
          y :
        X.N) ↔
    x ≤ y
have dsimp : mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry ≤
    mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry ↔
  x ≤ y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.op.N
⊢ mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯ ≤
      mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯ ↔
    x ≤ y
have simp : (∃ (f :
    ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).dim⦌ ⟶
      ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).dim⦌) →
            X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).dim⦌)
        (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).simplex =
      (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).simplex) ↔
  ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
      x.simplex
Tactic: simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.op.N
⊢ (∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex
have mp : (∃ (f :
    ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).dim⦌ ⟶
      ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).dim⦌) →
            X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).dim⦌)
        (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).simplex =
      (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).simplex) →
  ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
      x.simplex
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X : SSet
x y : X.op.N
mp :
  (∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex) →
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex
⊢ (∃ (f :
      ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌ ⟶
        ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
            (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).dim⦌) →
              X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).dim⦌)
          (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) ⋯).simplex =
        (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
        x.simplex
have mpr : (∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.op.map f.op) : (a : X.op _⦋y.dim⦌) → X.op _⦋x.dim⦌) y.simplex =
      x.simplex) →
  ∃ (f :
    ⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).dim⦌ ⟶
      ⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) :
          (a : X _⦋(mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).dim⦌) →
            X _⦋(mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).dim⦌)
        (mk ((opObjEquiv : (a : X.op _⦋y.dim⦌) → X _⦋y.dim⦌) y.simplex) sorry).simplex =
      (mk ((opObjEquiv : (a : X.op _⦋x.dim⦌) → X _⦋x.dim⦌) x.simplex) sorry).simplex
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
⊢ LE.le (α := Y.N)
      (({
              toFun := fun (x : X.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
                    x.simplex)
                  ⋯,
              invFun := fun (y : Y.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋y.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
                    y.simplex)
                  ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.N) → Y.N)
          x :
        Y.N)
      (({
              toFun := fun (x : X.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (X _⦋x.dim⦌)) → (fun (X : Type u) ↦ X) (Y _⦋x.dim⦌))
                    x.simplex)
                  ⋯,
              invFun := fun (y : Y.N) ↦
                mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.inv.app (Opposite.op ⦋y.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) (Y _⦋y.dim⦌)) → (fun (X : Type u) ↦ X) (X _⦋y.dim⦌))
                    y.simplex)
                  ⋯,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : X.N) → Y.N)
          y :
        Y.N) ↔
    x ≤ y
have dsimp : mk
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
        x.simplex)
      sorry ≤
    mk
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
        y.simplex)
      sorry ↔
  x ≤ y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
⊢ mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
          x.simplex)
        ⋯ ≤
      mk
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
          y.simplex)
        ⋯ ↔
    x ≤ y
have simp : (∃ (f :
    ⦋(mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
              x.simplex)
            sorry).dim⦌ ⟶
      ⦋(mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex)
            sorry).dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
          (a :
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌) y.simplex)
                    sorry).dim⦌) →
            Y _⦋(mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                  sorry).dim⦌)
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex)
            sorry).simplex =
      (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
            x.simplex)
          sorry).simplex) ↔
  ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
Tactic: simp only [le_iff, Subcomplex.ofSimplex_le_iff, Subcomplex.mem_ofSimplex_obj_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
⊢ (∃ (f :
      ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                  (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
                x.simplex)
              ⋯).dim⦌ ⟶
        ⦋(mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
            (a :
                Y _⦋(mk
                      ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                        y.simplex)
                      ⋯).dim⦌) →
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                    ⋯).dim⦌)
          (mk
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                  (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
                y.simplex)
              ⋯).simplex =
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
              x.simplex)
            ⋯).simplex) ↔
    ∃ (f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌),
      (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
have refine : ∀
  (f :
    ⦋(mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) :
                (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
              x.simplex)
            sorry).dim⦌ ⟶
      ⦋(mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex)
            sorry).dim⦌),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
          (a :
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌) y.simplex)
                    sorry).dim⦌) →
            Y _⦋(mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                  sorry).dim⦌)
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex)
            sorry).simplex =
      (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
            x.simplex)
          sorry).simplex ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
Tactic: refine exists_congr (fun f ↦ ?_)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices (goal)
Goal:
X Y : SSet
e : X ≅ Y
x y : X.N
f :
  ⦋(mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
            x.simplex)
          ⋯).dim⦌ ⟶
    ⦋(mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
            y.simplex)
          ⋯).dim⦌
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) :
          (a :
              Y _⦋(mk
                    ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌) y.simplex)
                    ⋯).dim⦌) →
            Y _⦋(mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌) x.simplex)
                  ⋯).dim⦌)
        (mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) :
                (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
              y.simplex)
            ⋯).simplex =
      (mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
            x.simplex)
          ⋯).simplex ↔
    (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
have dsimp : Eq (α := Y _⦋x.dim⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f.op) : (a : Y _⦋y.dim⦌) → Y _⦋x.dim⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋y.dim⦌)) : (a : X _⦋y.dim⦌) → Y _⦋y.dim⦌)
            y.simplex :
          Y _⦋y.dim⦌) :
      Y _⦋x.dim⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (e.hom.app (Opposite.op ⦋x.dim⦌)) : (a : X _⦋x.dim⦌) → Y _⦋x.dim⦌)
        x.simplex :
      Y _⦋x.dim⦌) ↔
  (ConcreteCategory.hom (FC := TypeCat.Fun) (X.map f.op) : (a : X _⦋y.dim⦌) → X _⦋x.dim⦌) y.simplex = x.simplex
Tactic: dsimp at f ⊢