mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Point.Skyscraper

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
⊢ ∃ l,
    ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
      (ConcreteCategory.hom (Φ.fiber.map g)) y = x → s.π.app (op (R.arrows.categoryMk g hg)) ≫ Pi.π (fun t ↦ M) y = l

Tactic:
obtain ⟨Y₁, f₁, hf₁, y₁, hy₁⟩ := Φ.jointly_surjective _ hR x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasProducts A
M : A
X : C
R : Sieve X
hR : R ∈ J X
s : Cone (R.arrows.diagram.op ⋙ Φ.skyscraperPresheaf M)
x : Φ.fiber.obj X
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
⊢ ∃ l,
    ∀ ⦃Y : C⦄ (g : Y ⟶ X) (hg : R.arrows g) (y : Φ.fiber.obj Y),
      (ConcreteCategory.hom (Φ.fiber.map g)) y = x → s.π.app (op (R.arrows.categoryMk g hg)) ≫ Pi.π (fun t ↦ M) y = l
Module: Mathlib.CategoryTheory.Sites.Point.Conservative

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ∈ J X

Tactic:
hP.jointly_reflect_ofArrows_mem

Goal state after:
case refine_2.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : HasSheafify J (Type w)
inst✝¹ : J.WEqualsLocallyBijective (Type w)
hP : P.IsConservativeFamilyOfPoints
inst✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
X : C
ι : Type u_1
U : ι → C
f : (i : ι) → U i ⟶ X
hf : ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (f i))) y = x
ι' : Type (max w (max u v) (w + 1)) := (Φ : P.FullSubcategory) × Φ.obj.fiber.obj X
i : ι' → ι
y : (j : ι') → j.fst.obj.fiber.obj (U (i j))
hy : ∀ (j : ι'), (ConcreteCategory.hom (j.fst.obj.fiber.map (f (i j)))) (y j) = j.snd
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj X), ∃ i_1 y, (ConcreteCategory.hom (Φ.obj.fiber.map (f (i i_1)))) y = x
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : S.Etale
R : Sieve X
hR : R ∈ S.smallEtaleTopology X
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj X
⊢ ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f)) y = φ

Tactic:
cases X with | _ X f

Goal state after:
case mk
S : Scheme
Ω : Type u
inst✝¹ : Field Ω
inst✝ : IsSepClosed Ω
s : Spec (CommRingCat.of Ω) ⟶ S
X : Scheme
f : X ⟶ S
x✝ : Etale f
R : Sieve (Etale.mk f)
hR : R ∈ S.smallEtaleTopology (Etale.mk f)
φ : (Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).obj (Etale.mk f)
⊢ ∃ Y f_1,
    ∃ (_ : R.arrows f_1), ∃ y, (ConcreteCategory.hom ((Etale.forget S ⋙ coyoneda.obj (op (Over.mk s))).map f_1)) y = φ
Module: Mathlib.AlgebraicGeometry.Sites.EtalePoint

Goal state before:
pp: ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
this : X.hom x ∈ Set.univ
⊢ ∃ i, (s i) default = X.hom x

Tactic:
simp only [← hs, Functor.id_obj, Set.mem_iUnion, Set.mem_range] at this

Goal state after:
ι : Type u_1
S : Scheme
Ω : ι → Type u
inst✝¹ : (i : ι) → Field (Ω i)
inst✝ : ∀ (i : ι), IsSepClosed (Ω i)
s : (i : ι) → Spec (CommRingCat.of (Ω i)) ⟶ S
hs : ⋃ i, Set.range ⇑(s i) = Set.univ
X : S.Etale
α : Type (u + 1)
T : α → S.Etale
f : (i : α) → T i ⟶ X
hR :
  ∀ (Φ : (ObjectProperty.ofObj fun i ↦ pointSmallEtale (s i)).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : (Sieve.ofArrows T f).arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
x : ↥X.left
this : ∃ i y, (s i) y = X.hom x
⊢ ∃ i, (s i) default = X.hom x
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ max (Quotient.lift PadicSeq.norm ⋯ q) (Quotient.lift PadicSeq.norm ⋯ r) ≤
    Quotient.lift PadicSeq.norm ⋯ q + Quotient.lift PadicSeq.norm ⋯ r

Tactic:
apply max_le_add_of_nonneg
      · induction q using Quotient.inductionOn; apply PadicSeq.norm_nonneg
      · induction r using Quotient.inductionOn; apply PadicSeq.norm_nonneg

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ hσ' 0 0 1 ⋯ ≫ K[X].d 1 0 = 0

pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (q + 1) 0 1 ⋯ ≫ K[X].d 1 0 = 0

Tactic:
· rw [hσ'_eq (show 0 = 0 + 0 by rfl) (c_mk 1 0 rfl)]
    suffices X.σ 0 ≫ X.δ 0 + -X.σ 0 ≫ X.δ 1 = 0 by simpa
    rw [← Fin.succ_zero_eq_one, δ_comp_σ_succ, δ_comp_σ_self' X (Fin.castSucc_zero.symm)]
    simp

Goal state after:
case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (q + 1) 0 1 ⋯ ≫ K[X].d 1 0 = 0
Module: Mathlib.AlgebraicTopology.DoldKan.Homotopies

Goal state before:
pp: case succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ hσ' (q + 1) 0 1 ⋯ ≫ K[X].d 1 0 = 0

Tactic:
rw [hσ'_eq_zero (Nat.succ_pos q) (c_mk 1 0 rfl), zero_comp]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ DenseRange Rat.cast

Tactic:
intro x

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x ∈ closure (Set.range Rat.cast)
Module: Mathlib.AlgebraicTopology.DoldKan.Projections

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X x✝¹ x✝ : SimplicialObject C
f : x✝¹ ⟶ x✝
⊢ (alternatingFaceMapComplex C).map f ≫ P 0 = P 0 ≫ (alternatingFaceMapComplex C).map f

Tactic:
dsimp [alternatingFaceMapComplex]
      simp only [P_zero, id_comp, comp_id]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
⊢ f ≈ const norm q

Tactic:
intro ε hε

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f : CauSeq ℚ_[p] norm
cau_seq_norm_e : IsCauSeq ⇑padicNormE ↑f
q : ℚ_[p]
hq : ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (↑⟨↑f, cau_seq_norm_e⟩ i - q) < ε
ε : ℝ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, ‖↑(f - const norm q) j‖ < ε
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ↑p ^ (-x.valuation) * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
norm_eq_zpow_neg_valuation hy,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ↑p ^ (-x.valuation) * ↑p ^ (-y.valuation)
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation
Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K✝ K' : ChainComplex C ℕ
f : K✝ ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
K : ChainComplex C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h✝ : ¬Δ = Δ'
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
· by_cases Isδ₀ i
    · exact K.d Δ.len Δ'.len
    · exact 0

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.Degeneracies

Goal state before:
pp: case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)

Tactic:
intro x

Goal state after:
case zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : ⦋0⦌ ⟶ Δ'
hθ : ¬Function.Injective ⇑(SimplexCategory.Hom.toOrderHom θ)
x : Fin (⦋0⦌.len + 1)
⊢ ∀ ⦃a₂ : Fin (⦋0⦌.len + 1)⦄, (SimplexCategory.Hom.toOrderHom θ) x = (SimplexCategory.Hom.toOrderHom θ) a₂ → x = a₂
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
⊢ Compatibility.τ₀ = Compatibility.τ₁ isoN₁ isoΓ₀ N₁Γ₀

Tactic:
by
  ext K : 3
  simp only [Compatibility.τ₀_hom_app, Compatibility.τ₁_hom_app]
  exact (N₂Γ₂_compatible_with_N₁Γ₀ K).trans (by simp)

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂N₂ToKaroubiIso.inv.app X ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) = 𝟙 (Γ₂.obj (N₁.obj X))

Tactic:
Γ₂N₂ToKaroubiIso_inv_app,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : IsIdempotentComplete C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ Γ₂.map (toKaroubiCompN₂IsoN₁.inv.app X) ≫ Γ₂.map (toKaroubiCompN₂IsoN₁.hom.app X) = 𝟙 (Γ₂.obj (N₁.obj X))
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: F✝ : Type u_1
X : Type u
Y : Type v
Z : Type w
Z' : Type x
ι : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
x : ↑I × X
hx : ↑x.1 = 1 / 2
⊢ (F.extend (2 * ↑x.1)) x.2 = (G.extend (2 * ↑x.1 - 1)) x.2

Tactic:
by norm_num [hx]

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ ((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝ = (𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝

Tactic:
apply FundamentalGroupoid.ext

Goal state after:
case h_obj
A : TopCat
B : TopCat
X✝ : ↑(π.obj (TopCat.of (↑A × ↑B)))
⊢ (((projLeft A B).prod' (projRight A B) ⋙ prodToProdTop A B).obj X✝).as =
    ((𝟭 ↑(π.obj (TopCat.of (↑A × ↑B)))).obj X✝).as
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p₀ q₀ : Path x₀ x₁
p₁ q₁ : Path x₁ x₂
F : p₀.Homotopy q₀
G : p₁.Homotopy q₁
x : ↑I × ↑I
hx : ↑x.2 = 1 / 2
⊢ (F.eval x.1).extend (2 * ↑x.2) = (G.eval x.1).extend (2 * ↑x.2 - 1)

Tactic:
by norm_num [hx]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
this : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
have _ : IsFibrant Y' := isFibrant_of_fibration p

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
this : ∀ (Y : C) [IsFibrant Y], IsCofibrant Y → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsCofibrant Y
Y' : C
w✝ : IsCofibrant Y'
p : Y' ⟶ Y
left✝ : Fibration p
right✝ : WeakEquivalence p
x✝ : IsFibrant Y'
⊢ Function.Bijective (rightHomotopyClassToHom L)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this✝ : IsCofibrant P.P
this : IsIso (F.map (homMk P.ι))
⊢ F.map f = F.map g

Tactic:
simp only [show f = homMk h.h ≫ homMk P.p₀ by cat_disch,
      show g = homMk h.h ≫ homMk P.p₁ by cat_disch, Functor.map_comp]

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
H : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this✝ : IsCofibrant P.P
this : IsIso (F.map (homMk P.ι))
⊢ F.map (homMk h.h) ≫ F.map (homMk P.p₀) = F.map (homMk h.h) ≫ F.map (homMk P.p₁)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj X)) ≫
      adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj X)) =
    𝟙 (bifibrantResolution.obj (toHoCat.obj X))

Tactic:
obtain ⟨X, _, rfl⟩ := CofibrantObject.mk_surjective X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : C
w✝ : IsCofibrant X
⊢ bifibrantResolution.map (adjUnit.app (toHoCat.obj (mk X))) ≫
      adjCounitIso.hom.app (bifibrantResolution.obj (toHoCat.obj (mk X))) =
    𝟙 (bifibrantResolution.obj (toHoCat.obj (mk X)))
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : weakEquivalences (HoCat C) (toHoCat.map f)
⊢ IsIso (HoCat.bifibrantResolution.map (toHoCat.map f))

Tactic:
rw [← weakEquivalence_iff, weakEquivalence_toHoCat_map_iff] at hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ IsIso (HoCat.bifibrantResolution.map (toHoCat.map f))
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case mp.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
⊢ ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
intro x

Goal state after:
case mp.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
x : c.pt
⊢ ∃ i a, c.ι (WalkingMultispan.right i) a = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: m : SimplexCategoryᵒᵖ
x : Δ[0].obj m
⊢ Function.Surjective ⇑(stdSimplex.asOrderHom x)

Tactic:
intro x

Goal state after:
m : SimplexCategoryᵒᵖ
x✝ : Δ[0].obj m
x : Fin 1
⊢ ∃ a, (stdSimplex.asOrderHom x✝) a = x
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : Type u''
inst✝¹ : Category.{v'', u''} J
inst✝ : HasPushouts C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (epimorphisms C).functorCategory J f ↔ epimorphisms (J ⥤ C) f

Tactic:
simp only [functorCategory, epimorphisms.iff, NatTrans.epi_iff_epi_app]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ Subfunctor.lift (stdSimplex.δ j) ⋯ ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
Subfunctor.lift_ι

Goal state after:
n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ stdSimplex.δ j = stdSimplex.δ j
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ : c₁.pt
⊢ ∀ ⦃a₂ : c₁.pt⦄, (hom φ) x₁ = (hom φ) a₂ → x₁ = a₂

Tactic:
y₁

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ y₁ : c₁.pt
⊢ (hom φ) x₁ = (hom φ) y₁ → x₁ = y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: ⊢ I ≤ monomorphisms SSet

Tactic:
by
  rintro _ _ _ ⟨n⟩
  exact monomorphisms.infer_property _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
d n : ℕ
h : d < n
⊢ ⊤ ⊆ (X.skeleton n).obj (op ⦋d⦌)

Tactic:
intro x

Goal state after:
X : SSet
d n : ℕ
h : d < n
x : X _⦋d⦌
⊢ x ∈ ⊤ → x ∈ (X.skeleton n).obj (op ⦋d⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case a.right
X : SSet
n : ℕ
⊢ ∀ (i : ↑(X.nonDegenerate n)), Subcomplex.ofSimplex ↑i ≤ X.skeleton (n + 1)

Tactic:
intro x

Goal state after:
case a.right
X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
⊢ Subcomplex.ofSimplex ↑x ≤ X.skeleton (n + 1)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯)
      (𝟙 (homEquiv h) ≫ Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
2,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((((ρ_ (X ⟶[V] Y)).inv ≫ (X ⟶[V] Y) ◁ (eHomEquiv V) α.hom ≫ eComp V X Y Y₁) ≫
          (ρ_ (X ⟶[V] Y₁)).inv ≫ (X ⟶[V] Y₁) ◁ (eHomEquiv V) α.inv ≫ eComp V X Y₁ Y) ▷
        Y ⟶[V] Z) ≫
      eComp V X Y Z =
    eComp V X Y Z

Tactic:
change (eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ _ ≫ _ = _

Goal state after:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Y₁ Z : C
α : Y ≅ Y₁
⊢ ((eHomWhiskerLeft V X α.hom ≫ eHomWhiskerLeft V X α.inv) ▷ Y ⟶[V] Z) ≫ eComp V X Y Z = eComp V X Y Z
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom ⋯ = G.map X Y
⊢ F = G

Tactic:
by
  match F, G with
  | mk F_obj F_map _ _, mk G_obj G_map _ _ =>
    obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
    congr
    ext X Y
    simpa using h_map X Y

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
x y : ↑((nerveFunctor₂ ⋙ oneTruncation₂).obj X✝)
f : x ⟶ y
⊢ ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).map f =
    Eq.recOn ⋯ (Eq.recOn ⋯ (((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).map f))

Tactic:
obtain ⟨f, rfl, rfl⟩ := f

Goal state after:
X✝ Y✝ : Cat
F : X✝ ⟶ Y✝
f : (nerveFunctor₂.obj X✝).obj (op { obj := ⦋1⦌, property := Truncated.Edge._proof_2 })
⊢ ((nerveFunctor₂ ⋙ oneTruncation₂).map F ≫ (ofNerve₂ ↑Y✝).hom).map { edge := f, src_eq := ⋯, tgt_eq := ⋯ } =
    Eq.recOn ⋯ (Eq.recOn ⋯ (((ofNerve₂ ↑X✝).hom ≫ ReflQuiv.forget.map F).map { edge := f, src_eq := ⋯, tgt_eq := ⋯ }))
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Z Y : C
f : X ⟶ Z
g : Z ⟶ Y
hfg : r.degHom (f ≫ g) < r.deg Z
⊢ r.degHom f < r.deg Z ∨ r.degHom g < r.deg Z

Tactic:
contrapose! hfg
  let φ := MorphismProperty.MapFactorizationData.mk Z f g rfl
    (r.prop₁_of_degHom_eq_deg_right (le_antisymm (r.degHom_le_deg_right f) hfg.left))
    (r.prop₂_of_degHom_eq_deg_left (le_antisymm (r.degHom_le_deg_left g) hfg.right))
  rw [r.degHom_eq φ]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
⊢ generators.multiplicativeClosure f

Tactic:
induction f using CategoryTheory.Quotient.induction with | _ f

Goal state after:
case h
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
f : x✝ ⟶ y✝
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : SimplexCategoryGenRel → Sort u_1
H : (n : ℕ) → P (mk n)
⊢ (x : SimplexCategoryGenRel) → P x

Tactic:
intro x

Goal state after:
P : SimplexCategoryGenRel → Sort u_1
H : (n : ℕ) → P (mk n)
x : SimplexCategoryGenRel
⊢ P x
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + t.length + 1 + L₁.length = m₁
h' : m₃ + (t.length + 1) = m₃ + t.length + 1
⊢ standardσ L₁ h ≫ standardσ t ⋯ ≫ σ ↑a = standardσ (t ++ L₁) ⋯ ≫ σ ↑a

Tactic:
simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
      (by grind) (by grind))]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst✝ : Mono f
⊢ toSimplexCategory.map (homOfMono f) = f

Tactic:
by
  aesop

Goal state after: