mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.Prod

Goal state before:
pp: G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' ((fun x ↦ x⁻¹) '' A) = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * ((fun x ↦ x⁻¹) '' A).indicator 1 x⁻¹ ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞

Tactic:
indicator_image inv_injective,

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
s✝ : Set G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
hμs : μ' s ≠ ∞
sm : MeasurableSet s
A : Set G
hA : MeasurableSet A
a✝ : μ' A < ∞
h3A : ν' A⁻¹ < ∞
h1 : μ' s * ν' ((fun x ↦ x⁻¹) '' A) = ∫⁻ (x : G), ν' ((fun z ↦ z * x) ⁻¹' s) * A.indicator (1 ∘ Inv.inv) x ∂μ'
⊢ ∫⁻ (x : G) in A, ν' ((fun y ↦ y * x) ⁻¹' s) ∂μ' ≠ ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case e_a.e_6
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
⊢ {x | f x ≠ 0} ∩ {a | ¬p a} = {a | ¬(f a ≠ 0 → p a)}

Tactic:
ext x

Goal state after:
case e_a.e_6
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
f : α → ℝ≥0∞
hf : AEMeasurable f μ
x : α
⊢ x ∈ {x | f x ≠ 0} ∩ {a | ¬p a} ↔ x ∈ {a | ¬(f a ≠ 0 → p a)}
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.ht
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f' x ≠ 0} → (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
filter_upwards [hg', hf'_ae] with a ha h'a h_a_nonneg

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
g' : α → ℝ≥0∞
g'meas : Measurable g'
hg' : ∀ᵐ (x : α) ∂μ, ↑(f x) ≠ 0 → g x = g' x
A : MeasurableSet {x | f' x ≠ 0}
a : α
ha : ↑(f a) ≠ 0 → g a = g' a
h'a : f a = f' a
h_a_nonneg : f' a ≠ 0
⊢ ↑(f a) * g a = ↑(f' a) * g' a
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: case mp.inl
x : ℝ
hle : 0 ≤ x
⊢ √x * √x = x ∧ 0 ≤ √x ∨ x < 0 ∧ √x = 0

Tactic:
exact Or.inl ⟨mul_self_sqrt hle, sqrt_nonneg x⟩

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = √y ↔ x = y

Tactic:
simp [le_antisymm_iff, hx, hy]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ √x < x ↔ 1 < x

Tactic:
by simp [← not_le]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
⊢ x < √x ↔ x ≠ 0 ∧ x < 1

Tactic:
by simp [← not_le]

Goal state after:
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ 1 < √2

Tactic:
rw [← Real.sqrt_one]

Goal state after:
⊢ √1 < √2
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: ⊢ √2 < 3 / 2

Tactic:
by
  rw [← sq_lt_sq₀ (by positivity) (by positivity)]
  grind

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (-↑x - -(I * ↑√(1 - x ^ 2))) = 1

Tactic:
sub_neg_eq_add

Goal state after:
x : ℝ
hx : ‖x‖ ≤ 1
⊢ normSq (-↑x + I * ↑√(1 - x ^ 2)) = 1
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: z w : ℂ
⊢ (z / w).re = z.re * w.re / normSq w + z.im * w.im / normSq w

Tactic:
by
  simp [div_eq_mul_inv, mul_assoc, sub_eq_add_neg]

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

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

Tactic:
ext x

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

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

Tactic:
ext x

Goal state after:
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
⊢ IsLocallyFiniteMeasure (μ.withDensity fun x ↦ ↑(f x))

Tactic:
refine ⟨fun x ↦ ?_⟩

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
⊢ (μ.withDensity fun x ↦ ↑(f x)).FiniteAtFilter (nhds x)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
⊢ (incl s).range = s

Tactic:
ext x

Goal state after:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
⊢ x ∈ (incl s).range ↔ x ∈ s
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
⊢ f.comp (ι f g) = g.comp (ι f g)

Tactic:
ext x

Goal state after:
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f g : NormedAddGroupHom V W
x : ↥(f.equalizer g)
⊢ (f.comp (ι f g)) x = (g.comp (ι f g)) x
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
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
g : Quotient (orbitRel α β) → R
⊢ automorphize (g ∘ Quotient.mk' • f) = g • automorphize f

Tactic:
ext x

Goal state after:
α : Type u_1
β : Type u_2
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
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
⊢ automorphize (g ∘ Quotient.mk' • f) x = (g • automorphize f) x
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ r • s • x = s • r • x

Tactic:
by ext <;> simp [smul_re, smul_im, smul_comm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ 1 • x = x

Tactic:
ext <;> simp [smul_re, smul_im, one_smul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) = c

Tactic:
by
        ext i
        fin_cases i <;> simp

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

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + -(algebraMap ℝ A) (y₁ * y₂)

Tactic:
← sub_eq_add_neg,

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ - (algebraMap ℝ A) (y₁ * y₂)
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
simp only [add_zero, mul_zero, map_zero]

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
⊢ ℑ.ker = selfAdjoint.submodule ℝ A

Tactic:
ext x

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ x ∈ ℑ.ker ↔ x ∈ selfAdjoint.submodule ℝ A
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: z : ℂ
⊢ ↑(ℜ z) = ↑z.re

Tactic:
by
  conv_lhs => rw [← re_add_im z]
  simp [-re_add_im, realPart_I_smul, mul_comm _ I, ← smul_eq_mul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ ↑x ≤ ↑y ↔ x ≤ y

Tactic:
rw [le_iff_re_im]
  simp

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Continuity

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
x : X
hx : x ∈ e.source
x' : X
hx' : ↑e.symm (↑e x') = x'
h : ↑e x' = ↑e x
⊢ x' ∈ {x}

Tactic:
rw [mem_singleton_iff, ← e.left_inv hx, ← h, hx']

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖reLm x‖ ≤ ‖x‖

Tactic:
exact abs_re_le_norm x

Goal state after:
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'''
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ ‖f x‖ ≤ max c 1 * ‖g x‖

Tactic:
apply hx.trans

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‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
⊢ c * ‖g x‖ ≤ max c 1 * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
h : IsBigOWith c l f g
⊢ f =O[l] g

Tactic:
by rw [IsBigO_def]; exact ⟨c, h⟩

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'

Tactic:
isBigOWith_insert

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ IsBigOWith c (𝓝[s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'

α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ ‖g x‖ ≤ c * ‖g' x‖
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type u_4
E : Type u_5
E₂ : Type u_6
E₃ : Type u_7
E₄ : Type u_8
F : Type u_9
𝓕 : Type u_10
inst✝³³ : Semiring R
inst✝³² : Semiring R₂
inst✝³¹ : Semiring R₃
inst✝³⁰ : Semiring R₄
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
σ₁₃ : R →+* R₃
σ₃₁ : R₃ →+* R
σ₁₄ : R →+* R₄
σ₄₁ : R₄ →+* R
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
σ₂₄ : R₂ →+* R₄
σ₄₂ : R₄ →+* R₂
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝²⁹ : RingHomInvPair σ₁₂ σ₂₁
inst✝²⁸ : RingHomInvPair σ₂₁ σ₁₂
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁴ : RingHomInvPair σ₃₂ σ₂₃
inst✝²³ : RingHomInvPair σ₁₄ σ₄₁
inst✝²² : RingHomInvPair σ₄₁ σ₁₄
inst✝²¹ : RingHomInvPair σ₂₄ σ₄₂
inst✝²⁰ : RingHomInvPair σ₄₂ σ₂₄
inst✝¹⁹ : RingHomInvPair σ₃₄ σ₄₃
inst✝¹⁸ : RingHomInvPair σ₄₃ σ₃₄
inst✝¹⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹⁶ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
inst✝¹⁵ : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹⁴ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝¹³ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
inst✝¹² : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁
inst✝¹¹ : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂
inst✝¹⁰ : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁
inst✝⁹ : SeminormedAddCommGroup E
inst✝⁸ : SeminormedAddCommGroup E₂
inst✝⁷ : SeminormedAddCommGroup E₃
inst✝⁶ : SeminormedAddCommGroup E₄
inst✝⁵ : Module R E
inst✝⁴ : Module R₂ E₂
inst✝³ : Module R₃ E₃
inst✝² : Module R₄ E₄
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : E →ₛₗ[σ₁₂] E₂
hf : Isometry ⇑f
⊢ ∀ (x : E), ‖f x‖ = ‖x‖

Tactic:
by
      simp_rw [← dist_zero_right]
      simpa using (hf.dist_eq · 0)

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
⊢ Finset.univ = elems

Tactic:
ext x

Goal state after:
α : Type u_1
inst✝ : Fintype α
elems : Finset α
complete : ∀ (x : α), x ∈ elems
x : α
⊢ x ∈ Finset.univ ↔ x ∈ elems
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 : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖

Tactic:
intro c hc

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
B : ι → α → ℝ
i : α → Finset ι
hAB : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (⊤ ×ˢ l) (Function.uncurry A) (Function.uncurry B)
c : ℝ
hc : 0 < c
⊢ IsBigOWith c l (fun H ↦ ∑ j ∈ i H, A j H) fun H ↦ ∑ j ∈ i H, ‖B j H‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ (cexp x + cexp (-x)) * (cexp y + cexp (-y)) + (cexp x - cexp (-x)) * (cexp y - cexp (-y)) =
    2 * (cexp x * cexp y + cexp (-x) * cexp (-y))

Tactic:
exact cosh_add_aux

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
by_cases hf : f x = 0

Goal state after:
case pos
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

case neg
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hx : C⁻¹ ≤ ‖g x‖ / ‖f x‖
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
⊢ f₁ x - -f₂ x = f₁ x + f₂ x

Tactic:
sub_neg_eq_add

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c : ℝ
l : Filter α
f₁ f₂ : α → E'
h : IsBigOWith c l f₁ f₂
hc : c < 1
x : α
⊢ f₁ x + f₂ x = f₁ x + f₂ x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ (starRingEnd ℂ) (tan ↑x) = tan ↑x

Tactic:
← tan_conj,

Goal state after:
x : ℝ
⊢ tan ((starRingEnd ℂ) ↑x) = tan ↑x
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1 - x‖ = ‖cexp x - ∑ m ∈ range 2, x ^ m / ↑m.factorial‖

Tactic:
simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc, Nat.factorial]

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1 - x‖ = ‖cexp x - ∑ m ∈ range 2, x ^ m / ↑m.factorial‖

Tactic:
by
      simp [sub_eq_add_neg, sum_range_succ_comm, add_assoc, Nat.factorial]

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

Goal state before:
pp: E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h✝ : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
by_cases hf : f x = 0

Goal state after:
case pos
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h✝ : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
hf : f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖

case neg
E'' : Type u_9
F'' : Type u_10
inst✝¹ : NormedAddCommGroup E''
inst✝ : NormedAddCommGroup F''
f : ℕ → E''
g : ℕ → F''
hfg : f =O[atTop] g
l : Filter ℕ
h✝ : ∀ᶠ (n : ℕ) in l, g n = 0 → f n = 0
C : ℝ
hC_pos : C > 0
hC : ∀ ⦃x : ℕ⦄, g x ≠ 0 → ‖f x‖ ≤ C * ‖g x‖
x : ℕ
h : g x = 0 → f x = 0
hf : ¬f x = 0
⊢ ‖f x‖ ≤ C * ‖g x‖
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
⊢ a ^ 0 = b ^ 0 ↔ 0 = 0 ∨ a = b ∨ a = -b ∧ Even 0

case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b : α
n : ℤ
hn : n ≠ 0
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
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
hε : ε / (2 * P) * P + ε / (4 * Q) * (2 * Q) = ε
hNMK : max N M + 1 < K
hKN : N < K
hsumlesum :
  ∑ i ∈ range (max N M + 1), abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range (max N M + 1), abv (f i) * (ε / (2 * P))
hsumltP : ∑ n ∈ range (max N M + 1), abv (f n) < P
⊢ ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * abv (∑ k ∈ range (K - i), g k - ∑ k ∈ range K, g k) ≤
    ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q)

Tactic:
gcongr
        rw [sub_eq_add_neg]
        grw [abv_add abv]
        rw [two_mul, abv_neg abv]
        gcongr <;> exact le_of_lt (hQ _)

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
⊢ ∀ n ≥ 0, (1 - abv x ^ n) / (1 - abv x) ≤ (1 - abv x ^ n.succ) / (1 - abv x)

Tactic:
· intro n _
    rw [← one_mul (abv x ^ n), pow_succ']
    gcongr

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

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x ↦ x ^ n / (b' * rexp x + c')) = (fun x ↦ (b' * rexp x + c') / x ^ n)⁻¹

Tactic:
ext x

Goal state after:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * rexp x + c') = (fun x ↦ (b' * rexp x + c') / x ^ n)⁻¹ x
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ).succ) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ) * r

Tactic:
refine
      le_trans (by rw [mul_comm] <;> exact h _ (Nat.le_of_succ_le kn))
        (mul_le_mul_of_nonneg_right ?_ hr0)

Goal state after:
case inr.succ
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
r : α
hr0 : 0 ≤ r
hr1 : r < 1
har1 : |r| < 1
hr : 0 < r
k : ℕ
ih :
  ∀ (n : ℕ),
    (∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)) →
      ∀ (m : ℕ), n.succ ≤ m → m = k + n.succ → abv (f m) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ m
n : ℕ
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
m : ℕ
hmn : n.succ ≤ m
hk : m = k + 1 + n.succ
kn : k + n.succ ≥ n.succ
⊢ abv (f (k + n.succ)) ≤ abv (f n.succ) * r⁻¹ ^ n.succ * r ^ (k + n.succ)
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ (fun x ↦ x ^ n / (b * rexp x + c)) = fun x ↦ -(x ^ n / (-b * rexp x + -c))

Tactic:
ext x

Goal state after:
case e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: n : ℕ
⊢ cos (↑n * π) = (-1) ^ n

Tactic:
simpa using cos_add_nat_mul_pi 0 n

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

Goal state before:
pp: M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
⊢ g = lift S f hf

Tactic:
ext x

Goal state after:
M : Type u_1
inst✝¹ : SeminormedAddCommGroup M
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ s ∈ S, f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : g.comp S.normedMk = f
x : M ⧸ S
⊢ g x = (lift S f hf) x
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
⊢ ball x✝¹ δ = {x✝¹} * ball 1 δ

Tactic:
ext x

Goal state after:
case e'_3.f
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
x✝¹ : E
x✝ : x✝¹ ∈ s
x : E
⊢ x ∈ ball x✝¹ δ ↔ x ∈ {x✝¹} * ball 1 δ
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ

Tactic:
ext x

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ x ∈ s * closedBall 1 δ ↔ x ∈ ⋃ x ∈ s, closedBall x δ