mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

Goal state before:
pp: J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : α ≤i J
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
this : Nonempty ↑(Set.Iio j)
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Tactic:
exact hasColimitsOfShape_of_initialSeg _
      (InitialSeg.trans (Set.principalSegIio j) h)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
⊢ W ((h.iic j).F.map (homOfLE ⋯))

Tactic:
have := h.map_mem i.1 (by
      rw [not_isMax_iff] at hi ⊢
      obtain ⟨i', hi'⟩ := hi
      exact ⟨j, lt_of_lt_of_le hi' i'.2⟩)

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Iic j)
hi : ¬IsMax i
this : W (h.F.map (homOfLE ⋯))
⊢ W ((h.iic j).F.map (homOfLE ⋯))
Module: Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
⊢ Arrow.mk ((h.ici j).F.map (homOfLE ⋯)) ∈ W.toSet

Tactic:
have eq : Arrow.mk ((Subtype.mono_coe _).functor.map (homOfLE (Order.le_succ i))) =
      Arrow.mk (homOfLE (Order.le_succ i.1)) :=
        Arrow.ext rfl (coe_succ_of_mem (i.2.trans (Order.le_succ _))) rfl

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
W : MorphismProperty C
J : Type w
inst✝⁷ : LinearOrder J
inst✝⁶ : SuccOrder J
inst✝⁵ : OrderBot J
inst✝⁴ : WellFoundedLT J
J' : Type w'
inst✝³ : LinearOrder J'
inst✝² : SuccOrder J'
inst✝¹ : OrderBot J'
inst✝ : WellFoundedLT J'
X Y : C
f : X ⟶ Y
h : W.TransfiniteCompositionOfShape J f
j : J
i : ↑(Set.Ici j)
hi : ¬IsMax i
this : Arrow.mk (h.F.map (homOfLE ⋯)) ∈ W.toSet
eq : Arrow.mk (⋯.functor.map (homOfLE ⋯)) = Arrow.mk (homOfLE ⋯)
⊢ Arrow.mk ((h.ici j).F.map (homOfLE ⋯)) ∈ W.toSet
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty

Goal state before:
pp: case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ =
    arrowMap (functor hj iter) (↑⟨l₁, pf✝²⟩) (↑⟨l₂, pf✝¹⟩) pf✝ pf✝¹

Tactic:
arrowMap_functor hj iter l₁ l₂ _ (hl₂.trans hij),

Goal state after:
case inl.e_F
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
Φ : SuccStruct C
J : Type u
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
inst✝² : SuccOrder J
inst✝¹ : WellFoundedLT J
inst✝ : HasIterationOfShape J C
j : J
hj : Order.IsSuccLimit j
iter : (i : J) → i < j → Φ.Iteration i
i : J
hi : Order.IsSuccLimit i
hij✝ : i ≤ j
k : J
hk : k < i
hij : i < j
l₁ : J
hl₁ : l₁ ∈ Set.Iio i
l₂ : J
hl₂ : l₂ ∈ Set.Iio i
f : ⟨l₁, hl₁⟩ ⟶ ⟨l₂, hl₂⟩
pf✝⁵ : l₁ ∈ Set.Iic i
pf✝⁴ : l₂ ∈ Set.Iic i
pf✝³ : ⟨l₁, pf✝⁵⟩ ≤ ⟨l₂, pf✝⁴⟩
pf✝² : l₁ ∈ Set.Iic j
pf✝¹ : l₂ ∈ Set.Iic j
pf✝ : ⟨l₁, pf✝²⟩ ≤ ⟨l₂, pf✝¹⟩
⊢ arrowMap (iter i hij).F (↑⟨l₁, pf✝⁵⟩) (↑⟨l₂, pf✝⁴⟩) pf✝³ pf✝⁴ = Arrow.mk ((iter l₁ ⋯).mapObj (iter l₂ ⋯) pf✝ ⋯ ⋯ pf✝)
Module: Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.ToType
inst✝ : I.IsCardinalForSmallObjectArgument κ
X Y : C
f : X ⟶ Y
j : κ.ord.ToType
h₁ :
  Arrow.Hom.left (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom) ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (((iterationFunctor I κ).obj (Order.succ j)).obj (Arrow.mk f)).hom ≫
      Arrow.Hom.right (Arrow.Hom.right (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom)
h₂ :
  (iterationFunctor I κ).map (homOfLE ⋯) ≫
      (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j) =
    (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j
⊢ (iterationFunctorMapSuccAppArrowIso I κ (Arrow.mk f) j).hom.right.left ≫
      πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom ≫
        (((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app j).app (Arrow.mk f)).right ≫
          𝟙 ((iteration I κ).obj (Arrow.mk f)).right =
    ((((transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.app (Order.succ j)).app (Arrow.mk f)).left ≫
        𝟙 ((iteration I κ).obj (Arrow.mk f)).left) ≫
      ((iteration I κ).obj (Arrow.mk f)).hom

Tactic:
simp only [reassoc_of% h₁, comp_id, comp_id, Arrow.w_mk_right, ← h₂,
    NatTrans.comp_app, Arrow.comp_right,
    iterationFunctorMapSuccAppArrowIso_hom_right_right_comp_assoc]

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

Goal state before:
pp: p : ℕ
q : ℚ
hq : q ≠ 0
⊢ padicNorm p q = ↑p ^ (-padicValRat p q)

Tactic:
simp [hq, padicNorm]

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

Goal state before:
pp: p : ℕ
q : ℚ
hq : q = 0
⊢ 0 ≤ padicNorm p q

Tactic:
simp [hq, padicNorm]

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

Goal state before:
pp: p : ℕ
⊢ padicNorm p 0 = 0

Tactic:
simp [padicNorm]

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

Goal state before:
pp: p : ℕ
⊢ padicNorm p 1 = 1

Tactic:
simp [padicNorm]

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hqr : q + r ≠ 0
h : padicValRat p r ≤ padicValRat p q
⊢ r + q ≠ 0

Tactic:
rwa [add_comm]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
z : ℤ
⊢ ↑(p ^ n) ∣ z ↔ padicNorm p ↑z ≤ ↑p ^ (-↑n)

Tactic:
by
  unfold padicNorm; split_ifs with hz
  · norm_cast at hz
    simp [hz]
  · rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int,
      padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
    · norm_cast
      rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]
      · norm_cast
      · apply Int.finiteMultiplicity_iff.2 ⟨by simp [hp.out.ne_one], mod_cast hz⟩
    · exact_mod_cast hz
    · exact_mod_cast hp.out.one_lt

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p a : ℕ
hp : Fact (Nat.Prime p)
ha : p < a
k : ℕ
hk : a = p * k
⊢ padicValNat p k < k

Tactic:
calc
      _ ≤ log p k := padicValNat_le_nat_log k
      _ < _ := log_lt_self p (by lia)

Goal state after:
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ ↑p ^ padicValInt p a ∣ a

Tactic:
rw [padicValInt_dvd_iff_of_ne_one hp]

Goal state after:
case neg
p : ℕ
a : ℤ
hp : ¬p = 1
⊢ a = 0 ∨ padicValInt p a ≤ padicValInt p a
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case ha₀
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
⊢ 0 < ↑p

Tactic:
exact mod_cast (Fact.out : p.Prime).pos

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

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
f g : PadicSeq p
hf : ¬f ≈ 0
hg : ¬g ≈ 0
hfg : f ≈ g
h : ¬padicNorm p (↑f (stationaryPoint hf)) = padicNorm p (↑g (stationaryPoint hg))
hle : padicNorm p (↑f (stationaryPoint hf)) ≤ padicNorm p (↑g (stationaryPoint hg))
⊢ False

Tactic:
| inr hle =>

Goal state after:
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
Y₁ : C
f₁ : Y₁ ⟶ X
hf₁ : R.arrows f₁
y₁ : Φ.fiber.obj Y₁
hy₁ : (ConcreteCategory.hom (Φ.fiber.map f₁)) y₁ = x
Y₂ : C
f₂ : Y₂ ⟶ X
hf₂ : R.arrows f₂
y₂ : Φ.fiber.obj Y₂
hy₂ : (ConcreteCategory.hom (Φ.fiber.map f₂)) y₂ = x
⊢ ∃ Z p₁ p₂ z,
    p₁ ≫ f₁ = p₂ ≫ f₂ ∧ (ConcreteCategory.hom (Φ.fiber.map p₁)) z = y₁ ∧ (ConcreteCategory.hom (Φ.fiber.map p₂)) z = y₂

Tactic:
by
    let α₁ : Φ.fiber.elementsMk _ y₁ ⟶ Φ.fiber.elementsMk _ x := ⟨f₁, hy₁⟩
    let α₂ : Φ.fiber.elementsMk _ y₂ ⟶ Φ.fiber.elementsMk _ x := ⟨f₂, hy₂⟩
    obtain ⟨z, q₁, q₂, fac⟩ := IsCofiltered.cospan α₁ α₂
    rw [Subtype.ext_iff] at fac
    refine ⟨z.1, q₁.1, q₂.1, z.2, fac, ?_, ?_⟩
    all_goals rw [CategoryOfElements.map_snd]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
G : C ⥤ D
inst✝ : G.Additive
X : SimplicialObject C
q n m : ℕ
hnm : c.Rel m n
⊢ hσ' q n m hnm = G.map (hσ' q n m hnm)

Tactic:
by
  unfold hσ' hσ
  split_ifs
  · simp only [Functor.map_zero, zero_comp]
  · simp only [eqToHom_map, Functor.map_comp, Functor.map_zsmul]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Representable

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (Limits.diag X)

Tactic:
rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)]

Goal state after:
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝⁷ : HasBinaryProducts C
inst✝⁶ : HasPullbacks D
inst✝⁵ : HasBinaryProducts D
inst✝⁴ : HasTerminal D
inst✝³ : F.Full
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
X : D
h : ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
⊢ F.relativelyRepresentable (pullback.lift (𝟙 X) (𝟙 X) ⋯ ≫ (prodIsoPullback X X).inv)
Module: Mathlib.NumberTheory.Padics.PadicNumbers

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

Tactic:
dsimp [norm]
  exact mod_cast padicNormE.nonarchimedean' _ _

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

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

Tactic:
by
  dsimp [norm]
  exact mod_cast padicNormE.nonarchimedean' _ _

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ‖(↑p)⁻¹‖

Tactic:
norm_inv,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ 1 < ‖↑p‖⁻¹
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
⊢ QInfty ≫ QInfty = QInfty

Tactic:
ext n
  exact QInfty_f_idem n

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : ChainComplex C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst✝ : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ mapMono K i = 0

Tactic:
by
  unfold mapMono
  rw [Ne] at h₁
  split_ifs
  rfl

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

Goal state before:
pp: case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = PInfty.f n' ≫ X.map i.op

Tactic:
PInfty_comp_map_mono_eq_zero

Goal state after:
case neg
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = 0

case neg.h₁
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n⦌.len ≠ n'

case neg.h₂
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i
Module: Mathlib.Combinatorics.Quiver.Cast

Goal state before:
pp: U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ Hom.cast ⋯ ⋯ e = e'

Tactic:
rw [Hom.cast_eq_iff_heq]

Goal state after:
U : Type u_1
inst✝ : Quiver U
u v v' w : U
p : Path u v
p' : Path u v'
e : v ⟶ w
e' : v' ⟶ w
h : p.cons e = p'.cons e'
⊢ e ≍ e'
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
p : Path x₀ x₁
x : ↑I
⊢ p ⟨reflTransSymmAux (1, x), ⋯⟩ = (p.trans p.symm).toContinuousMap x

Tactic:
simp only [reflTransSymmAux, Path.trans]
    cases le_or_gt (x : ℝ) 2⁻¹ with
    | inl hx => simp [hx, ← extend_apply]
    | inr hx =>
      have : p.extend (2 - 2 * ↑x) = p.extend (1 - (2 * ↑x - 1)) := by ring_nf
      simpa [hx.not_ge, ← extend_apply]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R : (localizerMorphism C).LeftResolution X
⊢ WeakEquivalence R.w

Tactic:
by
  simpa only [weakEquivalence_iff] using R.hw

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : ModelCategory C
X : C
R₀ : (localizerMorphism C).LeftResolution X :=
  { X₁ := mk (HoCat.resolutionObj X), w := HoCat.pResolutionObj X, hw := ⋯ }
R : (localizerMorphism C).LeftResolution X
sq :
  CommSq (initial.to ((localizerMorphism C).functor.obj R₀.X₁)) (initial.to ((localizerMorphism C).functor.obj R.X₁))
    R₀.w R.w
⊢ Nonempty (Zigzag R R₀)

Tactic:
exact ⟨Zigzag.of_hom { f := homMk (sq.lift) }⟩

Goal state after:
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
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
⊢ WeakEquivalence (homMk P.ι).hom

Tactic:
exact inferInstanceAs (WeakEquivalence P.ι)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
j : J.R
⊢ F.map (c.ι (J.fst j)) ≫ F.map (d.fst j) = F.map (c.ι (J.snd j)) ≫ F.map (d.snd j)

Tactic:
rw [← F.map_comp, ← F.map_comp, condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
j : J.L
⊢ F.map (d.fst j) ≫ F.map (c.π (J.fst j)) = F.map (d.snd j) ≫ F.map (c.π (J.snd j))

Tactic:
rw [← F.map_comp, ← F.map_comp, condition]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : SimplexCategoryᵒᵖ
j : Δ[n].obj m
⊢ j ∈ Λ[n, i].obj m ↔ j ∈ (⨆ j, stdSimplex.face {↑j}ᶜ).obj m

Tactic:
simp [stdSimplex.face_obj, horn, Set.eq_univ_iff_forall]

Goal state after:
n : ℕ
i : Fin (n + 1)
m : SimplexCategoryᵒᵖ
j : Δ[n].obj m
⊢ (∃ x, ¬x = i ∧ ∀ (x_1 : Fin ((unop m).len + 1)), ¬(stdSimplex.asOrderHom j) x_1 = x) ↔
    ∃ i_1, ¬i_1 = i ∧ ∀ (x : Fin ((unop m).len + 1)), ¬(SimplexCategory.Hom.toOrderHom (stdSimplex.objEquiv j)) x = i_1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.range (stdSimplex.map (SimplexCategory.δ i)) ≤ ∂Δ[n + 1]

Tactic:
simp only [Subcomplex.range_eq_ofSimplex]

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.map (SimplexCategory.δ i))) ≤ ∂Δ[n + 1]
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel' f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) =
    Quot.mk (Rel' f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Quot.sound

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) y₀)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) y₀))

Tactic:
apply Quot.sound

Goal state after:
case inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀
h₀ : Rel f g (Sum.inl ((ConcreteCategory.hom f) x₀)) (Sum.inr ((ConcreteCategory.hom g) x₀))
⊢ Rel f g (Sum.inl ((ConcreteCategory.hom f) y₀)) (Sum.inr ((ConcreteCategory.hom g) y₀))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Quot.sound

Goal state after:
case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

Tactic:
apply Quot.sound

Goal state after:
case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Rel f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr ((ConcreteCategory.hom g) s✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d n : ℕ
y : sigmaStdSimplex i d _⦋n⦌
hy : y ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
⊢ ∃ c f, ∃ (_ : Epi f), (ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) (stdSimplex.objEquiv.symm f) = y

Tactic:
obtain ⟨c, s, rfl⟩ := ιSigmaStdSimplex_jointly_surjective y
  have hs : s ∉ ∂Δ[d].obj _ :=
    fun hs ↦ hy (⟨c.ιSigmaBoundary.app _ ⟨s, hs⟩, congr($(c.ι_l).app _ ⟨s, _⟩)⟩)
  refine ⟨c, stdSimplex.objEquiv s, ?_, by simp⟩
  simpa [SimplexCategory.epi_iff_surjective, boundary] using! hs

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

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ x₂ : sigmaStdSimplex i d _⦋n⦌
⊢ x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
    x₂ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
      (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₂ → x₁ = x₂

Tactic:
hx₁

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ x₂ : sigmaStdSimplex i d _⦋n⦌
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
⊢ x₂ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
    (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₂ → x₁ = x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m + 1⦌, property := hm })
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc i) ⋯ hm).op))
      ((ConcreteCategory.hom (f.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x) =
    (ConcreteCategory.hom (Y.map (tr (mkOfSucc i) ⋯ hm).op))
      ((ConcreteCategory.hom (g.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x)

Tactic:
simp [← NatTrans.naturality_apply, h]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp η (𝟙 (𝟙 b)) = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
by
  simp [← heq_eq_eq, hComp_id_heq]

Goal state after:
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 X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        ((λ_ (X' ⟶[V] X'')).inv ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
            (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (X ⟶[V] X') ◁ eComp V X' X'' Y ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y

Tactic:
leftUnitor_inv_whiskerRight_assoc,

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 X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        (λ_ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y)).inv ≫
          (α_ (𝟙_ V) (X' ⟶[V] X'') (X'' ⟶[V] Y)).inv ≫
            (((eHomEquiv V) f ▷ X' ⟶[V] X'') ▷ X'' ⟶[V] Y) ≫
              (α_ (X ⟶[V] X') (X' ⟶[V] X'') (X'' ⟶[V] Y)).hom ≫ (X ⟶[V] X') ◁ eComp V X' X'' Y ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y