mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
r : ℝ
⊢ IntegrableOn (fun x ↦ f ‖x‖) (ball 0 r) μ ↔ IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioo 0 r) volume

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

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

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

Tactic:
have : L.lattice ≤ G.toIntSubmodule := by
    rw [lattice, Submodule.span_le]
    rintro _ (rfl | rfl)
    · ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₁_mem_lattice⟩ L.ω₁_div_two_notMem_lattice
    · ext i
      exact L.weierstrassP_add_coe_aux _ ⟨_, L.ω₂_mem_lattice⟩ L.ω₂_div_two_notMem_lattice

Goal state after:
L : PeriodPair
z : ℂ
l : ↥L.lattice
G : AddSubgroup ℂ := { carrier := {z | (fun x ↦ ℘[L] (x + z)) = ℘[L]}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
this : L.lattice ≤ AddSubgroup.toIntSubmodule G
⊢ ℘[L] (z + ↑l) = ℘[L] z
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

Goal state after:
case inl
⊢ √(2 * π * ↑0) * (↑0 / rexp 1) ^ 0 ≤ ↑0!

case inr
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) * (↑n / rexp 1) ^ n ≤ ↑n !
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
⊢ ∀ (a : ℚ), θ = ↑a * π → θ - π / 2 = ↑(a - 1 / 2) * π

Tactic:
intros

Goal state after:
θ : ℝ
hθ : ∃ r, θ = ↑r * π
hcos : ∃ q, sin θ = ↑q
a✝¹ : ℚ
a✝ : θ = ↑a✝¹ * π
⊢ θ - π / 2 = ↑(a✝¹ - 1 / 2) * π
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ z x : ℂ
hx : ∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖
⊢ Summable (Function.uncurry fun b c ↦ L.weierstrassPExceptSummand l₀ x b c * (z - x) ^ b)

Tactic:
exact L.summable_weierstrassPExceptSummand l₀ z x hx

Goal state after:
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(box (n + 1)) = #(Icc (-↑n.succ) ↑n.succ) * #(Icc (-↑n.succ) ↑n.succ) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
by
  rw [box_succ_eq_sdiff, card_sdiff_of_subset (Icc_neg_mono n.le_succ), Finset.card_Icc_prod,
    Finset.card_Icc_prod]
  simp_rw [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, neg_add_rev, fst_add, fst_neg,
    fst_one, fst_natCast, snd_add, snd_neg, snd_one, snd_natCast]

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

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    eval x ((⇑derivative)^[k] P)

Tactic:
convert!
    (Lagrange.eval_iterate_derivative_eq_sum (strictAntiOn_node n).injOn h₁
        (show k < _ by simp [hk]) x).symm

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
h₁ : P.degree < ↑(Finset.range (n + 1)).card
⊢ ∑ i ≤ n,
      eval (node n i) P *
        (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹ *
          ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)) =
    ↑k.factorial *
      ∑ i ∈ Finset.range (n + 1),
        (eval (node n i) P / ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)) *
          ∑ t ∈ Finset.powersetCard ((Finset.range (n + 1)).card - (k + 1)) ((Finset.range (n + 1)).erase i),
            ∏ a ∈ t, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

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

Tactic:
by
  constructor
  · intro hx
    obtain ⟨k, hk₁, hk₂⟩ := (abs_eval_T_real_eq_one_iff hn x).mp
      ((abs_eq_abs.mpr (.inl hx)).trans ((abs_neg 1).trans abs_one))
    use k
    refine ⟨hk₁, ?_, hk₂⟩
    rw [hk₂, eval_T_real_cos_int_mul_pi_div hn, Int.cast_negOnePow_natCast] at hx
    exact (neg_one_pow_eq_neg_one_iff_odd (by grind)).mp hx
  · rintro ⟨k, hk₁, hk₂, hx⟩
    rw [hx, eval_T_real_cos_int_mul_pi_div hn, Int.negOnePow_odd k ((Int.odd_coe_nat k).mpr hk₂)]
    norm_cast

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
⊢ meromorphicOrderAt ℘[L] l₀ = -2

Tactic:
by
  trans ↑(-2 : ℤ)
  · rw [meromorphicOrderAt_eq_int_iff (L.meromorphic_weierstrassP l₀)]
    refine ⟨fun z ↦ (z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2, ?_, ?_, ?_⟩
    · have : AnalyticAt ℂ ℘[L - l₀] l₀ := L.analyticOnNhd_weierstrassPExcept l₀ l₀ (by simp)
      suffices AnalyticAt ℂ (fun z ↦ (z - l₀) ^ 2 / l₀ ^ 2) l₀ by fun_prop
      by_cases hl₀ : l₀ = 0
      · simpa [hl₀] using analyticAt_const
      · fun_prop (disch := simpa)
    · simp
    · filter_upwards [self_mem_nhdsWithin] with z (hz : _ ≠ _)
      have : (z - l₀) ^ 2 ≠ 0 := by simpa [sub_eq_zero]
      simp [← L.ite_eq_one_sub_sq_mul_weierstrassP l₀ h,
        if_neg hz, inv_mul_cancel_left₀ this, zpow_ofNat]
  · norm_num

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

Goal state before:
pp: case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

Tactic:
by_cases hi₃ : i = 0

Goal state after:
case pos
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : i = 0
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0

case neg
L : PeriodPair
i : ℕ
hi₁ : i < 7
hi₂ : ¬Odd i
hi₃ : ¬i = 0
⊢ iteratedDeriv i (L.relation * id ^ 6) 0 = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case mp
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ cos ((↑k + 1) * π / (↑(n - 1) + 1)) = cos (↑(k + 1) * π / ↑n)

Tactic:
congr <;> norm_cast

Goal state after:
case mp.e_a
n : ℕ
hn : 2 ≤ n
x : ℝ
hx✝ : x ∈ Finset.image (fun k ↦ cos ((↑k + 1) * π / (↑(n - 1) + 1))) (Finset.range (n - 1))
k : ℕ
hk₁ : k ∈ Finset.range (n - 1)
hx : cos ((↑k + 1) * π / (↑(n - 1) + 1)) = x
⊢ n - 1 + 1 = n
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝⁵ : Field R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
inst✝² : Archimedean R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
ha_pos : 0 ≤ a
ha : a < 1
⊢ Tendsto (fun n ↦ a ^ n * (u₀ - b / (1 - a))) atTop (𝓝 (0 * (u₀ - b / (1 - a))))

Tactic:
exact (tendsto_pow_atTop_nhds_zero_of_lt_one ha_pos ha).mul_const _

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

Goal state before:
pp: ⊢ (1 + √5) / 2 < (1 + 3) / 2

Tactic:
gcongr; rw [sqrt_lt'] <;> norm_num

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✝² : IsCofiltered A
inst✝¹ : IsCofiltered B
inst✝ : ∀ (b : B), IsCofiltered (CostructuredArrow L (R.obj b))
b : B
X : CostructuredArrow L (R.obj b)
⊢ Nonempty (Comma L R)

Tactic:
exact ⟨⟨X.left, b, X.hom⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this : IsFiltered (CostructuredArrow yoneda (colimit F))
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))

Tactic:
have : ∀ i, ∃ (s : Set (CostructuredArrow yoneda (F.obj i))) (_ : Small.{v} s),
      ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j) :=
    fun i => (hF i).finallySmall.exists_small_weakly_terminal_set

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
I : Type v
inst✝¹ : SmallCategory I
inst✝ : IsFiltered I
F : I ⥤ Cᵒᵖ ⥤ Type v
hF : ∀ (i : I), IsIndObject (F.obj i)
this✝ : IsFiltered (CostructuredArrow yoneda (colimit F))
this :
  ∀ (i : I),
    ∃ s, ∃ (_ : Small.{v, max u v} ↑s), ∀ (i_1 : CostructuredArrow yoneda (F.obj i)), ∃ j ∈ s, Nonempty (i_1 ⟶ j)
⊢ FinallySmall (CostructuredArrow yoneda (colimit F))
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✝² : IsFiltered A
inst✝¹ : IsFiltered B
inst✝ : ∀ (a : A), IsFiltered (StructuredArrow (L.obj a) R)
⊢ (snd L R).Final

Tactic:
by
  have (a : Aᵒᵖ) : IsCofiltered (CostructuredArrow R.op (L.op.obj a)) :=
    IsCofiltered.of_equivalence (structuredArrowOpEquivalence R (L.obj a.unop))
  have : (fst R.op L.op).Initial := initial_fst_of_isCofiltered_costructuredArrow _ _
  have : ((opFunctor L R).leftOp ⋙ fst R.op L.op).Initial :=
    initial_equivalence_comp (opEquiv L R).functor.leftOp _
  have : (snd L R).op.Initial := initial_of_natIso <| opFunctorCompFst _ _
  apply final_of_initial_op

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
P : IndObjectPresentation X.obj
Q : IndObjectPresentation Y.obj
e₁ : { pt := X.obj, ι := P.ι }.pt ≅ (colimit.cocone (P.F ⋙ yoneda)).pt :=
  P.isColimit.coconePointUniqueUpToIso (colimit.isColimit (P.F ⋙ yoneda))
e₂ : { pt := Y.obj, ι := Q.ι }.pt ≅ (colimit.cocone (Q.F ⋙ yoneda)).pt :=
  Q.isColimit.coconePointUniqueUpToIso (colimit.isColimit (Q.F ⋙ yoneda))
e₃ : (X.obj ⟶ Y.obj) ≃ (colimit (P.F ⋙ yoneda) ⟶ colimit (Q.F ⋙ yoneda)) := e₁.homCongr e₂
⊢ Small.{v, max u v} (X ⟶ Y)

Tactic:
exact small_map (InducedCategory.homEquiv.trans e₃)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ R.ι'.f 0 =
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) 0 X).hom ≫
      R.ι.f 0 ≫ (R.cochainComplexXIso 0 0 ι'_f_zero._proof_1).inv

Tactic:
by
  dsimp [ι']
  rw [HomologicalComplex.extendMap_f _ _ (i := 0) (by simp),
    HomologicalComplex.extendSingleIso_inv_f]
  cat_disch

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt (ofCocomplex Z) (n + 1)

Tactic:
rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
  simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofCocomplex,
    CochainComplex.mk', CochainComplex.mk, CochainComplex.of_d]
  match n with
  | 0 => apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ 0).f)
  | n + 1 => apply exact_f_d ((CochainComplex.mkAux _ _ _
      (d (Injective.ι Z)) (d (d (Injective.ι Z))) _ _ (n + 1)).f)

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 : Over P
hf : f.hom = 0
⊢ 0 = biprod.snd ≫ 0

Tactic:
HasZeroMorphisms.comp_zero

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ 0 = 0
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
F : C ⥤ D
inst✝¹ : F.Additive
X : C
inst✝ : Injective X
⊢ IsIso ((self X).toRightDerivedZero' F)

Tactic:
dsimp [InjectiveResolution.toRightDerivedZero']
  rw [CochainComplex.isIso_liftCycles_iff]
  refine ⟨ShortComplex.Splitting.exact ?_, inferInstance⟩
  exact
    { r := 𝟙 _
      s := 0
      s_g := (F.map_isZero (isZero_zero _)).eq_of_src _ _ }

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
⊢ (∃ X_1 s, ∃ (_ : P.isoModSerre s), s ≫ f = s ≫ 0) ↔ P (Abelian.image f)

Tactic:
simp [← exists_isoModSerre_comp_eq_zero_iff P]

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.IsClosedUnderCokernels
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : HasCokernel f.hom
⊢ CreatesColimit (parallelPair f 0) P.ι

Tactic:
fapply createsColimitFullSubcategoryInclusion'
  · exact (Cocone.precompose (diagramIsoParallelPair _).hom).obj
      (Cofork.ofπ (cokernel.π f.hom) (by simp))
  · exact (IsColimit.precomposeHomEquiv _ _).symm (cokernelIsCokernel f.hom)
  · exact P.prop_cokernel f.hom X.property Y.property

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
⊢ ∀ (t : X) (g : G), F.map (homOfPair t g) = F.map (homOfPair (ActionCategory.back ⟨(), t⟩) ↑(homOfPair t g))

Tactic:
intros

Goal state after:
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
t✝ : X
g✝ : G
⊢ F.map (homOfPair t✝ g✝) = F.map (homOfPair (ActionCategory.back ⟨(), t✝⟩) ↑(homOfPair t✝ g✝))
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v a b : G
h : a ≈ b
⊢ a * v⁻¹ ≈ b * v⁻¹

Tactic:
apply (QuotientGroup.leftRel_apply).mpr

Goal state after:
G : Type u_1
inst✝² : Group G
H N : Subgroup G
inst✝¹ : Fintype (G ⧸ N)
inst✝ : N.Normal
v a b : G
h : a ≈ b
⊢ (a * v⁻¹)⁻¹ * (b * v⁻¹) ∈ N
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
⊢ ∀ (x y : N), ⟨x * y, 1⟩ = ⟨x, 1⟩ * ⟨y, 1⟩

Tactic:
intros

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ ⟨x✝ * y✝, 1⟩ = ⟨x✝, 1⟩ * ⟨y✝, 1⟩
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
⊢ ∀ (x y : G), ⟨1, x * y⟩ = ⟨1, x⟩ * ⟨1, y⟩

Tactic:
intros

Goal state after:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ ⟨1, x✝ * y✝⟩ = ⟨1, x✝⟩ * ⟨1, y✝⟩
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inr g⁻¹ * inl n * inr g⁻¹⁻¹ = inr g⁻¹ * inl n * inr g

Tactic:
inv_inv

Goal state after:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inr g⁻¹ * inl n * inr g = inr g⁻¹ * inl n * inr g
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
r : R
α : F ⟶ G
⊢ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.map f ≫ (r • α.app Y) = (r • α.app X) ≫ G.map f

Tactic:
intros

Goal state after:
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
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ F.map f✝ ≫ (r • α.app Y✝) = (r • α.app X✝) ≫ G.map f✝
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
⊢ ∀ (x y : R) (b : F ⟶ G), (x * y) • b = x • y • b

Tactic:
intros

Goal state after:
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
x✝ y✝ : R
b✝ : F ⟶ G
⊢ (x✝ * y✝) • b✝ = x✝ • y✝ • b✝
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:
intros

Goal state after:
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✝
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
⊢ ∀ (a : R), a • 0 = 0

Tactic:
intros

Goal state after:
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
a✝ : R
⊢ a✝ • 0 = 0
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
⊢ ∀ (a : R) (x y : F ⟶ G), a • (x + y) = a • x + a • y

Tactic:
intros

Goal state after:
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
a✝ : R
x✝ y✝ : F ⟶ G
⊢ a✝ • (x✝ + y✝) = a✝ • x✝ + a✝ • y✝
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
⊢ ∀ (r s : R) (x : F ⟶ G), (r + s) • x = r • x + s • x

Tactic:
intros

Goal state after:
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
r✝ s✝ : R
x✝ : F ⟶ G
⊢ (r✝ + s✝) • x✝ = r✝ • x✝ + s✝ • x✝
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
⊢ ∀ (x : F ⟶ G), 0 • x = 0

Tactic:
intros

Goal state after:
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
x✝ : F ⟶ G
⊢ 0 • x✝ = 0
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
⊢ ∀ (X Y Z : C ⥤ D) (r : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r • f) ≫ g = r • f ≫ g

Tactic:
intros

Goal state after:
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
X✝ Y✝ Z✝ : C ⥤ D
r✝ : R
f✝ : X✝ ⟶ Y✝
g✝ : Y✝ ⟶ Z✝
⊢ (r✝ • f✝) ≫ g✝ = r✝ • f✝ ≫ g✝
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
⊢ ∀ (X Y Z : C ⥤ D) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g

Tactic:
intros

Goal state after:
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
X✝ Y✝ Z✝ : C ⥤ D
f✝ : X✝ ⟶ Y✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ≫ (r✝ • g✝) = r✝ • f✝ ≫ g✝
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case inr
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.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w

Tactic:
obtain ⟨l, hl⟩ := this _ (L.map φ.f) (by rw [← hφ, reassoc_of% hw, zero_comp]) ⟨_, rfl, by simp⟩

Goal state after:
case inr
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.PreservesEpimorphisms
this✝ : L.EssSurj
W : D
w : L.obj Y ⟶ W
hw : L.map f ≫ w = 0
this :
  ∀ (W : D) (w : L.obj Y ⟶ W),
    L.map f ≫ w = 0 → (∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ) → ∃ l, L.map (cokernel.π f) ≫ l = w
hw' : ¬∃ Z, ∃ (hZ : L.obj Z = W), ∃ z, w = L.map z ≫ eqToHom hZ
φ : P.isoModSerre.LeftFraction Y (L.objPreimage W)
hφ : w ≫ (L.objObjPreimageIso W).inv ≫ L.map φ.s = L.map φ.f
l : L.obj (cokernel f) ⟶ L.obj φ.Y'
hl : L.map (cokernel.π f) ≫ l = L.map φ.f
⊢ ∃ l, L.map (cokernel.π f) ≫ l = w