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

Goal state before:
pp: case refine_2.refine_1
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')) ≤ Sieve.ofArrows U f

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:
· rw [Sieve.generate_le_iff, Presieve.ofArrows_le_iff]
      exact fun _ ↦ Sieve.ofArrows_mk _ _ _

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
⊢ (Sieve.ofArrows (fun i' ↦ U (i i')) fun i' ↦ f (i i')) ∈ J X
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
⊢ f.norm = g.norm

Tactic:
have hg : g ≈ 0 := equiv_zero_of_val_eq_of_equiv_zero h hf

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
h : ∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)
hf : f ≈ 0
hg : g ≈ 0
⊢ f.norm = g.norm
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case inr
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
⊢ (q' - const (padicNorm p) (↑q' N)).norm < ε

Tactic:
simp only [PadicSeq.norm, dif_neg hne']
        change padicNorm p (q' _ - q' _) < ε
        rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
        · have := (stationaryPoint_spec hne' le_rfl hle).symm
          simp only [const_apply, CauSeq.sub_apply, padicNorm.zero, sub_self] at this
          simpa only [this]
        · exact hN _ (lt_of_not_ge hle).le _ le_rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * 1 < 1

Tactic:
by
        rw [mul_one, norm_p]
        exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e : Y ⟶ X _⦋n + 1⦌
⊢ ∀ (f : Y ⟶ X _⦋n + 1⦌), b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f

Tactic:
f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y : C
n a✝ q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
hnaq : n = a✝ + q
hnaq_shift : ∀ (d : ℕ), n + d = a✝ + d + q
a b c d e f : Y ⟶ X _⦋n + 1⦌
⊢ b = f → d + e = 0 → c + a = 0 → a + b + (c + d + e) = f
Module: Mathlib.AlgebraicTopology.DoldKan.PInfty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + QInfty = 𝟙 K[X]

Tactic:
by
  dsimp only [QInfty]
  simp only [add_sub_cancel]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q : ℚ
⊢ (↑q).valuation = padicValRat p q

Tactic:
by
  rcases eq_or_ne q 0 with rfl | hq
  · simp only [Rat.cast_zero, valuation_zero, padicValRat.zero]
  refine neg_injective ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective
    <| (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_)
  rw [eq_padicNorm, ← Rat.cast_natCast, ← Rat.cast_zpow, Rat.cast_inj]
  exact padicNorm.eq_zpow_of_nonzero hq

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hxy : x + y ≠ 0
⊢ min x.valuation y.valuation ≤ (x + y).valuation

Tactic:
by
  by_cases hx : x = 0
  · simpa only [hx, zero_add] using min_le_right _ _
  by_cases hy : y = 0
  · simpa only [hy, add_zero] using min_le_left _ _
  have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := nonarchimedean x y
  simpa only [norm_eq_zpow_neg_valuation hxy, norm_eq_zpow_neg_valuation hx,
    norm_eq_zpow_neg_valuation hy, le_max_iff,
    zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt : 1 < (p : ℝ)), neg_le_neg_iff, ← min_le_iff]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ x⁻¹.valuation = -x.valuation

Tactic:
by
  obtain rfl | hx := eq_or_ne x 0
  · simp
  have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x
  have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
  have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
  rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx,
    ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P (q + 1) = P q + P q ≫ Hσ q

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] + P q ≫ 0 = 𝟙 K[X]

Tactic:
· simp only [P_succ, comp_add, comp_id]

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ 𝟙 K[X] + P q ≫ 0 = 𝟙 K[X]
Module: Mathlib.AlgebraicTopology.DoldKan.Normalized

Goal state before:
pp: A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (NormalizedMooreComplex.objX X (n + 1)).factorThru (PInfty.f (n + 1)) ⋯ ≫ N[X].d (n + 1) n =
    K[X].d (n + 1) n ≫ (NormalizedMooreComplex.objX X n).factorThru (PInfty.f n) ⋯

Tactic:
rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow,
      ← inclusionOfMooreComplexMap_f, NormalizedMooreComplex.obj_d, ChainComplex.of_d,
      ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
      inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, alternatingFaceMapComplex_obj_d,
      ← alternatingFaceMapComplex_obj_d]
    exact PInfty.comm (n + 1) n

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

Goal state before:
pp: case h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ i)

Tactic:
simpa only [Isδ₀.iff] using hi

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
⊢ IsIso Γ₂N₁.natTrans

Tactic:
by
  have : ∀ X : SimplicialObject C, IsIso (Γ₂N₁.natTrans.app X) := by
    intro X
    rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]
    infer_instance
  apply NatIso.isIso_of_isIso_app

Goal state after:
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ (listToPath (pathToList a✝¹)).cons a✝ = a✝¹.cons a✝

Tactic:
ih

Goal state after:
case cons
α : Type u_1
x b✝ c✝ : SingleObj α
a✝¹ : Path (star α) b✝
a✝ : b✝ ⟶ c✝
ih : listToPath (pathToList a✝¹) = a✝¹
⊢ a✝¹.cons a✝ = a✝¹.cons a✝
Module: Mathlib.Combinatorics.Quiver.SingleObj

Goal state before:
pp: case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l

Tactic:
ih

Goal state after:
case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: l = a :: l
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
⊢ ∀ (f : X✝ ⟶ Y✝),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
      CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯

Tactic:
f

Goal state after:
case h_map
I : Type u
X : I → TopCat
X✝ Y✝ : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
f : X✝ ⟶ Y✝
⊢ (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
    CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : { as := x } ⟶ { as := y }
⊢ (map f).map p ≫ ⟦H.evalAt { as := y }.as⟧ = ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map p

Tactic:
rcases Path.Homotopic.Quotient.mk_surjective p with ⟨p, rfl⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
H : f.Homotopy g
x y : X
p : Path { as := x }.as { as := y }.as
⊢ (map f).map (Path.Homotopic.Quotient.mk p) ≫ ⟦H.evalAt { as := y }.as⟧ =
    ⟦H.evalAt { as := x }.as⟧ ≫ (map g).map (Path.Homotopic.Quotient.mk p)
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
dsimp [toHoCat]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (Quotient.functor (homRel C)).Full
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : CofibrantObject C
inst✝ : IsFibrant Y.obj
f g : X ⟶ Y
⊢ toHoCat.map f = toHoCat.map g ↔ homRel C f g

Tactic:
dsimp [toHoCat]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X Y : CofibrantObject C
inst✝ : IsFibrant Y.obj
f g : X ⟶ Y
⊢ (Quotient.functor (homRel C)).map f = (Quotient.functor (homRel C)).map g ↔ homRel C f g
Module: Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : ModelCategory C
D : Type u_2
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝ : L.IsLocalization (weakEquivalences C)
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (resolution ⋙ toLocalization L).map f ≫ L.map (pResolutionObj x✝) = L.map (pResolutionObj x✝¹) ≫ L.map f

Tactic:
by
    simpa only [Functor.map_comp] using! L.congr_map (HoCat.resolutionMap_fac f)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ toHoCat.Full

Tactic:
dsimp [toHoCat]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ (Quotient.functor (homRel C)).Full
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K L : BifibrantObject C
⊢ ∀ (f g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g

Tactic:
f

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K L : BifibrantObject C
f : K ⟶ L
⊢ ∀ (g : K ⟶ L), homRel C f g → toHoCat.map f = toHoCat.map g
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₁ f₂ : X ⟶ Y), homRel C f₁ f₂ → bifibrantResolution'.map f₁ = bifibrantResolution'.map f₂

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f : X ⟶ Y
⊢ ∀ (f₂ : X ⟶ Y), homRel C f f₂ → bifibrantResolution'.map f = bifibrantResolution'.map f₂
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
this : WeakEquivalence (h.p ≫ pullback.snd p g)
⊢ sq'.lift ≫ h.p ≫ pullback.fst p g ≫ p = g

Tactic:
pullback.condition,

Goal state after:
C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
this : WeakEquivalence (h.p ≫ pullback.snd p g)
⊢ sq'.lift ≫ h.p ≫ pullback.snd p g ≫ g = g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

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

Tactic:
f

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : HoCat C
f : X ⟶ Y
⊢ weakEquivalences (HoCat C) f → IsIso (HoCat.bifibrantResolution.map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.MultiequalizerPullback

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
J : MultispanShape
inst✝ : Unique J.L
I : MultispanIndex J C
h : {J.fst default, J.snd default} = Set.univ
h' : J.fst default ≠ J.snd default
s : PushoutCocone (I.fst default) (I.snd default)
⊢ (if hk : J.fst default = J.fst default then eqToHom ⋯ ≫ s.inl else eqToHom ⋯ ≫ s.inr) = s.inl

Tactic:
rw [dif_pos rfl, eqToHom_refl, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := ⋯
⊢ Nonempty (IsColimit (c.multicofork.map Set.functorToTypes))

Tactic:
rw [Types.isColimit_iff_coconeTypesIsColimit,
    Functor.CoconeTypes.isMulticoequalizer_iff]

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
⊢ (∀ (i₁ i₂ : (MultispanShape.prod ι).R) (x₁ : (c.multispanIndex.map Set.functorToTypes).right i₁)
      (x₂ : (c.multispanIndex.map Set.functorToTypes).right i₂),
      ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
                (c.multicofork.map Set.functorToTypes)).ι
            (WalkingMultispan.right i₁) x₁ =
          ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
                (c.multicofork.map Set.functorToTypes)).ι
            (WalkingMultispan.right i₂) x₂ →
        (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
          (c.multispanIndex.map Set.functorToTypes).multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
    ∀
      (x :
        ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
            (c.multicofork.map Set.functorToTypes)).pt),
      ∃ i a,
        ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm
                (c.multicofork.map Set.functorToTypes)).ι
            (WalkingMultispan.right i) a =
          x
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} = Set.univ

Tactic:
ext (_ | _) <;> tauto

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
⊢ ∀ (f : (j : T) → X₁ j ⟶ X₂ j), (∀ (j : T), monomorphisms (Type u) (f j)) → monomorphisms (Type u) (Limits.Sigma.map f)

Tactic:
f

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
⊢ (∀ (j : T), monomorphisms (Type u) (f j)) → monomorphisms (Type u) (Limits.Sigma.map f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ ⨆ j, stdSimplex.face {↑j}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}

Tactic:
iSup_le_iff

Goal state after:
case a
⊢ ∀ (i : ↑{0}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {0, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ ⨆ j, stdSimplex.face {↑j}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}

Tactic:
iSup_le_iff

Goal state after:
case a
⊢ ∀ (i : ↑{1}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 1} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a
⊢ ⨆ j, stdSimplex.face {↑j}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}

Tactic:
iSup_le_iff

Goal state after:
case a
⊢ ∀ (i : ↑{2}ᶜ), stdSimplex.face {↑i}ᶜ ≤ stdSimplex.face {0, 2} ⊔ stdSimplex.face {1, 2}
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ⨆ n, Y.skeleton n ≤ ⨆ n, (skeletonOfMono i) n

Tactic:
iSup_le_iff

Goal state after:
X Y : SSet
i : X ⟶ Y
⊢ ∀ (i_1 : ℕ), Y.skeleton i_1 ≤ ⨆ n, (skeletonOfMono i) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
i : Fin 2
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] i) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] i.castSucc

Tactic:
by
    fin_cases i
    · exact p.arrow_src 0
    · exact (q.arrow_src 0).trans h.symm

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
m✝ : ℕ
X Y : Truncated (n + 1)
m : ℕ
f : X.Path m
σ : X ⟶ Y
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj Y).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋1⦌, property := ⋯ }))) (f.arrow i)) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋0⦌, property := ⋯ })))
      ((ConcreteCategory.hom (X.map (tr (SimplexCategory.δ 1) ⋯ ⋯).op)) (f.arrow i))

Tactic:
exact ConcreteCategory.congr_hom (σ.naturality (tr (δ 1)).op) _ |>.symm

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

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
⊢ sy.spineToSimplex (m + 1) ⋯ (f.map σ) =
    (ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f)

Tactic:
apply sy.spineInjective (m + 1)

Goal state after:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
⊢ (sy.spineEquiv (m + 1) ⋯) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (sy.spineEquiv (m + 1) ⋯)
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
⊢ ∀ (f : X✝ ⟶ Y✝), ⊤ f → (morphismPropertyHomMk V).multiplicativeClosure f

Tactic:
f

Goal state after:
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
f : X✝ ⟶ Y✝
⊢ ⊤ f → (morphismPropertyHomMk V).multiplicativeClosure f
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x y : FreeRefl V
f : x ⟶ y
⊢ f = homMk default

Tactic:
induction f using hom_induction with
    | id => congr; subsingleton
    | @comp_homMk x y z _ g h =>
      obtain rfl := Subsingleton.elim y z
      obtain rfl := Subsingleton.elim g (𝟙rq _)
      simp [h]

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

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
⊢ ∀ (f : X✝ ⟶ Y✝), generators.multiplicativeClosure f → P f

Tactic:
f

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ generators.multiplicativeClosure f → P f