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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ⨆ n, (SimpleFunc.eapprox f n).lintegral m.join = ∫⁻ (μ : Measure α), ⨆ n, (SimpleFunc.eapprox f n).lintegral μ ∂m

Tactic:
SimpleFunc.lintegral,

Goal state after:
α : Type u_1
mα : MeasurableSpace α
m : Measure (Measure α)
f : α → ℝ≥0∞
hf : AEMeasurable f m.join
hfm : Measurable f
⊢ ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * m.join (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) =
    ∫⁻ (μ : Measure α), ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (⇑(SimpleFunc.eapprox f n) ⁻¹' {x}) ∂m
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
m : MeasurableSpace X
inst✝³ : BorelSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
mZ : MeasurableSpace Z
inst✝¹ : BorelSpace Z
μ : Measure Z
inst✝ : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst✝⁴] U
Une : U.Nonempty
⊢ (comap f μ) U ≠ 0

Tactic:
hf.measurableEmbedding.comap_apply

Goal state after:
X : Type u_1
inst✝⁴ : TopologicalSpace X
m : MeasurableSpace X
inst✝³ : BorelSpace X
Z : Type u_3
inst✝² : TopologicalSpace Z
mZ : MeasurableSpace Z
inst✝¹ : BorelSpace Z
μ : Measure Z
inst✝ : μ.IsOpenPosMeasure
f : X → Z
hf : IsOpenEmbedding f
U : Set X
hU : IsOpen[inst✝⁴] U
Une : U.Nonempty
⊢ μ (f '' U) ≠ 0
Module: Mathlib.MeasureTheory.Measure.OpenPos

Goal state before:
pp: X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NullSingletonClass μ
x : X
r : ℝ
h : r ≤ 0
⊢ μ (closedBall x r) ≤ 0

Tactic:
(subsingleton_closedBall x h).measure_zero μ

Goal state after:
X : Type u_2
inst✝² : MetricSpace X
m : MeasurableSpace X
μ : Measure X
inst✝¹ : μ.IsOpenPosMeasure
inst✝ : NullSingletonClass μ
x : X
r : ℝ
h : r ≤ 0
⊢ 0 ≤ 0
Module: Mathlib.Topology.MetricSpace.PiNat

Goal state before:
pp: case inr
X : Type u_3
inst✝¹ : MetricSpace X
inst✝ : SeparableSpace X
n : ℕ
h✝ : Nonempty X
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    fun x ↦ denseSeq X n

Tactic:
convert! continuous_const (y := denseSeq X n)

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

Goal state before:
pp: M : Type u_1
inst✝⁴ : Monoid M
inst✝³ : MeasurableSpace M
inst✝² : MeasurableMul₂ M
μ ν ρ : Measure M
inst✝¹ : SFinite ν
inst✝ : SFinite ρ
⊢ (μ ∗ₘ ν) ∗ₘ ρ = μ ∗ₘ ν ∗ₘ ρ

Tactic:
by
  refine ext_of_lintegral _ fun f hf ↦ ?_
  repeat rw [lintegral_mconv (by fun_prop)]
  refine lintegral_congr fun x ↦ ?_
  rw [lintegral_mconv (by fun_prop)]
  repeat refine lintegral_congr fun x ↦ ?_
  simp [mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S
hx : (↑x)⁻¹ * g ∈ T
hx' : ∀ (y : ↑S), (fun s ↦ (↑s)⁻¹ * g ∈ T) y → y = x
⊢ ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = (x, ⟨(↑x)⁻¹ * g, hx⟩)

Tactic:
by aesop

Goal state after:
Module: Mathlib.GroupTheory.Complement

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t ↦ g * (↑t)⁻¹ ∈ S) y → y = x
⊢ ∀ (y : ↑S × ↑T), (fun x ↦ ↑x.1 * ↑x.2 = g) y → y = (⟨g * (↑x)⁻¹, hx⟩, x)

Tactic:
by aesop

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
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i < r - μ (⋃ n, A n)
⊢ ∃ U ⊇ ⋃ n, A n, IsOpen[inst✝¹] U ∧ μ U < r

Tactic:
lt_tsub_iff_right,

Goal state after:
α : 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
r : ℝ≥0∞
hm : ∀ (n : ℕ), MeasurableSet (s n)
A : ℕ → Set α
hAm : ∀ (n : ℕ), MeasurableSet (A n)
hAs : ∀ (n : ℕ), A n ⊆ s n
hAd : Pairwise (Disjoint on A)
hA : MeasurableSet (⋃ n, A n)
hr : r > μ (⋃ n, A n)
HA : μ (⋃ n, A n) < ∞
δ : ℕ → ℝ≥0∞
δ0 : ∀ (i : ℕ), 0 < δ i
hδε : ∑' (i : ℕ), δ i + μ (⋃ n, A n) < r
⊢ ∃ U ⊇ ⋃ n, A n, IsOpen[inst✝¹] U ∧ μ U < r
Module: Mathlib.MeasureTheory.Group.Action

Goal state before:
pp: G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
rw [← measure_toMeasurable s,
    ← SMulInvariantMeasure.measure_preimage_smul c (measurableSet_toMeasurable μ s)]

Goal state after:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝¹ : SMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : NullMeasurableSet s μ
c : G
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ ((fun x ↦ c • x) ⁻¹' toMeasurable μ s)
Module: Mathlib.MeasureTheory.Group.Measure

Goal state before:
pp: G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : TopologicalSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : μ.IsMulLeftInvariant
K : Set G
hK : IsCompact K
h : μ K ≠ 0
⊢ μ.IsOpenPosMeasure

Tactic:
refine ⟨fun U hU hne => ?_⟩
  contrapose h
  rw [← nonpos_iff_eq_zero]
  rw [← hU.interior_eq] at hne
  obtain ⟨t, hKt⟩ : ∃ t : Finset G, K ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U :=
    compact_covered_by_mul_left_translates hK hne
  calc
    μ K ≤ μ (⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U) := measure_mono hKt
    _ ≤ ∑ g ∈ t, μ ((fun h : G => g * h) ⁻¹' U) := measure_biUnion_finset_le _ _
    _ = 0 := by simp [measure_preimage_mul, h]

Goal state after:
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, r < (∑ i ∈ a, μ i) s

Tactic:
by
    simp only [coe_finsetSum, Finset.sum_apply]
    exact ((tendsto_order.1 this).1 r hr).exists

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
a b c : R
inst✝¹ : NeZero 2
inst✝ : NoZeroDivisors R
ha✝ : a ≠ 0
x : R
h : b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2
ha : 2 * 2 * a ≠ 0
⊢ 2 * 2 * a * (a * (x * x) + b * x + c) = 2 * 2 * a * 0

Tactic:
linear_combination -h

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

Goal state before:
pp: case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
hfx : ¬f x = ∞
⊢ ENNReal.ofReal (f x).toReal ≤ f x

Tactic:
lift f x to ℝ≥0 using hfx with fx h

Goal state after:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
h✝ : ∀ (x : α), ‖(f x).toReal‖ₑ = ENNReal.ofReal (f x).toReal
x : α
fx : ℝ≥0
h : ↑fx = f x
⊢ ENNReal.ofReal (↑fx).toReal ≤ ↑fx
Module: Mathlib.Analysis.Real.Sqrt

Goal state before:
pp: x : ℝ
h : 0 ≤ x
⊢ √(x * x) = x

Tactic:
sqrt_mul_self h

Goal state after:
x : ℝ
h : 0 ≤ x
⊢ x = x
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(m ^ 2 + m ^ 2) = √2 * m

Tactic:
← two_mul,

Goal state after:
x y : ℝ
m : ℝ := max |x| |y|
hm₀ : 0 ≤ m
⊢ √(2 * m ^ 2) = √2 * m
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.im - -z.im| = 2 * |z.im|

Tactic:
sub_neg_eq_add,

Goal state after:
z : ℂ
⊢ |z.im + z.im| = 2 * |z.im|
Module: Mathlib.Analysis.Complex.Norm

Goal state before:
pp: z : ℂ
⊢ |z.im + z.im| = 2 * |z.im|

Tactic:
← two_mul,

Goal state after:
z : ℂ
⊢ |2 * z.im| = 2 * |z.im|
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: p : ℂ → Prop
⊢ (∀ (x : ℂ), p x) ↔ ∀ (a b : ℝ), p { re := a, im := b }

Tactic:
by aesop

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

Goal state before:
pp: p : ℂ → Prop
⊢ (∃ x, p x) ↔ ∃ a b, p { re := a, im := b }

Tactic:
by aesop

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

Goal state before:
pp: z : ℂ
⊢ 0 ≤ z.re ^ 2 - z.im ^ 2 ∧ (z.re = 0 ∨ z.im = 0) → z.im = 0

Tactic:
by aesop

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

Goal state before:
pp: z : ℂ
⊢ z.re ^ 2 - z.im ^ 2 ≤ 0 ∧ (z.re = 0 ∨ z.im = 0) → z.re = 0

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : 0 ≤ f
⊢ ∀ i ∈ univ, 0 ≤ f i

Tactic:
by aesop

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ ∀ i ∈ univ, f i ≤ 0

Tactic:
by aesop

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

Goal state before:
pp: case refine_1
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ |C| + 1 > 0

pp: case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ f.SurjectiveOnWith K (|C| + 1)

Tactic:
· linarith [abs_nonneg C]

Goal state after:
case refine_2
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : f.SurjectiveOnWith K C
⊢ f.SurjectiveOnWith K (|C| + 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: 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
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
simp only [tsum_bot hL, eq_symm_apply]
      constructor <;> rintro rfl
      exacts [e.map_finsum f, (e.map_finsum f).symm]

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

Goal state before:
pp: 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
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ 0 = e.symm y

Tactic:
tsum_eq_zero_of_not_summable hf'

Goal state after:
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
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ 0 = y ↔ 0 = e.symm y
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(im z) * I + ↑(im z) * I = 2 * ↑(im z) * I

Tactic:
← two_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 2 * (↑(im z) * I) = 2 * ↑(im z) * I
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
x✝ : (starRingEnd K) z = z
⊢ IsSelfAdjoint z

Tactic:
rwa [isSelfAdjoint_iff]

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
c₁ c₂ : ℝ
l : Filter α
f₁ f₂ : α → E'
g₁ g₂ : α → ℝ
h₁ : ∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
h₂ : ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
x : α
hx₁ : ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖
hx₂ : ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
⊢ c₁ * ‖g₁ x‖ + c₂ * ‖g₂ x‖ ≤ max c₁ c₂ * ‖g₁ x‖ + max c₁ c₂ * ‖g₂ x‖

Tactic:
by
        gcongr <;> simp [le_max_left _ _, le_max_right _ _]

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

Goal state before:
pp: 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'

Tactic:
· apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
    exact fun x hx ↦ (h x hx).symm

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

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

Tactic:
rw [← sub_add_cancel y x, Real.exp_add]

Goal state after:
x y : ℝ
h : x < y
⊢ rexp x < rexp (y - x) * rexp x
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ cosh (3 * x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
have h1 : x + 2 * x = 3 * x := by ring
  rw [← h1, cosh_add x (2 * x)]
  simp only [cosh_two_mul, sinh_two_mul]
  have h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2 := by ring
  rw [h2, sinh_sq]
  ring

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

Goal state before:
pp: x : ℂ
⊢ sin x ^ 2 + cos x ^ 2 = cos x ^ 2 - -sin x ^ 2

Tactic:
sub_neg_eq_add,

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

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

Tactic:
by simp [sin_add_sin]

Goal state after:
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:
rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

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:
rw [norm_mul, norm_div, ← mul_div_assoc, le_div_iff₀' (norm_pos_iff.mpr hx)]

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
hx' : x < 2
⊢ rexp x ≤ (2 + x) / (2 - x)

Tactic:
obtain rfl | hx₀ := hx.eq_or_lt

Goal state after:
case inl
hx : 0 ≤ 0
hx' : 0 < 2
⊢ rexp 0 ≤ (2 + 0) / (2 - 0)

case inr
x : ℝ
hx : 0 ≤ x
hx' : x < 2
hx₀ : 0 < x
⊢ rexp x ≤ (2 + x) / (2 - x)
Module: Mathlib.Algebra.Order.CauSeq.BigOperators

Goal state before:
pp: case hab
α : Type u_1
β : Type u_2
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Ring β
abv : β → α
inst✝² : IsAbsoluteValue abv
inst✝¹ : Archimedean α
inst✝ : Nontrivial β
x : β
hx1 : abv x < 1
hx1' : abv x ≠ 1
this : 0 < 1 - abv x
n : ℕ
a✝ : n ≥ 0
⊢ 1 - abv x ^ n ≤ 1

Tactic:
exact sub_le_self _ (abv_pow abv x n ▸ abv_nonneg _ _)

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

Goal state before:
pp: x : ℝ
⊢ |sin (x / 2)| = √((1 - cos x) / 2)

Tactic:
← sqrt_sq_eq_abs,

Goal state after:
x : ℝ
⊢ √(sin (x / 2) ^ 2) = √((1 - cos x) / 2)
Module: Mathlib.Analysis.Normed.Group.Pointwise

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

Tactic:
rw [hs.cthickening_eq_biUnion_closedBall hδ]

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
⊢ s * closedBall 1 δ = ⋃ x ∈ s, closedBall x δ
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ frontier (sphere x r) = sphere x r

Tactic:
isClosed_sphere.frontier_eq,

Goal state after:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r \ interior (sphere x r) = sphere x r
Module: Mathlib.Analysis.Normed.Module.RCLike.Real

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (sphere x r) = sphere x r

Tactic:
isClosed_sphere.frontier_eq,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ sphere x r \ interior (sphere x r) = sphere x r
Module: Mathlib.Analysis.SpecificLimits.Normed

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁵ : Field R
inst✝⁴ : Field S
inst✝³ : LinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : IsStrictOrderedRing S
inst✝ : Archimedean S
_i : OrderTopology S
v : AbsoluteValue R S
a : R
ha : v a < 1
h_add : Tendsto (fun x ↦ 1 + v a ^ x) atTop (𝓝 (1 + 0))
h_sub : Tendsto (fun x ↦ 1 - v a ^ x) atTop (𝓝 (1 - 0))
⊢ Tendsto ?m.138 atTop (𝓝 1)

Tactic:
by simpa using h_add

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

Goal state before:
pp: ⊢ cos (π / 2 - π / 6) = 1 / 2

Tactic:
← cos_pi_div_three

Goal state after:
⊢ cos (π / 2 - π / 6) = cos (π / 3)
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 : E
⊢ x ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)

Tactic:
by
    simp_rw [mem_thickening_iff]
    rintro ⟨z, hz, hxz⟩
    rw [add_comm] at hxz
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz
    exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩

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

Goal state before:
pp: E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)

Tactic:
(isCompact_closedBall _ _).add_closedBall hδ b,

Goal state after:
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
Module: Mathlib.Topology.Path

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
⊢ ∃ a, f a = t

Tactic:
have h₁ : Continuous (Set.IccExtend (zero_le_one' ℝ) f) := by fun_prop

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t : ↑I
h₁ : Continuous (IccExtend ⋯ f)
⊢ ∃ a, f a = t
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x : ℝ
hx : x ≤ -1
⊢ π / 2 - -(π / 2) = π

Tactic:
sub_neg_eq_add,

Goal state after:
x : ℝ
hx : x ≤ -1
⊢ π / 2 + π / 2 = π
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ -(π / 2) ≤ θ

Tactic:
by aesop

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc (-(π / 2)) (π / 2)
⊢ θ ≤ π / 2

Tactic:
by aesop

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

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-1) 1
⊢ -1 ≤ x

Tactic:
by aesop

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

Goal state before:
pp: x✝ y x : ℝ
hx : x ∈ Icc (-1) 1
⊢ x ≤ 1

Tactic:
by aesop

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc 0 π
⊢ 0 ≤ θ

Tactic:
by aesop

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

Goal state before:
pp: x y θ : ℝ
hθ : θ ∈ Icc 0 π
⊢ θ ≤ π

Tactic:
by aesop

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

Goal state before:
pp: z : ℂ
⊢ (cexp z).arg =
    (↑(rexp z.re) * (cos ↑(toIocMod Real.two_pi_pos (-π) z.im) + sin ↑(toIocMod Real.two_pi_pos (-π) z.im) * I)).arg

Tactic:
rw [← exp_mul_I, ofReal_exp, toIocMod]

Goal state after:
z : ℂ
⊢ (cexp z).arg = (cexp ↑z.re * cexp (↑(z.im - toIocDiv Real.two_pi_pos (-π) z.im • (2 * π)) * I)).arg
Module: Mathlib.Analysis.SpecialFunctions.Complex.Arg

Goal state before:
pp: case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (π + π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π

Tactic:
← two_mul,

Goal state after:
case inr
z : ℂ
hπ : 0 < π
hz : z ≠ 0
N : ℤ
hN : z.arg + N • (2 * π) ∈ Ioc (-π) π
⊢ z.arg ∈ Ioc (-π) π
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: ⊢ rexp (log 1) = rexp 0

Tactic:
by rw [exp_log zero_lt_one, exp_zero]

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

Goal state before:
pp: x y : ℝ
hx : x ≠ 0
hy : y ≠ 0
⊢ rexp (log (x * y)) = rexp (log x + log y)

Tactic:
by
    rw [exp_log_eq_abs (mul_ne_zero hx hy), exp_add, exp_log_eq_abs hx, exp_log_eq_abs hy, abs_mul]

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

Goal state before:
pp: case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0

Tactic:
← log_exp this.1 this.2,

Goal state after:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Ioc (-π) π
⊢ log (cexp (x + ↑n * (2 * ↑π * I))) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
sub_neg_eq_add,

Goal state after:
case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(π + π / 2 + π / 2) = 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

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

Tactic:
← two_mul,

Goal state after:
case e_b.e_a
θ : Angle
h : ↑π = ↑(2 • (π / 2))
⊢ ↑(2 * π) = 0
Module: Mathlib.Analysis.SpecialFunctions.Log.Basic

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ log '' Ioo 0 a = Iio (log a)

Tactic:
nth_rw 1 [← exp_log ha, ← image_exp_Iio, ← image_comp, log_comp_exp, image_id]

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

Goal state before:
pp: x y : ℂ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp only [cpow_def]
  split_ifs <;> simp [*, exp_ne_zero]

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

Goal state before:
pp: e : ℝ
n : ℕ
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
by
  rw [NormNum.IsInt.neg_to_eq h rfl]
  rw [Real.log_neg_eq_log]
  apply Real.log_pos
  simpa using w

Goal state after: