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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
this : Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 ((sum μ) s))
a : Finset ι
ha : r < (∑ i ∈ a, μ i) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K

Tactic:
rcases MeasurableSet.exists_lt_isCompact hs ha with ⟨K, Ks, hK, h'K⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
μ✝ : Measure α
inst✝¹ : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst✝ : ∀ (i : ι), (μ i).InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < (sum μ) s
this : Tendsto (fun a ↦ ∑ i ∈ a, (μ i) s) atTop (𝓝 ((sum μ) s))
a : Finset ι
ha : r < (∑ i ∈ a, μ i) s
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : r < (∑ i ∈ a, μ i) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (sum μ) K
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
hμs : μ' s ≠ ∞
this : ∀ {s : Set G}, μ' s ≠ ∞ → MeasurableSet s → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) < ∞
sm : ¬MeasurableSet s
x : G
hx : ν' ((fun x_1 ↦ x_1 * x) ⁻¹' toMeasurable μ' s) < ∞
⊢ ν' ((fun x_1 ↦ x_1 * x) ⁻¹' s) ≤ ν' ((fun x_1 ↦ x_1 * x) ⁻¹' toMeasurable μ' s)

Tactic:
by gcongr; apply subset_toMeasurable

Goal state after:
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
t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0}
⊢ (μ.withDensity g) {x | g x = 0} = 0

Tactic:
have M : MeasurableSet { x : α | g x = 0 } := hg (measurableSet_singleton _)

Goal state after:
α : 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
t : {x | f x = 0} =ᵐ[μ.withDensity f] {x | g x = 0}
M : MeasurableSet {x | g x = 0}
⊢ (μ.withDensity g) {x | g x = 0} = 0
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
⊢ QuasiMeasurePreserving (fun h ↦ g / h) μ μ

Tactic:
simp_rw [div_eq_mul_inv]
  exact
    (measurePreserving_mul_left μ g).quasiMeasurePreserving.comp (quasiMeasurePreserving_inv μ)

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

Goal state before:
pp: case mpr
x y : ℝ
h : 0 ≤ y
⊢ -√y ≤ x ∧ x ≤ √y → x ^ 2 ≤ y

Tactic:
← abs_le,

Goal state after:
case mpr
x y : ℝ
h : 0 ≤ y
⊢ |x| ≤ √y → x ^ 2 ≤ y
Module: Mathlib.Analysis.Complex.Norm

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

Tactic:
by
  rw [edist_nndist, edist_nndist, nndist_of_re_eq h]

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

Goal state before:
pp: z : ℂ
hz : z ∈ Metric.sphere 0 1
⊢ ‖z‖ = 1

Tactic:
by simpa using hz

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

Goal state before:
pp: z : ℂ
⊢ z.re = -‖z‖ ↔ z ≤ 0

Tactic:
← neg_eq_iff_eq_neg,

Goal state after:
z : ℂ
⊢ -z.re = ‖z‖ ↔ z ≤ 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: x : ℂ
⊢ (fun z ↦ { re := z.re, im := -z.im }) ((fun z ↦ { re := z.re, im := -z.im }) x) = x

Tactic:
simp only [eta, neg_neg]

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

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z • f v‖ ≤ ‖z‖ * (b * ‖v‖)

Tactic:
exact (norm_zsmul_le _ _).trans (by gcongr; apply hb)

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ re 1 = 1

Tactic:
by rw [← ofReal_one, ofReal_re]

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

Goal state before:
pp: x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ x.re ↔ 0 ≤ x

Tactic:
rw [← RCLike.re_eq_complex_re]
  exact RCLike.re_nonneg_of_nonneg hx

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

Goal state before:
pp: z : ℂ
hz : z.re = 0 → ¬z.im = 0
⊢ (0 < z.re ∨ ¬z.im = 0) ∨ z.re < 0 ∨ ¬z.im = 0

Tactic:
by_contra! contra

Goal state after:
z : ℂ
hz : z.re = 0 → ¬z.im = 0
contra : (z.re ≤ 0 ∧ z.im = 0) ∧ 0 ≤ z.re ∧ z.im = 0
⊢ False
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖2⁻¹ • (x + star x)‖ ≤ 2⁻¹ * (2 * ‖x‖)

Tactic:
norm_smul,

Goal state after:
A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ ‖2⁻¹‖ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ normSq (z - w) = normSq z + normSq w - 2 * re (z * (starRingEnd K) w)

Tactic:
by
  simp only [normSq_add, sub_eq_add_neg, map_neg, mul_neg, normSq_neg, map_neg]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
⊢ (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n

Tactic:
by
  cases n
  · simpa only [Int.ofNat_eq_natCast, zpow_natCast] using h.pow _
  · simpa only [zpow_negSucc] using (h.pow _).inv

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
f : ℕ → β
a : ℕ → α
n : ℕ
hm : ∀ (m : ℕ), n ≤ m → abv (f m) ≤ a m
⊢ (IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i) → IsCauSeq abv fun n ↦ ∑ i ∈ range n, f i

Tactic:
intro hg ε ε0
  obtain ⟨i, hi⟩ := hg (ε / 2) (div_pos ε0 (by simp))
  exists max n i
  intro j ji
  have hi₁ := hi j (le_trans (le_max_right n i) ji)
  have hi₂ := hi (max n i) (le_max_right n i)
  have sub_le :=
    abs_sub_le (∑ k ∈ range j, a k) (∑ k ∈ range i, a k) (∑ k ∈ range (max n i), a k)
  have := add_lt_add hi₁ hi₂
  rw [abs_sub_comm (∑ k ∈ range (max n i), a k), add_halves ε] at this
  refine lt_of_le_of_lt (le_trans (le_trans ?_ (le_abs_self _)) sub_le) this
  generalize hk : j - max n i = k
  clear this hi₂ hi₁ hi ε0 ε hg sub_le
  rw [tsub_eq_iff_eq_add_of_le ji] at hk
  rw [hk]
  dsimp only
  clear hk ji j
  induction k with
  | zero => simp [abv_zero abv]
  | succ k hi =>
    simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
    simp only [add_assoc, sub_eq_add_neg]
    simp only [sub_eq_add_neg] at hi
    grw [abv_add abv, hm _ (by omega), hi]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ c * c' * ‖k₂ a✝ • g' a✝‖ = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)

Tactic:
norm_smul,

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
R : Type u_13
𝕜' : Type u_16
inst✝⁷ : SeminormedAddCommGroup E'
inst✝⁶ : SeminormedAddCommGroup F'
inst✝⁵ : SeminormedRing R
inst✝⁴ : NormedDivisionRing 𝕜'
c c' : ℝ
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : ∀ᶠ (x : α) in l, ‖k₁ x‖ ≤ c * ‖k₂ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f' x‖ ≤ c' * ‖g' x‖
a✝ : α
hx₁ : ‖k₁ a✝‖ ≤ c * ‖k₂ a✝‖
hx₂ : ‖f' a✝‖ ≤ c' * ‖g' a✝‖
⊢ c * c' * (‖k₂ a✝‖ * ‖g' a✝‖) = c * ‖k₂ a✝‖ * (c' * ‖g' a✝‖)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x : ℂ
n : ℕ
⊢ cexp (↑n * x) * cexp (1 * x) = cexp x ^ n * cexp x

Tactic:
← exp_nat_mul _ n,

Goal state after:
x : ℂ
n : ℕ
⊢ cexp (↑n * x) * cexp (1 * x) = cexp (↑n * x) * cexp x
Module: Mathlib.Analysis.Complex.Trigonometric

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

Tactic:
two_cos,

Goal state after:
x : ℂ
⊢ cexp (x * I) + cexp (-(x * I)) = cexp (x * I) + cexp (-x * I)
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
⊢ (↑n.succ - ↑n.succ * (↑n.succ)⁻¹ ^ (j - n)) / (↑n.factorial * ↑n) ≤ ↑n.succ / (↑n.factorial * ↑n)

Tactic:
by gcongr; apply sub_le_self; positivity

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⟩

Goal state after:
α : 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
C : ℝ
hC : 0 < C
ha : C⁻¹ < ‖a‖
⊢ f =O[l] g
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'
⊢ ∀ (x : α), C * ‖g'' x‖ < ‖f x‖ → ‖f x‖ / ‖g'' x‖ ≤ C'

Tactic:
simpa using hC'

Goal state after:
Module: Mathlib.Analysis.Normed.Ring.InfiniteSum

Goal state before:
pp: case refine_1
f : ℕ → ℝ
r : ℝ
hr : Tendsto (fun n ↦ ∑ i ∈ range n, |f i|) atTop (𝓝 r)
⊢ ∀ (i : ℕ), 0 ≤ ‖f i‖

Tactic:
exact fun i ↦ norm_nonneg _

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 : ℕ → β
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) ≤ ?m.259 * r

Tactic:
rw [mul_comm]

Goal state after:
α : 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) ≤ r * ?a

case a
α : 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
⊢ α
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
| ↑i * c

Tactic:
rw [mul_comm]

Goal state after:
c : ℝ
hc : c < 0
f : ℕ → ℝ
hf : ∀ (i : ℕ), ↑i ≤ f i
i : ℕ
| c * ↑i
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * closedBall y δ = closedBall (x * y) δ

Tactic:
singleton_mul,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ (fun x_1 ↦ x * x_1) '' closedBall y δ = closedBall (x * y) δ
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} * sphere y δ = sphere (x * y) δ

Tactic:
singleton_mul,

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ (fun x_1 ↦ x * x_1) '' sphere y δ = sphere (x * y) δ
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : f.IsQuotient
ε : ℝ
hε : 0 < ε
m : M
nonemp : ((fun m' ↦ ‖m + m'‖) '' ↑f.ker).Nonempty
x : M
hx : x ∈ ↑f.ker
H : ‖m + x‖ < sInf ((fun m' ↦ ‖m + m'‖) '' ↑f.ker) + ε
⊢ f (m + x) = f m

Tactic:
by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]

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
fb : f.NormNoninc
x : M ⧸ S
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖

Tactic:
have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb

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
fb : f.NormNoninc
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖(lift S f hf) x‖ ≤ ‖x‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
⊢ ‖t • x‖ = t * ‖x‖

Tactic:
norm_smul,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
t : ℝ
ht : 0 ≤ t
x : E
⊢ ‖t‖ * ‖x‖ = t * ‖x‖
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖c • (y - x)‖ < r

Tactic:
norm_smul,

Goal state after:
case convert_3
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
y : E
hy : y ∈ closedBall x r
this : ContinuousWithinAt (fun c ↦ c • (y - x) + x) (Ico 0 1) 1
c : ℝ
hc0 : 0 ≤ c
hc1 : c < 1
⊢ ‖c‖ * ‖y - x‖ < r
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ -1 ≤ c ∧ c ≤ 1

Tactic:
← abs_le,

Goal state after:
case inr.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c ↦ c • (y - x) + x
c : ℝ
hc : c ∈ f ⁻¹' closedBall x (dist y x)
⊢ |c| ≤ 1
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ cos (π / 2 - π / 3) = √3 / 2

Tactic:
← cos_pi_div_six

Goal state after:
⊢ cos (π / 2 - π / 3) = cos (π / 6)
Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise

Goal state before:
pp: E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < ε + δ
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
rw [add_comm] at hxz

Goal state after:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
⊢ ∃ z, (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ sin (↑π / 2) = ↑(Real.sin (π / 2))

Tactic:
rw [ofReal_sin]; simp

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 : C(X, Y)
⊢ (𝓝 f).HasBasis
    (fun S ↦ S.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst✝] U ∧ MapsTo (⇑f) K U) fun x ↦
    ⋂ KU ∈ x, {g | MapsTo (⇑g) KU.1 KU.2}

Tactic:
by
  refine ⟨fun s ↦ ?_⟩
  simp_rw [nhds_compactOpen, iInf_comm.{_, 0, _ + 1}, iInf_prod', iInf_and']
  simp [mem_biInf_principal, and_assoc]

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hr : r < 1
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
a : α
ha : HasSum f a
n : ℕ
⊢ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 a)

Tactic:
exact ha.tendsto_sum_nat

Goal state after:
Module: Mathlib.Topology.CompactOpen

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst✝²] (Function.uncurry fun x y ↦ x.uncurry y)

Tactic:
← (Homeomorph.prodAssoc _ _ _).comp_continuous_iff'

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Z
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
⊢ Continuous[instTopologicalSpaceProd, inst✝²]
    ((Function.uncurry fun x y ↦ x.uncurry y) ∘ ⇑(Homeomorph.prodAssoc C(X, C(Y, Z)) X Y))
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ range ⇑(γ₁.trans γ₂).extend = range ⇑γ₁ ∪ range ⇑γ₂

Tactic:
← image_univ,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
a b c : X
γ₁ : Path a b
γ₂ : Path b c
⊢ ⇑(γ₁.trans γ₂).extend '' univ = range ⇑γ₁ ∪ range ⇑γ₂
Module: Mathlib.Topology.Instances.Sign

Goal state before:
pp: α : Type u_1
inst✝⁴ : Zero α
inst✝³ : TopologicalSpace α
inst✝² : PartialOrder α
inst✝¹ : DecidableLT α
inst✝ : OrderTopology α
a : α
h : 0 < a
⊢ ∃ t, (∀ y ∈ t, 1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t

Tactic:
exact ⟨{ x | 0 < x }, fun x hx => (sign_pos hx).symm, isOpen_lt' 0, h⟩

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

Goal state before:
pp: case refine_2
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|

Tactic:
norm_smul,

Goal state after:
case refine_2
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b
n : ℕ
⊢ ‖f (n + 1) + -f n‖ * ‖(Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|
Module: Mathlib.Analysis.Normed.Group.AddCircle

Goal state before:
pp: p : ℝ
hp : Fact (0 < p)
u : AddCircle p
hu' : u ≠ 0
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
⊢ n ≠ 0

Tactic:
contrapose hu'

Goal state after:
p : ℝ
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
hn : ‖u‖ = p * (↑n / ↑(addOrderOf u))
hu : ↑(addOrderOf u) ≠ 0
hu' : n = 0
⊢ u = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
⊢ ↑(IccExtend arcsin._proof_2 ⇑sinOrderIso.symm ↑(projIcc (-1) 1 ⋯ x)) =
    (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) x

Tactic:
IccExtend_val,

Goal state after:
x : ℝ
⊢ ↑(sinOrderIso.symm (projIcc (-1) 1 ⋯ x)) = (Subtype.val ∘ IccExtend arcsin._proof_2 ⇑sinOrderIso.symm) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: case inr.inr.refine_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x

Tactic:
rw [sin_neg, sin_arcsin hx₁ hx₂]

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

Goal state before:
pp: r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < -Real.cos θ

Tactic:
← Real.cos_add_pi

Goal state after:
r : ℝ
hr : 0 < r
θ : ℝ
h₁ : θ < -(π / 2)
hθ : -π < θ
⊢ 0 < Real.cos (θ + π)
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ ‖g x‖ ≤ c / ‖f x‖

Tactic:
norm_smul,

Goal state after:
α : Type u_1
R : Type u_4
K : Type u_5
inst✝⁵ : NormedRing K
inst✝⁴ : IsDomain K
inst✝³ : NormedAddCommGroup R
inst✝² : Module K R
inst✝¹ : IsTorsionFree K R
inst✝ : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun x ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x‖ * ‖g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
hc0 : 0 < c
⊢ ‖g x‖ ≤ c / ‖f x‖
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: case hf₁
R : Type u_4
K : Type u_5
inst✝¹⁰ : NormedRing K
inst✝⁹ : IsDomain K
inst✝⁸ : NormedAddCommGroup R
inst✝⁷ : Module K R
inst✝⁶ : IsTorsionFree K R
inst✝⁵ : NormSMulClass K R
inst✝⁴ : NormSMulClass ℤ K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorSemiring K
inst✝ : HasSolidNorm K
g : ℕ → R
t : R
hg : Tendsto (fun n ↦ ↑n • g n) atTop (𝓝 t)
⊢ Tendsto (fun x ↦ ↑⌊x⌋₊) atTop (cobounded K)

Tactic:
exact tendsto_natCast_atTop_cobounded.comp tendsto_nat_floor_atTop

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

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ x < log y ↔ rexp x < y

Tactic:
rw [← exp_lt_exp, exp_log hy]

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

Goal state before:
pp: x y : ℝ
h : log x ≤ y
⊢ x ≤ rexp y

Tactic:
rcases le_or_gt x 0 with hx | hx

Goal state after:
case inl
x y : ℝ
h : log x ≤ y
hx : x ≤ 0
⊢ x ≤ rexp y

case inr
x y : ℝ
h : log x ≤ y
hx : 0 < x
⊢ x ≤ rexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: x y : ℝ
h : log x < y
⊢ x < rexp y

Tactic:
rcases le_or_gt x 0 with hx | hx

Goal state after:
case inl
x y : ℝ
h : log x < y
hx : x ≤ 0
⊢ x < rexp y

case inr
x y : ℝ
h : log x < y
hx : 0 < x
⊢ x < rexp y
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: n : ℕ
⊢ 0 ≤ log ↑n

Tactic:
exact log_natCast_nonneg _

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

Goal state before:
pp: x : ℝ
hx1 : 0 < x
hx2 : x ≠ 1
⊢ 1 ∈ Ioi 0

Tactic:
exact mem_Ioi.mpr zero_lt_one

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

Goal state before:
pp: case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑π + ↑(π / 2) = ↑(-π / 2)

Tactic:
← coe_add,

Goal state after:
case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π + π / 2) = ↑(-π / 2)