mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Regular

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OpensMeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
f : α ≃ₜ β
μ : Measure α
inst✝ : μ.OuterRegular
⊢ (map (⇑f) μ).OuterRegular

Tactic:
by
  refine ⟨fun A hA r hr => ?_⟩
  rw [map_apply f.measurable hA, ← f.image_symm] at hr
  rcases Set.exists_isOpen_lt_of_lt _ r hr with ⟨U, hAU, hUo, hU⟩
  have : IsOpen (f.symm ⁻¹' U) := hUo.preimage f.symm.continuous
  refine ⟨f.symm ⁻¹' U, image_subset_iff.1 hAU, this, ?_⟩
  rwa [map_apply f.measurable this.measurableSet, f.preimage_symm, f.preimage_image]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
inst✝ : OpensMeasurableSpace α
μ : Measure α
s : ℕ → Set α
h : ∀ (n : ℕ), (μ.restrict (s n)).OuterRegular
h' : ∀ (n : ℕ), IsOpen[inst✝¹] (s n)
h'' : univ ⊆ ⋃ n, s n
A : Set α
hA : MeasurableSet A
r : ℝ≥0∞
hr : r > μ A
HA : μ A < ∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
⊢ ∃ A', (∀ (n : ℕ), MeasurableSet (A' n)) ∧ (∀ (n : ℕ), A' n ⊆ s n) ∧ Pairwise (Disjoint on A') ∧ A = ⋃ n, A' n

Tactic:
refine
      ⟨fun n => A ∩ disjointed s n, fun n => hA.inter (MeasurableSet.disjointed hm _), fun n =>
        inter_subset_right.trans (disjointed_subset _ _),
        (disjoint_disjointed s).mono fun k l hkl => hkl.mono inf_le_right inf_le_right, ?_⟩
    rw [← inter_iUnion, iUnion_disjointed, univ_subset_iff.mp h'', inter_univ]

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

Goal state before:
pp: α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
p : Set α → Prop
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
H : μ.InnerRegularWRT p IsOpen[inst✝¹]
hd : ∀ ⦃s U : Set α⦄, p s → IsOpen[inst✝¹] U → p (s \ U)
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
h0 : p ∅
ε : ℝ≥0∞
hε : ε ≠ 0
hεs : ε + ε ≤ μ s
hr : μ s - (ε + ε) < μ s
U : Set α
hsU : U ⊇ s
hUo : IsOpen[inst✝¹] U
hUt : μ U < ∞
hμU : μ (U \ s) < ε
U' : Set α
hU'o : IsOpen[inst✝¹] U'
hμU' : μ U' < ε
hsU' : U \ U' ⊆ s
K : Set α
hKU : K ⊆ U
hKc : p K
hKr : μ U < μ K + ε
⊢ μ (K \ U') + μ U' + ε ≤ μ (K \ U') + ε + ε

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ ρ.snd s = ρ (Prod.snd ⁻¹' s)

Tactic:
snd,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ (map Prod.snd ρ) s = ρ (Prod.snd ⁻¹' s)
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 γ
inst✝¹ : SFinite ν
ρ : Measure (α × β)
inst✝ : IsZeroOrProbabilityMeasure ρ
⊢ IsZeroOrProbabilityMeasure ρ.snd

Tactic:
by
  rcases eq_zero_or_isProbabilityMeasure ρ with h | h
  · simp only [h, snd_zero]
    infer_instance
  · infer_instance

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

Goal state before:
pp: case succ
G : Type u_1
inst✝⁸ : MeasurableSpace G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : BorelSpace G
inst✝⁵ : Group G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : WeaklyLocallyCompactSpace G
inst✝² : NoncompactSpace G
μ : Measure G
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : μ.IsMulLeftInvariant
K : Set G
K1 : K ∈ 𝓝 1
hK : IsCompact K
Kclosed : IsClosed[inst✝⁷] K
K_pos : 0 < μ K
g : Set G → G
hg : ∀ (L : Set G), IsCompact L → Disjoint L (g L • K)
L : ℕ → Set G := fun n ↦ (fun T ↦ T ∪ g T • K)^[n] K
Lcompact : ∀ (n : ℕ), IsCompact (L n)
n : ℕ
IH : IsClosed[inst✝⁷] (L n)
⊢ IsClosed[inst✝⁷] (((fun T ↦ T ∪ g T • K) ∘ (fun T ↦ T ∪ g T • K)^[n]) K)

Tactic:
apply IsClosed.union IH (Kclosed.smul (g (L n)))

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (U \ s) ≤ μ (U \ K)

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ K ≤ μ s

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ≥0∞
hε : ε ≠ 0
this : ε / 2 ≠ 0
K : Set α
hKs : K ⊆ s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁴] K
hμK : μ (s \ K) < ε / 2
U : Set α
hKU : K ⊆ U
hUo : IsOpen[inst✝⁴] U
hμU : μ U < μ K + ε / 2
⊢ μ (s \ U) ≤ μ (s \ K)

Tactic:
by gcongr

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ (map (fun x ↦ a • x) μ) K < ∞

Tactic:
change map F μ K < ∞

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹⁰ : MeasurableSpace G
inst✝⁹ : MeasurableSpace H
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
μ : Measure G
inst✝⁶ : μ.IsHaarMeasure
α : Type u_3
inst✝⁵ : BorelSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : Group α
inst✝² : MulAction α G
inst✝¹ : SMulCommClass α G G
inst✝ : ContinuousConstSMul α G
a : α
K : Set G
hK : IsCompact K
F : G ≃ᵐ G := (Homeomorph.smul a).toMeasurableEquiv
⊢ (map (⇑F) μ) K < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case mp.htc
α : 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' : g =ᵐ[μ.withDensity fun x ↦ ↑(f x)] g'
A : MeasurableSet {x | f' x ≠ 0}
⊢ ∀ᵐ (x : α) ∂μ.restrict {x | f' x ≠ 0}ᶜ, (fun x ↦ ↑(f x) * g x) x = (fun x ↦ ↑(f' x) * g' x) x

Tactic:
rw [ae_restrict_iff' A.compl]
      filter_upwards [hf'_ae] with a ha ha_null
      have ha_null : f' a = 0 := Function.notMem_support.mp ha_null
      rw [ha_null] at ha ⊢
      rw [ha]
      simp only [ENNReal.coe_zero, zero_mul]

Goal state after:
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ε : Type u_7
inst✝¹ : TopologicalSpace ε
inst✝ : ESeminormedAddMonoid ε
F' : ℕ → α → ε
f' : α → ε
bound' : α → ℝ≥0∞
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F' n a‖ₑ ≤ bound' a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ F' n a) atTop (𝓝 (f' a))
⊢ ∀ᵐ (a : α) ∂μ, ‖f' a‖ₑ ≤ bound' a

Tactic:
rw [← ae_all_iff] at h_bound
  apply h_bound.mp ((ae_tendsto_enorm h_lim).mono _)
  intro a tendsto_norm h_bound
  exact le_of_tendsto' tendsto_norm h_bound

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

Goal state before:
pp: z : ℂ
⊢ (z - (starRingEnd ℂ) z).re = (↑(2 * z.im) * I).re ∧ (z - (starRingEnd ℂ) z).im = (↑(2 * z.im) * I).im

Tactic:
simp [two_mul, sub_eq_add_neg, ofReal]

Goal state after:
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 ↦ ?_⟩
  rcases (μ.finiteAt_nhds x).exists_mem_basis ((nhds_basis_opens' x).restrict_subset
    ((hf.tendsto x).eventually_le_const (lt_add_one _))) with ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩
  refine ⟨U, hUx, ?_⟩
  rw [withDensity_apply _ hUo.measurableSet]
  exact setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩

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 C' : ℝ
h : f.SurjectiveOnWith K C
H : C ≤ C'
g : V₁
k_in : f g ∈ K
hg : ‖g‖ ≤ C * ‖f g‖
Hg : ¬‖f g‖ = 0
⊢ C * ‖f g‖ ≤ C' * ‖f g‖

Tactic:
by gcongr

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₂
c : ℝ
h : ‖f‖ ≤ c
x : V₁
⊢ ‖f‖ * ‖x‖ ≤ c * ‖x‖

Tactic:
by gcongr

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star (star U) * star U = 1

Tactic:
star_star,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ U * star U = 1
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star U * star (star U) = 1

Tactic:
star_star,

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star U * U = 1
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b

Tactic:
star_inv,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
a b : G
⊢ (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : star g * g = 1 ∧ g * star g = 1
⊢ star g⁻¹ * g⁻¹ = 1 ∧ g⁻¹ * star g⁻¹ = 1

Tactic:
star_inv,

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : star g * g = 1 ∧ g * star g = 1
⊢ (star g)⁻¹ * g⁻¹ = 1 ∧ g⁻¹ * (star g)⁻¹ = 1
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
U : ↥(unitary R)
⊢ -↑U ∈ unitary R

Tactic:
by simp [mem_iff, star_neg]

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Semiring B
inst✝⁵ : TopologicalSpace B
inst✝⁴ : Semiring C
inst✝³ : TopologicalSpace C
inst✝² : Algebra R A
inst✝¹ : Algebra R B
inst✝ : Algebra R C
f g : A ≃A[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by
    obtain ⟨f', _⟩ := f
    obtain ⟨g', _⟩ := g
    rcases f' with ⟨⟨_, _⟩, _⟩
    rcases g' with ⟨⟨_, _⟩, _⟩
    congr

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
by_cases hf : Summable f L

Goal state after:
case pos
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
L : SummationFilter ι
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y
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
a : A
⊢ I • a ∈ skewAdjoint A ↔ IsSelfAdjoint a

Tactic:
by
  simp [skewAdjoint.mem_iff, IsSelfAdjoint, smul_right_inj]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
enorm_le_iff_norm_le

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖re (x - y)‖ ≤ ‖x - y‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im (x - y)‖ₑ ≤ ‖x - y‖ₑ

Tactic:
enorm_le_iff_norm_le

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : K
⊢ ‖im (x - y)‖ ≤ ‖x - y‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ 𝕜 →+ ℝ

Tactic:
exact h.re

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c c' : ℝ
f : α → E
g' : α → F'
l : Filter α
h : IsBigOWith c l f g'
hc : c ≤ c'
x : α
hx : x ∈ {x | (fun x ↦ ‖f x‖ ≤ c * ‖g' x‖) x}
⊢ c * ‖g' x‖ ≤ c' * ‖g' x‖

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : Norm E
inst✝¹ : Norm F
inst✝ : Norm G
c c' : ℝ
f : α → E
g : α → F
k : α → G
l : Filter α
hc : 0 ≤ c
hfg : ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
hgk : ∀ᶠ (x : α) in l, ‖g x‖ ≤ c' * ‖k x‖
x : α
hx : ‖f x‖ ≤ c * ‖g x‖
hx' : ‖g x‖ ≤ c' * ‖k x‖
⊢ c * ‖g x‖ ≤ c * (c' * ‖k x‖)

Tactic:
by gcongr

Goal state after:
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 ↦ c • f' x) =O[l] g ↔ f' =O[l] g

Tactic:
rw [← isBigO_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
⊢ (fun x ↦ ‖c • f' x‖) =O[l] g ↔ f' =O[l] g
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ cexp (x + y) = cexp x * cexp y

Tactic:
simp_rw [exp, exp', lim_mul_lim]

Goal state after:
x y : ℂ
hj :
  ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
⊢ lim ⟨fun n ↦ ∑ m ∈ range n, (x + y) ^ m / ↑m.factorial, ⋯⟩ =
    (⟨fun n ↦ ∑ m ∈ range n, x ^ m / ↑m.factorial, ⋯⟩ * ⟨fun n ↦ ∑ m ∈ range n, y ^ m / ↑m.factorial, ⋯⟩).lim
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ sinh (-x) = -sinh x

Tactic:
by simp [sinh, exp_neg, (neg_div _ _).symm]

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)

Tactic:
have h₄ : (n.succ - 1 : α) = n := by simp

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
h₄ : ↑n.succ - 1 = ↑n
⊢ (↑n.factorial)⁻¹ * ∑ m ∈ range (j - n), (↑n.succ)⁻¹ ^ m =
    (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ tan x * cos x = sin x

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℂ
hx : cos x ≠ 0
⊢ sin x / cos x * cos x = sin x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
hx : cos x ≠ 0
⊢ (1 + tan x ^ 2)⁻¹ = cos x ^ 2

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℂ
hx : cos x ≠ 0
⊢ (1 + (sin x / cos x) ^ 2)⁻¹ = cos x ^ 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 : α
hx : f x ≠ 0
⊢ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖ ↔ ‖g x‖ ≤ c * ‖h✝ x / f x‖

Tactic:
norm_div,

Goal state after:
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 : α
hx : f x ≠ 0
⊢ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖ ↔ ‖g x‖ ≤ c * (‖h✝ x‖ / ‖f x‖)
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℝ
⊢ ↑(cos x + cos y) = ↑(2 * cos ((x + y) / 2) * cos ((x - y) / 2))

Tactic:
by simp [cos_add_cos]

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 : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * ‖h✝ x / f x‖ ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖

Tactic:
norm_div,

Goal state after:
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 : α
hx : f x ≠ 0
⊢ ‖g x‖ ≤ c * (‖h✝ x‖ / ‖f x‖) ↔ ‖f x‖ * ‖g x‖ ≤ c * ‖h✝ x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
hx : cos x ≠ 0
⊢ tan x * cos x = sin x

Tactic:
tan_eq_sin_div_cos,

Goal state after:
x : ℝ
hx : cos x ≠ 0
⊢ sin x / cos x * cos x = sin x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: F : Type u_1
ι : Type u_2
inst✝³ : NormedRing F
inst✝² : NormMulClass F
inst✝¹ : NormOneClass F
inst✝ : CompleteSpace F
f g : ι → F
hf : Summable fun n ↦ ‖f n‖
c : F
hg : Tendsto g cofinite (𝓝 c)
⊢ Summable fun n ↦ f n * g n

Tactic:
apply summable_of_isBigO hf

Goal state after:
F : Type u_1
ι : Type u_2
inst✝³ : NormedRing F
inst✝² : NormMulClass F
inst✝¹ : NormOneClass F
inst✝ : CompleteSpace F
f g : ι → F
hf : Summable fun n ↦ ‖f n‖
c : F
hg : Tendsto g cofinite (𝓝 c)
⊢ (fun n ↦ f n * g n) =O[cofinite] fun n ↦ ‖f n‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ (fun n ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n

Tactic:
by
  refine (IsLittleO.of_norm_left ?_).of_norm_right
  exact (isLittleO_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)

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
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
⊢ |r| < 1

Tactic:
abs_of_nonneg hr0

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n : ℕ
r : α
hr0 : 0 ≤ r
hr1 : r < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ r * abv (f m)
⊢ r < 1
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ
⊢ Tendsto (fun x ↦ rexp (f x)) l (𝓝 0) ↔ Tendsto f l atBot

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

Goal state after:
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
tfae_1_to_3 : (∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_2_to_1 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =o[atTop] fun x ↦ a ^ x
tfae_3_to_2 : (∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x
tfae_2_to_4 : (∃ a ∈ Set.Ioo 0 R, f =o[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_3 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x
tfae_4_to_6 : (∃ a ∈ Set.Ioo 0 R, f =O[atTop] fun x ↦ a ^ x) → ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n
tfae_6_to_5 :
  (∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n) →
    ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n
a : ℝ
ha : a < R
C : ℝ
h₀ : 0 < C ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ C * a ^ n
⊢ ∃ a ∈ Set.Ioo (-R) R, f =O[atTop] fun x ↦ a ^ x

Tactic:
by
    rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
    · obtain rfl : f = 0 := by
        ext n
        simpa using H n
      simp only [lt_irrefl, false_or] at h₀
      exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩
    exact ⟨a, A ⟨ha₀, ha⟩,
      isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq, sq, sq, right_eq_add, mul_eq_zero, or_self]

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ infDist (-m) ↑S = ⨅ a, ‖m + ↑a‖

Tactic:
infDist_eq_iInf

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
m : M
⊢ ⨅ y, dist (-m) ↑y = ⨅ a, ‖m + ↑a‖
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 : 𝕜
hc : c ≠ 0
s : Set E
x : E
this : Function.Surjective fun x ↦ c • x
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y

Tactic:
have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
this✝ : Function.Surjective fun x ↦ c • x
this : ↑‖c‖₊ ≠ 0
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = ‖c‖₊ • ⨅ y ∈ s, edist x y