mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : x✝ = 0
⊢ 0 ≤ max 0 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ 0 ≤ max 0 (exp (-x✝.valuation))

pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : x✝ = 0
⊢ 0 ≤ max (exp (-x✝¹.valuation)) 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ 0 ≤ max (exp (-x✝¹.valuation)) (exp (-x✝.valuation))

pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max 0 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max 0 (exp (-x✝.valuation))

pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max (exp (-x✝¹.valuation)) 0

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ exp (-(x✝¹ + x✝).valuation) ≤ max (exp (-x✝¹.valuation)) (exp (-x✝.valuation))

Tactic:
any_goals simp_all [inv_le_inv₀]

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x✝¹ x✝ : ℚ_[p]
h✝² : ¬x✝¹ + x✝ = 0
h✝¹ : ¬x✝¹ = 0
h✝ : ¬x✝ = 0
⊢ x✝¹.valuation ≤ (x✝¹ + x✝).valuation ∨ x✝.valuation ≤ (x✝¹ + x✝).valuation
Module: Mathlib.NumberTheory.Padics.PadicNumbers

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x ≠ 0
⊢ addValuation x = ↑x.valuation

Tactic:
by
  simp only [Padic.addValuation, AddValuation.of_apply, addValuationDef, if_neg hx]

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

Goal state before:
pp: j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0

Tactic:
by
  constructor
  · rintro ⟨_, h₂⟩
    by_contra h
    exact h₂ (Fin.succAbove_ne_zero_zero h)
  · rintro rfl
    exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩

Goal state after:
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 : ℕ
⊢ PInfty.f (n + 1) ≫ ((alternatingFaceMapComplex A).obj X).d (n + 1) n = K[X].d (n + 1) n ≫ PInfty.f n

Tactic:
exact PInfty.comm (n + 1) 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
inst✝ : HasFiniteCoproducts C
K : ChainComplex C ℕ
n : ℕ
⊢ ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n =
    ((Γ₀.splitting K).cofan (op ⦋n⦌)).inj (Splitting.IndexSet.id (op ⦋n⦌))

Tactic:
rw [PInfty_f]
  rcases n with _ | n
  · simpa only [P_f_0_eq] using! comp_id _
  · exact (HigherFacesVanish.on_Γ₀_summand_id K n).comp_P_eq_self

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

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

Tactic:
· intros; ext; simp

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 : F ⊣ G
W : MorphismProperty C₁
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.counit
⊢ G.IsLocalization W

Tactic:
by
  simpa using isLocalization_leftAdjoint adj.op W.op hW.op (fun X ↦ hW' X.unop)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence (HoCat.adjUnit.app (toHoCat.obj X))

Tactic:
rw [HoCat.adjUnit_app, weakEquivalence_toHoCat_map_iff,
    weakEquivalence_iff_of_objectProperty]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ WeakEquivalence X.iBifibrantResolutionObj.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject.HoCat C
⊢ IsIso (HoCat.adjCounit'.app X)

Tactic:
obtain ⟨X, rfl⟩ := BifibrantObject.toHoCat_obj_surjective X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ IsIso (HoCat.adjCounit'.app (BifibrantObject.toHoCat.obj X))
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

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

Tactic:
obtain ⟨X, rfl⟩ := BifibrantObject.toHoCat_obj_surjective X

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : BifibrantObject C
⊢ adjUnit.app (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X)) ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (adjCounitIso.hom.app (BifibrantObject.toHoCat.obj X)) =
    𝟙 (BifibrantObject.HoCat.ιCofibrantObject.obj (BifibrantObject.toHoCat.obj X))
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:
simp [horn_eq_iSup]

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : Sᶜ.card = 1
⊢ ∃ j, S = {j}ᶜ

Tactic:
Finset.card_eq_one

Goal state after:
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
S : Finset (Fin (n + 1 + 1))
hx : stdSimplex.face S ≤ A
hd : n ≤ n
hS : ∃ a, Sᶜ = {a}
⊢ ∃ j, S = {j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ stdSimplex.objEquiv.symm f ∉ Λ[n, i].obj (op d)

Tactic:
rw [mem_horn_iff, ne_eq, not_not]

Goal state after:
n : ℕ
i : Fin (n + 1)
d : SimplexCategory
f : d ⟶ ⦋n⦌
inst✝ : IsIso f
⊢ Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm f)) ∪ {i} = Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: ⊢ J ≤ monomorphisms SSet

Tactic:
rintro _ _ _ h
  simp only [J, iSup_iff] at h
  obtain ⟨n, ⟨i⟩⟩ := h
  exact monomorphisms.infer_property _

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ Cofibration f ↔ Mono f

Tactic:
rw [HomotopicalAlgebra.cofibration_iff]

Goal state after:
X Y : SSet
f : X ⟶ Y
⊢ cofibrations SSet f ↔ Mono f
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x✝¹ : Δ[n + 1] ⟶ ⊤_ SSet
x✝ : CommSq t Λ[n + 1, i].ι (terminal.from Z) x✝¹
⊢ x✝.HasLift

Tactic:
obtain ⟨φ, hφ⟩ := h _ (horn.IsCompatible.of_hom t)

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x✝¹ : Δ[n + 1] ⟶ ⊤_ SSet
x✝ : CommSq t Λ[n + 1, i].ι (terminal.from Z) x✝¹
φ : Δ[n + 1] ⟶ Z
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t
⊢ x✝.HasLift
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case a.left
⊢ stdSimplex.face {0, 1} ≤ Λ[2, 0]

Tactic:
exact face_le_horn (2 : Fin 3) 0 (by simp)

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

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ y₃ : X₄
⊢ (ConcreteCategory.hom k) x₃ = (ConcreteCategory.hom k) y₃ → x₃ = y₃

Tactic:
eq

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
w :
  ∀ (x : ToType X₁),
    (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom b) ((ConcreteCategory.hom l) x)
x₃ y₃ : X₄
eq : (ConcreteCategory.hom k) x₃ = (ConcreteCategory.hom k) y₃
⊢ x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
c : Cell i d
n : SimplexCategory
f : n ⟶ ⦋d⦌
⊢ ↑((ConcreteCategory.hom ((b i d).app (op n)))
        ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op n))) (stdSimplex.objEquiv.symm f))) =
    (ConcreteCategory.hom ((c.ιSigmaStdSimplex ≫ b i d ≫ ((skeletonOfMono i) (d + 1)).ι).app (op n)))
      (stdSimplex.objEquiv.symm f)

Tactic:
dsimp +instances

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 ≫
      (((λ_ (𝟙_ V)).inv ≫ ((eHomEquiv V) f ⊗ₘ (eHomEquiv V) f') ≫ eComp V X X' X'') ▷ X'' ⟶[V] 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:
comp_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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        ((((eHomEquiv V) f ⊗ₘ (eHomEquiv V) f') ≫ eComp V X X' X'') ▷ X'' ⟶[V] 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
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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        ((((eHomEquiv V) f ⊗ₘ (eHomEquiv V) f') ≫ eComp V X X' X'') ▷ X'' ⟶[V] 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:
comp_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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        (((eHomEquiv V) f ⊗ₘ (eHomEquiv V) f') ▷ X'' ⟶[V] Y) ≫ (eComp V X X' X'' ▷ X'' ⟶[V] 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
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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        ((𝟙_ V ◁ (eHomEquiv V) f' ≫ (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:
comp_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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        ((𝟙_ V ◁ (eHomEquiv V) f') ▷ 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
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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        (((λ_ (𝟙_ V)).hom ≫ (eHomEquiv V) f' ≫ (λ_ (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:
comp_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 ≫
      ((λ_ (𝟙_ V)).inv ▷ X'' ⟶[V] Y) ≫
        ((λ_ (𝟙_ V)).hom ▷ X'' ⟶[V] Y) ≫
          (((eHomEquiv V) f' ≫ (λ_ (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
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] 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:
comp_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'')).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
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ Y₁ X₂ Y₂ : Center C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ (f.f ▷ X₂.fst ≫ Y₁.fst ◁ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd.β U).hom =
    ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ▷ X₂.fst ≫ Y₁.fst ◁ g.f)

Tactic:
comp_whiskerRight_assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ Y₁ X₂ Y₂ : Center C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
⊢ f.f ▷ X₂.fst ▷ U ≫ (Y₁.fst ◁ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd.β U).hom =
    ((X₁.tensorObj X₂).snd.β U).hom ≫ U ◁ (f.f ▷ X₂.fst ≫ Y₁.fst ◁ g.f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (associativity'Iso X Y Z).hom.app xyz =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)

Tactic:
change 𝟙 _ ≫ _ ≫ 𝟙 _ = _
  rw [Category.id_comp, Category.comp_id]
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ (i : Fin (n + 1)), (f i).castSucc < x) → ∀ b ∈ finset f x, b = Fin.last (n + 1)

Tactic:
intro h i hi

Goal state after:
case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), (f i).castSucc < x
i : Fin (n + 2)
hi : i ∈ finset f x
⊢ i = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inr (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₂ ≫ inr (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
change inr' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₂ ≫ inr' _ _
    ext i : 3
    dsimp [tensorHomOf]
    have e₁ := inr'_eval x₁ x₂ i
    have e₂ := inr'_eval y₁ y₂ <| (WithInitial.down f₂).toOrderHom i
    simp only [SimplexCategory.len_mk] at e₁ e₂
    rw [e₁, e₂]
    simp only [SimplexCategory.eqToHom_toOrderHom, SimplexCategory.len_mk,
      Nat.succ_eq_add_one, OrderEmbedding.toOrderHom_coe,
      OrderIso.coe_toOrderEmbedding, Fin.castOrderIso_apply,
      Fin.cast_cast, Fin.cast_eq_self, Fin.cast_inj]
    conv_lhs =>
      change Fin.addCases
        (fun i ↦ Fin.castAdd (y₂.len + 1) (f₁.toOrderHom i))
        (fun i ↦ Fin.natAdd (y₁.len + 1) (f₂.toOrderHom i))
        (Fin.natAdd (x₁.len + 1) i)
      rw [Fin.addCases_right]
    rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
Y : SSet
e : X ≅ Y
d : ℕ
hd : x.dim = d
⊢ ⋯.index hd = hxy.index hd

Tactic:
obtain ⟨dx, x, rfl⟩ := x.mk_surjective

Goal state after:
X : SSet
y : X.S
Y : SSet
e : X ≅ Y
d dx : ℕ
x : X _⦋dx⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace y
hd : { dim := dx, simplex := x }.dim = d
⊢ ⋯.index hd = hxy.index hd
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : SimplexCategory
⊢ Quiver.Hom.unop (op (Hom.mk { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ })) = (𝟙 (op ⦋n.len + 1⦌)).unop

Tactic:
ext x : 3
    exact II.map'_id x

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
hS : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
X Y : C
i : X ⟶ Y
x✝ : Mono i
hi : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i

Tactic:
· obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS Y
    replace hi (j : ι) := hi (s j) (hs j) (c.inj j ≫ p)
    choose φ hφ using hi
    exact ExtremalEpi.isIso p (Cofan.IsColimit.desc hc φ) _
      (Cofan.IsColimit.hom_ext hc _ _ (by simp [hφ]))

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
⊢ F.isDenseAt = G.isDenseAt

Tactic:
ext X

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
X : D
⊢ F.isDenseAt X ↔ G.isDenseAt X
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ IsCardinalLocallyPresentable (Cᵒᵖ ⥤ A) κ

Tactic:
IsCardinalLocallyPresentable.iff_exists_isStrongGenerator

Goal state after:
A : Type u'
inst✝⁴ : Category.{v', u'} A
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : IsCardinalLocallyPresentable A κ
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
P : ObjectProperty A
w✝ : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
⊢ ∃ P,
    ∃ (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Cᵒᵖ ⥤ A) κ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: A B X Y : SSet
i : A ⟶ B
hi : innerHornInclusions i
f : X ⟶ Y
hf : RelativeCellComplex (fun x ↦ innerHornInclusions.homFamily) f
⊢ Limits.PreservesColimit hf.F (coyoneda.obj (Opposite.op A))

Tactic:
by
    have : IsFinitelyPresentable.{u} A := by
      simp only [innerHornInclusions_eq_iSup, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance
    infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
⊢ (x.cast hd).simplex.1 i < k.succ ↔ i < l.succ

Tactic:
← not_le,

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
⊢ ¬k.succ ≤ (x.cast hd).simplex.1 i ↔ i < l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
hi : (min x hd).castSucc < i
⊢ φ x hd i = (objEquiv (x.cast hd).simplex) (i.pred ⋯)

Tactic:
φ_of_ne _ _ _ hi.ne',

Goal state after:
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 2)
hi : (min x hd).castSucc < i
⊢ (objEquiv (x.cast hd).simplex) ((min x hd).predAbove i) = (objEquiv (x.cast hd).simplex) (i.pred ⋯)