mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
⊢ E.presieve₀ ⊔ F.presieve₀ ∈ P.precoverage.coverings X

Tactic:
← PreZeroHypercover.presieve₀_sum

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : PreZeroHypercoverFamily C
h : ∀ ⦃X : C⦄ ⦃E F : PreZeroHypercover X⦄, P.property E → P.property F → P.property (E.sum F)
X : C
E : PreZeroHypercover X
hR : E.presieve₀ ∈ P.precoverage.coverings X
F : PreZeroHypercover X
hS : F.presieve₀ ∈ P.precoverage.coverings X
⊢ (E.sum F).presieve₀ ∈ P.precoverage.coverings X
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense

Goal state before:
pp: C₀ : Type u₀
C : Type u
inst✝⁴ : Category.{v₀, u₀} C₀
inst✝³ : Category.{v, u} C
F : C₀ ⥤ C
J₀ : GrothendieckTopology C₀
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : IsDenseSubsite J₀ J F
data : (X : C) → F.OneHypercoverDenseData J₀ J X
inst✝ : HasLimitsOfSize.{w, w, v', u'} A
G₀ : Sheaf J₀ A
X₀ : C₀
⊢ ∀ ⦃I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback F (data (F.obj X₀)).toPreOneHypercover.sieve₀, ⋯⟩⦄
    (r : I₁.Relation I₂),
    (match I₁ with
        | { Y := W₀, f := a, hf := ha } =>
          presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
            IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha)) ≫
        G₀.obj.map r.g₁.op =
      (match I₂ with
        | { Y := W₀, f := a, hf := ha } =>
          presheafObjπ data G₀ (F.obj X₀) (Sieve.ofArrows.i ha) ≫
            IsDenseSubsite.mapPreimage J F G₀ (Sieve.ofArrows.h ha)) ≫
        G₀.obj.map r.g₂.op

Tactic:
rintro ⟨W₀, a, ha⟩ ⟨T₀, b, hb⟩ ⟨U₀, p₁, p₂, fac⟩
        have ha' := Sieve.ofArrows.fac ha
        have hb' := Sieve.ofArrows.fac hb
        dsimp at ha hb ha' hb' p₁ p₂ fac ⊢
        rw [assoc, assoc, IsDenseSubsite.mapPreimage_comp_map,
          IsDenseSubsite.mapPreimage_comp_map,
          ← restriction_eq_of_fac data G₀ (F.map (p₁ ≫ a))
            (F.map p₁ ≫ Sieve.ofArrows.h ha) (by rw [assoc, ha', map_comp]),
          restriction_eq_of_fac data G₀ (F.map (p₁ ≫ a))
            (F.map p₂ ≫ Sieve.ofArrows.h hb) (by rw [assoc, hb', fac, map_comp])]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u'
inst✝⁴ : Category.{v', u'} J
X : J ⥤ C
inst✝³ : ∀ (j j' : J) (φ : j ⟶ j'), Mono (X.map φ)
c : Cocone X
hc : IsColimit c
inst✝² : IsFiltered J
j₀ : J
inst✝¹ : HasColimitsOfShape (Under j₀) C
inst✝ : colim.PreservesMonomorphisms
x✝¹ x✝ : Under j₀
g : x✝¹ ⟶ x✝
⊢ ((Functor.const (Under j₀)).obj (X.obj j₀)).map g ≫ X.map x✝.hom = X.map x✝¹.hom ≫ (Under.forget j₀ ⋙ X).map g

Tactic:
dsimp
        simp only [Category.id_comp, ← X.map_comp, Under.w]

Goal state after:
Module: Mathlib.Order.Interval.Set.SuccOrder

Goal state before:
pp: J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ ↑(Order.succ i) = Order.succ ↑i

Tactic:
coe_succ_of_mem

Goal state after:
J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i = Order.succ ↑i

J : Type u_1
inst✝¹ : PartialOrder J
inst✝ : SuccOrder J
j : J
i : ↑(Iic j)
hi : ¬IsMax i
⊢ Order.succ ↑i ∈ Iic j
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
Φ : SuccStruct C
X Y : C
f : X ⟶ Y
h : Arrow.mk f = Φ.toSuccArrow X
⊢ Φ.toSuccArrow X ∈ Φ.prop.toSet

Tactic:
apply prop_toSucc

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.Iteration.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j✝ j : J
h₁ : Order.IsSuccLimit j
h₂ : ∀ b < j, ∀ (iter₁ iter₂ : Φ.Iteration b), iter₁.F = iter₂.F
iter₁ iter₂ : Φ.Iteration j
k₁ : J
this✝ : ∀ (k₁ k₂ : J) (h₁₂ : k₁ ≤ k₂) (h₃ : k₂ ≤ j), k₂ < j → MapEq iter₁.F iter₂.F k₁ k₂ h₁₂ h₃
h₁₂ : k₁ ≤ j
h₃ : j ≤ j
h₄ : ¬j < j
this : restrictionLT iter₁.F ⋯ = restrictionLT iter₂.F ⋯
h₅ : k₁ < j
⊢ arrowMap iter₁.F k₁ j h₁₂ h₃ = arrowMap iter₂.F k₁ j h₁₂ h₃

Tactic:
simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
inst✝⁴ : LinearOrder J
inst✝³ : OrderBot J
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
p : X ⟶ Y
f : F.obj ⊥ ⟶ X
g : c.pt ⟶ Y
inst✝² : F.IsWellOrderContinuous
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hF : ∀ (j : J), ¬IsMax j → HasLiftingPropertyFixedBot (F.map (homOfLE ⋯)) p (c.ι.app (Order.succ j) ≫ g)
sq : CommSq f (c.ι.app ⊥) p g
⊢ sq.HasLift

Tactic:
obtain ⟨s, hs⟩ := (wellOrderInductionData c f g hF).surjective { w₂ := sq.w, .. }
  replace hs := congr_arg SqStruct.f' hs
  dsimp at hs
  let t : Cocone F := Cocone.mk X
    { app j := (s.1 ⟨j⟩).f'
      naturality j j' g := by simpa using congr_arg SqStruct.f' (s.2 g.op) }
  let l := hc.desc t
  have hl (j : J) : c.ι.app j ≫ l = (s.1 ⟨j⟩).f' := hc.fac t j
  exact ⟨⟨{
    l := l
    fac_left := by rw [hl, hs]
    fac_right := hc.hom_ext (fun j ↦ by rw [reassoc_of% (hl j), SqStruct.w₂])}⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

Goal state before:
pp: J : Type u
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝¹ : OrderBot J
val₀ : F.obj (op ⊥)
inst✝ : WellFoundedLT J
j : J
hj : Order.IsSuccLimit j
e : (i : J) → i < j → d.Extension val₀ i
⊢ (ConcreteCategory.hom (F.map (homOfLE ⋯).op))
      (d.lift j hj
        ⟨fun x ↦
          match x with
          | op ⟨i, hi⟩ => (e i hi).val,
          ⋯⟩) =
    val₀

Tactic:
by
    rw [d.map_lift _ _ _ _ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)]
    simpa using (e ⊥ (by simpa [bot_lt_iff_ne_bot] using hj.not_isMin)).map_zero

Goal state after:
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
⊢ πFunctorObj I.homFamily (((iterationFunctor I κ).obj j).obj (Arrow.mk f)).hom =
    (relativeCellComplexιObjFObjSuccIso I κ f j).inv ≫
      (relativeCellComplexιObj I κ f).incl.app (Order.succ j) ≫
        πObj I κ f ≫ (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).inv

Tactic:
by
  have h₁ := (iterationFunctorMapSuccAppArrowIso I κ f j).hom.right.w
  have h₂ := (transfiniteCompositionOfShapeSuccStructPropιIteration I κ).incl.naturality
    (homOfLE (Order.le_succ j))
  dsimp at h₁ h₂
  rw [comp_id] at h₂
  rw [← cancel_mono (iterationFunctorObjObjRightIso I κ (Arrow.mk f) j).hom,
    ← cancel_mono ((ιIteration I κ).app f).right, assoc, assoc, assoc, assoc, assoc,
    Iso.inv_hom_id_assoc, πObj_ιIteration_app_right,
    iterationFunctorObjObjRightIso_ιIteration_app_right,
    ← cancel_epi (relativeCellComplexιObjFObjSuccIso I κ f j).hom, Iso.hom_inv_id_assoc]
  dsimp [relativeCellComplexιObjFObjSuccIso,
    relativeCellComplexιObj, transfiniteCompositionOfShapeιIterationAppRight]
  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.PadicVal.Basic

Goal state before:
pp: p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValRat p ↑z = ↑(multiplicity (↑p) z)

Tactic:
by
  rw [of_int, padicValInt.of_ne_one_ne_zero hp hz]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
G : C
inst✝² : Abelian C
hG : IsSeparator G
X : C
inst✝¹ : IsGrothendieckAbelian.{w, v, u} C
A : C
f : A ⟶ X
inst✝ : Mono f
o : Ordinal.{w}
j : o.ToType
hj : transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤
this✝ : Nonempty o.ToType
this : OrderBot o.ToType
⊢ ∃ J x x_1 x_2,
    ∃ (x_3 : WellFoundedLT J), Nonempty ((generatingMonomorphisms G).pushouts.TransfiniteCompositionOfShape J f)

Tactic:
exact ⟨_, _, _, _, _, ⟨transfiniteCompositionOfShapeOfEqTop hG hj⟩⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
r : ℕ
⊢ padicValRat p (↑p ^ r)⁻¹ = -↑r

Tactic:
rw [padicValRat.inv, neg_inj, padicValRat.pow p, padicValRat.self hp.elim.one_lt, mul_one]

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq : Fact (Nat.Prime q)
n m : ℕ
ne : p ≠ q
⊢ padicValNat p (p ^ n * q ^ m) = n

Tactic:
rw [padicValNat.mul (NeZero.ne' (p ^ n)).symm (NeZero.ne' (q ^ m)).symm,
    padicValNat.prime_pow, padicValNat_prime_prime_pow m ne, add_zero]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε

Tactic:
obtain ⟨k, hk⟩ := @exists_pow_neg_lt p _ ε (mod_cast hε)

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ∃ k, ↑p ^ (-↑k) < ε
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: p n : ℕ
hn : n ≠ 0
⊢ Finset.image (fun x ↦ p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ n.divisors

Tactic:
intro t ht

Goal state after:
p n : ℕ
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun x ↦ p ^ x) (Finset.range (padicValNat p n + 1))
⊢ t ∈ n.divisors
Module: Mathlib.NumberTheory.Padics.PadicVal.Basic

Goal state before:
pp: case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
⊢ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n)) ⊆ n.divisors.erase 1

Tactic:
intro t ht

Goal state after:
case inr
p n : ℕ
hp : Fact (Nat.Prime p)
hn : n ≠ 0
t : ℕ
ht : t ∈ Finset.image (fun t ↦ p ^ (t + 1)) (Finset.range (padicValNat p n))
⊢ t ∈ n.divisors.erase 1
Module: Mathlib.NumberTheory.Padics.PadicIntegers

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
h : ‖↑r‖ ≤ 1
norm_denom_lt : ‖↑r.den‖ < 1
hr : ‖↑r‖ * ‖↑r.den‖ = ‖↑r.num‖
key : ‖↑r.num‖ < 1
⊢ ‖↑↑r.num‖ < 1 ∧ ‖↑↑↑r.den‖ < 1

Tactic:
exact ⟨key, norm_denom_lt⟩

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
c : ℤ_[p]
hx : ↑p ^ n * c ≠ 0
this : c ≠ 0
⊢ n ≤ (↑p ^ n * c).valuation

Tactic:
by
      rw [valuation_p_pow_mul _ _ this]
      exact le_self_add

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

Goal state before:
pp: p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k + (n + k - k - (p.digits (n + k - k)).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum

Tactic:
Nat.add_sub_cancel n k,

Goal state after:
p k n : ℕ
hp : Fact (Nat.Prime p)
h : k ≤ n + k
⊢ n + k - (p.digits (n + k)).sum - (k + (n - (p.digits n).sum) - (p.digits k).sum) =
    (p.digits k).sum + (p.digits n).sum - (p.digits (n + k)).sum
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (u : ℕ → ℚ_[p]), CauchySeq u → ∃ a, Tendsto u atTop (nhds a)

Tactic:
intro u

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
u : ℕ → ℚ_[p]
⊢ CauchySeq u → ∃ a, Tendsto u atTop (nhds a)
Module: Mathlib.AlgebraicTopology.SimplicialObject.Split

Goal state before:
pp: Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.EqId ↔ (unop A.fst).len = (unop Δ).len

Tactic:
eqId_iff_eq

Goal state after:
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ A.fst = Δ ↔ (unop A.fst).len = (unop Δ).len
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' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst✝¹ : Mono i'
inst✝ : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h : Δ = Δ''
⊢ False

Tactic:
simp only [left_eq_add, h, add_eq_zero, and_false, reduceCtorEq] at eq

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

Goal state before:
pp: case mk
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + k + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
rcases k with _ | k

Goal state after:
case mk.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
hk : ⦋n⦌.len = ⦋m⦌.len + 0 + 1
⊢ PInfty.f n ≫ X.map i.op = 0

case mk.succ
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + (k + 1) + 1
⊢ PInfty.f n ≫ X.map i.op = 0
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
P : Karoubi (SimplicialObject C)
⊢ ((𝟙 N₂ ◫ N₂Γ₂.inv) ≫ (N₂.associator Γ₂ N₂).inv ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂).app P = (𝟙 N₂).app P

Tactic:
dsimp only [NatTrans.comp_app, NatTrans.hcomp_app, Functor.comp_map, Functor.associator,
    NatTrans.id_app, Functor.comp_obj]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂.map (𝟙 (N₂.obj P)))) ≫
      𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ 𝟙 (N₂.obj (Γ₂.obj (N₂.obj P))) ≫ N₂.map (Γ₂N₂.natTrans.app P) =
    𝟙 (N₂.obj P)
Module: Mathlib.Combinatorics.Quiver.SingleObj

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

Tactic:
by
  induction l with
  | nil => rfl
  | cons a l ih => change a :: pathToList (listToPath l) = a :: l; rw [ih]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
Φ : W.Localization ⥤ C₂ := Localization.lift G hW W.Q
e : W.Q ⋙ Φ ≅ G := Localization.fac G hW W.Q
this : IsIso (Functor.whiskerRight adj.unit W.Q)
⊢ G.IsLocalization W

Tactic:
exact Functor.IsLocalization.of_equivalence_target W.Q W _
    (Equivalence.mk Φ (F ⋙ W.Q)
      (Localization.liftNatIso W.Q W W.Q (G ⋙ F ⋙ W.Q) _ _
        (W.Q.leftUnitor.symm ≪≫ asIso (Functor.whiskerRight adj.unit W.Q) ≪≫
        Functor.associator _ _ _))
      (Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ e ≪≫ asIso adj.counit)) e

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : ModelCategory C
X : C
inst✝ : IsCofibrant X
Y : C
f g : X ⟶ resolutionObj Y
h : LeftHomotopyClass.mk (f ≫ pResolutionObj Y) = LeftHomotopyClass.mk (g ≫ pResolutionObj Y)
⊢ LeftHomotopyClass.mk (homMk f).hom = LeftHomotopyClass.mk (homMk g).hom

Tactic:
exact (LeftHomotopyClass.postcomp_bijective_of_fibration_of_weakEquivalence
    (X := X) (g := pResolutionObj Y)).injective h

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 := ⋯ }
hR₀ : ∀ (R : (localizerMorphism C).LeftResolution X), Nonempty (Zigzag R R₀)
this : Nonempty ((localizerMorphism C).LeftResolution X)
⊢ IsConnected ((localizerMorphism C).LeftResolution X)

Tactic:
exact zigzag_isConnected (fun R₁ R₂ ↦ (hR₀ R₁).some.trans (hR₀ R₂).some.symm)

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

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
inst✝³ : ModelCategory D
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : CategoryWithWeakEquivalences C
e : C ≌ D
h₁ : cofibrations C = (cofibrations D).inverseImage e.functor
h₂ : fibrations C = (fibrations D).inverseImage e.functor
h₃ : weakEquivalences C = (weakEquivalences D).inverseImage e.functor
h₁' : trivialCofibrations C = (trivialCofibrations D).inverseImage e.functor
⊢ trivialFibrations C = (trivialFibrations D).inverseImage e.functor

Tactic:
simp [trivialFibrations, h₂, h₃]

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
i : Fin (n + 1)
⊢ s ∈ Λ[n, i].obj (op ⦋d⦌) ↔ ∃ j, ∃ (_ : j ≠ i), j ∉ Set.range ⇑s

Tactic:
by
  simp [horn_eq_iSup]

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

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x

Tactic:
have (x : d.multispan.ColimitType) :
      ∃ (i : J.R) (a : d.right i), d.multispan.ιColimitType (.right i) a = x := by
    obtain ⟨(l | r), z, rfl⟩ := d.multispan.ιColimitType_jointly_surjective x
    · exact ⟨J.fst l, d.multispan.map (WalkingMultispan.Hom.fst l) z, by rw [ιColimitType_map]⟩
    · exact ⟨r, z, by simp⟩

Goal state after:
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
⊢ c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
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
y : d.multispan.ColimitType
⊢ ∃ i a, c.ι (WalkingMultispan.right i) a = d.multispan.descColimitType c y

Tactic:
obtain ⟨i, z, rfl⟩ := this y

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
i : J.R
z : d.right i
⊢ ∃ i_1 a,
    c.ι (WalkingMultispan.right i_1) a =
      d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
j : Fin (n + 1)
hij : j ≠ i
hj : j ∉ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
this : ∃ j, ¬j = i ∧ ∀ (i : Fin (m + 1)), ¬(stdSimplex.objEquiv.symm f) i = j
⊢ stdSimplex.objEquiv.symm f ∈ Λ[n, i].obj (op ⦋m⦌) ↔ stdSimplex.objEquiv.symm f ∈ Set.univ

Tactic:
simpa [horn_eq_iSup] using this

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ ∂Δ[n].obj (op ⦋d⦌) ↔ ∃ j, j ∉ Set.range ⇑s

Tactic:
boundary_eq_iSup

Goal state after:
n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ (⨆ i, stdSimplex.face {i}ᶜ).obj (op ⦋d⦌) ↔ ∃ j, j ∉ Set.range ⇑s
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ∂Δ[n]

Tactic:
boundary_eq_iSup

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ⨆ i, stdSimplex.face {i}ᶜ
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' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (α_ (X ⟶[V] Y) (𝟙_ V) (𝟙_ V)).inv ≫
          (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).hom ≫
            (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
              (X ⟶[V] Y) ◁ (ρ_ (Y ⟶[V] Y')).inv ≫
                (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                  (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''

Tactic:
whiskerLeft_rightUnitor_inv_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 Y Y' Y'' : C
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (λ_ (𝟙_ V)).inv ≫
        (α_ (X ⟶[V] Y) (𝟙_ V) (𝟙_ V)).inv ≫
          (ρ_ ((X ⟶[V] Y) ⊗ 𝟙_ V)).hom ≫
            (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
              (ρ_ ((X ⟶[V] Y) ⊗ Y ⟶[V] Y')).inv ≫
                (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (𝟙_ V)).hom ≫
                  (X ⟶[V] Y) ◁ (Y ⟶[V] Y') ◁ (eHomEquiv V) g' ≫
                    (α_ (X ⟶[V] Y) (Y ⟶[V] Y') (Y' ⟶[V] Y'')).inv ≫ (eComp V X Y Y' ▷ Y' ⟶[V] Y'') ≫ eComp V X Y' Y'' =
    (ρ_ (X ⟶[V] Y)).inv ≫
      (X ⟶[V] Y) ◁ (eHomEquiv V) g ≫
        eComp V X Y Y' ≫ (ρ_ (X ⟶[V] Y')).inv ≫ (X ⟶[V] Y') ◁ (eHomEquiv V) g' ≫ eComp V X Y' Y''
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: x✝² : SSet
x✝¹ : x✝² ⟶ Δ[0]
n : SimplexCategory
x✝ : x✝².obj (Opposite.op n)
⊢ (ConcreteCategory.hom (x✝¹.app (Opposite.op n))).toFun x✝ =
    (ConcreteCategory.hom ((SSet.const (obj₀Equiv.symm 0)).app (Opposite.op n))).toFun x✝

Tactic:
exact objEquiv.injective (by ext; simp)

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
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W ((e (X ⟶[V] X)) (ForgetEnrichment.homTo V (𝟙 X))) = 𝟙 (ForgetEnrichment.of W X)

Tactic:
by
    rw [h, ForgetEnrichment.homTo_id, ← TransportEnrichment.eId_eq]
    simp [ForgetEnrichment.to]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : Center C
⊢ (λ_ X).inv.f = (λ_ X.fst).inv

Tactic:
by
  apply Iso.inv_ext' -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): Originally `ext`
  rw [← leftUnitor_hom_f, ← comp_f, Iso.hom_inv_id]; rfl

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

Goal state before:
pp: x : SimplexCategoryGenRel
⊢ ℕ

Tactic:
by rcases x with ⟨n⟩; exact n

Goal state after: