mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 1 2
⊢ 0 ≤ (∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1)⁻¹

Tactic:
rw [inv_nonneg]

Goal state after:
p : ℝ
hp : p ∈ Ioo 1 2
⊢ 0 ≤ ∫ (t : ℝ) in Ioi 0, (p - 1).rpowIntegrand₀₁ t 1
Module: Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation

Goal state before:
pp: case right
a : ℂ
ha : a.re < 0
b : ℂ
s x : ℝ
hx : 0 < x
⊢ x ^ s = |x| ^ s

Tactic:
abs_of_pos hx

Goal state after:
Module: Mathlib.Data.Int.Log

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ log b r = 0

Tactic:
log_of_right_le_one _ (hr.trans zero_le_one),

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 0
⊢ -↑(Nat.clog b ⌈r⁻¹⌉₊) = 0
Module: Mathlib.Data.Int.Log

Goal state before:
pp: case inl.inr
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
b : ℕ
r : R
hrp : 0 < r
hr : r ≤ 1
⊢ clog b r⁻¹ = -log b r

Tactic:
· rw [clog_of_one_le_right _ ((one_le_inv₀ hrp).2 hr), log_of_right_le_one _ hr, neg_neg]

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

Goal state before:
pp: case h
b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
e a : ℝ
ha : 1 ≤ a
⊢ 0 < a

Tactic:
· exact lt_of_lt_of_le zero_lt_one ha

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: 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 → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
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
key : limsup (fun i ↦ ∫ (x : X), (f + const X ‖f‖) x ∂μs i) L ≤ ∫ (x : X), (f + const X ‖f‖) x ∂μ
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
f.integral_add_const ‖f‖

Goal state after:
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 → limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
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
key : limsup (fun i ↦ ∫ (x : X), f x ∂μs i + (μs i).real Set.univ • ‖f‖) L ≤ ∫ (x : X), f x ∂μ + μ.real Set.univ • ‖f‖
⊢ limsup (fun i ↦ ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: case inr.hinf
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
key : ∫ (x : X), (f + const X ‖f‖) x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), (f + const X ‖f‖) x ∂μs i) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L

Tactic:
f.integral_add_const ‖f‖

Goal state after:
case inr.hinf
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
key : ∫ (x : X), f x ∂μ + μ.real Set.univ • ‖f‖ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i + (μs i).real Set.univ • ‖f‖) L
⊢ ∫ (x : X), f x ∂μ ≤ liminf (fun i ↦ ∫ (x : X), f x ∂μs i) L
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
⊢ y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)

Tactic:
have hy₀ : y ≠ 0 := by
    rintro rfl
    have : 1 - ε / 4 < ε / 4 := by simpa [norm_smul, habs, hx] using hy
    linarith

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)
Module: Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas

Goal state before:
pp: n : ℕ
⊢ n.nthRoot 1 = 1

Tactic:
rcases n with _ | _ | _ <;> simp [nthRoot, nthRoot.go, Nat.add_comm 1]

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

Goal state before:
pp: case pos
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ↑l = l₀
⊢ ‖0‖ ≤ 10 * r * ‖l‖ ^ (-3)

pp: case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
⊢ ‖1 / (s - ↑l) ^ 2 - 1 / ↑l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)

Tactic:
· simpa using! show 0 ≤ 10 * r * (‖↑l‖ ^ 3)⁻¹ by positivity

Goal state after:
case neg
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
⊢ ‖1 / (s - ↑l) ^ 2 - 1 / ↑l ^ 2‖ ≤ 10 * r * ‖l‖ ^ (-3)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case e'_9
h : -1 ≠ 1
⊢ 1 / √(1 - (-1) ^ 2) = 0

Tactic:
simp +contextual [arcsin_of_le_neg_one]

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

Goal state before:
pp: case inl.convert_3
h : -1 ≠ 1
⊢ ∀ x ∈ Iic (-1), arcsin x = -(π / 2)

Tactic:
simp +contextual [arcsin_of_le_neg_one]

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

Goal state before:
pp: case inl.convert_4
h : -1 ≠ 1
⊢ arcsin (-1) = -(π / 2)

Tactic:
simp +contextual [arcsin_of_le_neg_one]

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

Goal state before:
pp: case inr.refine_2
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
⊢ ↑x * (π / ↑n) ≤ π

Tactic:
← mul_div_cancel₀ π (Nat.cast_ne_zero.mpr hn)

Goal state after:
case inr.refine_2
n : ℕ
hn : n ≠ 0
x : ℕ
hx : x ≤ n
⊢ ↑x * (π / ↑n) ≤ ↑n * (π / ↑n)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: q : ℚ
⊢ cexp (↑q * ↑π * I) ^ (2 * q.den) = 1

Tactic:
nth_rw 1 [← q.num_div_den, ← exp_nat_mul]

Goal state after:
q : ℚ
⊢ cexp (↑(2 * q.den) * (↑(↑q.num / ↑q.den) * ↑π * I)) = 1
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

Tactic:
rcases niven hθ hcos with h | h | h | h | h <;>
  -- define `h₂` appropriately for each proof branch
  [have h₂ := cos_pi;
    have h₂ : cos (π * (2 / 3)) = -1 / 2 := by
      have := cos_pi_sub (π / 3)
      have := cos_pi_div_three
      grind;;
    have h₂ := cos_pi_div_two;
    have h₂ := cos_pi_div_three;
    have h₂ := cos_zero]

Goal state after:
case inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1
h₂ : cos π = -1
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = -1 / 2
h₂ : cos (π * (2 / 3)) = -1 / 2
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 0
h₂ : cos (π / 2) = 0
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inr.inr.inl
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ = 1 / 2
h₂ : cos (π / 3) = 1 / 2
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}

case inr.inr.inr.inr
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, cos θ = ↑q
h_bnd : θ ∈ Set.Icc 0 π
h : cos θ ∈ {1}
h₂ : cos 0 = 1
⊢ θ ∈ {0, π / 3, π / 2, π * (2 / 3), π}
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ ∃ k ≤ n, x = cos (↑k * π / ↑n)

Tactic:
refine ⟨k, by simpa using hkn, ?_⟩

Goal state after:
case mp
n : ℕ
hn : n ≠ 0
x : ℝ
hx : |x| ≤ 1
k : ℕ
hk : ↑k * π = ↑n * arccos x
hk' : ↑k = ↑n * (arccos x / π)
hkn : ↑k ≤ ↑n
⊢ x = cos (↑k * π / ↑n)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mpr
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ (∃ k ≤ n, Even k ∧ x = cos (↑k * π / ↑n)) → eval x (T ℝ ↑n) = 1

Tactic:
rintro ⟨k, hk₁, hk₂, hx⟩
    rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_even k ((Int.even_coe_nat k).mpr hk₂)]
    norm_cast

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

Goal state before:
pp: case ho
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ (fun c ↦ ↑d) =o[cofinite] fun n ↦ ↑n

Tactic:
· simp only [isLittleO_const_left, Int.cast_eq_zero,
      tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real, or_true]

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Odd k
⊢ IsLocalExtr (fun x ↦ eval x (T ℝ ↑n)) (cos (↑k * π / ↑n))

Tactic:
exact .inl (isLocalMin_T_real hn hk₁ hk₂)

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

Goal state before:
pp: case inr
n : ℕ
hn0 : ¬2 * n + 1 = 0
this : -↑(2 * n + 1) + 1 = -↑(2 * n + 1 - 1)
⊢ (-1) ^ (2 * n + 1 + 1) * (↑(Nat.fib (2 * n + 1)) - ↑(Nat.fib (2 * n + 1 + 1))) = fib (-↑(2 * n + 1) + 1)

Tactic:
rw [Nat.fib_add_one hn0, this, fib_neg_natCast, pow_add]
          simp

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

Goal state before:
pp: x✝ : ℤ
⊢ fib (↑1 + x✝) = fib (↑1 - 1) * fib x✝ + fib ↑1 * fib (x✝ + 1)

Tactic:
simp [add_comm]

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

Goal state before:
pp: ⊢ -1 < ψ

Tactic:
rw [neg_lt, ← inv_goldenRatio]

Goal state after:
⊢ φ⁻¹ < 1
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
⊢ Function.Surjective (preadditiveCoyonedaObj G).map

Tactic:
rw [← Functor.coe_mapAddHom, ← AddCommGrpCat.hom_ofHom (preadditiveCoyonedaObj G).mapAddHom,
    ← AddCommGrpCat.epi_iff_surjective]
  let cm : ShortComplex C := ⟨kernel.ι p, p, by simp⟩
  have exact : cm.Exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel _)
  have mono : Mono cm.op.f := by dsimp [cm]; infer_instance
  let φ := preadditiveCoyonedaObj G
  have faithful : φ.Faithful := by rwa [← isSeparator_iff_faithful_preadditiveCoyonedaObj]
  apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))
  · exact exact.op.map_of_mono_of_preservesKernel _ mono inferInstance
  · simp only [ShortComplex.map_f]
    infer_instance
  · suffices φ.map.Surjective by simpa [AddCommGrpCat.epi_iff_surjective, Functor.coe_mapAddHom]
    exact fun f => ⟨f (𝟙 G), by cat_disch⟩
  · simp [AddCommGrpCat.mono_iff_injective, Functor.coe_mapAddHom, Functor.map_injective]

Goal state after:
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)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft
                    (colimit.ι (CostructuredArrow.proj yoneda A ⋙ yoneda) i ≫
                      ((colimit.isColimit (CostructuredArrow.proj yoneda A ⋙ yoneda)).coconePointUniqueUpToIso
                          (Presheaf.isColimitTautologicalCocone A)).hom)).app
                j

Tactic:
colimit.comp_coconePointUniqueUpToIso_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)).app
            i ≫
          ((functorToInterchangeIso A K).inv.app j).app i ≫
            ((flipFunctorToInterchange A K).hom.app i).app j ≫
              (K.whiskerLeft ((Presheaf.tautologicalCocone A).ι.app i)).app j
Module: Mathlib.CategoryTheory.Limits.IndYoneda

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{u₂, u₁} C
I : Type v₁
inst✝² : Category.{v₂, v₁} I
F : I ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasLimitsOfShape Iᵒᵖ (Type u₂)
A : C
i : I
⊢ ((colimitHomIsoLimitYoneda F A).inv ≫ ↾fun g ↦ colimit.ι F i ≫ g) = limit.π (F.op ⋙ yoneda.obj A) (op i)

Tactic:
rw [← dsimp% colimitHomIsoLimitYoneda_hom_comp_π, ← Category.assoc,
    Iso.inv_hom_id, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
c' : (i : ι) → Cocone (F i)
hc' : (i : ι) → IsColimit (c' i)
h✝ : Nonempty (IsColimit (coconePointwiseProduct c'))
e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
  coconePointwiseProductIso F fun i ↦ (hc i).uniqueUpToIso (hc' i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
rwa [(IsColimit.equivIsoColimit e).nonempty_congr]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms

Tactic:
injective_iff_preservesEpimorphisms_yoneda_obj

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYoneda.obj J).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Injective

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ Injective J ↔ (preadditiveYonedaObj J).PreservesEpimorphisms

Tactic:
injective_iff_preservesEpimorphisms_yoneda_obj

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
J : C
⊢ (yoneda.obj J).PreservesEpimorphisms ↔ (preadditiveYonedaObj J).PreservesEpimorphisms
Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ { X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := J.cocomplex.X 0, X₃ := J.cocomplex.X 1, f := J.ι.f 0,
          g := J.cocomplex.d 0 1, zero := ⋯ }.f ≫
      descFZero f I J ≫ I.cocomplex.d 0 1 =
    0

Tactic:
by dsimp; simp only [← assoc, descFZero]; simp [assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
R : ProjectiveResolution X
⊢ QuasiIso R.π'

Tactic:
by dsimp [π']; infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
⊢ R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CohomologyClass.mk (Cocycle.fromSingleMk (f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ⋯ ↑m ⋯ ⋯)

Tactic:
by
  simp [extMk]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n m : ℕ
hm : n + 1 = m
⊢ R.extMk 0 m hm ⋯ = 0

Tactic:
by
  simp [extMk]

Goal state after:
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
⊢ R.extEquivCohomologyClass (R.extMk f m hm hf) =
    CohomologyClass.mk (Cocycle.toSingleMk ((R.cochainComplexXIso (-↑n) n ⋯).hom ≫ f) ⋯ (-↑m) ⋯ ⋯)

Tactic:
by
  simp [extMk]

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₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha

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₁
a : Over S.X₁
ha : pseudoApply S.f ⟦a⟧ = Quot.mk (PseudoEqual S.X₂) (Over.mk (kernel.ι S.g))
ha' : ⟦a⟧ = a'
Z : C
r : Z ⟶ ((fun g ↦ app S.f g) a).left
q : Z ⟶ (Over.mk (kernel.ι S.g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g ↦ app S.f g) a).hom = q ≫ (Over.mk (kernel.ι S.g)).hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
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 m : ℕ
hm : n + 1 = m
⊢ R.extMk 0 m hm ⋯ = 0

Tactic:
by
  simp [extMk]

Goal state after:
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✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
x✝ : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
⊢ IsIso (F.map f)

Tactic:
have : Mono (F.map f) :=
    (((ShortComplex.mk _ _ (kernel.condition f)).exact_of_f_is_kernel
      (kernelIsKernel f)).map F).mono_g (((hF _ h₁).eq_of_src _ _))

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✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
hF : P ≤ F.kernel
X Y : C
f : X ⟶ Y
x✝ : P.isoModSerre f
h₁ : P.monoModSerre f
h₂ : P.epiModSerre f
this : Mono (F.map f)
⊢ IsIso (F.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P Q : ObjectProperty C
inst✝ : Q.IsClosedUnderIsomorphisms
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
hY : P X
hZ : Q Y
⊢ ofObjectProperty P Q (f ≫ i)

Tactic:
exact ⟨hY, (Q.prop_iff_of_isIso i).mp hZ⟩

Goal state after:
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
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : HomSubtype V G X✝ Y✝
⊢ ⟨ConcreteCategory.hom { hom := ConcreteCategory.ofHom ↑x✝, comm := ⋯ }.hom, ⋯⟩ = x✝

Tactic:
by dsimp; ext; simp [ConcreteCategory.hom_ofHom]

Goal state after:
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
FV : V → V → Type u_3
CV : V → Type u_4
inst✝¹ : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)
inst✝ : ConcreteCategory V FV
X✝ Y✝ : Action V G
x✝ : X✝ ⟶ Y✝
⊢ ConcreteCategory.hom { hom := ConcreteCategory.ofHom ↑⟨ConcreteCategory.hom x✝.hom, ⋯⟩, comm := ⋯ }.hom =
    ConcreteCategory.hom x✝.hom

Tactic:
simp [ConcreteCategory.ofHom_hom]

Goal state after:
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
X : Action V PUnit.{?u.12 + 1}
x✝ : PUnit.{?u.12 + 1}
⊢ ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).ρ PUnit.unit ≫ (Iso.refl ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).V).hom =
    (Iso.refl ((𝟭 (Action V PUnit.{?u.12 + 1})).obj X).V).hom ≫
      ((forget V PUnit.{?u.12 + 1} ⋙
                { obj := fun X ↦ { V := X, ρ := 1 }, map := fun {X Y} f ↦ { hom := f, comm := ⋯ }, map_id := ⋯,
                  map_comp := ⋯ }).obj
            X).ρ
        PUnit.unit

Tactic:
simp only [Functor.id_obj, MonoidHom.one_apply, End.one_def, Functor.comp_obj,
        forget_obj, Iso.refl_hom, Category.comp_id]

Goal state after:
V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
G : Type u_2
inst✝ : Monoid G
X : Action V PUnit.{?u.12 + 1}
x✝ : PUnit.{?u.12 + 1}
⊢ X.ρ PUnit.unit = 𝟙 X.V
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✝
G : Type u_3
H : Type u_4
inst✝¹ : Monoid G
inst✝ : Monoid H
f : G →* H
X Y : Action V H
g₁ g₂ : X ⟶ Y
h : (res V f).map g₁ = (res V f).map g₂
⊢ g₁ = g₂

Tactic:
ext
    rw [← res_map_hom _ f g₁, ← res_map_hom _ f g₂, h]

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
inst✝¹ : H.Full
inst✝ : H.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.adj₁.counit.app (H.obj X))

Tactic:
by
  rw [← map_adj₂_counit_app_leftToRight_app, mono_comp_iff_of_isIso]

Goal state after:
Module: Mathlib.Data.PFun

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →. β ⊕ α
a : α
b : β
h : b ∈ f.fix a
⊢ (f a).Dom

Tactic:
by
  let ⟨h₁, h₂⟩ := Part.mem_assert_iff.1 h
  rw [WellFounded.fixF_eq] at h₂; exact h₂.fst.fst

Goal state after: