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
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn (fun x ↦ f ‖x‖) (ball 0 r) μ ↔ IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioo 0 r) volume

Tactic:
calc
    _ ↔ Integrable (fun x ↦ (Iio r).indicator f ‖x‖) μ := by
      rw [← integrable_indicator_iff measurableSet_ball]
      apply integrable_congr
      filter_upwards with x
      simp [indicator]
    _ ↔ IntegrableOn ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioi 0) := by
      rw [integrable_fun_norm_addHaar μ (f := indicator (Iio r) f),
        integrableOn_congr_fun _ measurableSet_Ioi]
      intro x (hx : 0 < x)
      by_cases hxr : x < r <;> simp [hxr, hx]
    _ ↔ Integrable ((Ioo 0 r).indicator fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) := by
      rw [MeasureTheory.integrableOn_iff_integrable_of_support_subset]
      intro x hx
      simp only [support_indicator, mem_inter_iff, mem_Ioo, Function.mem_support, ne_eq,
        smul_eq_zero, pow_eq_zero_iff', not_or, not_and, Decidable.not_not] at hx
      refine mem_Ioi.mpr hx.1.1
    _ ↔ IntegrableOn (fun y ↦ y ^ (Module.finrank ℝ E - 1) • f y) (Ioo 0 r) volume := by
      rw [← integrable_indicator_iff measurableSet_Ioo, ← integrableOn_univ]

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

Goal state before:
pp: case add_two
θ : ℂ
n : ℕ
ih1 : eval (cos θ) (T ℂ (↑n + 1)) = cos (↑(↑n + 1) * θ)
ih2 : eval (cos θ) (T ℂ ↑n) = cos (↑↑n * θ)
⊢ eval (cos θ) (T ℂ (↑n + 2)) = cos (↑(↑n + 2) * θ)

Tactic:
simp only [T_add_two, eval_sub, eval_mul, eval_X, eval_ofNat, ih1, ih2, sub_eq_iff_eq_add,
      cos_add_cos]
    push_cast
    ring_nf

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

Goal state before:
pp: case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - log (√(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1)) =
    log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

pp: case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

pp: case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

Tactic:
log_mul,

Goal state after:
case succ
n✝ : ℕ
⊢ log ↑(n✝ + 1)! - (log √(2 * ↑(n✝ + 1)) + log ((↑(n✝ + 1) / rexp 1) ^ (n✝ + 1))) =
    log ↑(n✝ + 1)! - 1 / 2 * log (2 * ↑(n✝ + 1)) - ↑(n✝ + 1) * log (↑(n✝ + 1) / rexp 1)

case succ.hx
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) ≠ 0

case succ.hy
n✝ : ℕ
⊢ (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0

case succ.hx
n✝ : ℕ
⊢ ↑(n✝ + 1)! ≠ 0

case succ.hy
n✝ : ℕ
⊢ √(2 * ↑(n✝ + 1)) * (↑(n✝ + 1) / rexp 1) ^ (n✝ + 1) ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr.refine_1
n : ℕ
hn : n ≠ 0
⊢ StrictMonoOn (fun x ↦ ↑x * π / ↑n) ↑(Finset.range (n + 1))

Tactic:
apply StrictMono.strictMonoOn
    exact StrictMono.mul_const
      (StrictMono.mul_const Nat.strictMono_cast (by positivity)) (by positivity)

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

Goal state before:
pp: case degree_f_lt
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
h : ∑ i ≤ n, eval (node n i) P * c i = ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
⊢ P.degree < ↑(Finset.image (fun x ↦ node n x) (Finset.range (n + 1))).card

Tactic:
apply lt_of_le_of_lt hPdeg
    rw [Nat.cast_lt, Finset.card_image_of_injOn (strictAntiOn_node n).injOn,
      Finset.card_range, Nat.lt_succ_iff]

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hn : n ≠ 0
hP : P.degree < 2 * ↑n
⊢ ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

Tactic:
by
  have hmem : P ∈ degreeLT ℝ (2 * n) := by rwa [mem_degreeLT]
  rw [← Sequence.span_degreeLT (chebyshevTsequence ℝ) (by simp),
    show Set.Iio (2 * n) = Finset.range (2 * n) by simp,
    Submodule.mem_span_image_finset_iff_exists_fun'] at hmem
  obtain ⟨c, rfl⟩ := hmem
  simp_rw [eval_finsetSum, eval_smul]
  rw [MeasureTheory.integral_finsetSum, sumZeroes_sum]
  · simp_rw [sumZeroes_smul, smul_eq_mul, MeasureTheory.integral_const_mul]
    congr! with i hrange
    simp_rw [chebyshevTsequence]
    by_cases i = 0
    case pos hi => rw [hi, Nat.cast_zero, integral_eval_T_real_measureT_zero, sumZeroes_T_zero hn]
    case neg hi =>
      have : ¬ (2 * n : ℤ) ∣ i := by
        refine (Int.not_dvd_iff_lt_mul_succ _ (by grind)).mpr ⟨0, ⟨by grind, ?_⟩⟩
        rw_mod_cast [zero_add, mul_one]
        exact mem_range.mp hrange
      rw [integral_eval_T_real_measureT_of_ne_zero (by grind), sumZeroes_T_of_not_dvd this]
  · simp_rw [← eval_smul]
    exact fun i hi => integrable_measureT (by fun_prop)

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

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ HasSum (fun i ↦ (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (℘[L - l₀] z)

Tactic:
by
  refine (Summable.hasSum_iff ?_).mpr (L.weierstrassPExcept_eq_tsum l₀ z x hx).symm
  simp_rw [coeff_weierstrassPExceptSeries, ← tsum_mul_right]
  exact (L.summable_weierstrassPExceptSummand l₀ z x hx).prod

Goal state after:
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
⊢ z.im ^ 2 / (z.re ^ 2 + z.im ^ 2) ≤ (c * z.re + d) ^ 2 + (c * z.im) ^ 2

Tactic:
H1,

Goal state after:
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
⊢ z.im ^ 2 / (z.re ^ 2 + z.im ^ 2) ≤ c ^ 2 * (z.re ^ 2 + z.im ^ 2) + d * 2 * c * z.re + d ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: x : Fin 2 → ℤ
hx : ↑(max (x 0).natAbs (x 1).natAbs) ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0

Tactic:
H1,

Goal state after:
x : Fin 2 → ℤ
hx : ↑(x 1).natAbs ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ x 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case refine_2
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ (i : Finset ℕ), 0 ≤ ∏ a ∈ i, (x - node n a)

Tactic:
· exact fun t => Finset.prod_nonneg (fun a _ => by grind [show node n a ≤ 1 from cos_le_one _])

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

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = 1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Even k

Tactic:
hk₂,

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = 1
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Even k
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case h
n : ℕ
hn : n ≠ 0
x : ℝ
hx : eval x (T ℝ ↑n) = -1
k : ℕ
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Odd k

Tactic:
hk₂,

Goal state after:
case h
n : ℕ
hn : n ≠ 0
x : ℝ
k : ℕ
hx : eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = -1
hk₁ : k ≤ n
hk₂ : x = cos (↑k * π / ↑n)
⊢ Odd k
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ ∑ x ∈ Finset.range (4 + 1),
            ↑(Nat.choose 4 x) *
                (∑ x_1 ∈ Finset.range (x + 1),
                    ↑(x.choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) * ↑(if x - x_1 = 3 then 3! else 0) -
                  if x = 0 then 2 else 0) *
              (∑ x_1 ∈ Finset.range (4 - x + 1),
                  ↑((4 - x).choose x_1) * (↑(x_1 + 2)! * L.sumInvPow 0 (x_1 + 3)) *
                    ↑(if 4 - x - x_1 = 3 then 3! else 0) -
                if 4 - x = 0 then 2 else 0) -
          ∑ x ∈ Finset.range (4 + 1),
            (↑(Nat.choose 4 x) * if x = 0 then 4 else 0) *
              ∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) *
                    ∑ x ∈ Finset.range (x_1 + 1),
                      ↑(x_1.choose x) *
                          (∑ x_2 ∈ Finset.range (x + 1),
                              (↑(x.choose x_2) *
                                  if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                                ↑(if x - x_2 = 2 then 2! else 0) +
                            if x = 0 then 1 else 0) *
                        (∑ x_2 ∈ Finset.range (x_1 - x + 1),
                            (↑((x_1 - x).choose x_2) *
                                if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                              ↑(if x_1 - x - x_2 = 2 then 2! else 0) +
                          if x_1 - x = 0 then 1 else 0)) *
                  (∑ x_2 ∈ Finset.range (4 - x - x_1 + 1),
                      (↑((4 - x - x_1).choose x_2) *
                          if x_2 = 0 then ℘[L - 0] 0 else ↑(x_2 + 1)! * L.sumInvPow 0 (x_2 + 2)) *
                        ↑(if 4 - x - x_1 - x_2 = 2 then 2! else 0) +
                    if 4 - x - x_1 = 0 then 1 else 0) +
        ∑ x ∈ Finset.range (4 + 1),
          (↑(Nat.choose 4 x) * if x = 0 then L.g₂ else 0) *
            (∑ x_1 ∈ Finset.range (4 - x + 1),
                (↑((4 - x).choose x_1) * if x_1 = 0 then ℘[L - 0] 0 else ↑(x_1 + 1)! * L.sumInvPow 0 (x_1 + 2)) *
                  ↑(if 4 - x - x_1 = 6 then 6! else 0) +
              ↑(if 4 - x = 4 then 4! else 0)) +
      ∑ x ∈ Finset.range (4 + 1), (↑(Nat.choose 4 x) * if x = 0 then L.g₃ else 0) * ↑(if 4 - x = 6 then 6! else 0) =
    0

Tactic:
simp [Finset.sum_range_succ, show Nat.choose 4 2 = 6 by rfl, g₂]

Goal state after:
case neg.inr
L : PeriodPair
hi₁ : 4 < 7
hi₂ : ¬Odd 4
hi₃ : ¬4 = 0
hi₄ : ¬4 = 6
⊢ -(2 * (4 * (↑3! * L.G 4) * ↑3!)) + -(4 * (↑3! * L.G 4) * ↑3! * 2) -
        4 * (6 * (↑3! * L.G 4) * 2 + (6 * (↑3! * L.G 4) * 2 + 6 * (↑3! * L.G 4) * 2)) +
      60 * L.G 4 * ↑4! =
    0
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ -1 < ψ

Tactic:
rw [neg_lt, ← inv_goldenRatio]
  exact inv_lt_one_of_one_lt₀ one_lt_goldenRatio

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

Goal state before:
pp: ⊢ fibRec.IsSolution fun x ↦ φ ^ x

Tactic:
fibRec.geom_sol_iff_root_charPoly,

Goal state after:
⊢ fibRec.charPoly.IsRoot φ
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ fibRec.IsSolution fun x ↦ ψ ^ x

Tactic:
fibRec.geom_sol_iff_root_charPoly,

Goal state after:
⊢ fibRec.charPoly.IsRoot ψ
Module: Mathlib.Analysis.VonNeumannAlgebra.Basic

Goal state before:
pp: H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ S.commutant ↔ ∀ g ∈ S, g * z = z * g

Tactic:
rw [← SetLike.mem_coe, coe_commutant]

Goal state after:
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ (↑S).centralizer ↔ ∀ g ∈ S, g * z = z * g
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
h : ∀ i ∈ Ico a b, ∀ x ∈ Ico ↑i ↑(i + 1), g x ≤ f ↑i
hg : IntegrableOn g (Ico ↑a ↑b) volume
⊢ ∫ (x : ℝ) in ↑a..↑b, g x ≤ ∑ i ∈ Finset.Ico a b, f ↑i

Tactic:
by
  convert! neg_le_neg (sum_Ico_le_integral_of_le (f := -f) (g := -g) hab
    (fun i hi x hx ↦ neg_le_neg (h i hi x hx)) hg.neg) <;> simp

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

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
⊢ Tendsto (fun n ↦ u n / ↑n) atTop (𝓝 l)

Tactic:
apply tendsto_div_of_monotone_of_exists_subseq_tendsto_div u l hmono

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
⊢ ∀ (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)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
⊢ ∀ (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)

Tactic:
intro a ha

Goal state after:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun n ↦ u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)
a : ℝ
ha : 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)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
L : C ⥤ T
R : D ⥤ T
C' : Type u₄
inst✝³ : Category.{v₄, u₄} C'
D' : Type u₅
inst✝² : Category.{v₅, u₅} D'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L' : C' ⥤ T'
R' : D' ⥤ T'
F₁ : C ⥤ C'
F₂ : D ⥤ D'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝ : IsIso β
X : Comma L' R'
Y Z : Comma (map₂ (𝟙 (L'.obj X.left)) α) (map₂ X.hom (inv β))
f : Y ⟶ Z
⊢ (mk { left := Y.left.hom, right := Y.right.hom, w := ⋯ }).right.left ⟶
    (mk { left := Z.left.hom, right := Z.right.hom, w := ⋯ }).right.left

Tactic:
by exact f.left.right

Goal state after:
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' : coimageImageComparisonFunctor.obj (Arrow.mk f) ≅
  coimageImageComparisonFunctor.obj (Arrow.mk ((Ind.lim I).map ϕ)) :=
  coimageImageComparisonFunctor.mapIso i
⊢ IsIso (coimageImageComparison f)

Tactic:
dsimp only [coimageImageComparisonFunctor_obj, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom] at 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
⊢ IsIso (coimageImageComparison f)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0

Tactic:
suffices g ≫ f = 0 ≫ f by simpa

Goal state after:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPushouts C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
F : J ⥤ C
c : Cone F
hc : IsLimit c
X Y : C
g : Y ⟶ c.pt
f : c.pt ⟶ X
hf : ∀ (j : J), g ≫ f ≫ pushout.inr (c.π.app j) f = 0
⊢ g ≫ f = 0 ≫ f
Module: Mathlib.CategoryTheory.Abelian.Preradical.Colon

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
Φ : Preradical C
X : C
⊢ Φ.ι.app X ≫ Φ.π.app X = 0

Tactic:
simp [← NatTrans.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
⊢ (ofObjectProperty P Q).map F ≤ ofObjectProperty (P.map F) (Q.map F)

Tactic:
intro X Y f ⟨X', Y', f', ⟨hX', hY'⟩, ⟨i⟩⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hX' : P X'
hY' : Q Y'
i : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ ofObjectProperty (P.map F) (Q.map F) f
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:
by 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:
by simp [rightHom]

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
C : Type u_3
inst✝ : Category.{v_2, u_3} C
F : C ⥤ Action V G
h : PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F ⋙ forget V G)
⊢ PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F

Tactic:
by
  constructor
  intro J _
  apply Action.preservesColimitsOfShape_of_preserves
  exact PreservesColimitsOfSize.preservesColimitsOfShape

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
inst✝² : Preadditive V
R : Type u_3
inst✝¹ : Semiring R
inst✝ : Linear R V
X Y : Action V G
⊢ ∀ (x : X ⟶ Y), 0 • x = 0

Tactic:
intros; ext; exact zero_smul _ _

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✝¹ : F.Full
inst✝ : F.Faithful
⊢ (∀ (X : C), Mono (t.leftToRight.app X)) ↔ ∀ (X : D), Mono (t.adj₁.counit.app X ≫ t.adj₂.unit.app X)

Tactic:
by
  refine ⟨fun h X ↦ by rw [← leftToRight_app_obj]; exact h _, fun h X ↦ ?_⟩
  rw [mono_leftToRight_app_iff_mono_adj₂_unit_app]
  simpa using h (F.obj X)

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Coherence

Goal state before:
pp: B : Type u
inst✝ : Quiver B
a b c : B
p : Path a b
f g : Hom b c
η : f ⟶ g
⊢ (preinclusion B).map { as := p } ◁ η ≫ (normalizeIso p g).hom =
    (normalizeIso p f).hom ≫ (preinclusion B).map₂ (eqToHom ⋯)

Tactic:
rcases η with ⟨η'⟩; clear η
  induction η' with
  | id => simp
  | vcomp η θ ihf ihg =>
    simp only [mk_vcomp, whiskerLeft_comp]
    slice_lhs 2 3 => rw [ihg]
    slice_lhs 1 2 => rw [ihf]
    simp
  -- p ≠ nil required! See the docstring of `normalizeAux`.
  | whisker_left _ _ ih =>
    dsimp
    rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih]
    simp
  | whisker_right h η' ih =>
    dsimp
    rw [associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ih, comp_whiskerRight]
    have := dcongr_arg (fun x => (normalizeIso x h).hom) (normalizeAux_congr p (Quot.mk _ η'))
    dsimp at this; simp [this]
  | _ => simp

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor

Goal state before:
pp: B : Type u₁
C : Type u₂
inst✝² : Bicategory B
inst✝¹ : Strict B
inst✝ : Bicategory C
F : B ⥤ᵖ C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B
t : X₁ ⟶ Y₁
l : X₁ ⟶ X₂
r : Y₁ ⟶ Y₂
b : X₂ ⟶ Y₂
sq : CommSq t l r b
φ : X₁ ⟶ Y₂
hφ : t ≫ r = φ
⊢ l ≫ b = φ

Tactic:
rw [← hφ, sq.w]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
C : α → Sort u_7
f : α →. β ⊕ α
b : β
a a' : α
h : b ∈ f.fix a
h' : b ∈ f.fix a'
fa : Sum.inr a' ∈ f a
hbase : (a_final : α) → Sum.inl b ∈ f a_final → C a_final
hind : (a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀
⊢ fixInduction' h hbase hind = hind a a' h' fa (fixInduction' h' hbase hind)

Tactic:
unfold fixInduction'
  rw [fixInduction_spec]
  -- Porting note: the explicit motive required because `simp` does not apply `Part.get_eq_of_mem`
  refine Eq.rec (motive := fun x e =>
      Sum.casesOn (motive := fun y => (f a).get (dom_of_mem_fix h) = y → C a) x ?_ ?_
      (Eq.trans (Part.get_eq_of_mem fa (dom_of_mem_fix h)) e) = _) ?_
    (Part.get_eq_of_mem fa (dom_of_mem_fix h)).symm
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: case mp
X Y : RelCat
r : X ⟶ Y
⊢ IsIso r → ∃ f, graphFunctor.map f.hom = r

Tactic:
intro h
    have h1 := congr_fun₂ congr((· ~[($h.hom_inv_id).rel] ·))
    have h2 := congr_fun₂ congr((· ~[($h.inv_hom_id).rel] ·))
    simp only [RelCat.Hom.rel_comp_apply₂, RelCat.Hom.rel_id_apply₂, eq_iff_iff] at h1 h2
    obtain ⟨f, hf⟩ := Classical.axiomOfChoice (fun a => (h1 a a).mpr rfl)
    obtain ⟨g, hg⟩ := Classical.axiomOfChoice (fun a => (h2 a a).mpr rfl)
    suffices hif : IsIso (C := Type u) (↾f) by
      use asIso (↾f)
      ext ⟨x, y⟩
      exact ⟨by aesop, fun hxy ↦ (h2 (f x) y).1 ⟨x, (hf x).2, hxy⟩⟩
    use ↾g
    constructor
    · ext x
      apply (h1 _ _).mp
      use f x, (hg _).2, (hf _).2
    · ext y
      apply (h2 _ _).mp
      use g y, (hf (g y)).2, (hg y).2

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
W✝ X✝ Y✝ Z✝ : Dial C
f : W✝.Hom X✝
g : X✝.Hom Y✝
h : Y✝.Hom Z✝
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
    simp only [Category.assoc, Hom.mk.injEq, true_and]
    rw [← Category.assoc, ← Category.assoc]; congr 1
    ext <;> simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : D
f : inl X ⟶ inr Y
⊢ False

Tactic:
by
  cases f

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
Y : D
f : inr X ⟶ inl Y
⊢ False

Tactic:
by
  cases f

Goal state after: