mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
c d : ℝ
hd : 1 ≤ d ^ 2
H1 : (c * z.re + d) ^ 2 + (c * z.im) ^ 2 = c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
H2 :
  (c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2) * (z.re ^ 2 + z.im ^ 2) - z.im ^ 2 =
    (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2
⊢ 0 ≤ (c * (z.re ^ 2 + z.im ^ 2) + d * z.re) ^ 2 + (d ^ 2 - 1) * z.im ^ 2

Tactic:
exact add_nonneg (sq_nonneg _) (mul_nonneg (sub_nonneg.mpr hd) (sq_nonneg _))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
n : ℕ
hn : Odd n
⊢ L.G n = 0

Tactic:
rw [← CharZero.eq_neg_self_iff, G, ← tsum_neg, ← (Equiv.neg _).tsum_eq]

Goal state after:
L : PeriodPair
n : ℕ
hn : Odd n
⊢ ∑' (c : ↥L.lattice), (↑((Equiv.neg ↥L.lattice) c) ^ n)⁻¹ = ∑' (b : ↥L.lattice), -(↑b ^ n)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Set.Icc (-1) 1
h✝ : IsExtrOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
h : IsMinOn (fun x ↦ eval x (T ℝ ↑n)) (Set.Icc (-1) 1) x
⊢ cos (1 * π / ↑n) ∈ Set.Icc (-1) 1

Tactic:
grind [abs_cos_le_one]

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

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

Tactic:
by
  rw [arithGeom_same_eq_mul_div' ha n, ← neg_sub _ a, div_neg,
    ← neg_sub _ (a ^ (n + 1)), mul_neg, neg_div, neg_neg]

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

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝² : Field R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ StrictMono (arithGeom a b u₀)

Tactic:
by
  refine strictMono_nat_of_lt_succ fun n ↦ ?_
  have h_lt : b / (1 - a) < arithGeom a b u₀ n := div_lt_arithGeom (by positivity) ha.ne' h0 n
  rw [div_lt_iff_of_neg (sub_neg.mpr ha)] at h_lt
  rw [arithGeom_succ]
  linarith

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: n : ℤ
⊢ fib (n + 1) = fib (n + 2) - fib n

Tactic:
by
  simp only [fib_add_two, add_sub_cancel_left]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
i : ℕ
h1 : x + ↑(↑i + 1) ≠ 0
⊢ x - (↑i + 1) ≠ 0

Tactic:
simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hx (-(i + 1))

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j

Tactic:
by
  rw [logDeriv_prod]
  · simp_rw [logDeriv_sineTerm_eq_cotTerm hx]
  · exact fun i _ ↦ sineTerm_ne_zero hx i
  · fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case ha
x : ℂ
hz : x ∈ ℂ_ℤ
n : ℕ
⊢ x - (↑n + 1) ≠ 0

Tactic:
simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hz (-(n + 1) : ℤ)

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:

Tactic:
_ = φ * (Nat.fib n) + φ ^ 2 * (Nat.fib (n + 1)) := by
        simp only [Nat.fib_add_one (Nat.succ_ne_zero n), Nat.succ_sub_succ_eq_sub,
          Nat.cast_add, goldenRatio_sq, Nat.sub_zero]; ring
      _ = φ * ((Nat.fib n) + φ * (Nat.fib (n + 1))) := by ring
      _ = φ ^ (n + 2) := by rw [add_comm, ih]; ring

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x ^ (↑k + 1 - 1) * rexp (-(c * x)) = ↑k ! / c ^ (k + 1)

Tactic:
simp_rw [key, Gamma_nat_eq_factorial, div_eq_mul_inv,
          one_mul, mul_comm, inv_rpow hc.le, ← rpow_natCast]

Goal state after:
k : ℕ
M c : ℝ
hM : 0 ≤ M
hc : 0 < c
hk : 0 < ↑k + 1
key : ∫ (t : ℝ) in Ioi 0, t ^ (↑k + 1 - 1) * rexp (-(c * t)) = (1 / c) ^ (↑k + 1) * Gamma (↑k + 1)
hint : IntegrableOn (fun x ↦ x ^ (↑k + 1 - 1) * rexp (-(c * x))) (Ioi 0) volume
⊢ ↑k ! * (c ^ (↑k + 1))⁻¹ = ↑k ! * (c ^ ↑(k + 1))⁻¹
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 : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n

Tactic:
have L : ∀ᶠ n in atTop, u (c n) - c n * l ≤ ε * c n := by
      rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ,
        Asymptotics.isLittleO_iff] at clim
      filter_upwards [clim εpos, ctop (Ioi_mem_atTop 0)] with n hn cnpos'
      have cnpos : 0 < c n := cnpos'
      calc
        u (c n) - c n * l = (u (c n) / c n - l) * c n := by field
        _ ≤ ε * c n := by
          gcongr
          refine (le_abs_self _).trans ?_
          simpa using hn

Goal state after:
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 : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
⊢ ∀ᶠ (n : ℕ) in atTop, u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case hg
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ IntegrableOn (fun x ↦ f x * g (x - 1)) (Ico ↑a ↑b) volume

Tactic:
apply Integrable.mono_measure _ (volume.restrict_mono_set Ico_subset_Icc_self)
    apply (hf.integrableOn_isCompact isCompact_Icc).mul_of_top_left
    apply MonotoneOn.memLp_isCompact isCompact_Icc
    intro _ _ _ _ _
    apply hg <;> grind

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Final

Goal state before:
pp: case refine_1
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
⊢ ∃ W x x, True

Tactic:
obtain ⟨Q⟩ : Nonempty (CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))) :=
        IsCofiltered.nonempty

Goal state after:
case refine_1
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
j₁ j₂ : Comma L R
Q : CostructuredArrow L (R.obj (IsCofiltered.min j₁.right j₂.right))
⊢ ∃ W x x, True
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι : Type u_2
inst✝⁵ : HasProductsOfShape ι C
inst✝⁴ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst✝³ : (i : ι) → SmallCategory (J i)
inst✝² : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
inst✝¹ : ∀ (i : ι), HasColimit (F i)
inst✝ : HasColimit (pointwiseProduct F)
⊢ IsIso ((colimit.isColimit (pointwiseProduct F)).desc (coconePointwiseProduct fun s ↦ colimit.cocone (F s)))

Tactic:
refine ((colimit.isColimit (pointwiseProduct F)).nonempty_isColimit_iff_isIso_desc).mp ?_

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
ι : Type u_2
inst✝⁵ : HasProductsOfShape ι C
inst✝⁴ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
J : ι → Type w
inst✝³ : (i : ι) → SmallCategory (J i)
inst✝² : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
inst✝¹ : ∀ (i : ι), HasColimit (F i)
inst✝ : HasColimit (pointwiseProduct F)
⊢ Nonempty (IsColimit (coconePointwiseProduct fun s ↦ colimit.cocone (F s)))
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ IsColimit (coconePointwiseProduct c)

Tactic:
apply IsColimit.equivOfNatIsoOfIso _ _ _ _ <|
        h.whiskerEquivalence (Pi.equivalenceOfEquiv J e).symm

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ ((Pi.equivalenceOfEquiv J e).symm.functor ⋙ pointwiseProduct fun i ↦ F (e i)) ≅ pointwiseProduct F

C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
inst✝² : HasProductsOfShape ι C
ι' : Type u_3
inst✝¹ : HasProductsOfShape ι' C
inst✝ : IsIPCOfShape.{w, u_2, v_1, u_1} ι C
e : ι ≃ ι'
J : ι' → Type w
x✝¹ : (i : ι') → SmallCategory (J i)
x✝ : ∀ (i : ι'), IsFiltered (J i)
F : (i : ι') → J i ⥤ C
c : (i : ι') → Cocone (F i)
hc : (i : ι') → IsColimit (c i)
h : IsColimit (coconePointwiseProduct fun i ↦ c (e i))
⊢ (Cocone.precompose (Iso.inv ?m.48)).obj
      (Cocone.whisker (Pi.equivalenceOfEquiv J e).symm.functor (coconePointwiseProduct fun i ↦ c (e i))) ≅
    coconePointwiseProduct c
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
inst✝³ : HasProductsOfShape ι C
inst✝² : IsIPCOfShape.{w, u_1, v, u} ι C
inst✝¹ : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ D ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
refine ⟨evaluationJointlyReflectsColimits _ fun X ↦ ?_⟩

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
ι : Type u_1
inst✝³ : HasProductsOfShape ι C
inst✝² : IsIPCOfShape.{w, u_1, v, u} ι C
inst✝¹ : HasFilteredColimitsOfSize.{w, w, v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ D ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
X : D
⊢ IsColimit (((evaluation D C).obj X).mapCocone (coconePointwiseProduct c))
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
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
E : Type u''
inst✝¹ : Category.{v'', u''} E
inst✝ : Abelian E
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : P.isoModSerre s
eq : f₁ ≫ s = f₂ ≫ s
⊢ P.isoModSerre (kernel.ι (f₁ - f₂))

Tactic:
rw [isoModSerre_iff_of_mono]
      exact P.prop_of_iso (Abelian.coimageIsoImage (f₁ - f₂)).symm
        ((exists_comp_isoModSerre_eq_zero_iff P _).1 ⟨_ ,s, hs, by simpa [sub_eq_zero]⟩)

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
X : Action V PUnit.{?u.12 + 1}
x✝ : PUnit.{?u.12 + 1}
⊢ ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).ρ PUnit.unit ≫ (Iso.refl ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).V).hom =
    (Iso.refl ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).V).hom ≫
      ((forget V PUnit.{?u.12 + 1} ⋙
                { obj := fun X ↦ { V := X, ρ := 1 }, map := fun {X Y} f ↦ { hom := f, comm := ⋯ }, map_id := ⋯,
                  map_comp := ⋯ }).obj
            X).ρ
        PUnit.unit

Tactic:
simp only [Functor.id_obj, MonoidHom.one_apply, End.one_def, Functor.comp_obj,
        forget_obj, Iso.refl_hom, Category.comp_id]
      exact ρ_one X

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
⊢ PreservesFiniteLimits L

Tactic:
let := abelian L P

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
this : Abelian D := abelian L P
⊢ PreservesFiniteLimits L
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
⊢ PreservesFiniteColimits L

Tactic:
let := abelian L P

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
this : Abelian D := abelian L P
⊢ PreservesFiniteColimits L
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 : C
f : X ⟶ Y
⊢ IsIso (L.map f) ↔ P.isoModSerre f

Tactic:
let := abelian L P

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 : C
f : X ⟶ Y
this : Abelian D := abelian L P
⊢ IsIso (L.map f) ↔ P.isoModSerre f
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits G

Tactic:
let := abelian L P

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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this : Abelian D := abelian L P
⊢ PreservesFiniteLimits (L ⋙ G) ↔ PreservesFiniteLimits G
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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G

Tactic:
let := abelian L P

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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
this : Abelian D := abelian L P
⊢ PreservesFiniteColimits (L ⋙ G) ↔ PreservesFiniteColimits G
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
H : D ⥤ E
J : Type u
inst✝³ : Category.{v, u} J
inst✝² : HasColimitsOfShape J C
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ PreservesColimitsOfShape J H ↔ PreservesColimitsOfShape J (F ⋙ H)

Tactic:
have := adj.isLeftAdjoint
  refine ⟨fun _ ↦ inferInstance, fun _ ↦ ⟨fun {K} ↦ ?_⟩⟩
  let iso : (K ⋙ G) ⋙ F ≅ K :=
    Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ K.rightUnitor
  refine preservesColimit_of_preserves_colimit_cocone
    ((IsColimit.precomposeInvEquiv iso _).symm
      (isColimitOfPreserves F (colimit.isColimit (K ⋙ G)))) ?_
  exact IsColimit.ofIsoColimit
    ((IsColimit.precomposeInvEquiv
      ((Functor.associator _ _ _).symm ≪≫ Functor.isoWhiskerRight iso H) _).symm
        (isColimitOfPreserves (F ⋙ H) (colimit.isColimit (K ⋙ G))))
          (Cocone.ext (Iso.refl _))

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
inst✝ : HasReflexiveCoequalizers A
h : (X : B) → RegularEpi (adj₁.counit.app X)
Y : A
X : B
⊢ { f // F'.map (U.map (adj₁.counit.app X)) ≫ f = otherMap R F' adj₁ adj₂ X ≫ f } ≃
    { g // U.map (F.map g ≫ adj₁.counit.app (R.obj Y)) = U.map (adj₁.counit.app X) ≫ g }

Tactic:
by
      apply (adj₂.homEquiv _ _).subtypeEquiv _
      intro f
      rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, adj₂.homEquiv_naturality_left,
        otherMap, assoc, adj₂.homEquiv_naturality_left, ← adj₂.counit_naturality,
        adj₂.homEquiv_naturality_left, adj₂.homEquiv_unit, adj₂.right_triangle_components,
        comp_id, Functor.comp_map, ← U.map_comp, assoc]
      dsimp
      rw [← adj₁.counit_naturality]
      simp [dsimp% adj₂.homEquiv_unit _ _ f ]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Monad.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.map (𝟙 { as := { as := () } }) ◁ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
          F.map (𝟙 { as := { as := () } }) ◁ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) =
    F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ▷ F.map (𝟙 { as := { as := () } }) ≫
          F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ▷ F.map (𝟙 { as := { as := () } }) ≫
            (α_ (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
                (F.map (𝟙 { as := { as := () } }))).hom

Tactic:
← F.mapComp_naturality_left_assoc,

Goal state after:
B : Type u
inst✝ : Bicategory B
a : B
F : LocallyDiscrete (Discrete Unit) ⥤ᵒᵖᴸ B
⊢ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
        F.map (𝟙 { as := { as := () } }) ◁ F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
          F.map (𝟙 { as := { as := () } }) ◁ F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) =
    F.map₂ (ρ_ (𝟙 { as := { as := () } })).inv ≫
      F.map₂ ((ρ_ (𝟙 { as := { as := () } })).inv ▷ 𝟙 { as := { as := () } }) ≫
        F.mapComp (𝟙 { as := { as := () } } ≫ 𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ≫
          F.mapComp (𝟙 { as := { as := () } }) (𝟙 { as := { as := () } }) ▷ F.map (𝟙 { as := { as := () } }) ≫
            (α_ (F.map (𝟙 { as := { as := () } })) (F.map (𝟙 { as := { as := () } }))
                (F.map (𝟙 { as := { as := () } }))).hom
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{?u.4, u_1} C
I : Type u_2
D : I → Type u_3
inst✝³ : (i : I) → Category.{?u.13, u_3} (D i)
F : (i : I) → C ⥤ D i
hF : JointlyReflectIsomorphisms F
J : Type u_4
inst✝² : Category.{v_1, u_4} J
G : J ⥤ C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst✝¹ : HasColimit G
inst✝ : ∀ (i : I), PreservesColimit G (F i)
⊢ IsColimit c

Tactic:
suffices IsIso (colimit.desc _ c) from
    IsColimit.ofIsoColimit (colimit.isColimit _)
      (Cocone.ext (asIso (colimit.desc _ c) :))
  rw [hF.isIso_iff]
  intro i
  let H := isColimitOfPreserves (F i) (colimit.isColimit G)
  let e := IsColimit.coconePointUniqueUpToIso H (hc i)
  have : e.hom = (F i).map (colimit.desc G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsColimit.comp_coconePointUniqueUpToIso_hom H (hc i) j)
  rw [← this]
  infer_instance

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

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).obj
i : ι
⊢ (ConcreteCategory.hom (Pi.π X i)) ((productEquiv X).symm x) = x i

Tactic:
by
  rw [← productEquiv_apply, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.SingleObj

Goal state before:
pp: G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
⊢ J.ColimitTypeRel ⟨SingleObj.star G, x⟩ ⟨SingleObj.star G, y⟩ ↔ (MulAction.orbitRel G (J.obj (SingleObj.star G))) y x

Tactic:
change (∃ g : G, y = g • x) ↔ (∃ g : G, g • x = y)

Goal state after:
G : Type v
inst✝ : Group G
J : SingleObj G ⥤ Type u
x y : J.obj (SingleObj.star G)
⊢ (∃ g, y = g • x) ↔ ∃ g, g • x = y
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 Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
⊢ Nat.card (F.obj X).obj < Nat.card (F.obj Y).obj

Tactic:
by_contra hlt
  apply h
  apply isIso_of_mono_of_eq_card_fiber F f
  simp only [not_lt] at hlt
  exact Nat.le_antisymm
    (Nat.card_le_card_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

Goal state after:
Module: Mathlib.CategoryTheory.Galois.Topology

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝¹ : GaloisCategory C
inst✝ : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w✝ : Fintype ↑I
hc : ∀ X ∈ I, IsConnected X
hmem : ∀ (σ : Aut F), (∀ (X : ↑I), σ.hom.app ↑X = 𝟙 (F.obj ↑X)) → σ ∈ U
P : C := ∏ᶜ fun X ↦ ↑X
A : C
a : (F.obj A).obj
hgal : IsGalois A
hbij : Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f)) a
t : Aut F
ht : (ConcreteCategory.hom (t.hom.app A)) a = a
this✝ : ∀ (X : ↑I), IsConnected ↑X
this : ∀ (X : ↑I), Nonempty (F.obj ↑X).obj
X : ↑I
f : A ⟶ P
⊢ (ConcreteCategory.hom (t.hom.app ↑X))
      ((ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)) =
    (ConcreteCategory.hom (F.map (Pi.π (fun X ↦ ↑X) X))) ((fun f ↦ (ConcreteCategory.hom (F.map f)) a) f)

Tactic:
rw [NatTrans.naturality_apply, NatTrans.naturality_apply, ht]

Goal state after: