mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
rw [arithGeom_succ, hn, mul_add, ← mul_assoc, add_comm n, pow_add, pow_one, add_assoc]
    congr
    rw [add_comm _ n, Finset.sum_range_succ', Finset.mul_sum, pow_zero, mul_add, mul_one,
      Finset.mul_sum, Finset.mul_sum]
    congr with k
    ring

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : CommSemiring R
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * u₀ + b * ∑ k ∈ Finset.range n, a ^ k
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * u₀ + b * ∑ k ∈ Finset.range (n + 1), a ^ k

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝ : Field R
ha : a ≠ 1
n : ℕ
hn : arithGeom a b u₀ n = a ^ n * (u₀ - b / (1 - a)) + b / (1 - a)
⊢ arithGeom a b u₀ (n + 1) = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: case succ
R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha_pos : 0 < a
ha_ne : a ≠ 1
h0 : b / (1 - a) < u₀
n : ℕ
hn : b / (1 - a) < arithGeom a b u₀ n
⊢ b / (1 - a) < arithGeom a b u₀ (n + 1)

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ h.lim ≤ u n / ↑n

Tactic:
Subadditive.lim

Goal state after:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
n : ℕ
hn : n ≠ 0
⊢ sInf ((fun n ↦ u n / ↑n) '' Ici 1) ≤ u n / ↑n
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > h.lim
⊢ ∃ n, 0 < n ∧ u n / ↑n < L

Tactic:
Subadditive.lim

Goal state after:
u : ℕ → ℝ
h : Subadditive u
hbdd : BddBelow (range fun n ↦ u n / ↑n)
L : ℝ
hL : L > sInf ((fun n ↦ u n / ↑n) '' Ici 1)
⊢ ∃ n, 0 < n ∧ u n / ↑n < L
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -x⁻¹) ℍₒ z

Tactic:
apply ContDiffWithinAt.neg

Goal state after:
case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) Inv.inv ℍₒ z
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ u (c n) - ↑(c n) * l = (u (c n) / ↑(c n) - l) * ↑(c n)

Tactic:
by field

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ (1 + ε) * ↑(c n)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / ↑(c x) - l‖ ≤ c_1 * ‖1‖
n : ℕ
hn : ‖u (c n) / ↑(c n) - l‖ ≤ ε * ‖1‖
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ ↑(c n) * l - u (c n) = -(u (c n) / ↑(c n) - l) * ↑(c n)

Tactic:
by field

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ c,
        (∀ᶠ (n : ℕ) in atTop, ↑(c (n + 1)) ≤ a * ↑(c n)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, ↑n * l - u n ≤ ε * (1 + l) * ↑n
d : ℝ
hd : d > l
ε : ℝ
hε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
npos : 0 < n
⊢ (↑n * l + ε * (1 + ε + l) * ↑n) / ↑n = l + ε * (1 + ε + l)

Tactic:
by field

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f (max n m).succ).snd
      (⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)) =
    min ((CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).snd x)
      ((CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).snd y)

Tactic:
CofilteredClosureSmall.bundledAbstractCofilteredClosure

Goal state after:
case min.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
⊢ ⟨CofilteredClosureSmall.InductiveStep (max n m + 1) fun m_1 x ↦
            CofilteredClosureSmall.bundledAbstractCofilteredClosure f m_1,
          CofilteredClosureSmall.inductiveStepRealization (max n m + 1) fun m_1 x ↦
            CofilteredClosureSmall.bundledAbstractCofilteredClosure f m_1⟩.snd
      (⋯.mpr (CofilteredClosureSmall.InductiveStep.min ⋯ ⋯ x y)) =
    min ((CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).snd x)
      ((CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).snd y)
Module: Mathlib.CategoryTheory.Filtered.Small

Goal state before:
pp: case eq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ (CofilteredClosureSmall.bundledAbstractCofilteredClosure f (max n m).succ).snd
      (⋯.mpr (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    eq g g'

Tactic:
CofilteredClosureSmall.bundledAbstractCofilteredClosure

Goal state after:
case eq.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsCofilteredOrEmpty C
α : Type w
f : α → C
j : C
n : ℕ
x : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f n).fst
hj₁ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩)
m : ℕ
y : (CofilteredClosureSmall.bundledAbstractCofilteredClosure f m).fst
hj₂ : cofilteredClosure f (CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩)
g g' :
  CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨n, x⟩ ⟶
    CofilteredClosureSmall.abstractCofilteredClosureRealization f ⟨m, y⟩
⊢ ⟨CofilteredClosureSmall.InductiveStep (max n m + 1) fun m_1 x ↦
            CofilteredClosureSmall.bundledAbstractCofilteredClosure f m_1,
          CofilteredClosureSmall.inductiveStepRealization (max n m + 1) fun m_1 x ↦
            CofilteredClosureSmall.bundledAbstractCofilteredClosure f m_1⟩.snd
      (⋯.mpr (CofilteredClosureSmall.InductiveStep.eq ⋯ ⋯ x y g g')) =
    eq g g'
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * (1 / (c ^ i) ^ 2) ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2

Tactic:
← mul_sum,

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < 1 - c⁻¹
⊢ (1 - c⁻¹)⁻¹ ^ 2 * ∑ i ∈ range N with j < c ^ i, 1 / (c ^ i) ^ 2 ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.op ⋙ coyoneda) A).hom ≫ limit.π (F.op ⋙ yoneda.obj A) (op i) =
    (yoneda.obj A).map (colimit.ι F i).op

Tactic:
erw [limitObjIsoLimitCompEvaluation_hom_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda F).hom.app A ≫ (limit.π (F.op ⋙ coyoneda) (op i)).app A =
    (yoneda.obj A).map (colimit.ι F i).op
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫
      (limitObjIsoLimitCompEvaluation (F.rightOp ⋙ coyoneda) A).hom ≫ limit.π (F.rightOp ⋙ yoneda.obj A) i =
    (yoneda.obj A).map (colimit.ι F (op i)).op

Tactic:
erw [limitObjIsoLimitCompEvaluation_hom_π]

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (yoneda.obj A).map (colimit.ι F (op i)).op
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ (coyonedaOpColimitIsoLimitCoyoneda' F).hom.app A ≫ (limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (yoneda.obj A).map (colimit.ι F (op i)).op

Tactic:
change ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ _).app A = _

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : Iᵒᵖ ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape I (Type u₂)
A : C
i : I
⊢ ((coyonedaOpColimitIsoLimitCoyoneda' F).hom ≫ limit.π (F.rightOp ⋙ coyoneda) i).app A =
    (yoneda.obj A).map (colimit.ι F (op i)).op
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
⊢ HasColimit F

Tactic:
let G : ∀ s, I s ⥤ C := fun s => (F.obj ⟨s⟩).presentation.F

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
α : Type v
inst✝¹ : Finite α
inst✝ : HasColimitsOfShape (Discrete α) C
F : Discrete α ⥤ Ind C
I : α → Type v := fun s ↦ (F.obj { as := s }).presentation.I
G : (s : α) → I s ⥤ C := fun s ↦ (F.obj { as := s }).presentation.F
⊢ HasColimit F
Module: Mathlib.CategoryTheory.Abelian.Indization

Goal state before:
pp: C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w✝¹ : SmallCategory I
w✝ : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map ϕ)
i' : Arrow.mk (coimageImageComparison f) ≅ Arrow.mk (coimageImageComparison ((Ind.lim I).map ϕ)) :=
  coimageImageComparisonFunctor.mapIso i
⊢ IsIso (coimageImageComparison f)

Tactic:
have := Iso.isIso_hom i'

Goal state after:
C : Type v
inst✝¹ : SmallCategory C
inst✝ : Abelian C
X Y : Ind C
f : X ⟶ Y
I : Type v
w✝¹ : SmallCategory I
w✝ : IsFiltered I
F G : I ⥤ C
ϕ : F ⟶ G
i : Arrow.mk f ≅ Arrow.mk ((Ind.lim I).map ϕ)
i' : Arrow.mk (coimageImageComparison f) ≅ Arrow.mk (coimageImageComparison ((Ind.lim I).map ϕ)) :=
  coimageImageComparisonFunctor.mapIso i
this : IsIso i'.hom
⊢ IsIso (coimageImageComparison f)
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ Action V G
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ forget V G)
F' : C ⥤ SingleObj G ⥤ V := F ⋙ (functorCategoryEquivalence V G).functor
this : PreservesColimit K F'
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_reflects_of_preserves F (Action.functorCategoryEquivalence V G).functor

Goal state after:
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
J : Type u_3
inst✝¹ : Category.{v_2, u_3} J
K : J ⥤ Action V G
inst✝ : HasLimit (K ⋙ forget V G)
⊢ PreservesLimit K (forget V G)

Tactic:
by
  change PreservesLimit K ((Action.functorCategoryEquivalence V G).functor ⋙
    (evaluation (SingleObj G) V).obj (SingleObj.star G))
  have (k : SingleObj G) :
      HasLimit ((K ⋙ (functorCategoryEquivalence V G).functor).flip.obj k) :=
    inferInstanceAs (HasLimit (K ⋙ forget V G))
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Nonempty (NormalMono f)

Tactic:
rw [mono_iff L P] at hf

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Abelian C
D : Type u'
inst✝⁴ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝³ : P.IsSerreClass
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X✝ Y✝ : D
f : X✝ ⟶ Y✝
hf : ∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)
⊢ Nonempty (NormalMono f)
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (f : Fin (n + 1) → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)
f : Fin (n + 1 + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).hom.hom) f = (f 0, fun i ↦ (f i.castSucc)⁻¹ * f i.succ)

Tactic:
| succ n hn =>

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

Goal state before:
pp: case succ
G : Type u
inst✝ : Group G
n : ℕ
hn :
  ∀ (g : G) (f : Fin n → G),
    (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
g : G
f : Fin (n + 1) → G
⊢ (ConcreteCategory.hom (diagonalSuccIsoTensorTrivial G (n + 1)).inv.hom) (g, f) = g • Fin.partialProd f

Tactic:
| succ n hn =>

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

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
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ Epi (t.rightToLeft.app X) ↔ Epi (H.map (t.adj₁.unit.app X))

Tactic:
← epi_comp_iff_of_isIso _ (t.adj₂.unit.app (F.obj X)),

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ Epi (t.rightToLeft.app X ≫ t.adj₂.unit.app (F.obj X)) ↔ Epi (H.map (t.adj₁.unit.app X))
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X : PartialFun
⊢ partialFunToPointed.map
        ((NatIso.ofComponents
                (fun X ↦
                  PartialFun.Iso.mk
                    { toFun := fun a ↦ ⟨some a, ⋯⟩, invFun := fun a ↦ Option.get ↑a ⋯, left_inv := ⋯, right_inv := ⋯ })
                ⋯).hom.app
          X) ≫
      (NatIso.ofComponents (fun X ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯).hom.app
        (partialFunToPointed.obj X) =
    𝟙 (partialFunToPointed.obj X)

Tactic:
ext (_ | x)
    · rfl
    · simp
      rfl

Goal state after:
Module: Mathlib.CategoryTheory.Dialectica.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply le_of_eq

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
e₁ : X.src ≅ Y.src
e₂ : X.tgt ≅ Y.tgt
eq : X.rel = (Subobject.pullback (prod.map e₁.hom e₂.hom)).obj Y.rel
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ f = p.map φ

Tactic:
by simpa using h.symm

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.HomLift

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ f = p.map φ

Tactic:
by simpa using h.symm

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ ⋯ (map p g ψ ⋯ τ)

Tactic:
intro π'

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCartesian f φ
inst✝ : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
⊢ (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) π' → π' = map p f φ ⋯ (map p g ψ ⋯ τ)
Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ ∀ (y : a' ⟶ a), (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)

Tactic:
intro π'

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCartesian g ψ
inst✝¹ : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
⊢ (fun χ ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) π' → π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (τ ≫ ψ)
Module: Mathlib.CategoryTheory.Enriched.FunctorCategory

Goal state before:
pp: V : Type u₁
inst✝⁶ : Category.{v₁, u₁} V
inst✝⁵ : MonoidalCategory V
C : Type u₂
inst✝⁴ : Category.{v₂, u₂} C
J : Type u₃
inst✝³ : Category.{v₃, u₃} J
inst✝² : EnrichedOrdinaryCategory V C
F₁ F₂ : J ⥤ C
inst✝¹ : HasEnrichedHom V F₁ F₁
inst✝ : HasEnrichedHom V F₁ F₂
⊢ (λ_ (enrichedHom V F₁ F₂)).inv ≫ enrichedId V F₁ ▷ enrichedHom V F₁ F₂ ≫ enrichedComp V F₁ F₁ F₂ =
    𝟙 (enrichedHom V F₁ F₂)

Tactic:
by
  ext j
  rw [assoc, assoc, enrichedComp_π, id_comp, tensorHom_def, assoc,
    ← comp_whiskerRight_assoc, enrichedId_π, ← whisker_exchange_assoc,
    id_whiskerLeft, assoc, assoc, Iso.inv_hom_id_assoc]
  dsimp
  rw [e_id_comp, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: 𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst✝² : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst✝¹ : p.IsHomLift g ψ
inst✝ : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
⊢ ψ = ψ'

Tactic:
by
  rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' h.symm]

Goal state after:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
⊢ ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y → y = map p g ψ ⋯ (map p f φ ⋯ τ)

Tactic:
intro π'

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝³ : Category.{v₁, u₁} 𝒮
inst✝² : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝¹ : p.IsStronglyCocartesian f φ
inst✝ : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
⊢ (fun χ ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) π' → π' = map p g ψ ⋯ (map p f φ ⋯ τ)
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
intro π'

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
π' : c ⟶ c'
⊢ (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) π' → π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
Module: Mathlib.CategoryTheory.Galois.Basic

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
h : ¬Nonempty (F.obj X).obj
⊢ False

Tactic:
have ⟨hin⟩ : Nonempty (IsInitial X) := (initial_iff_fiber_empty F X).mpr (not_nonempty_iff.mp h)

Goal state after:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsConnected X
h : ¬Nonempty (F.obj X).obj
hin : IsInitial X
⊢ False