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✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (x : G), ∫⁻ (y : G), f (y * x) x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ∫⁻ (y : G), f x y ∂ν ∂μ

Tactic:
simp_rw [lintegral_lintegral h2f, lintegral_lintegral hf]

Goal state after:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
f : G → G → ℝ≥0∞
hf : AEMeasurable (uncurry f) (μ.prod ν)
h : Measurable fun z ↦ (z.2 * z.1, z.1⁻¹)
h2f : AEMeasurable (uncurry fun x y ↦ f (y * x) x⁻¹) (μ.prod ν)
⊢ ∫⁻ (z : G × G), f (z.2 * z.1) z.1⁻¹ ∂μ.prod ν = ∫⁻ (z : G × G), f z.1 z.2 ∂μ.prod ν
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 α
K : Set α
hK : IsCompact K
⊢ μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U

Tactic:
apply le_antisymm

Goal state after:
case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ μ K ≤ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U

case a
α : Type u_1
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : TopologicalSpace α
inst✝³ : μ.InnerRegularCompactLTTop
inst✝² : IsLocallyFiniteMeasure μ
inst✝¹ : R1Space α
inst✝ : BorelSpace α
K : Set α
hK : IsCompact K
⊢ ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen[inst✝⁴] U), μ U ≤ μ K
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁴ : MeasurableSpace G
inst✝³ : TopologicalSpace G
inst✝² : BorelSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : MeasurableSet s
⊢ s * closure[inst✝³] {1} = s

Tactic:
induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact hU.mul_closure_one_eq
  | compl t _ iht => exact compl_mul_closure_one_eq_iff.2 iht
  | iUnion f _ _ ihf => simp_rw [iUnion_mul f, ihf]

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

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
  convert! h.map f.symm
  rw [map_map f.symm.continuous.measurable f.continuous.measurable]
  simp

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEMeasurable (fun x ↦ ↑(f x) * g x) μ

Tactic:
have t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f' := hf

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hf : AEMeasurable f μ
g : α → ℝ≥0∞
t : ∃ f', Measurable f' ∧ f =ᵐ[μ] f'
⊢ AEMeasurable g (μ.withDensity fun x ↦ ↑(f x)) ↔ AEMeasurable (fun x ↦ ↑(f x) * g x) μ
Module: Mathlib.MeasureTheory.Function.Egorov

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst✝⁴ : PseudoEMetricSpace β
μ : Measure α
inst✝³ : SemilatticeSup ι
inst✝² : Nonempty ι
inst✝¹ : Countable ι
f : ι → α → β
g : α → β
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ι), Measurable fun a ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ
hε : 0 < ε
t : Set α
left✝ : t ⊆ univ
ht : MeasurableSet t
htendsto : μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop (univ \ t)
⊢ μ t ≤ ENNReal.ofReal ε ∧ TendstoUniformlyOn f g atTop tᶜ

Tactic:
rwa [Set.compl_eq_univ_sdiff]

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

Goal state before:
pp: x : ℝ
⊢ √(|x| * |x|) = |x|

Tactic:
sqrt_mul_self (abs_nonneg _)

Goal state after:
x : ℝ
⊢ |x| = |x|
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: n : ℤ
⊢ ‖↑n‖ = |↑n|

Tactic:
← ofReal_intCast,

Goal state after:
n : ℤ
⊢ ‖↑↑n‖ = |↑n|
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z w : ℂ
h : z.im = w.im
⊢ dist z w = dist z.re w.re

Tactic:
rw [dist_eq_re_im, h, sub_self, zero_pow two_ne_zero, add_zero, Real.sqrt_sq_eq_abs, Real.dist_eq]

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

Goal state before:
pp: z w : ℂ
⊢ ¬z.re ≤ w.re ∨ ¬z.im = w.im ↔ w.re < z.re ∨ z.im ≠ w.im

Tactic:
not_le

Goal state after:
z w : ℂ
⊢ w.re < z.re ∨ ¬z.im = w.im ↔ w.re < z.re ∨ z.im ≠ w.im
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ✝ : Measure α
f : α → ℝ≥0∞
hfm : Measurable f
μ : Measure α
inst✝ : SFinite μ
hμ : IsFiniteMeasure μ
s : Set α := {x | f x = ∞}
hs : MeasurableSet s
⊢ ∀ (i : ℕ), Measurable (s.indicator 1)

Tactic:
measurability

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

Goal state before:
pp: z : ℂ
x : ℝ
⊢ z / ↑x = { re := z.re / x, im := z.im / x }

Tactic:
by
  simp_rw [div_eq_inv_mul, ← ofReal_inv, ofReal_mul']

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

Goal state before:
pp: V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
⊢ 1 ≤ ‖id V‖

Tactic:
have := (id V).ratio_le_opNorm x

Goal state after:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : ‖(id V) x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝¹ : NonUnitalNormedRing E
inst✝ : StarRing E
h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖
x : E
⊢ ‖x⋆‖ ≤ ‖x‖

Tactic:
obtain (hx | hx) := eq_zero_or_norm_pos x⋆
        · simp [hx]
        · refine le_of_mul_le_mul_right ?_ hx
          simpa [sq, mul_comm ‖x⋆‖] using h x⋆ |>.trans <| norm_mul_le _ _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
r : ℝ
x : ℂ
⊢ star (r • x) = star r • star x

Tactic:
simp only [star_def, star_trivial, real_smul, map_mul, conj_ofReal]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
tfae_1_to_5 : (starRingEnd K) z = z → IsSelfAdjoint z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z].TFAE

Tactic:
tfae_have 5 → 1 := fun hz => by rwa [isSelfAdjoint_iff] at hz

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
tfae_1_to_4 : (starRingEnd K) z = z → im z = 0
tfae_4_to_3 : im z = 0 → ↑(re z) = z
tfae_3_to_2 : ↑(re z) = z → ∃ r, ↑r = z
tfae_2_to_1 : (∃ r, ↑r = z) → (starRingEnd K) z = z
tfae_1_to_5 : (starRingEnd K) z = z → IsSelfAdjoint z
tfae_5_to_1 : IsSelfAdjoint z → (starRingEnd K) z = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z].TFAE
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
z : ℂ
a : A
this : ℑ (z • a) = ℑ ((↑z.re + ↑z.im * I) • a)
⊢ ℑ (z • a) = z.re • ℑ a + z.im • ℜ a

Tactic:
simpa [-re_add_im, add_smul, ← smul_smul]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑n = ↑n

Tactic:
← ofReal_intCast,

Goal state after:
K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ re ↑↑n = ↑n
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ im ↑n = 0

Tactic:
← ofReal_intCast,

Goal state after:
K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ im ↑↑n = 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ ‖↑r‖ * ‖x‖ = ‖r‖ * ‖x‖

Tactic:
← ofReal_intCast,

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ ‖↑↑r‖ * ‖x‖ = ‖r‖ * ‖x‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: 𝕜 : Type u_3
W : Type u_5
G : Type u_6
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
e : G ≃ₗᵢ[𝕜] W
α : ↥(unitary 𝕜)
⊢ (α • e).symm = α⁻¹ • e.symm

Tactic:
by ext; simp [symm_smul_apply]

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

Goal state before:
pp: α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
⊢ f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0

Tactic:
refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : f'' =o[𝓟 s] g'
x : α
hx : x ∈ s
⊢ ‖f'' x‖ ≤ 0

case refine_2
α : Type u_1
F' : Type u_7
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : NormedAddCommGroup E''
g' : α → F'
f'' : α → E''
s : Set α
h : ∀ x ∈ s, f'' x = 0
⊢ f'' =o[𝓟 s] g'
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E' : Type u_6
E'' : Type u_9
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : NormedAddCommGroup E''
f' : α → E'
l : Filter α
c : E''
hc : c ≠ 0
⊢ (fun _x ↦ c) =O[l] f' ↔ ∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖

Tactic:
by
  constructor
  · intro h
    rcases h.exists_pos with ⟨C, hC₀, hC⟩
    refine ⟨‖c‖ / C, div_pos (norm_pos_iff.2 hc) hC₀, ?_⟩
    exact hC.bound.mono fun x => (div_le_iff₀' hC₀).2
  · rintro ⟨b, hb₀, hb⟩
    refine IsBigO.of_bound (‖c‖ / b) (hb.mono fun x hx => ?_)
    rw [div_mul_eq_mul_div, mul_div_assoc]
    exact le_mul_of_one_le_right (norm_nonneg _) ((one_le_div hb₀).2 hx)

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
⊢ (fun x ↦ c • f' x) =o[l] g ↔ f' =o[l] g

Tactic:
have cne0 : ‖c‖ ≠ 0 := norm_ne_zero_iff.mpr hc
  rw [← isLittleO_norm_left]
  simp only [norm_smul]
  rw [isLittleO_const_mul_left_iff cne0, isLittleO_norm_left]

Goal state after:
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'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ s, A i =O[l] B i
⊢ (fun H ↦ ∑ i ∈ s, A i H) =O[l] fun H ↦ ∑ i ∈ s, ‖B i H‖

Tactic:
simp only [IsBigO_def] at *
  choose! C hC using hAB
  exact ⟨_, IsBigOWith.sum_congr hC⟩

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

Goal state before:
pp: case hgf
α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
⊢ ∀ᶠ (x : α) in l, g x = 0 → f x = 0

Tactic:
apply (Filter.Tendsto.eventually_ge_atTop h 1).mono
    intro x h h0
    simp only [h0, zero_div] at h
    grind

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

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

Tactic:
simp only [exp]
  rw [← lim_conj]
  refine congr_arg CauSeq.lim (CauSeq.ext fun _ => ?_)
  dsimp [exp', Function.comp_def, cauSeqConj]
  rw [map_sum (starRingEnd _)]
  refine sum_congr rfl fun n _ => ?_
  rw [map_div₀, map_pow, ← ofReal_natCast, conj_ofReal]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atBot
x✝ : α
⊢ -(g x✝ / -f x✝) = g x✝ / f x✝

Tactic:
simp [div_neg_eq_neg_div]

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

Goal state before:
pp: case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ ↑(n.factorial * n.succ ^ x) ≤ ↑(x + n).factorial

Tactic:
Nat.cast_le,

Goal state after:
case hba
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ range (j - n)
⊢ n.factorial * n.succ ^ x ≤ (x + n).factorial
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x y : ℂ
⊢ cos (x + y * I) = cos x * cosh y - sin x * sinh y * I

Tactic:
rw [cos_add, cos_mul_I, sin_mul_I, mul_assoc]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ ¬‖f x‖ ≤ C * ‖g'' x‖ → ‖f x‖ ≤ C' * ‖g'' x‖

Tactic:
not_le

Goal state after:
α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
f : α → E
g'' : α → F''
h : f =O[cofinite] g''
C : ℝ
C₀ : C > 0
hC : {x | ¬‖f x‖ ≤ C * ‖g'' x‖}.Finite
C' : ℝ
hC' : ∀ i ∈ Finset.image (fun x ↦ ‖f x‖ / ‖g'' x‖) hC.toFinset, i ≤ C'
this : ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'
x : α
h₀ : g'' x ≠ 0
⊢ C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ ≤ C' * ‖g'' x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ sin x ^ 2 ≤ 1

Tactic:
← sin_sq_add_cos_sq x

Goal state after:
x : ℝ
⊢ sin x ^ 2 ≤ sin x ^ 2 + cos x ^ 2
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℝ
⊢ cos x ^ 2 ≤ 1

Tactic:
← sin_sq_add_cos_sq x

Goal state after:
x : ℝ
⊢ cos x ^ 2 ≤ sin x ^ 2 + cos x ^ 2
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℝ
hx : |x| ≤ 1
this : ‖↑x‖ ≤ 1
⊢ |rexp x - 1 - x| ≤ |x| ^ 2

Tactic:
exact_mod_cast Complex.norm_exp_sub_one_sub_id_le this

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

Goal state before:
pp: b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x ↦ (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn)
  · simp only [pow_zero, div_one]
    exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds
  simp only [add_div, mul_div_assoc]
  exact
    ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add
      (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))

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

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

Tactic:
have : 0 < sin ((y - x) / 2) := by apply sin_pos_of_pos_of_lt_pi <;> linarith

Goal state after:
x y : ℝ
hx₁ : -(π / 2) ≤ x
hy₂ : y ≤ π / 2
hxy : x < y
this : 0 < sin ((y - x) / 2)
⊢ 0 < 2 * sin ((y - x) / 2) * cos ((y + x) / 2)
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = thickening δ s

Tactic:
rw [thickening_eq_biUnion_ball]

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ s * ball 1 δ = ⋃ x ∈ s, ball x δ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ cos (π / 2 ^ 2) = √2 / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ cos (π / 2 ^ 2) = √2 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ sin (π / 2 ^ 2) = √2 / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ sin (π / 2 ^ 2) = √2 / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ cos (π / 2 ^ 3) = √(2 + √2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ sin (π / 2 ^ 3) = √(2 - √2) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ cos (π / 2 ^ 4) = √(2 + √(2 + √2)) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ cos (π / 2 ^ 5) = √(2 + √(2 + √(2 + √2))) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

pp: ⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2

Tactic:
· congr
    norm_num

Goal state after:
⊢ sin (π / 2 ^ 5) = √(2 - √(2 + √(2 + √2))) / 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
⊢ cos (π / 3) = 1 / 2

Tactic:
have : cos π < cos (π / 3) := by
      refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]

Goal state after:
case inr
h₁ : (2 * cos (π / 3) - 1) ^ 2 * (2 * cos (π / 3) + 2) = 0
h : 2 * cos (π / 3) + 2 = 0
this : cos π < cos (π / 3)
⊢ cos (π / 3) = 1 / 2
Module: Mathlib.Topology.Connected.PathConnected

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
⊢ JoinedIn F x y

Tactic:
have h₀ : x ⤳ γ' 0 := by rw [← hf.specializes_iff, hγ', γ.source]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
F : Set X
f : X → Y
hf : IsInducing f
hx : x ∈ F
hy : y ∈ F
γ : Path (f x) (f y)
γ' : ↑I → X
hγ'F : ∀ (t : ↑I), γ' t ∈ F
hγ' : ∀ (t : ↑I), f (γ' t) = γ t
h₀ : x ⤳ γ' 0
⊢ JoinedIn F x y
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : TopologicalSpace T
K✝ : Set X
U✝ : Set Y
inst✝ : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝³] U
hf : MapsTo (⇑f) K U
V : Set Y
hVo : IsOpen[inst✝³] V
hKV : ⇑f '' K ⊆ V
hVU : closure[inst✝³] V ⊆ U
g : C(X, Y)
hg : g ∈ closure {x | MapsTo (⇑x) K V}
⊢ id g ∈ closure {f | MapsTo (⇑f) K (closure[inst✝³] V)}

Tactic:
exact closure_mono (fun _ h ↦ h.mono_right subset_closure) hg

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
this : ∀ x ∈ s, Continuous[inst✝², inst✝¹] (f x)
⊢ ContinuousOn (fun x ↦ mkD (f x) g) s

Tactic:
simp_rw [continuousOn_iff_continuous_domRestrict, s.domRestrict_def]

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
f : T → X → Y
g : C(X, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ univ)
this : ∀ x ∈ s, Continuous[inst✝², inst✝¹] (f x)
⊢ Continuous[instTopologicalSpaceSubtype, _] fun x ↦ mkD (f ↑x) g
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ x ∈ s, ContinuousOn (f x) t
⊢ ContinuousOn (fun x ↦ mkD (t.domRestrict (f x)) g) s

Tactic:
simp_rw [continuousOn_iff_continuous_domRestrict, s.domRestrict_def]

Goal state after:
X : Type u_2
Y : Type u_3
T : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace T
s : Set T
t : Set X
f : T → X → Y
g : C(↑t, Y)
f_cont : ContinuousOn (Function.uncurry f) (s ×ˢ t)
this : ∀ x ∈ s, ContinuousOn (f x) t
⊢ Continuous[instTopologicalSpaceSubtype, _] fun x ↦ mkD (t.domRestrict (f ↑x)) g
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(min (m % n) (n - m % n)) / ↑n)

Tactic:
have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]
  rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]

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

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
not_le

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = √(1 - x ^ 2)

Tactic:
not_le

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (arcsin x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ ¬θ ≤ π / 2
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ

Tactic:
not_le

Goal state after:
case neg
r : ℝ
hr : 0 < r
θ : ℝ
hθ : θ ∈ Ioc (-π) π
h₁ : θ < -(π / 2) ∨ π / 2 < θ
⊢ (if 0 ≤ Real.cos θ then Real.arcsin (Real.sin θ)
    else if 0 ≤ Real.sin θ then Real.arcsin (-Real.sin θ) + π else Real.arcsin (-Real.sin θ) - π) =
    θ
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
not_le

Goal state after:
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = √(1 - x ^ 2)

Tactic:
not_le

Goal state after:
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = √(1 - x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: ⊢ arcsin '' Icc (-1) 1 = Icc (-(π / 2)) (π / 2)

Tactic:
simpa using sinPartialEquiv.symm.image_source_eq_target

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ log x = expOrderIso.symm ⟨x, hx⟩

Tactic:
rw [log_of_ne_zero hx.ne']
  congr
  exact abs_of_pos hx

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

Goal state before:
pp: ⊢ ↑(-π) = ↑π

Tactic:
coe_neg,

Goal state after:
⊢ -↑π = ↑π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: case cons
a : ℝ
l : List ℝ
ih : log l.prod = (List.map (fun x ↦ log x) l).sum
h : ¬a = 0 ∧ ∀ a ∈ l, ¬a = 0
this : l.prod ≠ 0
⊢ log (a * l.prod) = log a + (List.map (fun x ↦ log x) l).sum

Tactic:
rw [log_mul h.1 this, add_right_inj, ih]

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

Goal state before:
pp: x : ℂ
hx : x.arg ≠ π
⊢ log x⁻¹ = -log x

Tactic:
log_inv_eq_ite,

Goal state after:
x : ℂ
hx : x.arg ≠ π
⊢ (if x.arg = π then -(starRingEnd ℂ) (log x) else -log x) = -log x