mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ (hST.equiv g).1 = ⟨1, h1⟩

Tactic:
by
  ext
  rw [equiv_fst_eq_mul_inv, equiv_snd_eq_self_of_mem_of_one_mem _ h1 hg, mul_inv_cancel]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: case refine_4
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h✝ :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
t : Set (α × β × γ)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ tᶜ = ν tᶜ

Tactic:
measure_compl ht (measure_ne_top _ _),

Goal state after:
case refine_4
α : Type u_4
β : Type u_5
γ : Type u_6
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ ν : Measure (α × β × γ)
inst✝ : IsFiniteMeasure μ
h✝ :
  ∀ {s : Set α} {t : Set β} {u : Set γ},
    MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
s : Set (α × β × γ)
hs : MeasurableSet s
h_univ : μ univ = ν univ
this : IsFiniteMeasure ν
C₂ : Set (Set (β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {t | MeasurableSet t} {u | MeasurableSet u}
C : Set (Set (α × β × γ)) := image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | MeasurableSet s} C₂
t : Set (α × β × γ)
ht : MeasurableSet t
h : μ t = ν t
⊢ μ univ - μ t = ν univ - ν t
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝⁶ : Group G
inst✝⁵ : MulAction G α
μ : Measure α
inst✝⁴ : SMulInvariantMeasure G α μ
inst✝³ : TopologicalSpace α
inst✝² : ContinuousConstSMul G α
inst✝¹ : MulAction.IsMinimal G α
U : Set α
inst✝ : μ.Regular
hμ : μ ≠ 0
hU : IsOpen[inst✝³] U
⊢ μ U = 0 ↔ U = ∅

Tactic:
rw [← not_iff_not, ← Ne, ← pos_iff_ne_zero,
    measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]

Goal state after:
Module: Mathlib.MeasureTheory.Group.Pointwise

Goal state before:
pp: G₀ : Type u_1
α : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableConstSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet (a • s)

Tactic:
← preimage_smul_inv₀ ha

Goal state after:
G₀ : Type u_1
α : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G₀ α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableConstSMul G₀ α
s : Set α
hs : MeasurableSet s
a : G₀
ha : a ≠ 0
⊢ MeasurableSet ((fun x ↦ a⁻¹ • x) ⁻¹' s)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G✝ : Type u_1
H✝ : Type u_2
inst✝⁷ : MeasurableSpace G✝
inst✝⁶ : MeasurableSpace H✝
inst✝⁵ : Mul G✝
μ✝ : Measure G✝
inst✝⁴ : MeasurableMul G✝
G : Type u_3
α : Type u_4
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
H : Subgroup G
y : ↥H
s : Set α
hs : MeasurableSet s
⊢ μ ((fun x ↦ y • x) ⁻¹' s) = μ s

Tactic:
convert! SMulInvariantMeasure.measure_preimage_smul (μ := μ) (y : G) hs

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

Goal state before:
pp: α : Type u_6
β : Type u_7
t : Set α
g : α → β
inst✝¹⁰ : TopologicalSpace α
inst✝⁹ : MeasurableSpace α
inst✝⁸ : BorelSpace α
inst✝⁷ : LinearOrder α
inst✝⁶ : OrderTopology α
inst✝⁵ : PolishSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : LinearOrder β
inst✝ : OrderTopology β
ht : MeasurableSet t
hg : MonotoneOn g t
h'g : ContinuousOn g t
⊢ MeasurableSet (g '' t)

Tactic:
by
  /- We use that the image of a measurable set by a continuous injective map is measurable.
  Therefore, we need to remove the points where the map is not injective. There are only countably
  many points that have several preimages, so this set is also measurable. -/
  let u : Set β := {c | ∃ x, ∃ y, x ∈ t ∧ y ∈ t ∧ x < y ∧ g x = c ∧ g y = c}
  have hu : Set.Countable u := MonotoneOn.countable_setOfPred_two_preimages hg
  let t' := t ∩ g ⁻¹' u
  have ht' : MeasurableSet t' := by
    have : t' = ⋃ c ∈ u, t ∩ g ⁻¹' {c} := by ext; simp [t']
    rw [this]
    apply MeasurableSet.biUnion hu (fun c hc ↦ ?_)
    obtain ⟨v, hv, tv⟩ : ∃ v, OrdConnected v ∧ t ∩ g ⁻¹' {c} = t ∩ v :=
      ordConnected_singleton.preimage_monotoneOn hg
    exact tv ▸ ht.inter hv.measurableSet
  have : g '' t = g '' (t \ t') ∪ g '' t' := by simp [← image_union, t']
  rw [this]
  apply MeasurableSet.union
  · apply (ht.diff ht').image_of_continuousOn_injOn (h'g.mono sdiff_subset)
    intro x hx y hy hxy
    contrapose! hxy
    wlog! H : x < y generalizing x y with h
    · have : y < x := lt_of_le_of_ne H hxy.symm
      exact (h hy hx hxy.symm this).symm
    intro h
    exact hx.2 ⟨hx.1, x, y, hx.1, hy.1, H, rfl, h.symm⟩
  · exact hu.mono (by simp [t']) |>.measurableSet

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ : Measure α
ν : Measure β
τ : Measure γ
ω : Type u_4
mω : MeasurableSpace ω
υ : Measure ω
inst✝² : SFinite μ
inst✝¹ : SFinite τ
inst✝ : SFinite υ
f : α → β
g : γ → ω
hf : QuasiMeasurePreserving f μ ν
hg : QuasiMeasurePreserving g τ υ
⊢ QuasiMeasurePreserving (Prod.map f g) (μ.prod τ) (ν.prod υ)

Tactic:
refine ⟨by fun_prop, ?_⟩
  rw [← map_prod_map _ _ (by fun_prop) (by fun_prop)]
  exact hf.absolutelyContinuous.prod hg.absolutelyContinuous

Goal state after:
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε

Tactic:
obtain ⟨U, hUk, hU, hμUk⟩ : ∃ (U : Set G), k ⊆ U ∧ IsOpen U ∧ μ U < μ k + ε :=
    hk.exists_isOpen_lt_add hε

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : BorelSpace G
μ : Measure G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : LocallyCompactSpace G
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : μ.InnerRegularCompactLTTop
k : Set G
hk : IsCompact k
h'k : IsClosed[inst✝⁶] k
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set G
hUk : k ⊆ U
hU : IsOpen[inst✝⁶] U
hμUk : μ U < μ k + ε
⊢ ∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε
Module: Mathlib.MeasureTheory.Constructions.Polish.Basic

Goal state before:
pp: X : Type u_6
E : Type u_7
ι : Type u_8
inst✝⁸ : MeasurableSpace X
inst✝⁷ : CommMonoid E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : PseudoMetrizableSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : MeasurableMul₂ E
L : SummationFilter ι
inst✝¹ : L.NeBot
inst✝ : L.filter.IsCountablyGenerated
μ : Measure X
f : ι → X → E
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (∏'[L] (i : ι), f i) μ

Tactic:
rw [tprod_def, finprod_def']
  split_ifs with hm
  any_goals exact aemeasurable_one
  · refine Finset.aemeasurable_prod _ (fun _ _ ↦ ?_)
    rw [Set.mulIndicator]
    split_ifs <;> fun_prop
  · apply aemeasurable_of_tendsto_metrizable_ae L.filter (f := fun s => ∏ i ∈ s, f i)
    · fun_prop
    · exact .of_forall fun x ↦ hm.choose_spec.apply_nhds x

Goal state after:
Module: Mathlib.Analysis.LConvolution

Goal state before:
pp: G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : CommGroup G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.IsInvInvariant
f g : G → ℝ≥0∞
x : G
⊢ ∫⁻ (y : G), f y * g (y⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ

Tactic:
← lintegral_mul_left_eq_self _ x,

Goal state after:
G : Type u_1
mG : MeasurableSpace G
inst✝⁴ : CommGroup G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : μ.IsInvInvariant
f g : G → ℝ≥0∞
x : G
⊢ ∫⁻ (x_1 : G), f (x * x_1) * g ((x * x_1)⁻¹ * x) ∂μ = ∫⁻ (y : G), g y * f (y⁻¹ * x) ∂μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case indicator
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
⊢ ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      ∫⁻ (a : α), s.indicator (fun x ↦ c) a ∂μ.withDensity f = ∫⁻ (a : α), (f * s.indicator fun x ↦ c) a ∂μ

Tactic:
intro c s h_ms
    simp [*, mul_comm _ c, ← indicator_mul_right]

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃! x, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0

Tactic:
simp_rw [quadratic_eq_zero_iff_discrim_eq_sq ha] at h
  generalize discrim a b c = d at h
  obtain ⟨x, rfl, hx⟩ := h
  specialize hx (-(x + b / a))
  grind

Goal state after:
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.re| < √(normSq z) ↔ z.im ≠ 0

Tactic:
Real.lt_sqrt (abs_nonneg _),

Goal state after:
z : ℂ
⊢ |z.re| ^ 2 < normSq z ↔ z.im ≠ 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a + b + c = a + (b + c)

Tactic:
intros; ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b : ℂ), a + b = b + a

Tactic:
intros; ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b c : ℂ), a * b * c = a * (b * c)

Tactic:
intros; ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: ⊢ ∀ (a b : ℂ), a * b = b * a

Tactic:
intros; ext <;> simp <;> ring

Goal state after:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case mp
a₁ a₂ b : ℝ
x : ℂ
hx : x ∈ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]]
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
obtain ⟨x₁, hx₁, hx₁'⟩ := hx

Goal state after:
case mp
a₁ a₂ b : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[a₁, a₂]]
hx₁' : (fun x ↦ ↑x + ↑b * I) x₁ = x
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case mp
a b₁ b₂ : ℝ
x : ℂ
hx : x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]]
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
obtain ⟨x₁, hx₁, hx₁'⟩ := hx

Goal state after:
case mp
a b₁ b₂ : ℝ
x : ℂ
x₁ : ℝ
hx₁ : x₁ ∈ [[b₁, b₂]]
hx₁' : (fun y ↦ ↑a + ↑y * I) x₁ = x
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖(-f.toAddMonoidHom) v‖ ≤ ‖f‖ * ‖v‖

Tactic:
simp [le_opNorm f v]

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : ↥(unitary R)
⊢ ↑(star (star x)) = ↑x

Tactic:
rw [coe_star, coe_star, star_star]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
⊢ ∃ C, ∀ (v : V₁), ‖⟨φ v, ⋯⟩‖ ≤ C * ‖v‖

Tactic:
obtain ⟨C, _C_pos, hC⟩ := φ.bound

Goal state after:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
C : ℝ
_C_pos : 0 < C
hC : ∀ (x : V₁), ‖φ x‖ ≤ C * ‖x‖
⊢ ∃ C, ∀ (v : V₁), ‖⟨φ v, ⋯⟩‖ ≤ C * ‖v‖
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) * ↑(ℑ x) = ↑(ℑ x) * ↑(ℜ x) ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
commute_iff_eq

Goal state after:
A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) * ↑(ℑ x) = ↑(ℑ x) * ↑(ℜ x) ↔ ↑(ℜ x) * ↑(ℑ x) = ↑(ℑ x) * ↑(ℜ x)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ z < w ↔ re z < re w ∧ im z = im w

Tactic:
simp_rw [lt_iff_le_and_ne, @RCLike.le_iff_re_im K]
  constructor
  · rintro ⟨⟨hr, hi⟩, heq⟩
    exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩
  · rintro ⟨⟨hr, hrn⟩, hi⟩
    exact ⟨⟨hr, hi⟩, ne_of_apply_ne _ hrn⟩

Goal state after:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, ↑x = z

Tactic:
simp_rw [neg_iff (K := K), ext_iff (K := K)]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z < 0 ∧ im z = 0 ↔ ∃ x < 0, re ↑x = re z ∧ im ↑x = im z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
h : ↑a * b ≤ ↑a * c
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b

Tactic:
rw [← ha2, ← sub_nonneg, ← mul_sub, le_iff_lt_or_eq] at h

Goal state after:
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
h : 0 < ↑a' * (c - b) ∨ 0 = ↑a' * (c - b)
ha1 : a' > 0
ha2 : ↑a' = ↑a
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ IsClosed {p | p.1 ≤ p.2}

Tactic:
conv in _ ≤ _ => rw [RCLike.le_iff_re_im]
    simp_rw [Set.ofPred_and]
    refine IsClosed.inter (isClosed_le ?_ ?_) (isClosed_eq ?_ ?_) <;> fun_prop

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖ = max c₁ c₂ * ‖‖g₁ x‖ + ‖g₂ x‖‖

Tactic:
rw [Real.norm_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _)), mul_add]

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : f₂ =o[l] g₂
⊢ (fun x ↦ f₁ x * f₂ x) =o[l] fun x ↦ g₁ x * g₂ x

Tactic:
by
  simp only [IsLittleO_def] at *
  intro c cpos
  rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩
  exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel₀ _ (ne_of_gt c'pos))

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ ‖f'' x‖ ≤ 0

Tactic:
apply le_of_tendsto_of_tendsto tendsto_const_nhds this

Goal state after:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
x : α
hx : x ∈ s
h : ∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in 𝓟 s, ‖f'' x‖ ≤ c * ‖g' x‖
this : Tendsto (fun c ↦ c * ‖g' x‖) (𝓝[>] 0) (𝓝 0)
⊢ (fun x_1 ↦ ‖f'' x‖) ≤ᶠ[𝓝[>] 0] fun c ↦ c * ‖g' x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖

Tactic:
have hc : 0 < c := pos_of_mul_pos_left ((norm_pos_iff.2 hx).trans_le hle) (norm_nonneg _)

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_15
𝕜' : Type u_16
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : NormedDivisionRing 𝕜'
c : ℝ
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : IsBigOWith c l f g
h₀✝ : ∀ᶠ (x : α) in l, f x = 0 → g x = 0
x : α
h₀ : f x = 0 → g x = 0
hle : ‖f x‖ ≤ c * ‖g x‖
hx : f x ≠ 0
hc : 0 < c
⊢ ‖(g x)⁻¹‖ ≤ c * ‖(f x)⁻¹‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm E
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
f : α → E
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ (f =o[l] fun x ↦ ‖c‖ * ‖f' x‖) ↔ f =o[l] f'

Tactic:
rw [isLittleO_const_mul_right_iff cne0, isLittleO_norm_right]

Goal state after:
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε

Tactic:
← div_div,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 / P * P + ε / (4 * Q) * (2 * Q) = ε
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z * z ^ m / (↑m.factorial * ↑m.succ)‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖

Tactic:
← div_div,

Goal state after:
z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
m : ℕ
hm : n ≤ m
⊢ ‖z * z ^ m / ↑m.factorial / ↑m.succ‖ ≤ ‖z‖ / ↑n * ‖z ^ m / ↑m.factorial‖
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 + ε / (2 * (2 * Q)) * (2 * Q) = ε

Tactic:
← div_div,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Ring β
abv : β → α
inst✝ : IsAbsoluteValue abv
f g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
h₂ : (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k
h₃ :
  ∑ i ∈ range K, f i * ∑ k ∈ range (K - i), g k =
    ∑ i ∈ range K, f i * (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) + ∑ i ∈ range K, f i * ∑ k ∈ range K, g k
two_mul_two : 4 = 2 * 2
hQ0 : Q ≠ 0
h2Q0 : 2 * Q ≠ 0
⊢ ε / 2 + ε / 2 / (2 * Q) * (2 * Q) = ε
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
⊢ (fun x ↦ (Multiset.map (fun x_1 ↦ f x_1 x) s).prod) =o[l] fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) s).prod

Tactic:
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
  exact mod_cast IsLittleO.listProd h₁ h₂

Goal state after:
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
ι : Type u_17
R : Type u_18
𝕜 : Type u_19
inst✝¹ : SeminormedCommRing R
inst✝ : NormedField 𝕜
s : Multiset ι
f : ι → α → R
g : ι → α → 𝕜
h₁ : ∀ i ∈ s, f i =O[l] g i
h₂ : ∃ i ∈ s, f i =o[l] g i
⊢ (fun x ↦ (Multiset.map (fun x_1 ↦ f x_1 x) s).prod) =o[l] fun x ↦ (Multiset.map (fun x_1 ↦ g x_1 x) s).prod

Tactic:
by
  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
  exact mod_cast IsLittleO.listProd h₁ h₂

Goal state after:
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (sinh ↑x).im = 0

Tactic:
← ofReal_sinh_ofReal_re,

Goal state after:
x : ℝ
⊢ (↑(sinh ↑x).re).im = 0