mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ ENNReal.ofReal ‖F n a - f a‖ ≤ ENNReal.ofReal (‖F n a‖ + ‖f a‖)

pp: case hp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖F n a‖

pp: case hq
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖f a‖

Tactic:
· apply ofReal_le_ofReal
          apply norm_sub_le

Goal state after:
case hp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖F n a‖

case hq
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : HasFiniteIntegral bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F n a) atTop (𝓝 (f a))
f_measurable : AEStronglyMeasurable f μ
b : α → ℝ≥0∞ := fun a ↦ 2 * ENNReal.ofReal (bound a)
n : ℕ
a : α
h₁ : ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
h₂ : ENNReal.ofReal ‖f a‖ ≤ ENNReal.ofReal (bound a)
⊢ 0 ≤ ‖f a‖
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
⊢ ‖z + w‖ * ‖z + w‖ ≤ (‖z‖ + ‖w‖) * (‖z‖ + ‖w‖)

Tactic:
rw [norm_mul_self_eq_normSq, add_mul_self_eq, norm_mul_self_eq_normSq, norm_mul_self_eq_normSq,
      add_right_comm, normSq_add, mul_assoc, norm_def, norm_def, ← Real.sqrt_mul <| normSq_nonneg z,
      ← normSq_conj w, ← map_mul]

Goal state after:
z w : ℂ
⊢ normSq z + normSq ((starRingEnd ℂ) w) + 2 * (z * (starRingEnd ℂ) w).re ≤
    normSq z + normSq ((starRingEnd ℂ) w) + 2 * √(normSq (z * (starRingEnd ℂ) w))
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ.withDensity (f * fun i ↦ (f i)⁻¹) ≤ μ

Tactic:
refine (withDensity_mono this).trans ?_

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
this : (f * fun x ↦ (f x)⁻¹) ≤ᵐ[μ] 1
⊢ μ.withDensity 1 ≤ μ
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: x : ℝ
⊢ ∀ ⦃b : ℝ⦄, x ≤ b → ↑x ≤ ↑b

Tactic:
y

Goal state after:
x y : ℝ
⊢ x ≤ y → ↑x ≤ ↑y
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case mk.mk
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 : NormedAddGroupHom V₁ V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ }.toFun =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }

Tactic:
congr

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

Goal state before:
pp: case mk.mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H :
  ⇑{ toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }

Tactic:
congr

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
⊢ Function.Injective toFun

Tactic:
apply coe_inj

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

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ ∃ C' > 0, f.SurjectiveOnWith K C'

Tactic:
refine ⟨|C| + 1, ?_, ?_⟩
  · linarith [abs_nonneg C]
  · apply h.mono
    linarith [le_abs_self C]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B ∈ {U | star U * U = 1 ∧ U * star U = 1}

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star (U * B) * (U * B) = 1

case refine_2
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * star (U * B) = 1
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₃
s : AddSubgroup V
v : ↥s
⊢ ‖↑v‖ ≤ 1 * ‖v‖

Tactic:
rw [one_mul, AddSubgroup.coe_norm]

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)
⊢ ∀ (s : ↥(unitary R)), star (x * s) = star s * star x

Tactic:
y

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x y : ↥(unitary R)
⊢ star (x * y) = star y * star x
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
⊢ ∀ (y : F), ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
y

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * ‖y‖
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
⊢ ∑' (a_1 : α), f (a_1 • a • b₂) = ∑' (c : α), f ((c * a) • b₂)

Tactic:
congr

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
⊢ (fun a_1 ↦ f (a_1 • a • b₂)) = fun c ↦ f ((c * a) • b₂)
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ normSq
      ({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝) =
    RCLike.re x✝ * RCLike.re x✝ + RCLike.im x✝ * RCLike.im x✝

Tactic:
simp [normSq_add]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
⊢ re 1 * re 1 + im 1 * im 1 = 1

Tactic:
by simp only [one_im, add_zero, mul_one, one_re, mul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: r : ℝ
⊢ ℑ ↑r = 0

Tactic:
ext1; simp [imaginaryPart_apply_coe, conj_ofReal]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
⊢ (starRingEnd ℝ) 0 = -0

Tactic:
by simp only [map_zero, neg_zero]

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

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

Tactic:
simpa only [map_zero, eq_comm] using lt_iff_re_im (z := 0) (w := z)

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

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

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

Tactic:
· rw [ofReal_mul_pos_iff] at h
      exact le_of_lt <| h.rec (False.elim <| not_lt_of_gt ·.1 ha1) (·.2)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∀ (y : K), edist (re x) (re y) ≤ ↑1 * edist x y

Tactic:
y

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ edist (re x) (re y) ≤ ↑1 * edist x y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∀ (y : K), edist (im x) (im y) ≤ ↑1 * edist x y

Tactic:
y

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ edist (im x) (im y) ≤ ↑1 * edist x y
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
h : ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
obtain ⟨c, hc⟩ := h

Goal state after:
α : Type u_1
E : Type u_3
E''' : Type u_12
inst✝¹ : Norm E
inst✝ : SeminormedAddGroup E'''
f : α → E
l : Filter α
g : α → E'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
⊢ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
h : ∃ b, ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ b
⊢ ∃ b, ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b

Tactic:
obtain ⟨c, hc⟩ := h

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝⁴ : Norm E
inst✝³ : Norm F
f : α → E
inst✝² : One F
inst✝¹ : NormOneClass F
inst✝ : TopologicalSpace α
a : α
c : ℝ
hc : ∀ᶠ (a : α) in 𝓝[≠] a, ‖f a‖ ≤ c
⊢ ∃ b, ∀ᶠ (a : α) in 𝓝 a, ‖f a‖ ≤ b
Module: Mathlib.Analysis.Asymptotics.Lemmas

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

Tactic:
isLittleO_norm_left

Goal state after:
α : Type u_1
F : Type u_4
E' : Type u_6
𝕜 : Type u_15
inst✝⁴ : Norm F
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
g : α → F
f' : α → E'
l : Filter α
inst✝¹ : Module 𝕜 E'
inst✝ : NormSMulClass 𝕜 E'
c : 𝕜
hc : c ≠ 0
cne0 : ‖c‖ ≠ 0
⊢ f' =o[l] g ↔ f' =o[l] g
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ sSup (C '' ↑s) * ∑ i ∈ s, ‖B i x‖ = sSup (C '' ↑s) * ‖∑ i ∈ s, ‖B i x‖‖

Tactic:
congr

Goal state after:
case e_a
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∑ i ∈ s, ‖B i x‖ = ‖∑ i ∈ s, ‖B i x‖‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ C * ∑ j ∈ i H, ‖B j H‖ = C * ‖∑ j ∈ i H, ‖B j H‖‖

Tactic:
congr

Goal state after:
case e_a
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
C : ℝ
i : α → Finset ι
hAB : ∀ᶠ (x : ι × α) in ⊤ ×ˢ l, ‖Function.uncurry A x‖ ≤ C * ‖Function.uncurry B x‖
s₁ : ι → Prop
hs₁ : ∀ᶠ (x : ι) in ⊤, s₁ x
s₂ : α → Prop
hs₂ : ∀ᶠ (y : α) in l, s₂ y
hbound : ∀ {x : ι}, s₁ x → ∀ {y : α}, s₂ y → ‖Function.uncurry A (x, y)‖ ≤ C * ‖Function.uncurry B (x, y)‖
H : α
hH : s₂ H
⊢ ∑ j ∈ i H, ‖B j H‖ = ‖∑ j ∈ i H, ‖B j H‖‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: 𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x / g x‖
⊢ f =O[l] g

Tactic:
obtain ⟨c, hc⟩ := h

Goal state after:
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
α : Type u_17
l : Filter α
f g : α → 𝕜
hgf : ∀ᶠ (x : α) in l, g x = 0 → f x = 0
c : ℝ
hc : ∀ᶠ (x : ℝ) in map (fun x ↦ ‖f x / g x‖) l, (fun x1 x2 ↦ x1 ≤ x2) x c
⊢ f =O[l] g
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ↑(cauSeqNorm (exp' x - const norm (∑ m ∈ range n, x ^ m / ↑m.factorial))) j ≤
    ↑(const abs (‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹))) j

Tactic:
change
    ‖(∑ m ∈ range j, x ^ m / m.factorial) - ∑ m ∈ range n, x ^ m / m.factorial‖ ≤
      ‖x‖ ^ n * ((n.succ : ℝ) * (n.factorial * n : ℝ)⁻¹)

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
n : ℕ
hn : 0 < n
j : ℕ
hj : j ≥ n
⊢ ‖∑ m ∈ range j, x ^ m / ↑m.factorial - ∑ m ∈ range n, x ^ m / ↑m.factorial‖ ≤
    ‖x‖ ^ n * (↑n.succ * (↑n.factorial * ↑n)⁻¹)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: case calc_1
x y : ℂ
⊢ cos x + cos y = cos ((x + y) / 2 + (x - y) / 2) + cos ((x + y) / 2 - (x - y) / 2)

Tactic:
congr

Goal state after:
case calc_1.e_a
x y : ℂ
⊢ x = (x + y) / 2 + (x - y) / 2

case calc_1.e_a
x y : ℂ
⊢ y = (x + y) / 2 - (x - y) / 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sin ((starRingEnd ℂ) x) = (starRingEnd ℂ) (sin x)

Tactic:
by
  rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← map_mul, ← map_mul,
    sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]

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

Goal state before:
pp: x : ℂ
⊢ cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (cos x)

Tactic:
rw [← cosh_mul_I, ← conj_neg_I, ← map_mul, ← cosh_mul_I, cosh_conj, mul_neg, cosh_neg]

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

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (sin x) / cos ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tan x)

Tactic:
cos_conj,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (sin x) / (starRingEnd ℂ) (cos x) = (starRingEnd ℂ) (tan x)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cos ((starRingEnd ℂ) x) / (starRingEnd ℂ) (sin x) = (starRingEnd ℂ) x.cot

Tactic:
cos_conj,

Goal state after:
x : ℂ
⊢ (starRingEnd ℂ) (cos x) / (starRingEnd ℂ) (sin x) = (starRingEnd ℂ) x.cot
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖sin x - (x - x ^ 3 / 6)‖ =
    ‖(cexp (-x * I) - ∑ m ∈ range 5, (-x * I) ^ m / ↑m.factorial) * I / 2 -
        (cexp (x * I) - ∑ m ∈ range 5, (x * I) ^ m / ↑m.factorial) * I / 2‖

Tactic:
simp [sin, field, Finset.sum_range_succ, Nat.factorial]

Goal state after:
x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖(cexp (-(x * I)) - cexp (x * I)) * I / 2 - (x - x ^ 3 / 6)‖ =
    ‖(cexp (-(x * I)) - (1 + -(x * I) + (x * I) ^ 2 / 2 + (-(x * I)) ^ 3 / 6 + (-(x * I)) ^ 4 / 24)) * I / 2 -
        (cexp (x * I) - (1 + x * I + (x * I) ^ 2 / 2 + (x * I) ^ 3 / 6 + (x * I) ^ 4 / 24)) * I / 2‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖
⊢ ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖

Tactic:
refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
    rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

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

Goal state before:
pp: case refine_2
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g h✝ : α → 𝕜
c : ℝ
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c * ‖h✝ x / f x‖
⊢ ∀ᶠ (x : α) in l, ‖f x * g x‖ ≤ c * ‖h✝ x‖

Tactic:
refine h.congr <| Eventually.mp hf <| Eventually.of_forall fun x hx ↦ ?_
    rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : OpenPartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
⊢ f =O[𝓝 b] g ↔ (f ∘ ↑e) =O[𝓝 (↑e.symm b)] (g ∘ ↑e)

Tactic:
simp only [IsBigO_def]
  exact exists_congr fun C => e.isBigOWith_congr hb

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

Goal state before:
pp: x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x - z * cexp x‖ = ‖cexp x * (cexp z - 1 - z)‖

Tactic:
congr

Goal state after:
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case inr
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ‖cexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !‖ ≤ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖

Tactic:
convert! exp_bound hx.out.le hn using 1

Goal state after:
n : ℕ
hn : 0 < n
x : ℂ
hx : x ∈ {y | ‖y‖ < 1}
⊢ ↑n.succ / (↑n ! * ↑n) * ‖x ^ n‖ = ‖x‖ ^ n * (↑n.succ * (↑n ! * ↑n)⁻¹)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
⊢ ∀ y ∈ {x | x.re ≤ a}, dist x y < δ → dist (cexp x) (cexp y) < ε

Tactic:
y

Goal state after:
a ε : ℝ
hε : ε > 0
this : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) (cexp 0) < ε / (2 * Real.exp a)
x : ℂ
a✝ : x ∈ {x | x.re ≤ a}
y : ℂ
⊢ y ∈ {x | x.re ≤ a} → dist x y < δ → dist (cexp x) (cexp y) < ε
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x ↦ cexp (f x)) l (𝓝 0) ↔ Tendsto (fun x ↦ (f x).re) l atBot

Tactic:
by
  simp_rw [← comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
  rfl

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedGroup E
s t : Set E
hst : IsBounded (s * t)
⊢ IsBounded s ∨ IsBounded t

Tactic:
symm
  exact AntilipschitzWith.isBounded_of_image2_left _ (fun x => (isometry_mul_left x).antilipschitz)
    (by rwa [image2_swap])

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ diam (c • x) = ‖c‖ * diam x

Tactic:
diam,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
⊢ (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 1 - 2 / 2 ^ 2 - sqrtTwoAddSeries 0 n / 2 ^ 2 = 1 / 2 - sqrtTwoAddSeries 0 n / 4

Tactic:
congr

Goal state after:
case e_a
n : ℕ
⊢ 1 - 2 / 2 ^ 2 = 1 / 2

case e_a.e_a
n : ℕ
⊢ 2 ^ 2 = 4
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ 2 - sqrtTwoAddSeries 0 n = 1 / 2 * 2 ^ 2 - sqrtTwoAddSeries 0 n / 4 * 2 ^ 2

Tactic:
congr

Goal state after:
case e_a
n : ℕ
⊢ 2 = 1 / 2 * 2 ^ 2

case e_a
n : ℕ
⊢ sqrtTwoAddSeries 0 n = sqrtTwoAddSeries 0 n / 4 * 2 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 4) = cos (π / 2 ^ 2)

Tactic:
congr

Goal state after:
case e_a
⊢ 4 = 2 ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (π / 4) = sin (π / 2 ^ 2)

Tactic:
congr

Goal state after:
case e_a
⊢ 4 = 2 ^ 2