mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
r : ℝ
hx : Germ.Tendsto x atTop
⊢ ↑r < x

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩
  rw [tendsto_ofSeq] at hx
  exact ofSeq_lt_ofSeq.2 <| hx.eventually_mem (Ioi_mem_atTop r)

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x : ℝ*
hni : ¬x.Infinite
⊢ x.IsSt (sSup {y | ↑y < x})

Tactic:
rw [infinite_iff, not_lt] at hni

Goal state after:
x : ℝ*
hni : 0 ≤ ArchimedeanClass.mk x
⊢ x.IsSt (sSup {y | ↑y < x})
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
hx : x.Infinitesimal
hy : y.Infinitesimal
⊢ (x * y).Infinitesimal

Tactic:
simpa only [mul_zero] using! hx.mul hy

Goal state after:
Module: Mathlib.Analysis.Real.Hyperreal

Goal state before:
pp: x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-(x * y)).InfinitePos

Tactic:
neg_mul_eq_neg_mul

Goal state after:
x y : ℝ*
⊢ (-x).InfinitePos → ¬y.Infinitesimal → 0 < y → (-x * y).InfinitePos
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (cexp 0 - cexp (z.arctan * I) * cexp (z.arctan * I)) / (cexp (z.arctan * I) * cexp (z.arctan * I) + cexp 0) * I = z

Tactic:
exp_zero,

Goal state after:
z : ℂ
h₁ : z ≠ I
h₂ : z ≠ -I
⊢ (1 - cexp (z.arctan * I) * cexp (z.arctan * I)) / (cexp (z.arctan * I) * cexp (z.arctan * I) + 1) * I = z
Module: Mathlib.Analysis.Real.Pi.Wallis

Goal state before:
pp: case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (k + 1)

Tactic:
| succ k hk =>

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arctan

Goal state before:
pp: case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ 2 * z.re ≤ π

Tactic:
← le_div_iff₀' two_pos

Goal state after:
case hx₂
z : ℂ
h₀ : z ≠ ↑π / 2
h₁ : -(π / 2) < z.re
h₂ : z.re ≤ π / 2
h : cos z ≠ 0
⊢ z.re ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
n m k : ℕ
⊢ (x.agmSequences y k).1 ≤ (x.agmSequences y k).2

Tactic:
induction k generalizing x y with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean

Goal state before:
pp: x y : ℝ≥0
h : x ≠ y
n m k : ℕ
⊢ (x.agmSequences y k).1 < (x.agmSequences y k).2

Tactic:
induction k generalizing x y with

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto

Goal state before:
pp: s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
⊢ TendstoUniformlyOn (fun p x ↦ p⁻¹ * (x ^ p - 1)) log (𝓝[>] 0) s

Tactic:
Metric.uniformity_basis_dist_le.tendstoUniformlyOn_iff_of_uniformity

Goal state after:
s : Set ℝ
hs : s ⊆ Ioi 0
hs' : IsCompact s
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (n : ℝ) in 𝓝[>] 0, ∀ x ∈ s, (log x, n⁻¹ * (x ^ n - 1)) ∈ {p | dist p.1 p.2 ≤ i}
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
u : ℝ → E := fun x ↦ x⁻¹ • f x
key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x)
⊢ ∫ (x : ℝ) in ε..r, c • u (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x

Tactic:
intervalIntegral.integral_smul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
c ε r : ℝ
hc : c ≠ 0
u : ℝ → E := fun x ↦ x⁻¹ • f x
key : (fun x ↦ x⁻¹ • f (c * x)) = fun x ↦ c • u (c * x)
⊢ c • ∫ (x : ℝ) in ε..r, u (c * x) = ∫ (x : ℝ) in c * ε..c * r, x⁻¹ • f x
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
simp_rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero),
      Complex.sin_pi_div_two_sub]

Goal state after:
s : ℂ
⊢ ↑π ^ ((s - 1) / 2 + (-1 - s) / 2 + 1) / cos (↑π * s / 2) = (cos (↑π * s / 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ ∀ (x : ℕ), ¬s = -(2 * ↑x)

Tactic:
intro n h

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
n : ℕ
h : s = -(2 * ↑n)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)

Tactic:
intro n h

Goal state after:
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
n : ℕ
h : s = -(2 * ↑n + 1)
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (-b ^ x) = x

Tactic:
logb_neg_eq_logb,

Goal state after:
case h.right
b : ℝ
b_pos : 0 < b
b_ne_one : b ≠ 1
x : ℝ
a✝ : x ∈ univ
⊢ logb b (b ^ x) = x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ MonotoneOn (cfcₙ (p.rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
intro a (ha : 0 ≤ a) b (hb : 0 ≤ b) hab

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
a : A
ha : 0 ≤ a
b : A
hb : 0 ≤ b
hab : a ≤ b
⊢ cfcₙ (p.rpowIntegrand₀₁ t) a ≤ cfcₙ (p.rpowIntegrand₀₁ t) b
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < 0 ↔ 1 < x

Tactic:
rw [← @logb_one b, logb_lt_logb_iff_of_base_lt_one b_pos b_lt_one h zero_lt_one]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ P.real Kᶜ < √ε * √ε

Tactic:
mul_self_sqrt (le_of_lt hε)

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : P Kᶜ < ↑ε.toNNReal
⊢ P.real Kᶜ < ε
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ μ.toSphere univ = 0 ↔ dim E = 0

Tactic:
toSphere_apply_univ

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
⊢ ↑(dim E) * μ (ball 0 1) = 0 ↔ dim E = 0
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ (volumeIoiPow n) (Iio x) = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
volumeIoiPow,

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ((comap Subtype.val volume).withDensity fun r ↦ ENNReal.ofReal (↑r ^ n)) (Iio x) =
    ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: case neg
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
hb : ∃ k ∈ b, k = -↑n
⊢ regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))

Tactic:
obtain ⟨j, hj⟩ := hb

Goal state after:
case neg
a b : Multiset ℂ
n : ℕ
h : regularizedHGFunCoeff a b n ≠ 0
j : ℂ
hj : j ∈ b ∧ j = -↑n
⊢ regularizedHGFunCoeff a b (n + 1) / regularizedHGFunCoeff a b n =
    (Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z : ℂ
l : ↥L.lattice
⊢ ℘'[L - l₀] (z + ↑l) = ℘'[L - l₀ - ↑l] z

Tactic:
by
  simp only [derivWeierstrassPExcept]
  rw [← (Equiv.addRight l).tsum_eq]
  simp only [Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub, eq_sub_iff_add_eq]

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

Goal state before:
pp: case neg
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∉ L.lattice
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
· have := L.weierstrassPExcept_add_coe_aux 0 (zero_mem _) l hl (x := z) (by simp [hz])
    simp only [zero_sub, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, div_zero,
      even_two, Even.neg_pow, one_div] at this
    rw [← L.weierstrassPExcept_add 0, Submodule.coe_zero, this, ← L.weierstrassPExcept_add (-l)]
    simp
    ring

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

Goal state before:
pp: x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x

Tactic:
rcases em (x = -1) with (rfl | h')

Goal state after:
case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - (-1) ^ 2)) (Iic (-1)) (-1)

case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : LocallyFiniteOrder α
⊢ Monotone fun n ↦ Icc (-↑n) ↑n

Tactic:
by
  refine fun m n hmn ↦ by apply Icc_subset_Icc <;> simpa using Nat.mono_cast hmn

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + (↑c * z).im ^ 2

Tactic:
im_ofReal_mul,

Goal state after:
c d : ℝ
hc : 1 ≤ c ^ 2
z : ℂ
hz : 0 < z.im
⊢ z.im ^ 2 ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
⊢ eval x (T ℝ ↑n) = 0

Tactic:
obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((2 * ↑k + 1) * π / (2 * ↑n)) = x
⊢ eval x (T ℝ ↑n) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
⊢ eval x (U ℝ ↑n) = 0

Tactic:
obtain ⟨k, hk, hx⟩ := Finset.mem_image.mp hx

Goal state after:
case refine_1
n : ℕ
hn : n ≠ 0
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)
k : ℕ
hk : k ∈ Finset.range n
hx : cos ((↑k + 1) * π / (↑n + 1)) = x
⊢ eval x (U ℝ ↑n) = 0
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:
unfold arithGeom

Goal state after:
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)
⊢ a * arithGeom a b u₀ n + b = a ^ (n + 1) * (u₀ - b / (1 - a)) + b / (1 - a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
k : ℕ∞
hx : x ∈ ℂ_ℤ
⊢ ContDiffWithinAt ℂ (↑k)
    (fun x ↦ (cexp (↑π * x * I) + cexp (-(↑π * x) * I)) / 2 / ((cexp (-(↑π * x) * I) - cexp (↑π * x * I)) * I / 2)) ℍₒ x

Tactic:
exact ContDiffWithinAt.div (by fun_prop) (by fun_prop) (sin_pi_mul_ne_zero hx)

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

Goal state before:
pp: ⊢ 0 < 1 + √5

Tactic:
apply add_pos

Goal state after:
case ha
⊢ 0 < 1

case hb
⊢ 0 < √5
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + iteratedDerivWithin k (fun x ↦ -(1 / x)) ℍₒ z =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -((-1) ^ k * ↑k ! * z ^ (-1 + -↑k))

Tactic:
simpa [iteratedDerivWithin_fun_neg] using! iteratedDerivWithin_one_div k
      isOpen_upperHalfPlaneSet hz

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + ↑n) ^ (k + 1) = (z + ↑n) ^ (-1 - ↑k)

Tactic:
show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; lia,

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + ↑n) ^ (k + 1) = (z + ↑n) ^ (-↑(k + 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + ↑n) ^ (k + 1) = (z + ↑n) ^ (-↑(k + 1))

Tactic:
zpow_neg_coe_of_pos _ (by lia),

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
n : ℤ
⊢ 1 / (z + ↑n) ^ (k + 1) = ((z + ↑n) ^ (k + 1))⁻¹
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
⊢ (finiteSubcoproductsCocone f).ι.app S = ∑ a ∈ S.attach, Sigma.π (fun a ↦ f (↑a).as) a ≫ Sigma.ι f (↑a).as

Tactic:
by
  dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
    Functor.const_obj_obj, finiteSubcoproductsCocone_ι_app]
  ext v
  simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, Preadditive.comp_sum]
  rw [Finset.sum_eq_single v]
  · simp
  · intro b hb hb₁
    rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.RightDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
⊢ (I.isoRightDerivedToHomotopyCategoryObj F).inv ≫ F.rightDerivedToHomotopyCategory.map f =
    (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.up ℕ)).map φ ≫
      (J.isoRightDerivedToHomotopyCategoryObj F).inv

Tactic:
rw [← cancel_epi (I.isoRightDerivedToHomotopyCategoryObj F).hom, Iso.hom_inv_id_assoc]
    dsimp
    rw [← isoRightDerivedToHomotopyCategoryObj_hom_naturality_assoc f I J φ comm F,
      Iso.hom_inv_id, comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
W : MorphismProperty C
⊢ ∀ {X Y : C} (x : X ≅ Y), W.kernels X → W.kernels Y

Tactic:
rintro _ _ i ⟨f, k, hk, hf⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
W : MorphismProperty C
Y✝ X₁✝ X₂✝ : C
f : X₁✝ ⟶ X₂✝
k : KernelFork f
hk : IsLimit k
hf : W f
i : k.pt ≅ Y✝
⊢ W.kernels Y✝
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
W : MorphismProperty C
⊢ ∀ {X Y : C} (x : X ≅ Y), W.cokernels X → W.cokernels Y

Tactic:
rintro _ _ i ⟨f, k, hk, hf⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
W : MorphismProperty C
Y✝ X₁✝ X₂✝ : C
f : X₁✝ ⟶ X₂✝
k : CokernelCofork f
hk : IsColimit k
hf : W f
i : k.pt ≅ Y✝
⊢ W.cokernels Y✝
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : N
⊢ (rightHom.comp inl) x✝ = 1 x✝

Tactic:
simp [rightHom]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
x✝ : G
⊢ (rightHom.comp inr) x✝ = (MonoidHom.id G) x✝

Tactic:
simp [rightHom]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
n : N
⊢ rightHom (inl n) = 1

Tactic:
simp [rightHom]

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
⊢ rightHom (inr g) = g

Tactic:
simp [rightHom]

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 : C
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.EssSurj
⊢ PreservesLimit (parallelPair f 0) L

Tactic:
suffices ∀ (W : D) (z : W ⟶ L.obj X) (hz : z ≫ L.map f = 0),
      ∃ (l : W ⟶ L.obj (kernel f)), l ≫ L.map (kernel.ι f) = z from
    preservesLimit_of_preserves_limit_cone (kernelIsKernel f)
      ((KernelFork.isLimitMapConeEquiv _ L).2
        (Fork.IsLimit.ofExistsUnique
          (fun s ↦ existsUnique_of_exists_of_unique
            (this _ _ (KernelFork.condition s))
            (fun _ _ h₁ h₂ ↦ by simpa [cancel_mono] using h₁.trans h₂.symm))))

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✝ : L.PreservesMonomorphisms
this : L.EssSurj
⊢ ∀ (W : D) (z : W ⟶ L.obj X), z ≫ L.map f = 0 → ∃ l, l ≫ L.map (kernel.ι f) = z
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
W : Type u_2
inst✝¹ : Category.{v_2, u_2} W
F : V ⥤ W
G : Type u_3
inst✝ : Monoid G
M : Action V G
g h : G
⊢ F.map (M.ρ (g * h)) = F.map (M.ρ g) * F.map (M.ρ h)

Tactic:
by
            dsimp
            rw [map_mul, End.mul_def, F.map_comp]

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
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
this✝² : HasFiniteProducts D
this✝¹ : HasKernels D
this✝ : HasCokernels D
this : IsNormalMonoCategory D
⊢ Abelian D

Tactic:
have := isNormalEpiCategory 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
this✝³ : HasFiniteProducts D
this✝² : HasKernels D
this✝¹ : HasCokernels D
this✝ : IsNormalMonoCategory D
this : IsNormalEpiCategory D
⊢ Abelian D
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F
map_coeval : F.map coeval = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y
⊢ F.map (Y ◁ coeval ≫ (α_ Y X Y).inv ≫ eval ▷ Y) = F.map ((ρ_ Y).hom ≫ (λ_ Y).inv)

Tactic:
by
      simp [map_eval, map_coeval, Functor.Monoidal.map_whiskerLeft,
        Functor.Monoidal.map_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence

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✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory D
F : C ⥤ D
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
X Y : C
eval : Y ⊗ X ⟶ 𝟙_ C
coeval : 𝟙_ C ⟶ X ⊗ Y
inst✝ : ExactPairing (F.obj X) (F.obj Y)
map_eval : F.map eval = δ F Y X ≫ ε_ (F.obj X) (F.obj Y) ≫ ε F
map_coeval : F.map coeval = η F ≫ η_ (F.obj X) (F.obj Y) ≫ μ F X Y
⊢ F.map (coeval ▷ X ≫ (α_ X Y X).hom ≫ X ◁ eval) = F.map ((λ_ X).hom ≫ (ρ_ X).inv)

Tactic:
by
      simp [map_eval, map_coeval, Functor.Monoidal.map_whiskerLeft,
        Functor.Monoidal.map_whiskerRight]

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

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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ f ≫ U'.map (F.map (adj₁.unit.app X)) = f ≫ otherMap L U' adj₁ adj₂ X ↔
    F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((adj₂.homEquiv Y (F.obj X)).symm f)) =
      (adj₂.homEquiv Y (F.obj X)).symm f ≫ F.map (adj₁.unit.app X)

Tactic:
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, otherMap,
        ← adj₂.homEquiv_naturality_right_symm, adj₂.homEquiv_unit, ← adj₂.unit_naturality_assoc,
        adj₂.homEquiv_counit]

Goal state after:
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 : A ⥤ B
F : B ⥤ A
L : C ⥤ B
U' : A ⥤ C
adj₁ : F ⊣ U
adj₂ : L ⋙ F ⊣ U'
inst✝ : HasCoreflexiveEqualizers C
h : (X : B) → RegularMono (adj₁.unit.app X)
Y : C
X : B
f : Y ⟶ U'.obj (F.obj X)
⊢ adj₂.unit.app Y ≫
        U'.map ((L ⋙ F).map f) ≫
          U'.map (F.map (adj₁.unit.app (L.1 (U'.1 (F.obj X))) ≫ U.map (adj₂.counit.app (F.obj X)))) =
      f ≫ U'.map (F.map (adj₁.unit.app X)) ↔
    adj₂.unit.app Y ≫ U'.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map ((L ⋙ F).map f ≫ adj₂.counit.app (F.obj X)))) =
      (adj₂.homEquiv Y (F.obj (U.obj (F.obj X))))
        ((adj₂.homEquiv Y (F.obj ((F ⋙ U).obj X))).symm (f ≫ U'.map (F.map (adj₁.unit.app X))))
Module: Mathlib.CategoryTheory.Adjunction.Quadruple

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ (Function.Injective fun x ↦ (q.adj₁.homEquiv (F.obj (G.obj Y)) X) (L.map (q.adj₂.counit.app Y) ≫ x)) ↔
    Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)

Tactic:
q.adj₁.homEquiv_naturality_left

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
F : D ⥤ C
G : C ⥤ D
R : D ⥤ C
q : Quadruple L F G R
inst✝¹ : F.Full
inst✝ : F.Faithful
X : D
Y : C
⊢ (Function.Injective fun x ↦ q.adj₂.counit.app Y ≫ (q.adj₁.homEquiv Y X) x) ↔
    Function.Injective fun g ↦ g ≫ q.adj₃.unit.app (F.obj X)
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✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (F.map (t.adj₂.counit.app X) ≫ t.leftToRight.app X)

Tactic:
mono_comp_iff_of_isIso

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✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)
Module: Mathlib.CategoryTheory.Bicategory.Extension

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : b ⟶ a
g : c ⟶ a
s t : LeftLift f g
x : B
h : x ⟶ c
X✝ Y✝ : LeftLift f g
η : X✝ ⟶ Y✝
⊢ (h ◁ X✝.unit ≫ (α_ h X✝.lift f).inv) ≫ (h ◁ StructuredArrow.Hom.right η) ▷ f =
    h ◁ (X✝.unit ≫ StructuredArrow.Hom.right η ▷ f) ≫ (α_ h Y✝.lift f).inv

Tactic:
simp [-LeftLift.w]

Goal state after: