mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ ((fun x ↦ ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) = μ (image2 (fun a b ↦ ↑b • ↑a) s (Iio r))

Tactic:
← image_prod

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : MeasurableSpace E
μ : Measure E
s : Set ↑(sphere 0 1)
r : ↑(Ioi 0)
⊢ μ ((fun x ↦ ↑((homeomorphUnitSphereProd E).symm x)) '' s ×ˢ Iio r) = μ ((fun x ↦ ↑x.2 • ↑x.1) '' s ×ˢ Iio r)
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr.h'
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) L fun i ↦ ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) L fun i ↦ ∫ (x : X), f x ∂μs i
⊢ autoParam (IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) L fun i ↦ ∫ (x : X), f x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_3

Tactic:
exact bdd_below

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
L : PeriodPair
⊢ IsZLattice ℝ L.lattice

Tactic:
by
  simp_rw [L.lattice_eq_span_range_basis]
  infer_instance

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ (n + 1) + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))

Tactic:
pow_succ

Goal state after:
case e'_4
n a b : ℕ
hb : b ≠ 0
h : 0 ≤ (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
⊢ ↑a ^ n * ↑a + ↑n * ↑b * ↑b ^ n - (↑n + 1) * ↑a * ↑b ^ n =
    (↑b + (↑a - ↑b)) ^ (n + 1) - (↑b ^ (n + 1) + ↑(n + 1) * ↑b ^ (n + 1 - 1) * (↑a - ↑b))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case e'_5
L : PeriodPair
l : ↥L.lattice
x✝ : ℂ
⊢ 1 / (x✝ - ↑l) ^ 2 - 1 / ↑l ^ 2 = if ↑l = L.ω₁ / 2 then 0 else 1 / (x✝ - ↑l) ^ 2 - 1 / ↑l ^ 2

Tactic:
rw [if_neg]; exact fun e ↦ L.ω₁_div_two_notMem_lattice (e ▸ l.2)

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

Goal state before:
pp: L : PeriodPair
z : ℂ
⊢ ℘'[L] (-z) = -℘'[L] z

Tactic:
by
  simp only [derivWeierstrassP]
  rw [← (Equiv.neg L.lattice).tsum_eq]
  simp only [Equiv.neg_apply, NegMemClass.coe_neg, sub_neg_eq_add, neg_add_eq_sub, neg_neg,
    ← div_neg, ← tsum_neg]
  congr! with l
  ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
x : ℝ
hx : x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1))
hPx : eval x P ≠ eval x (T ℝ ↑n)
i : ℕ
hix : node n i = x
hi : i ∈ Finset.Iic n
this :
  ∑ i ≤ n, (-1) ^ i * eval (node n i) P * ((-1) ^ i * c i) <
    ∑ i ≤ n, (-1) ^ i * eval (node n i) (T ℝ ↑n) * ((-1) ^ i * c i)
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i

Tactic:
by
    simpa [negOnePow_mul_negOnePow_mul_cancel]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup

Tactic:
wlog! hn : n ≠ 0

Goal state after:
case inr
n : ℕ
this : ∀ (n : ℕ), n ≠ 0 → (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup
hn : n = 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup

n : ℕ
hn : n ≠ 0
⊢ (Multiset.map (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Multiset.range n)).Nodup
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

Tactic:
wlog! hn : n ≠ 0

Goal state after:
case inr
n : ℕ
this :
  ∀ (n : ℕ), n ≠ 0 → (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
hn : n = 0
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val

n : ℕ
hn : n ≠ 0
⊢ (T ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val

Tactic:
wlog! hn : n ≠ 0

Goal state after:
case inr
n : ℕ
this : ∀ (n : ℕ), n ≠ 0 → (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
hn : n = 0
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val

n : ℕ
hn : n ≠ 0
⊢ (U ℝ ↑n).roots = (Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑n + 1))) (Finset.range n)).val
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

Tactic:
replace hx := hx.deriv_eq_zero

Goal state after:
case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx : deriv (fun x ↦ eval x (T ℝ ↑n)) x = 0
⊢ ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x → ∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)

pp: case mpr
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ (∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)) → IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x

Tactic:
· intro hx
    replace hx := hx.deriv_eq_zero
    rw [Polynomial.deriv, T_derivative_eq_U, eval_mul, Int.cast_natCast, eval_natCast,
      mul_eq_zero_iff_left (by aesop)] at hx
    replace hx : x ∈ (U ℝ (n - 1)).roots :=
      (mem_roots (degree_ne_bot.mp (ne_of_eq_of_ne (by grind [degree_U_natCast])
        (WithBot.natCast_ne_bot (n - 1))))).mpr hx
    rw [show (n - 1 : ℤ) = (n - 1 : ℕ) by grind, roots_U_real, Finset.mem_val] at hx
    obtain ⟨k, hk₁, hx⟩ := Finset.mem_image.mp hx
    refine ⟨k + 1, Finset.mem_Ioo.mpr ⟨k.zero_lt_succ, by grind⟩, ?_⟩
    rw [← hx]
    congr <;> norm_cast
    exact Nat.sub_add_cancel (Nat.one_le_of_lt hn)

Goal state after:
case mpr
n : ℕ
hn : 2 ≤ n
x : ℝ
⊢ (∃ k ∈ Finset.Ioo 0 n, x = cos (↑k * π / ↑n)) → IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) x
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation (x - ↑l) = L.relation x

Tactic:
by
  rw [← L.relation_add_coe _ l, sub_add_cancel]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
⊢ |eval x ((⇑derivative)^[k] (T ℝ ↑n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))

Tactic:
have hf (y : ℝ) :
      ∑ p ∈ f.support, f p • p.eval y = (derivative^[k] (T ℝ n)).eval y := by
    rw [← hfderiv, Polynomial.eval_finsetSum]
    simp_rw [Polynomial.eval_smul]

Goal state after:
k : ℕ
x : ℝ
hx : |x| ≤ 1
n : ℕ
this : (⇑derivative)^[k] (T ℝ ↑n) ∈ Submodule.span ℕ ((fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k))
f : ℝ[X] →₀ ℕ
hfsupp : ↑f.support ⊆ (fun m ↦ T ℝ ↑m) '' Set.Icc 0 (n - k)
hfderiv : ∑ p ∈ f.support, f p • p = (⇑derivative)^[k] (T ℝ ↑n)
hf : ∀ (y : ℝ), ∑ p ∈ f.support, f p • eval y p = eval y ((⇑derivative)^[k] (T ℝ ↑n))
⊢ |eval x ((⇑derivative)^[k] (T ℝ ↑n))| ≤ eval 1 ((⇑derivative)^[k] (T ℝ ↑n))
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ Irrational φ

Tactic:
have := Nat.Prime.irrational_sqrt (show Nat.Prime 5 by norm_num)
  have := this.ratCast_add 1
  convert! this.ratCast_mul (show (0.5 : ℚ) ≠ 0 by norm_num)
  simp
  ring

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
⊢ SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ) ℍₒ

Tactic:
apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
  intro K hK hKc
  lift K to Set ℍ using hK
  obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact
    (isEmbedding_coe.isCompact_iff.mpr hKc)
  exact ⟨cotTermUpperBound k A B hB, summable_cotTermUpperBound A B hB hk,
    iteratedDerivWithin_cotTerm_bounded_uniformly A B hB <| by gcongr⟩

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

Goal state before:
pp: case hg
n l : ℕ
x : ℂ
hx : x ∈ ℍₒ
⊢ x - (↑n + 1) ≠ 0

Tactic:
simpa [sub_eq_zero] using (UpperHalfPlane.ne_intCast (.mk x hx) (n + 1))

Goal state after:
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: case hf
k M : ℕ
c : ℝ
hc : 0 < c
⊢ MonotoneOn (fun x ↦ x ^ k) (Icc ↑0 ↑M)

pp: case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))

pp: case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

pp: case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 1)))

Tactic:
· intro x hx y hy hxy
      apply pow_le_pow_left₀ (by simpa using hx.1) hxy

Goal state after:
case hg
k M : ℕ
c : ℝ
hc : 0 < c
⊢ AntitoneOn (fun x ↦ rexp (-(c * x))) (Icc (↑0 - 1) (↑M - 1))

case fpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ ↑0 ^ k

case gpos
k M : ℕ
c : ℝ
hc : 0 < c
⊢ 0 ≤ rexp (-(c * (↑M - 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)
L : ∀ᶠ (n : ℕ) in atTop, u (c n) - ↑(c n) * l ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
⊢ u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n

Tactic:
let N := Nat.find exN

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)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ u (c b) - ↑(c b) * l ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
⊢ u n - ↑n * l ≤ ε * (1 + ε + l) * ↑n
Module: Mathlib.CategoryTheory.Abelian.Projective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
⊢ (preadditiveCoyonedaObj P).PreservesHomology

Tactic:
by
  have := (projective_iff_preservesEpimorphisms_preadditiveCoyonedaObj P).mp hP
  apply Functor.preservesHomology_of_preservesEpis_and_kernels

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 : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n

Tactic:
let N := Nat.find exN

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
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 : Tendsto (fun n ↦ u (c n) / ↑(c n)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, ↑(c n) * l - u (c n) ≤ ε * ↑(c n)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → ↑(c (b + 1)) ≤ (1 + ε) * ↑(c b) ∧ ↑(c b) * l - u (c b) ≤ ε * ↑(c b)
M : ℕ := (image (fun i ↦ c i) (range (a + 1))).max' ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ N, n < c N
N : ℕ := Nat.find exN
⊢ ↑n * l - u n ≤ ε * (1 + l) * ↑n
Module: Mathlib.CategoryTheory.Abelian.Monomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
x✝³ x✝² x✝¹ : C
f : x✝³ ⟶ x✝¹
g : x✝³ ⟶ x✝²
x✝ : Limits.HasPushout f g
hf : monomorphisms C f
⊢ monomorphisms C (Limits.pushout.inr f g)

Tactic:
by
    simp only [monomorphisms.iff] at hf ⊢
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
⊢ kernel.ι (d g) ≫ d f = 0

Tactic:
refine (isColimitFiniteSubproductsCocone (fun (_ : M) => G)).pullback_zero_ext (fun F => ?_)
  dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
    Functor.const_obj_obj]
  classical
  rw [finiteSubcoproductsCocone_ι_app_eq_sum, ← pullback.condition_assoc]
  refine (Preadditive.isSeparator_iff G).1 hG _ (fun h => ?_)
  rw [Preadditive.comp_sum_assoc, Preadditive.comp_sum_assoc, Preadditive.sum_comp]
  simp only [Category.assoc, ι_d]
  let r (x : F) : (End G)ᵐᵒᵖ := MulOpposite.op (h ≫ pullback.fst _ _ ≫ Sigma.π _ x)
  suffices ∑ x ∈ F.attach, r x • f.hom x.1.as = 0 by simpa [End.smul_left, r] using this
  simp only [← map_smul, ← map_sum]
  suffices ∑ x ∈ F.attach, r x • x.1.as = 0 by simp [this]
  simp only [← g.hom.map_eq_zero_iff ((ModuleCat.mono_iff_injective _).1 hg), map_sum, map_smul]
  simp only [← ι_d g, End.smul_left, MulOpposite.unop_op, Category.assoc, r]
  simp [← Preadditive.comp_sum, ← Preadditive.sum_comp', pullback.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
⊢ ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M),
    (ModuleCat.Hom.hom ((preadditiveCoyonedaObj G).map l) ∘ₗ ↑(Preadditive.homSelfLinearEquivEndMulOpposite G).symm) x =
      g ⟨x, mem⟩

Tactic:
intro f hf

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
l : G ⟶ B
hl :
  d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
    d (ModuleCat.ofHom g)
f : (End G)ᵐᵒᵖ
hf : f ∈ M
⊢ (ModuleCat.Hom.hom ((preadditiveCoyonedaObj G).map l) ∘ₗ ↑(Preadditive.homSelfLinearEquivEndMulOpposite G).symm) f =
    g ⟨f, hf⟩
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ Injective.ι Z ≫ (ofCocomplex Z).d 0 1 = 0

Tactic:
rw [ofCocomplex_d_0_1, cokernel.condition_assoc, zero_comp]

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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : InjectiveResolution X
Q : InjectiveResolution Y
g : P.cocomplex ⟶ Q.cocomplex
w : P.ι ≫ g = (CochainComplex.single₀ C).map f ≫ Q.ι
⊢ P.ι.f 0 ≫ g.f 0 = f ≫ Q.ι.f 0

Tactic:
rw [← HomologicalComplex.comp_f, w, HomologicalComplex.comp_f,
    CochainComplex.single₀_map_f_zero]

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
β : (injectiveResolution X).cocomplex ⟶ P.cocomplex
hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map P.iso.hom ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)

Tactic:
rw [← hβ]

Goal state after:
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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : InjectiveResolution X
β : (injectiveResolution X).cocomplex ⟶ P.cocomplex
hβ : (HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β = P.iso.hom
⊢ (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app ((injectiveResolutions C).obj X).as) ≫
      (G.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β) =
    (F.mapHomotopyCategory (ComplexShape.up ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map β) ≫
      (HomotopyCategory.quotient D (ComplexShape.up ℕ)).map
        ((NatTrans.mapHomologicalComplex α (ComplexShape.up ℕ)).app P.cocomplex)
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), f ≫ s = 0

Tactic:
exact ⟨_, cokernel.π f, hf, by simp⟩

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✝
x✝ : Mono f
⊢ Mono (L.map f)

Tactic:
simpa only [mono_map_iff _ P] using P.monoModSerre_of_mono f

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
n : N
⊢ inl ((φ g)⁻¹ n) = inr g⁻¹ * inl n * inr g

Tactic:
by
  rw [← map_inv, inl_aut, inv_inv]

Goal state after:
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 * M.ρ h) = F.map (M.ρ h) ≫ F.map (M.ρ g)

Tactic:
End.mul_def,

Goal state after:
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.ρ h ≫ M.ρ g) = F.map (M.ρ h) ≫ F.map (M.ρ g)
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ (preinclusion B).map { as := p } ◁ η.mk ≫ (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
slice_lhs 1 2 => rw [ihf]

Goal state after:
case mk.vcomp
B : Type u
inst✝ : Quiver B
a b c : B
f g : Hom b c
a✝ b✝ : FreeBicategory B
f✝ g✝ h✝ : a✝ ⟶ b✝
η : Hom₂ f✝ g✝
θ : Hom₂ g✝ h✝
ihf :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel η ≫ (normalizeIso p g✝).hom =
      (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
ihg :
  ∀ (p : Path a a✝),
    (preinclusion B).map { as := p } ◁ Quot.mk Rel θ ≫ (normalizeIso p h✝).hom =
      (normalizeIso p g✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
p : Path a a✝
⊢ ((normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)) ≫ (preinclusion B).map₂ (eqToHom ⋯) =
    (normalizeIso p f✝).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
a b : ∫ᶜ F
f : a ⟶ b
⊢ (f ≫ 𝟙 b).fiber = f.fiber ≫ eqToHom ⋯

Tactic:
simp [F.mapComp_id_left_inv_app, Strict.leftUnitor_eqToIso, ← Functor.map_comp_assoc,
        ← Cat.Hom₂.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat.Adjunction

Goal state before:
pp: X : Type u
C : Cat
x✝² x✝¹ : Cat
x✝ : x✝² ⟶ x✝¹
⊢ ∀ (X Y : ↑((objects ⋙ typeToCat).obj x✝²)) (f : X ⟶ Y),
    ((objects ⋙ typeToCat).map x✝ ≫ x✝¹.typeToCatObjectsAdjCounitApp.toCatHom).toFunctor.map f ≍
      (x✝².typeToCatObjectsAdjCounitApp.toCatHom ≫ (𝟭 Cat).map x✝).toFunctor.map f

Tactic:
intro ⟨_⟩ ⟨_⟩ f
            obtain rfl := Discrete.eq_of_hom f
            cat_disch

Goal state after: