mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
⊢ Set.EqOn (deriv ℘[L - l₀]) ℘'[L - l₀] (↑L.lattice \ {l₀})ᶜ

Tactic:
refine ((L.hasSumLocallyUniformly_weierstrassPExcept l₀).tendstoLocallyUniformlyOn.deriv
    (.of_forall fun s ↦ ?_) L.isOpen_compl_lattice_sdiff).unique ?_
  · refine .fun_sum fun i hi ↦ ?_
    split_ifs
    · simp
    refine .sub (.div (by fun_prop) (by fun_prop) fun x hx ↦ ?_) (by fun_prop)
    have : x ≠ i := by rintro rfl; simp_all
    simpa [sub_eq_zero]
  · refine (L.hasSumLocallyUniformly_derivWeierstrassPExcept l₀).tendstoLocallyUniformlyOn.congr ?_
    intro s l hl
    simp only [Function.comp_apply]
    rw [deriv_fun_sum]
    · congr with x
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      rw [deriv_fun_sub (.fun_div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop),
        deriv_const]
      simp_rw [← zpow_natCast, one_div, ← zpow_neg, Nat.cast_ofNat]
      rw [deriv_comp_sub_const (f := (· ^ (-2 : ℤ))), deriv_zpow]
      simp
      field_simp
    · intros x hxs
      split_ifs with hl₁
      · simp
      have hl₁ : l - x ≠ 0 := fun e ↦ hl₁ (by
        obtain rfl := sub_eq_zero.mp e
        simpa using hl)
      exact .sub (.div (by fun_prop) (by fun_prop) (by simpa)) (by fun_prop)

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ

Tactic:
rw [countable_coe_iff]

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ ℘'[L - l₀] (x + ↑l) = ℘'[L - l₀ - ↑l] x

pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

pp: case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ

Tactic:
L.derivWeierstrassPExcept_add_coe

Goal state after:
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ ℘'[L - l₀ - ↑l] x = ℘'[L - l₀ - ↑l] x

case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ

case a
L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
x : ℂ
hx : x ∈ (↑L.lattice \ {l₀ - ↑l})ᶜ
⊢ x + ↑l ∈ (↑L.lattice \ {l₀})ᶜ
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: case inl
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
⊢ L.ω₁ ∈ ↑(AddSubgroup.toIntSubmodule G)

Tactic:
ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ ℘'[L - l₀] = ℘'[L]

Tactic:
delta derivWeierstrassPExcept derivWeierstrassP

Goal state after:
L : PeriodPair
l₀ : ℂ
hl : l₀ ∉ L.lattice
⊢ (fun z ↦ ∑' (l : ↥L.lattice), if ↑l = l₀ then 0 else -2 / (z - ↑l) ^ 3) = fun z ↦
    -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - (-1) ^ 2)) (Iic (-1)) (-1)

Tactic:
convert! (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _

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

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

case inl.convert_4
h : -1 ≠ 1
⊢ arcsin (-1) = -(π / 2)
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)

Tactic:
have g : HasSum (fun k : ℕ => (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2) ^ ↑(k + 1))
      (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)) := by
    have := (hasSum_geometric_of_lt_one h_nonneg ?_).mul_left (((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2)
    · simp_rw [← _root_.pow_succ'] at this
      exact this
    rw [one_div, inv_pow]
    exact inv_lt_one_of_one_lt₀ (one_lt_pow₀ (lt_add_of_pos_left _ <| by positivity) two_ne_zero)

Goal state after:
n : ℕ
h_nonneg : 0 ≤ (1 / (2 * ↑(n + 1) + 1)) ^ 2
g :
  HasSum (fun k ↦ ((1 / (2 * ↑(n + 1) + 1)) ^ 2) ^ (k + 1))
    ((1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2))
⊢ log (stirlingSeq (n + 1)) - log (stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ioo (min (-1) 1) (max (-1) 1)
⊢ HasDerivAt (-arccos) (√(1 - x ^ 2)⁻¹) x

Tactic:
simpa using! (hasDerivAt_arccos (by aesop) (by aesop)).neg

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

Goal state before:
pp: n : ℕ
c : ℕ → ℝ
hcnonneg : ∀ i ≤ n, 0 ≤ (-1) ^ i * c i
P : ℝ[X]
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
⊢ sumNodes n c P ≤ sumNodes n c (T ℝ ↑n)

Tactic:
by
  rw [sumNodes, sumNodes]
  refine Finset.sum_le_sum (fun i hi => ?_)
  calc
    P.eval (node n i) * (c i) =
      ((-1) ^ i * P.eval (node n i)) * ((-1) ^ i * (c i)) :=
      negOnePow_mul_negOnePow_mul_cancel.symm
    _ ≤ 1 * ((-1) ^ i * (c i)) := by
      gcongr
      · exact (hcnonneg i (Finset.mem_Iic.mp hi))
      · exact (negOnePow_mul_le (hPbnd _ node_mem_Icc))
    _ = (T ℝ n).eval (node n i) * (c i) := by
      rw [eval_T_real_node hi, one_mul]

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

Goal state before:
pp: case refine_2
x : Fin 2 → ℤ
hx : x ≠ 0
H1 : max (x 0).natAbs (x 1).natAbs = (x 1).natAbs
⊢ 1 ≤ (↑(x 1) / ‖x‖) ^ 2

Tactic:
· have : x 1 ≠ 0 := by
      rwa [← norm_ne_zero_iff, norm_eq_max_natAbs, H1, Nat.cast_ne_zero, Int.natAbs_ne_zero] at hx
    simp only [norm_eq_max_natAbs, H1, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

Goal state after:
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'
⊢ fib n' = a'

Tactic:
rw [← hn, fib_two_mul, H.1, H.2, ← h1]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ biprod.inl ≫ biprod.desc (g ≫ cokernel.π (f ≫ g)) (cokernel.π (f ≫ g)) = biprod.inl ≫ 0

Tactic:
biprod.inl_desc,

Goal state after:
case h₀
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ f ≫ g ≫ cokernel.π (f ≫ g) = biprod.inl ≫ 0
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (((Functor.whiskeringRight C AddCommGrpCat (Type v)).obj (forget AddCommGrpCat)).obj
        (preadditiveCoyoneda.obj (op G))).Faithful ↔
    (preadditiveCoyoneda.obj (op G)).Faithful

Tactic:
Functor.whiskeringRight_obj_obj

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveCoyoneda.obj (op G) ⋙ forget AddCommGrpCat).Faithful ↔ (preadditiveCoyoneda.obj (op G)).Faithful
Module: Mathlib.CategoryTheory.Generator.Preadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (((Functor.whiskeringRight Cᵒᵖ AddCommGrpCat (Type v)).obj (forget AddCommGrpCat)).obj
        (preadditiveYoneda.obj G)).Faithful ↔
    (preadditiveYoneda.obj G).Faithful

Tactic:
Functor.whiskeringRight_obj_obj

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
G : C
⊢ (preadditiveYoneda.obj G ⋙ forget AddCommGrpCat).Faithful ↔ (preadditiveYoneda.obj G).Faithful
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: case h₁
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
cm : ShortComplex C := ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : C ⥤ ModuleCat (End G)ᵐᵒᵖ := ⋯
faithful : φ.Faithful
⊢ Mono (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)).τ₃

Tactic:
· simp [AddCommGrpCat.mono_iff_injective, Functor.coe_mapAddHom, Functor.map_injective]

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ (i : ℕ), IntegrableOn f (Ioc (↑N) (↑i + ↑N)) volume

Tactic:
intro n
    rw [← intervalIntegrable_iff_integrableOn_Ioc_of_le (by grind)]
    exact (anti.mono <| by grind [uIcc_of_le]).intervalIntegrable

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

Goal state before:
pp: case e_β
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
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'
F : A ⥤ A'
G : B ⥤ B'
H : T ⥤ T'
iL : F ⋙ L' ≅ L ⋙ H
iR : G ⋙ R' ≅ R ⋙ H
inst✝⁴ : IsFiltered B
inst✝³ : R.Final
inst✝² : R'.Final
inst✝¹ : F.Final
inst✝ : G.Final
x✝ : Comma L' R'
i₂ : A'
j₂ : B'
u₂ : L'.obj i₂ ⟶ R'.obj j₂
this : (R ⋙ H).Final
⊢ iR.hom =
    (G.associator R' (𝟭 T' ⋙ 𝟭 T')).inv ≫
      whiskerRight (𝟙 (G ⋙ R')) (𝟭 T' ⋙ 𝟭 T') ≫
        ((𝟭 B).associator (G ⋙ R') (𝟭 T' ⋙ 𝟭 T')).hom ≫
          (𝟭 B).whiskerLeft
              (((G ⋙ R').associator (𝟭 T') (𝟭 T')).inv ≫
                whiskerRight iR.hom (𝟭 T') ≫
                  ((𝟭 B).associator (R ⋙ H) (𝟭 T')).hom ≫ (𝟭 B).whiskerLeft (𝟙 (R ⋙ H)) ≫ ((𝟭 B).associator R H).inv) ≫
            ((𝟭 B).associator (𝟭 B ⋙ R) H).inv

Tactic:
· ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : ObjectProperty.FullSubcategory IsIndObject
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
obtain ⟨⟨P⟩⟩ := X.2
    obtain ⟨⟨Q⟩⟩ := Y.2
    let e₁ := IsColimit.coconePointUniqueUpToIso (P.isColimit) (colimit.isColimit _)
    let e₂ := IsColimit.coconePointUniqueUpToIso (Q.isColimit) (colimit.isColimit _)
    let e₃ := Iso.homCongr e₁ e₂
    dsimp only [colimit.cocone_x] at e₃
    exact small_map (InducedCategory.homEquiv.trans e₃)

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v : ↥S
⊢ Sigma.ι f (↑v).as = ∑ j ∈ S.attach, Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) j ≫ Sigma.ι f (↑j).as

Tactic:
Finset.sum_eq_single v

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v : ↥S
⊢ Sigma.ι f (↑v).as = Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) v ≫ Sigma.ι f (↑v).as

case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v : ↥S
⊢ ∀ b ∈ S.attach, b ≠ v → Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) b ≫ Sigma.ι f (↑b).as = 0

case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteCoproducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
v : ↥S
⊢ v ∉ S.attach → Sigma.ι (fun x ↦ f (↑x).as) v ≫ Sigma.π (fun a ↦ f (↑a).as) v ≫ Sigma.ι f (↑v).as = 0
Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ Pi.π f (↑v).as =
    ∑ x ∈ (Opposite.unop S).attach, Pi.π f (↑x).as ≫ Pi.ι (fun a ↦ f (↑a).as) x ≫ Pi.π (fun x ↦ f (↑x).as) v

Tactic:
Finset.sum_eq_single v

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ Pi.π f (↑v).as = Pi.π f (↑v).as ≫ Pi.ι (fun a ↦ f (↑a).as) v ≫ Pi.π (fun x ↦ f (↑x).as) v

case h₀
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ ∀ b ∈ (Opposite.unop S).attach, b ≠ v → Pi.π f (↑b).as ≫ Pi.ι (fun a ↦ f (↑a).as) b ≫ Pi.π (fun x ↦ f (↑x).as) v = 0

case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasFiniteProducts C
α : Type w
inst✝¹ : DecidableEq α
f : α → C
inst✝ : HasProduct f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ v ∉ (Opposite.unop S).attach → Pi.π f (↑v).as ≫ Pi.ι (fun a ↦ f (↑a).as) v ≫ Pi.π (fun x ↦ f (↑x).as) v = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square

Goal state before:
pp: sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ sq₂.IsPullback

Tactic:
← IsPullback.map_iff sq₂ uliftFunctor.{max u v}

Goal state after:
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₂) = ⇑(ConcreteCategory.hom sq₂.f₁₂) ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ ⇑(ConcreteCategory.hom sq₁.f₁₃) = ⇑(ConcreteCategory.hom sq₂.f₁₃) ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₂₄) = ⇑(ConcreteCategory.hom sq₂.f₂₄) ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ ⇑(ConcreteCategory.hom sq₁.f₃₄) = ⇑(ConcreteCategory.hom sq₂.f₃₄) ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback
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'
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

Tactic:
obtain ⟨z, _, hz₂⟩ := @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π S.f))
        (kernel.ι S.g) _ (r ≫ a.hom ≫ Abelian.factorThruImage S.f) q (by
          simp only [Category.assoc, Abelian.image.fac]
          exact comm)

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
z : Z ⟶ pullback (kernel.ι (cokernel.π S.f)) (kernel.ι S.g)
left✝ : z ≫ pullback.fst (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = r ≫ a.hom ≫ Abelian.factorThruImage S.f
hz₂ : z ≫ pullback.snd (kernel.ι (cokernel.π S.f)) (kernel.ι S.g) = q
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ (ModuleCat.Hom.hom x.hom) a' = a

Tactic:
ha'

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑x.left
ha' : (ModuleCat.Hom.hom x.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom p) a'' = a'
⊢ a = a
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ (ModuleCat.Hom.hom y.hom) a' = a

Tactic:
ha'

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑G
a' : ↑y.left
ha' : (ModuleCat.Hom.hom y.hom) a' = a
a'' : ↑P
ha'' : (ConcreteCategory.hom q) a'' = a'
⊢ a = a
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 : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (((CochainComplex.single₀ C).obj X).d 0 1 ≫ P.ι.f 1) = 0

Tactic:
HomologicalComplex.single_obj_d,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X : C
P : InjectiveResolution X
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map (0 ≫ P.ι.f 1) = 0
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: case hc
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderKernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasKernel f.hom
⊢ IsLimit
    ((Cone.postcompose (diagramIsoParallelPair (parallelPair f 0 ⋙ P.ι)).symm.hom).obj (Fork.ofι (kernel.ι f.hom) ⋯))

Tactic:
exact (IsLimit.postcomposeInvEquiv _ _).symm (kernelIsKernel f.hom)

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
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
hz : ∃ Y' s, ∃ (_ : P.monoModSerre s), (z ≫ f) ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), z ≫ s = 0

Tactic:
obtain ⟨W, s, hs, eq⟩ := hz

Goal state after:
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
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
hf : P.monoModSerre f
Z : C
z : Z ⟶ X
W : C
s : Y ⟶ W
hs : P.monoModSerre s
eq : (z ≫ f) ≫ s = 0
⊢ ∃ Y' s, ∃ (_ : P.monoModSerre s), z ≫ s = 0
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✝¹ : HasCokernels C
inst✝ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
this : CreatesColimit (parallelPair f 0) P.ι
⊢ PreservesColimit (parallelPair f 0) P.ι

Tactic:
have := P.hasColimit_parallelPair_comp_ι f

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
P : ObjectProperty C
inst✝¹ : HasCokernels C
inst✝ : P.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
this✝ : CreatesColimit (parallelPair f 0) P.ι
this : HasColimit (parallelPair f 0 ⋙ P.ι)
⊢ PreservesColimit (parallelPair f 0) P.ι
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
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ φ.map L ⋯ = 0

Tactic:
← cancel_epi (L.map φ.s),

Goal state after:
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
this : L.EssSurj
tfae_1_to_2 : Mono (L.map f) → P.monoModSerre f
tfae_2_to_3 : P.monoModSerre f → ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
hf : ∀ ⦃Z : C⦄ (z : Z ⟶ X), L.map z ≫ L.map f = 0 → L.map z = 0
W : D
z : W ⟶ L.obj X
hz : z ≫ L.map f = 0
φ : P.isoModSerre.RightFraction (L.objPreimage W) X
hφ : (L.objObjPreimageIso W).hom ≫ z = φ.map L ⋯
⊢ L.map φ.s ≫ φ.map L ⋯ = L.map φ.s ≫ 0
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
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
hz : ∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ f ≫ z = 0
⊢ ∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ z = 0

Tactic:
obtain ⟨W, s, hs, eq⟩ := hz

Goal state after:
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
this : L.EssSurj
tfae_1_to_2 : Epi (L.map f) → P.epiModSerre f
hf : P.epiModSerre f
Z : C
z : Y ⟶ Z
W : C
s : W ⟶ X
hs : P.epiModSerre s
eq : s ≫ f ≫ z = 0
⊢ ∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ z = 0