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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable ((fun x ↦ f ‖x‖) ∘ Subtype.val) (Measure.comap Subtype.val μ) ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
comp_def,

Goal state after:
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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume
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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ↑x) (Measure.volumeIoiPow (dim E - 1)) ↔
    Integrable ((fun y ↦ y ^ (dim E - 1) • f y) ∘ Subtype.val) (Measure.comap Subtype.val volume)

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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ MeasurableSet (Ioi 0)

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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0

Tactic:
comp_def,

Goal state after:
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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ Integrable (fun x ↦ f ↑x) (Measure.volumeIoiPow (dim E - 1)) ↔
    Integrable (fun x ↦ ↑x ^ (dim E - 1) • f ↑x) (Measure.comap Subtype.val volume)

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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ MeasurableSet (Ioi 0)

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
this :
  Integrable (fun x ↦ f ‖↑x‖) (Measure.comap Subtype.val μ) ↔
    Integrable (fun x ↦ f ↑x.2) (μ.toSphere.prod (Measure.volumeIoiPow (dim E - 1)))
⊢ μ.toSphere ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: a b : ℝ
hab : a < b
⊢ a.sigmoid < b.sigmoid

Tactic:
simp only [sigmoid]

Goal state after:
a b : ℝ
hab : a < b
⊢ (1 + rexp (-a))⁻¹ < (1 + rexp (-b))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: x : ℝ
n : ℕ∞ω
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1

Tactic:
refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff

Goal state after:
case refine_1
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x

case refine_2
x : ℝ
n : ℕ∞ω
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑n + 1) + 1)) ^ 2 < 1

Tactic:
← n.zero_le

Goal state after:
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
⊢ (1 / (2 * (↑0 + 1) + 1)) ^ 2 < 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (0 + ∫ (x : ℝ), eval x (T ℝ (↑n - ↑n)) ∂measureT) / 2 = π / 2

Tactic:
sub_self,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (0 + ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT) / 2 = π / 2
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ IsIntegral ℤ (2 * cos (↑q * ↑π))

Tactic:
rw [cos.eq_1, mul_div_cancel₀ _ two_ne_zero]

Goal state after:
q : ℚ
⊢ IsIntegral ℤ (cexp (↑q * ↑π * I) + cexp (-(↑q * ↑π) * I))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss

Goal state before:
pp: n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)

Tactic:
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

Goal state after:
n : ℕ
hn : n ≠ 0
c : ℕ → ℝ
hP : (∑ i ∈ range (2 * n), c i • ↑(chebyshevTsequence ℝ) i).degree < 2 * ↑n
i : ℕ
hrange : i ∈ range (2 * n)
hi : ¬i = 0
this : ¬2 * ↑n ∣ ↑i
⊢ ∫ (a : ℝ), eval a (T ℝ ↑i) ∂measureT = sumZeroes n (T ℝ ↑i)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r : ℚ
hcos : ∃ q, cos (↑r * π) = ↑q
hr : 0 ≤ r
hr' : r ≤ 1
⊢ ↑r * π ∈ Set.Icc (0 * π) (1 * π)

Tactic:
constructor <;> gcongr <;> norm_cast

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

Tactic:
by_cases P = 0

Goal state after:
case pos
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h✝ : P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)

case neg
n : ℕ
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h✝ : ¬P = 0
⊢ P.leadingCoeff ≤ 2 ^ (n - 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ r { coe := { re := A, im := B }, coe_im_pos := h } ≤ r z

Tactic:
apply min_le_min hz.2

Goal state after:
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ √(r1 { coe := { re := A, im := B }, coe_im_pos := h }) ≤ √(r1 z)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ eval (cos (↑k * π / ↑n)) (T ℝ ↑n) = ↑↑(↑k).negOnePow

Tactic:
by
  rw [T_real_cos, Int.cast_negOnePow]
  convert! Real.cos_int_mul_pi k using 2
  simp [field]

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 + -x ^ 2 / (↑n + 1) ^ 2 = 0

Tactic:
rw [add_eq_zero_iff_eq_neg, neg_div', eq_div_iff]

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ ¬1 * (↑n + 1) ^ 2 = - -x ^ 2

x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ (↑n + 1) ^ 2 ≠ 0
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inr
n : ℕ
hn : Odd n
⊢ fib (-↑n) = (-1) ^ (n + 1) * ↑(Nat.fib n)

Tactic:
simp [fib_of_odd, hn]

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

Goal state before:
pp: m n : ℤ
h : m ∣ n
⊢ fib m ∣ fib n

Tactic:
obtain ⟨m, (rfl | rfl)⟩ := m.eq_nat_or_neg
  · exact fib_natCast_dvd h
  · simp [fib_neg_natCast, ← fib_natCast, fib_natCast_dvd <| Int.neg_dvd.mp h]

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

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ ↑(fib (n + 1)) / ↑(fib n)) atTop (𝓝 ((φ - ψ * 0) / (1 - 0)))

Tactic:
funext h₁

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
h₂ : Tendsto (fun n ↦ (ψ / φ) ^ n) atTop (𝓝 0)
⊢ Tendsto (fun x ↦ (φ - ψ * (ψ / φ) ^ x) / (1 - (ψ / φ) ^ x)) atTop (𝓝 ((φ - ψ * 0) / (1 - 0)))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k)

Tactic:
h0

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℂ
hz : z ∈ ℍₒ
h0 :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k) + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
⊢ iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z + -(-1) ^ k * ↑k ! * z ^ (-1 - ↑k) =
    iteratedDerivWithin k (fun x ↦ ↑π * (↑π * x).cot) ℍₒ z - (-1) ^ k * ↑k ! * z ^ (-1 - ↑k)
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                  (limit.π K j) ≫
                (functorToInterchangeIso A K).inv.app j).app
            i ≫
          (colimit.ι (functorToInterchange A K).flip i ≫
                  (HasColimit.isoOfNatIso (flipFunctorToInterchange A K)).hom).app
              j ≫
            (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
              (K.isoWhiskerLeft
                      ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                        (Presheaf.isColimitTautologicalCocone A))).hom.app
                j

Tactic:
HasColimit.isoOfNatIso_ι_hom,

Goal state after:
C : Type u
inst✝⁴ : SmallCategory C
inst✝³ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type u
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
K : J ⥤ Cᵒᵖ
inst✝ : IsFiltered (CostructuredArrow yoneda A)
j : J
i : CostructuredArrow yoneda A
⊢ i.hom.app (limit K) ≫ A.map (limit.π K j) =
    ((CostructuredArrow.proj yoneda A).associator yoneda ((evaluation Cᵒᵖ (Type u)).obj (limit K))).hom.app i ≫
      (fun X ↦ 𝟙 (Opposite.unop (limit K) ⟶ X.left)) i ≫
        ((coyoneda ⋙ (whiskeringLeft (CostructuredArrow yoneda A) C (Type u)).obj (CostructuredArrow.proj yoneda A)).map
                  (limit.π K j) ≫
                (functorToInterchangeIso A K).inv.app j).app
            i ≫
          ((flipFunctorToInterchange A K).hom.app i ≫
                  colimit.ι ((CostructuredArrow.proj yoneda A ⋙ yoneda) ⋙ (whiskeringLeft J Cᵒᵖ (Type u)).obj K) i).app
              j ≫
            (colimitCompWhiskeringLeftIsoCompColimit (CostructuredArrow.proj yoneda A ⋙ yoneda) K).hom.app j ≫
              (K.isoWhiskerLeft
                      ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                        (Presheaf.isColimitTautologicalCocone A))).hom.app
                j
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
inst✝ : Injective Z
n✝ : ℕ
⊢ IsZero (((single₀ C).obj Z).X (n✝ + 1))

Tactic:
apply HomologicalComplex.isZero_single_obj_X

Goal state after:
case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
inst✝ : Injective Z
n✝ : ℕ
⊢ n✝ + 1 ≠ 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
X Y : C
f : X ⟶ Y
α : { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ } ⟶
  { X₁ := X, X₂ := Y, X₃ := syzygies f, f := f, g := d f, zero := ⋯ } := ⋯
⊢ IsColimit (CokernelCofork.ofπ { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }.g ⋯)

Tactic:
apply cokernelIsCokernel

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
this : ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f

Tactic:
simp only [Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
a a' : Over P
ha : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
this : ⟦Over.mk (a.hom ≫ f)⟧ = ⟦Over.mk (a'.hom ≫ f)⟧
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
⊢ (a ≫ x.hom) ≫ f = (b ≫ y.hom) ≫ g

Tactic:
simp only [Category.assoc]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f ⟦x⟧ = pseudoApply g ⟦y⟧
Z : C
a : Z ⟶ ((fun g ↦ app f g) x).left
b : Z ⟶ ((fun g_1 ↦ app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g ↦ app f g) x).hom = b ≫ ((fun g_1 ↦ app g g_1) y).hom
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g
Module: Mathlib.CategoryTheory.Abelian.Projective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : ProjectiveResolution X
n : ℕ
f : R.complex.X n ⟶ Y
m : ℕ
hm : n + 1 = m
hf : R.complex.d m n ≫ f = 0
X' : C
R' : ProjectiveResolution X'
g : X' ⟶ X
φ : R'.Hom R g
this✝ : HasDerivedCategory C
this : (R'.cochainComplexXIso (-↑n) n ⋯).hom ≫ φ.hom.f n = φ.hom'.f (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom
⊢ R.cochainComplex.d (-↑m) (-↑n) ≫ (R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f = 0

Tactic:
simpa [R.cochainComplex_d _ _ _ _ rfl rfl]

Goal state after:
Module: Mathlib.CategoryTheory.Action

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
X : Type u
inst✝³ : MulAction M X
x : X
G : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
H : Type u_3
inst✝ : Group H
F : ActionCategory G X ⥤ SingleObj H
F_map_eq : ∀ {a b : ActionCategory G X} {f : a ⟶ b}, F.map f = F.map (homOfPair b.back ↑f)
⊢ ∀ (x y : G),
    ⟨fun b ↦ F.map (homOfPair b (x * y)), x * y⟩ =
      ⟨fun b ↦ F.map (homOfPair b x), x⟩ * ⟨fun b ↦ F.map (homOfPair b y), y⟩

Tactic:
intro g h
      ext b
      · exact F_map_eq.symm.trans (F.map_comp (homOfPair (g⁻¹ • b) h) (homOfPair b g))
      rfl

Goal state after:
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ lift (f.comp inl) (f.comp inr) ⋯ = lift (g.comp inl) (g.comp inr) ⋯

Tactic:
simp only [*]

Goal state after:
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
⊢ ∀ (b : F ⟶ G), 1 • b = b

Tactic:
by
        intros
        ext
        apply one_smul

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
⊢ IsIso (L.map f) ↔ P.isoModSerre f

Tactic:
by
  let := abelian L P
  rw [isIso_iff_mono_and_epi, mono_map_iff L P, epi_map_iff L P, isoModSerre_iff]

Goal state after:
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 : C), Epi (L.map (q.adj₂.counit.app X))) ↔ ∀ (X : D), Mono (q.adj₃.unit.app (F.obj X))

Tactic:
epi_iff_forall_injective,

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 : C) (Z : D), Function.Injective fun g ↦ L.map (q.adj₂.counit.app X) ≫ g) ↔
    ∀ (X : D), Mono (q.adj₃.unit.app (F.obj X))
Module: Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ((α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  (F.map f ≫ η.app b) ◁ θ.naturality g ≫
                    η.naturality f ▷ (θ.app b ≫ H.map g) ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv

Tactic:
whisker_exchange_assoc

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H : B ⥤ᵒᵖᴸ C
η : OplaxTrans F G
θ : OplaxTrans G H
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ ((α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
        η.naturality (f ≫ g) ▷ θ.app c ≫
          (α_ (η.app a) (G.map (f ≫ g)) (θ.app c)).hom ≫
            η.app a ◁ θ.naturality (f ≫ g) ≫ (α_ (η.app a) (θ.app a) (H.map (f ≫ g))).inv) ≫
      (η.app a ≫ θ.app a) ◁ H.mapComp f g =
    (α_ (F.map (f ≫ g)) (η.app c) (θ.app c)).inv ≫
      F.mapComp f g ▷ η.app c ▷ θ.app c ≫
        (α_ (F.map f) (F.map g) (η.app c)).hom ▷ θ.app c ≫
          (α_ (F.map f) (F.map g ≫ η.app c) (θ.app c)).hom ≫
            F.map f ◁ η.naturality g ▷ θ.app c ≫
              F.map f ◁ (α_ (η.app b) (G.map g) (θ.app c)).hom ≫
                (α_ (F.map f) (η.app b) (G.map g ≫ θ.app c)).inv ≫
                  η.naturality f ▷ (G.map g ≫ θ.app c) ≫
                    (η.app a ≫ G.map f) ◁ θ.naturality g ≫
                      (α_ (η.app a) (G.map f) (θ.app b ≫ H.map g)).hom ≫
                        η.app a ◁ (α_ (G.map f) (θ.app b) (H.map g)).inv ≫
                          η.app a ◁ θ.naturality f ▷ H.map g ≫
                            η.app a ◁ (α_ (θ.app a) (H.map f) (H.map g)).hom ≫
                              (α_ (η.app a) (θ.app a) (H.map f ≫ H.map g)).inv
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Pseudo

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (F.map f ≫ η.app b) ◁ Γ.as.app b ≫
        (η.naturality f).hom ▷ ι.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        (η.naturality f).hom ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
            η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
whisker_exchange_assoc

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᵖ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ (α_ (F.map f) (η.app b) (θ.app b)).inv ≫
      (η.naturality f).hom ▷ θ.app b ≫
        (η.app a ≫ G.map f) ◁ Γ.as.app b ≫
          (α_ (η.app a) (G.map f) (ι.app b)).hom ≫
            η.app a ◁ (ι.naturality f).hom ≫ (α_ (η.app a) (ι.app a) (H.map f)).inv =
    ((α_ (F.map f) (η.app b) (θ.app b)).inv ≫
        (η.naturality f).hom ▷ θ.app b ≫
          (α_ (η.app a) (G.map f) (θ.app b)).hom ≫
            η.app a ◁ (θ.naturality f).hom ≫ (α_ (η.app a) (θ.app a) (H.map f)).inv) ≫
      (η.app a ◁ Γ.as.app a) ▷ H.map f