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
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ μ ≪ map (fun h ↦ g * h⁻¹) μ

Tactic:
have := map_map (μ := μ) (measurable_const_mul g) measurable_inv

Goal state after:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
this : map (fun x ↦ g * x) (map Inv.inv μ) = map ((fun x ↦ g * x) ∘ Inv.inv) μ
⊢ μ ≪ map (fun h ↦ g * h⁻¹) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t ∪ {x | f x = 0}

Tactic:
left

Goal state after:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := ⋯
x : α
hx : x ∈ s
fx : f x ≠ 0
⊢ x ∈ t
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hs : μ ({x | f x ≠ 0} ∩ s) = 0
t : Set α := toMeasurable μ ({x | f x ≠ 0} ∩ s)
A : s ⊆ t ∪ {x | f x = 0}
g : α → ℝ≥0∞
hg : Measurable g
hfg : f =ᵐ[μ] g
a : α
ha : f a = g a
h : {x | g x = 0} a
⊢ {x | f x = 0} a

Tactic:
rw [h] at ha; exact ha

Goal state after:
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 * ν' A⁻¹ = ∫⁻ (x : G), A.indicator (fun j ↦ ν' ((fun x ↦ x * j) ⁻¹' s)) x ∂μ'
⊢ μ' s * ν' A⁻¹ ≠ ∞

Tactic:
finiteness

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
μ✝ : Measure α
inst✝⁶ : TopologicalSpace α
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : PseudoMetrizableSpace X
inst✝³ : SecondCountableTopology X
inst✝² : MeasurableSpace X
inst✝¹ : BorelSpace X
μ : Measure X
inst✝ : IsLocallyFiniteMeasure μ
⊢ μ.OuterRegular

Tactic:
by
    refine (μ.finiteSpanningSetsInOpen'.mono' fun U hU => ?_).outerRegular
    have : Fact (μ U < ∞) := ⟨hU.2⟩
    exact ⟨hU.1, inferInstance⟩

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

Goal state before:
pp: case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
f' : α → ℝ≥0
hf'_m : Measurable f'
hf'_ae : f =ᵐ[μ] f'
⊢ AEMeasurable (fun x ↦ ↑(f x) * g x) μ → AEMeasurable g (μ.withDensity fun x ↦ ↑(f x))

Tactic:
· rintro ⟨g', g'meas, hg'⟩
    refine ⟨fun x => ((f' x)⁻¹ : ℝ≥0∞) * g' x, hf'_m.coe_nnreal_ennreal.inv.smul g'meas, ?_⟩
    rw [EventuallyEq, ae_withDensity_iff' hf.coe_nnreal_ennreal]
    filter_upwards [hg', hf'_ae] with a hfga hff'a h'a
    rw [hff'a] at hfga h'a
    rw [← hfga, ← mul_assoc, ENNReal.inv_mul_cancel h'a ENNReal.coe_ne_top, one_mul]

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

Goal state before:
pp: x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = ↑(NNReal.sqrt (↑x).toNNReal)

Tactic:
Real.toNNReal_coe

Goal state after:
x : ℝ≥0
⊢ ↑(NNReal.sqrt x) = ↑(NNReal.sqrt x)
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℂ
⊢ 1 < normSq x ↔ 1 < ‖x‖ ^ 2

Tactic:
normSq_eq_norm_sq

Goal state after:
x : ℂ
⊢ 1 < ‖x‖ ^ 2 ↔ 1 < ‖x‖ ^ 2
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x : ℂ
⊢ 1 ≤ normSq x ↔ 1 ≤ ‖x‖ ^ 2

Tactic:
normSq_eq_norm_sq

Goal state after:
x : ℂ
⊢ 1 ≤ ‖x‖ ^ 2 ↔ 1 ≤ ‖x‖ ^ 2
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: case hr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
F : ℕ → α → β
f : α → β
bound : α → ℝ
F_measurable : ∀ (n : ℕ), AEStronglyMeasurable (F n) μ
bound_hasFiniteIntegral : ∫⁻ (a : α), ENNReal.ofReal (bound a) ∂μ < ∞
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)
hb : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a - f a‖ ≤ b a
h : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ ENNReal.ofReal ‖F n a - f a‖) atTop (𝓝 0)
⊢ 2 ≠ ∞

Tactic:
finiteness

Goal state after:
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : MulAction ℚ≥0 α
inst✝² : MulAction ℚ α
inst✝¹ : IsScalarTower ℚ≥0 ℚ α
inst✝ : PosSMulStrictMono ℚ α
_q : ℚ≥0
hq : 0 < _q
_a₁ _a₂ : α
ha : _a₁ < _a₂
⊢ ↑_q • _a₁ < ↑_q • _a₂

Tactic:
exact smul_lt_smul_of_pos_left (α := ℚ) ha hq

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

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

Tactic:
intro hx
    obtain ⟨x₁, hx₁, hx₁'⟩ := hx
    simp [← hx₁', mem_preimage, mem_prod, hx₁]

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

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

Tactic:
intro hx
    obtain ⟨x₁, hx₁, hx₁'⟩ := hx
    simp [← hx₁', mem_preimage, mem_prod, hx₁]

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'
k : V₂
⊢ k ∈ K → ∃ g, f g = k ∧ ‖g‖ ≤ C' * ‖k‖

Tactic:
k_in

Goal state after:
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'
k : V₂
k_in : k ∈ K
⊢ ∃ g, f g = k ∧ ‖g‖ ≤ C' * ‖k‖
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:
by
    refine ⟨?_, ?_⟩
    · calc
        star (U * B) * (U * B) = star B * star U * U * B := by simp only [mul_assoc, star_mul]
        _ = star B * (star U * U) * B := by rw [← mul_assoc]
        _ = 1 := by rw [hA₁, mul_one, hB₁]
    · calc
        U * B * star (U * B) = U * B * (star B * star U) := by rw [star_mul]
        _ = U * (B * star B) * star U := by simp_rw [← mul_assoc]
        _ = 1 := by rw [hB₂, mul_one, hA₂]

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

Goal state before:
pp: r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∀ x ∈ s, x ∈ slitPlane) ↔ -↑r ∉ s

Tactic:
mem_slitPlane_iff_not_le_zero

Goal state after:
r : ℝ
s : Set ℂ
hs : s ⊆ sphere 0 r
⊢ (∀ x ∈ s, ¬x ≤ 0) ↔ -↑r ∉ s
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
⊢ I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)

Tactic:
smul_eq_zero_iff_right I_ne_zero,

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) = 0 ↔ Commute ↑(ℜ x) ↑(ℑ x)
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s) ↔ IsOpen[inst✝¹] s

Tactic:
← e.symm.isOpen_symm_image_iff_of_subset_target hs,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : s ⊆ e.source
⊢ IsOpen[inst✝] (↑e '' s) ↔ IsOpen[inst✝] (↑e.symm.symm '' s)
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 [nonpos_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
⊢ LipschitzWith 1 ⇑im

Tactic:
by
  intro x y
  simp only [ENNReal.coe_one, one_mul, edist_eq_enorm_sub]
  calc ‖im x - im y‖ₑ
  _ = ‖im (x - y)‖ₑ := by rw [map_sub im x y]
  _ ≤ ‖x - y‖ₑ := by rw [enorm_le_iff_norm_le]; exact norm_im_le_norm (x - y)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =o[map k l] g ↔ (f ∘ k) =o[l] (g ∘ k)

Tactic:
by
  simp only [IsLittleO_def, isBigOWith_map]

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'
f : α → E
g' : α → F'
l : Filter α
⊢ (f =o[l] fun x ↦ ‖g' x‖) ↔ f =o[l] g'

Tactic:
simp only [IsLittleO_def]
  exact forall₂_congr fun _ _ => isBigOWith_norm_right

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

Goal state before:
pp: n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯

Tactic:
rw [pn.out, Nat.cast_id, pn', Finset.range_add_one, Finset.insert_eq_cons]

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : IsBigOWith c₁ l f₁ g
h₂ : IsBigOWith c₂ l f₂ g
⊢ IsBigOWith (c₁ + c₂) l (fun x ↦ f₁ x - f₂ x) g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =O[l] g
h₂ : f₂ =O[l] g
⊢ (fun x ↦ f₁ x - f₂ x) =O[l] g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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

Goal state before:
pp: α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
f₁ f₂ : α → E'
h₁ : f₁ =o[l] g
h₂ : f₂ =o[l] g
⊢ (fun x ↦ f₁ x - f₂ x) =o[l] g

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_left

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

Goal state before:
pp: «$n» «$l» «$en» «$el» «$m» : ℕ
«$em» : ℕ := «$el» / 2
«$r» : ℕ
«$er» : ℕ := «$el» - «$em»
«$this» : «$el» = «$em» + «$er»
«$nm» : ℕ
«$enm» : ℕ := «$en» + «$em»
«$a» «$ea» : ℕ
«$a_prf» : «$en».ascFactorial «$em» = «$ea»
«$b» «$eb» : ℕ
«$b_prf» : «$enm».ascFactorial «$er» = «$eb»
«$eab» : ℕ := «$ea» * «$eb»
⊢ «$en».ascFactorial «$el» = «$eab»

Tactic:
by convert! asc_factorial_aux «$en» «$em» «$er» «$ea» «$eb» «$a_prf» «$b_prf»

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

Goal state before:
pp: z : ℂ
n : ℕ
hn : ‖z‖ < ↑n
hn0 : 0 < ↑n
⊢ ‖z‖ / ↑n < 1

Tactic:
rwa [div_lt_iff₀ hn0, one_mul]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
ha : a ≠ 0
⊢ f =O[l] g

Tactic:
obtain ⟨C, hC, ha⟩ : ∃ C, 0 < C ∧ C⁻¹ < ‖a‖ := ⟨‖a‖⁻¹ + 1, by positivity, by field_simp; simpa⟩
  simp only [IsBigO]
  exact ⟨C, isBigOWith_of_div_tendsto_nhds h hC ha⟩

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

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

Tactic:
by
  rw [tan_eq_sin_div_cos, div_pow]
  simp [field]

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

Goal state before:
pp: f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∀ᶠ (n₀ : ℕ) in atTop,
    ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖

Tactic:
filter_upwards [eventually_forall_ge_atTop.mpr hg, eventually_forall_ge_atTop.mpr hf, hrec]
      with n₀ hn₀ hn₀' hnrec

Goal state after:
f g : ℕ → ℝ
hf : ∀ᶠ (n : ℕ) in atTop, 0 ≤ f n
hg : ∀ᶠ (n : ℕ) in atTop, 0 < g n
hrec : ∀ᶠ (n₀ : ℕ) in atTop, ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
n₀ : ℕ
hn₀ : ∀ (y : ℕ), n₀ ≤ y → 0 < g y
hn₀' : ∀ (y : ℕ), n₀ ≤ y → 0 ≤ f y
hnrec : ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, f m ≤ C * g m) → f n ≤ C * g n
⊢ ∃ C₀, ∀ᶠ (n : ℕ) in atTop, ∀ C ≥ C₀, (∀ m ∈ Finset.Ico n₀ n, ‖f m‖ ≤ C * ‖g m‖) → ‖f n‖ ≤ C * ‖g n‖
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
h₀ : 0 < 0 ∨ 0 < R
H : ∀ (n : ℕ), |f n| ≤ 0 * a ^ n
n : ℕ
⊢ f n = 0 n

Tactic:
simpa using H n

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

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x : M ⧸ S
m : M
r ε : ℝ
⊢ ∀ (x : M ⧸ ⊥), ‖quotientBot x‖ = ‖x‖

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
M : Type u_1
inst✝ : SeminormedCommGroup M
S T : Subgroup M
x✝¹ : M ⧸ S
m : M
r ε : ℝ
x✝ : M ⧸ ⊥
x : M
⊢ ‖quotientBot (Quot.mk (⇑(leftRel ⊥)) x)‖ = ‖Quot.mk (⇑(leftRel ⊥)) x‖
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ ‖S.normedMk‖ = 1

Tactic:
refine le_antisymm (norm_normedMk_le S) ?_

Goal state after:
M : Type u_1
inst✝ : SeminormedAddCommGroup M
S : AddSubgroup M
h : ↑S.topologicalClosure ≠ univ
⊢ 1 ≤ ‖S.normedMk‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ sin (π / 2 - y) < sin (π / 2 - x)

Tactic:
apply sin_lt_sin_of_lt_of_le_pi_div_two

Goal state after:
case hx₁
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ -(π / 2) ≤ π / 2 - y

case hy₂
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ π / 2 - x ≤ π / 2

case hxy
x y : ℝ
hx₁ : 0 ≤ x
hy₂ : y ≤ π
hxy : x < y
⊢ π / 2 - y < π / 2 - x
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ x * ∑' (i : ℕ), x ^ i = ∑' (i : ℕ), x ^ (i + 1)

Tactic:
← (summable_geometric_of_norm_lt_one h).tsum_mul_left,

Goal state after:
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x * x ^ i = ∑' (i : ℕ), x ^ (i + 1)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
⊢ Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y

Tactic:
by
  refine ⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩
  rw [add_comm] at hxy
  obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy
  rw [dist_comm] at hxz
  exact h.le_bot ⟨hxz, hzy⟩

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

Goal state before:
pp: case inr.coe
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < ↑r
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ↑r

Tactic:
| coe r =>

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

Goal state before:
pp: case inl
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
ε : ℝ
hε : 0 < ε
s : Set E
hδ : 0 ≤ 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

Tactic:
rw [cthickening_zero, thickening_closure, add_zero]

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

Goal state before:
pp: R : Type u_4
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
A : HasSum (fun n ↦ (↑n + 1) * x ^ n) ((1 - x)⁻¹ʳ ^ 2)
B : HasSum (fun n ↦ x ^ n) (1 - x)⁻¹ʳ
⊢ (1 - x)⁻¹ʳ ^ 2 - (1 - x)⁻¹ʳ = (1 - x)⁻¹ʳ ^ 2 - (1 - x) * (1 - x)⁻¹ʳ * (1 - x)⁻¹ʳ

Tactic:
simp [Ring.mul_inverse_cancel (1 - x) (isUnit_one_sub_of_norm_lt_one h)]

Goal state after:
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ Surjective mk

Tactic:
rintro ⟨x⟩

Goal state after:
case mk
X : Type u_1
inst✝ : TopologicalSpace X
b✝ : ZerothHomotopy X
x : X
⊢ ∃ a, mk a = Quot.mk (⇑(pathSetoid X)) x
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : JoinedIn F x y
⊢ x ∈ F ∧ y ∈ F

Tactic:
rcases h with ⟨γ, γ_in⟩
  have : γ 0 ∈ F ∧ γ 1 ∈ F := by constructor <;> apply γ_in
  simpa using this

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f g : C(X, Y)
h : ⇑f ⤳ ⇑g
⊢ ∀ (K : Set X), IsCompact K → ∀ (U : Set Y), IsOpen[inst✝] U → MapsTo (⇑g) K U → MapsTo (⇑f) K U

Tactic:
exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)

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

Goal state before:
pp: case inr
p x t : ℝ
ht : t ≠ 0
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖

Tactic:
simp only [norm_eq_infDist, ← Real.norm_eq_abs, ← infDist_smul₀ ht, smul_zero]

Goal state after:
case inr
p x t : ℝ
ht : t ≠ 0
⊢ infDist 0 {m | ↑m = ↑(t * x)} = infDist 0 (t • {m | ↑m = ↑x})
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p x t : ℝ
⊢ ‖↑(t * x)‖ = |t| * ‖↑x‖

Tactic:
obtain rfl | ht := eq_or_ne t 0
  · simp
  simp only [norm_eq_infDist, ← Real.norm_eq_abs, ← infDist_smul₀ ht, smul_zero]
  congr 1 with m
  simp_rw [zmultiples, eq_iff_sub_mem, zsmul_eq_mul, mul_left_comm, ← smul_eq_mul, Set.range_smul]
  simp [mem_smul_set_iff_inv_smul_mem₀ ht, mul_sub, ht]

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

Goal state before:
pp: p : ℝ
hp : 0 < p
x : ℝ
⊢ ‖↑x‖ = |x - p * ↑(round (p⁻¹ * x))|

Tactic:
norm_eq,

Goal state after:
p : ℝ
hp : 0 < p
x : ℝ
⊢ |x - ↑(round (p⁻¹ * x)) * p| = |x - p * ↑(round (p⁻¹ * x))|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ ‖↑x‖ ≤ |p| / 2

Tactic:
norm_eq,

Goal state after:
case mk
p : ℝ
x✝ : AddCircle p
hp : p ≠ 0
x : ℝ
⊢ |x - ↑(round (p⁻¹ * x)) * p| ≤ |p| / 2
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: case inr
p : ℝ
hp : p ≠ 0
⊢ ‖↑(p / 2)‖ = |p| / 2

Tactic:
norm_eq,

Goal state after:
case inr
p : ℝ
hp : p ≠ 0
⊢ |p / 2 - ↑(round (p⁻¹ * (p / 2))) * p| = |p| / 2
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x : ℝ
h : 0 < x
⊢ log x < log 1 ↔ x < 1

Tactic:
exact log_lt_log_iff h zero_lt_one

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

Goal state before:
pp: case inr.inr
n : ℤ
hn : n < 0
⊢ 0 ≤ log ↑n

Tactic:
have : (1 : ℝ) ≤ -n := by rw [← neg_zero, ← lt_neg] at hn; exact mod_cast hn
          rw [← log_neg_eq_log]
          exact log_nonneg this

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

Goal state before:
pp: case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

Tactic:
left

Goal state after:
case mp.inr
θ ψ : ℝ
n : ℤ
hn : ↑n * π = (θ - ψ) / 2
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

Tactic:
left

Goal state after:
case mp.inl
θ ψ : ℝ
Hsin : cos (π / 2 - θ) = cos (π / 2 - ψ)
h : ↑(π / 2 - θ) = ↑(π / 2 - ψ)
⊢ ↑θ = ↑ψ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: case h
θ : Angle
x✝ : ℝ
⊢ θ.sin = (↑x✝).sin ↔ θ = ↑x✝ ∨ θ + ↑x✝ = ↑π

Tactic:
exact sin_eq_real_sin_iff_eq_or_add_eq_pi

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

Goal state before:
pp: ⊢ Function.Antiperiodic cos ↑π

Tactic:
intro θ
  induction θ using Real.Angle.induction_on
  exact Real.cos_antiperiodic _

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

Goal state before:
pp: θ : Angle
⊢ ↑θ.toReal = θ

Tactic:
induction θ using Real.Angle.induction_on
  exact coe_toIocMod _ _

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

Goal state before:
pp: ⊢ ↑(π / 2) ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_pi_div_two, toReal_zero]

Goal state after:
⊢ π / 2 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Goal state before:
pp: θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ θ.cos ↔ |θ.toReal| ≤ π / 2

Tactic:
← cos_toReal,

Goal state after:
θ : Angle
this✝ : 0 < π / 2
this : θ.toReal ∈ Set.Ioc (-π) π
⊢ 0 ≤ Real.cos θ.toReal ↔ |θ.toReal| ≤ π / 2
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 1 = 1

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 1 = 0

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝² : ↑x = 0
h✝¹ : ↑y = 0
h✝ : ¬x = 0
⊢ Complex.re 1 = rexp (log x * y)

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case pos
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : y = 0
⊢ Complex.re 0 = 1

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Real

Goal state before:
pp: case neg
x : ℝ
hx : 0 ≤ x
y : ℝ
h✝³ : ↑x = 0
h✝² : ¬↑y = 0
h✝¹ : x = 0
h✝ : ¬y = 0
⊢ Complex.re 0 = 0

Tactic:
simp_all [(Complex.ofReal_log hx).symm, -Complex.ofReal_mul,
      (Complex.ofReal_mul _ _).symm, Complex.exp_ofReal_re, Complex.ofReal_eq_zero]

Goal state after: