mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / √(1 - x ^ 2)

Tactic:
rcases h with (rfl | rfl)

Goal state after:
case neg.inl
⊢ 0 = 1 / √(1 - (-1) ^ 2)

case neg.inr
⊢ 0 = 1 / √(1 - 1 ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

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

Tactic:
sub_add_cancel

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ ℘'[L] z = ℘'[L] z
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inl
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
hab : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (x : ℝ) in a..b, derivWithin f (Icc a b) x = f b - f a

Tactic:
exact integral_derivWithin_Icc_of_contDiffOn_Icc h hab

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

Goal state before:
pp: n : ℕ
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !

Tactic:
obtain rfl | hn := eq_or_ne n 0
  · simp
  have : √(2 * π * n) * (n / exp 1) ^ n = √π * (√(2 * n) * (n / exp 1) ^ n) := by
    simp [sqrt_mul']; ring
  rw [this, ← le_div_iff₀ (by positivity)]
  exact sqrt_pi_le_stirlingSeq hn

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

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

Tactic:
by simp [hP]

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

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

Tactic:
sub_add_cancel

Goal state after:
L : PeriodPair
x : ℂ
l : ↥L.lattice
⊢ L.relation x = L.relation x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic

Goal state before:
pp: ⊢ MeromorphicNFOn tan Set.univ

Tactic:
intro x _

Goal state after:
x : ℂ
a✝ : x ∈ Set.univ
⊢ MeromorphicNFAt tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic

Goal state before:
pp: ⊢ MeromorphicNFOn tanh Set.univ

Tactic:
intro x _

Goal state after:
x : ℂ
a✝ : x ∈ Set.univ
⊢ MeromorphicNFAt tanh x
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b : R
inst✝ : CommSemiring R
n : ℕ
⊢ a ^ n * b + b * ∑ k ∈ Finset.range n, a ^ k = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n

Tactic:
add_comm,

Goal state after:
R : Type u_1
a b : R
inst✝ : CommSemiring R
n : ℕ
⊢ b * ∑ k ∈ Finset.range n, a ^ k + a ^ n * b = b * ∑ x ∈ Finset.range n, a ^ x + b * a ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℕ
x : ℝ
hroot : (T ℝ ↑n).IsRoot x
hnz : x ≠ 0
⊢ Irrational x

Tactic:
rw [← mem_roots (T_ne_zero ℝ n), roots_T_real, Finset.mem_val] at hroot

Goal state after:
n : ℕ
x : ℝ
hroot : x ∈ Finset.image (fun k ↦ cos ((2 * ↑k + 1) * π / (2 * ↑n))) (Finset.range n)
hnz : x ≠ 0
⊢ Irrational x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
add_comm,

Goal state after:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * ((1 + cexp (2 * ↑π * I * ↑z)) * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case ofNat
n : ℕ
⊢ fib (↑n + ↑2) = ↑(Nat.fib n) + fib (↑n + 1)

Tactic:
← Nat.cast_add,

Goal state after:
case ofNat
n : ℕ
⊢ fib ↑(n + 2) = ↑(Nat.fib n) + fib (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
⊢ HasProdUniformlyOn (fun n z ↦ 1 + sineTerm z n) (fun x ↦ Complex.sin (↑π * x) / (↑π * x)) Z

Tactic:
apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right

Goal state after:
Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
⊢ Set.EqOn (fun x ↦ ∏' (i : ℕ), (1 + sineTerm x i)) (fun x ↦ Complex.sin (↑π * x) / (↑π * x)) Z
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ b * b + a * a = b'

Tactic:
add_comm,

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n = n'
h1 : a * (2 * b - a) = a'
h2 : a * a + b * b = b'
⊢ a * a + b * b = b'
Module: Mathlib.Tactic.NormNum.NatFib

Goal state before:
pp: n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ b * b + a * a = a'

Tactic:
add_comm,

Goal state after:
n a b n' a' b' : ℕ
H : IsFibAux n a b
hn : 2 * n + 1 = n'
h1 : a * a + b * b = a'
h2 : b * (2 * a + b) = b'
⊢ a * a + b * b = a'
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: case refine_2
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Complex.sin (↑π * x) / (↑π * x) ≠ 0

Tactic:
simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]
    exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩

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

Goal state before:
pp: ⊢ φ + ψ = 1

Tactic:
by
  rw [goldenRatio, goldenConj]
  ring

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

Goal state before:
pp: n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * (↑(Nat.fib n) + φ * ↑(Nat.fib (n + 1))) = φ ^ (n + 2)

Tactic:
add_comm,

Goal state after:
n : ℕ
ih : φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = φ ^ (n + 1)
⊢ φ * (φ * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n)) = φ ^ (n + 2)
Module: Mathlib.Analysis.SumIntegralExpDecay

Goal state before:
pp: k M : ℕ
c : ℝ
hc : 0 < c
⊢ ∫ (x : ℝ) in ↑0..↑M, x ^ k * rexp (-(c * (x - 1))) ≤ ↑k ! / c ^ (k + 1) * rexp c

Tactic:
by
    simp only [mul_sub, mul_one, neg_sub, CharP.cast_eq_zero]
    simp only [sub_eq_add_neg, Real.exp_add, mul_comm (rexp c), ← mul_assoc]
    rw [intervalIntegral.integral_mul_const]
    gcongr
    exact intervalIntegral_pow_mul_exp_neg_le (by simp) hc

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P : C
⊢ Projective P ↔ (preadditiveCoyoneda.obj (op P)).PreservesEpimorphisms

Tactic:
by
  rw [projective_iff_preservesEpimorphisms_coyoneda_obj]
  refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
      forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩
  · exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P))
        (forget _)
  · intro
    exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Icc 0 ↑N)
integrable : IntegrableOn f (Ioi 0) volume
nonneg : ∀ t ∈ Ioi 0, 0 ≤ f t
⊢ ∑ n ∈ Finset.range N, f ↑(n + 1) ≤ ∫ (x : ℝ) in Ioi 0, f x

Tactic:
by
  rw [Finset.range_eq_Ico]
  exact_mod_cast AntitoneOn.sum_Ico_le_integral (a := 0) (mod_cast anti)
    (mod_cast integrable) (mod_cast nonneg)

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

Goal state before:

Tactic:
(∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
        ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 := by
      gcongr
      intro i hi
      simp only [mem_filter, mem_range] at hi
      simp only [hi.1, mem_Ico, and_true]
      apply Nat.floor_le_of_le
      apply le_of_lt
      rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
      exact Real.log_lt_log hj hi.2
    _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by
      simp [← pow_mul, mul_comm]
    _ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) :=
      geom_sum_Ico_le_of_lt_one (sq_nonneg _) C
    _ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) := by
      gcongr
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
    _ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 := by
      have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Presheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteColimits C
A : Cᵒᵖ ⥤ Type v
inst✝ : PreservesFiniteLimits A
⊢ IsFiltered (CostructuredArrow yoneda A)

Tactic:
by
  suffices IsCofiltered A.Elements from
    IsFiltered.of_equivalence (CategoryOfElements.costructuredArrowYonedaEquivalence _)
  suffices HasFiniteLimits A.Elements from IsCofiltered.of_hasFiniteLimits A.Elements
  exact ⟨fun J _ _ => inferInstance⟩

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

Goal state before:
pp: A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : IsConnected A
inst✝ : R.Final
⊢ IsConnected (Comma L R)

Tactic:
isConnected_iff_of_final (fst L R)

Goal state after:
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
inst✝¹ : IsConnected A
inst✝ : R.Final
⊢ IsConnected A
Module: Mathlib.CategoryTheory.Limits.Indization.Products

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
⊢ IsIndObject (∏ᶜ f)

Tactic:
let F := fun a => (hf a).presentation.F ⋙ yoneda

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
α : Type v
h : ∀ (g : α → C), IsIndObject (∏ᶜ yoneda.obj ∘ g)
f : α → Cᵒᵖ ⥤ Type v
hf : ∀ (a : α), IsIndObject (f a)
F : (a : α) → ⋯.presentation.I ⥤ Cᵒᵖ ⥤ Type v := fun a ↦ ⋯.presentation.F ⋙ yoneda
⊢ IsIndObject (∏ᶜ 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✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
⊢ f ≫ g = 0

Tactic:
by
  suffices f ≫ g = f ≫ 0 by simpa
  exact hc.pullback_hom_ext (by simpa using hf)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
⊢ QuasiIsoAt (((ofCocomplex Z).fromSingle₀Equiv Z).symm ⟨Injective.ι Z, ⋯⟩) 0

Tactic:
rw [CochainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros]
      · refine (ShortComplex.exact_and_mono_f_iff_of_iso ?_).2
          ⟨exact_f_d (Injective.ι Z), by dsimp; infer_instance⟩
        exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
          (by simp [ofCocomplex])
      all_goals rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0

Tactic:
exact Quotient.eq'

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
⊢ Function.Injective (pseudoApply f)

Tactic:
intro abar abar'
  induction abar, abar' using Quotient.inductionOn₂ with | _ a a'
  refine fun ha ↦ Quotient.sound ?_
  have : (⟦(a.hom ≫ f : Over Q)⟧ : Quotient (setoid Q)) = ⟦↑(a'.hom ≫ f)⟧ := by convert!
    ha
  have ⟨R, p, q, ep, Eq, comm⟩ := Quotient.exact this
  exact ⟨R, p, q, ep, Eq, (cancel_mono f).1 <| by
    simp only [Category.assoc]
    exact comm⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
obtain ⟨a, ha'⟩ := Quotient.exists_rep a'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : ∀ (b : Pseudoelement S.X₂), pseudoApply S.g b = 0 → ∃ a, pseudoApply S.f a = b
this : pseudoApply S.g (Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))) = 0
a' : Pseudoelement S.X₁
ha : pseudoApply S.f a' = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
a : Over S.X₁
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
Module: Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Abelian D
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
⊢ P X ≤ F.kernel X

Tactic:
hX

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Abelian D
P : ObjectProperty C
inst✝¹ : P.IsSerreClass
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
hF : P.isoModSerre.IsInvertedBy F
X : C
hX : P X
⊢ F.kernel X
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
n : ℕ
⊢ (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
    (I.isoRightDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ

Tactic:
dsimp [isoRightDerivedObj, Functor.rightDerived]
  rw [assoc, ← Functor.map_comp_assoc,
    InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_hom_naturality f I J φ comm F,
    Functor.map_comp, assoc]
  erw [(HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.naturality]
  rfl

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
P : ObjectProperty C
inst✝ : P.IsClosedUnderSubobjects
⊢ (MorphismProperty.ofObjectProperty P P).kernels ≤ P

Tactic:
intro _ ⟨_, k, hk, hf⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
⊢ (MorphismProperty.ofObjectProperty P P).cokernels ≤ P

Tactic:
intro _ ⟨_, k, hk, hf⟩

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
i✝ X₁✝ X₂✝ : C
f✝ : X₁✝ ⟶ X₂✝
k : CokernelCofork f✝
hk : IsColimit k
hf : MorphismProperty.ofObjectProperty P P f✝
⊢ P k.pt
Module: Mathlib.CategoryTheory.Action.Basic

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)

Tactic:
Iso.conj_apply,

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
M N : Action V G
f : M ≅ N
g : G
⊢ N.ρ g = ((forget V G).mapIso f).inv ≫ M.ρ g ≫ ((forget V G).mapIso f).hom
Module: Mathlib.CategoryTheory.Monad.Coequalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }

Tactic:
have h₁ : (T : C ⥤ C).map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f :=
      congr_arg Monad.Algebra.Hom.f s.condition

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : T.Algebra
s : Cofork (FreeCoequalizer.topMap X) (FreeCoequalizer.bottomMap X)
h₁ : T.map X.a ≫ s.π.f = T.μ.app X.A ≫ s.π.f
⊢ { l //
    (beckAlgebraCofork X).π ≫ l = s.π ∧
      ∀ {m : (beckAlgebraCofork X).pt ⟶ s.pt}, (beckAlgebraCofork X).π ≫ m = s.π → m = l }
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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj X))

Tactic:
eq_comm

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
g : F.obj (L.obj Y) ⟶ F.obj X
⊢ adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (g ≫ F.map (adj₁.unit.app X)) =
      adj₁.unit.app ((𝟭 B).obj (L.obj Y)) ≫ U.map (F.map (adj₁.unit.app (L.obj Y) ≫ U.map g)) ↔
    (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ U.map (F.map (adj₁.unit.app X)) =
      (adj₁.unit.app (L.obj Y) ≫ U.map g) ≫ adj₁.unit.app (U.obj (F.obj 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 : C), Epi (q.leftTriple.rightToLeft.app X)) ↔ ∀ (X : D), Mono (q.rightTriple.adj₂.unit.app (F.obj X))

Tactic:
rightToLeft_eq_counits

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),
      Epi
        ((G.rightUnitor.inv ≫
              inv (G.whiskerLeft q.leftTriple.adj₁.counit) ≫
                (G.associator F L).inv ≫ whiskerRight q.leftTriple.adj₂.counit L ≫ L.leftUnitor.hom).app
          X)) ↔
    ∀ (X : D), Mono (q.rightTriple.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✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ (F.op.leftUnitor.inv ≫
          whiskerRight t.op.adj₁.unit F.op ≫
            (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
      x✝ =
    (NatTrans.op t.rightToLeft).app x✝

Tactic:
rightToLeft_eq_counits

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✝¹ : G.Full
inst✝ : G.Faithful
x✝ : Cᵒᵖ
⊢ (F.op.leftUnitor.inv ≫
          whiskerRight t.op.adj₁.unit F.op ≫
            (H.op.associator G.op F.op).hom ≫ inv (H.op.whiskerLeft t.op.adj₂.unit) ≫ H.op.rightUnitor.hom).app
      x✝ =
    (NatTrans.op
          (H.rightUnitor.inv ≫
            inv (H.whiskerLeft t.adj₁.counit) ≫
              (H.associator G F).inv ≫ whiskerRight t.adj₂.counit F ≫ F.leftUnitor.hom)).app
      x✝
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✝
η_ih✝ : (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p g✝
θ_ih✝ : (fun p ↦ normalizeAux p g✝) = fun p ↦ normalizeAux p h✝
⊢ (fun p ↦ normalizeAux p f✝) = fun p ↦ normalizeAux p h✝

Tactic:
apply Eq.trans <;> assumption

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : a ⟶ x
s : LeftExtension f (𝟙 a ≫ h)
τ₀ : (LeftExtension.mk u adj.unit).whisker h ⟶ s
τ : u ≫ h ⟶ s.extension := StructuredArrow.Hom.right τ₀
hτ : adj.unit ▷ h ⊗≫ f ◁ τ = s.unit
⊢ τ = 𝟙 (u ≫ h) ⊗≫ rightZigzag adj.unit adj.counit ▷ h ⊗≫ τ ⊗≫ 𝟙 s.extension

Tactic:
rw [adj.right_triangle]; bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
u : b ⟶ a
adj : f ⊣ u
x : B
h : x ⟶ a
s : LeftLift u (h ≫ 𝟙 a)
⊢ s.unit ⊗≫ s.lift ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (s.lift ≫ u) = s.unit

Tactic:
rw [adj.right_triangle]; bicategory

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ f a = ↑b ↔ ↑b = f a

Tactic:
eq_comm

Goal state after:
α : Type u_1
β : Type u_2
p : β → Prop
f : α → β
a : α
b : Subtype p
⊢ ↑b = f a ↔ ↑b = f a
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂

Tactic:
ext; simp [eHom_whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.HomCongr

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂

Tactic:
by
  ext; simp [eHom_whisker_exchange_assoc]

Goal state after: