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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ

Tactic:
have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hY
      exact measurable_snd.comp_aemeasurable hY

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
this : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ
⊢ (map (fun a ↦ (X a, Y a)) μ).snd = map Y μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
a✝ : Measurable h
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ →
    ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
      ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ

Tactic:
h_ind_g

Goal state after:
case add
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
h_mf : Measurable f
g h : α → ℝ≥0∞
a✝¹ : Disjoint (Function.support g) (Function.support h)
h_mea_g : Measurable g
a✝ : Measurable h
h_ind_g : ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
⊢ ∫⁻ (a : α), h a ∂μ.withDensity f = ∫⁻ (a : α), (f * h) a ∂μ →
    ∫⁻ (a : α), (g + h) a ∂μ.withDensity f = ∫⁻ (a : α), (f * (g + h)) a ∂μ
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
ε : Type u_4
inst✝ : ENorm ε
m : MeasurableSpace α
f : α → ε
⊢ HasFiniteIntegral f 0

Tactic:
by
  simp only [HasFiniteIntegral, lintegral_zero_measure, zero_lt_top]

Goal state after:
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: case inr.inl.inr
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
⊢ b * b - 4 * 0 * c ≤ 0

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x).toReal = f x

Tactic:
filter_upwards [hf] with x hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
x : α
hx : f x ≠ ∞
⊢ ENNReal.ofReal (f x).toReal = f x
Module: Mathlib.Algebra.QuadraticDiscriminant

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝¹ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this✝ : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
⊢ False

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
h : -1 ≤ x
⊢ 0 ≤ 1 + x / 2

Tactic:
linarith

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

Goal state before:
pp: case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ f * g
A : (fun x ↦ (f x)⁻¹ * i x) ≤ g
x : α
h'x : f x < ∞
hx : f x = 0
this : i x = 0
⊢ i x ≤ (f * fun i_1 ↦ (f i_1)⁻¹ * i i_1) x

Tactic:
simp [this]

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

Goal state before:
pp: z w : ℂ
⊢ ‖z * w‖ = ‖z‖ * ‖w‖

Tactic:
by
  rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]

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

Goal state before:
pp: f : CauSeq ℂ fun x ↦ ‖x‖
ε : ℝ
ε0 : ε > 0
x✝ : ℕ
H :
  ∀ j ≥ x✝,
    |↑(⟨fun n ↦ (↑f n).re, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).re, ⋯⟩)) j| < ε / 2 ∧
      |↑(⟨fun n ↦ (↑f n).im, ⋯⟩ - CauSeq.const abs (CauSeq.lim ⟨fun n ↦ (↑f n).im, ⋯⟩)) j| < ε / 2
j : ℕ
ij : j ≥ x✝
⊢ (fun x ↦ ‖x‖) (↑(f - CauSeq.const (fun x ↦ ‖x‖) (limAux f)) j) < ε

Tactic:
by
    obtain ⟨H₁, H₂⟩ := H _ ij
    apply lt_of_le_of_lt (norm_le_abs_re_add_abs_im _)
    simpa using! add_lt_add H₁ H₂

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

Goal state before:
pp: z : ℂ
hz : z.re * z.re + z.im * z.im = 1
⊢ z.im * z.im = 1 - z.re * z.re

Tactic:
linarith

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

Goal state before:
pp: z w : ℂ
⊢ (z.re ≤ w.re ∧ ¬w.re ≤ z.re) ∧ z.im = w.im ↔ (z.re ≤ w.re ∧ z.im = w.im) ∧ ¬(w.re ≤ z.re ∧ w.im = z.im)

Tactic:
tauto

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

Goal state before:
pp: M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ μ ∗ₘ (s • ν) = s • μ ∗ₘ ν

Tactic:
by
  unfold mconv
  rw [Measure.prod_smul_right, Measure.map_smul]

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

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : g ∈ unitary G
⊢ g⁻¹ ∈ unitary G

Tactic:
simp_rw [mem_iff, star_inv, ← mul_inv_rev, inv_eq_one] at *

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : star g * g = 1 ∧ g * star g = 1
⊢ g * star g = 1 ∧ star g * g = 1
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖↑U * A‖ = ‖A‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
  simp [sq, ← CStarRing.norm_star_mul_self, mul_assoc, ← mul_assoc (U : E)⋆]

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

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
⊢ Continuous[inst✝ i, inst✝ j] (AlgEquiv.cast h).toFun

Tactic:
cases h

Goal state after:
case refl
R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i : ι
__spread✝⁻⁰ : A i ≃ₐ[R] A i := AlgEquiv.cast ⋯
⊢ Continuous[inst✝ i, inst✝ i] (AlgEquiv.cast ⋯).toFun
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i j : ι
h : i = j
⊢ Continuous[inst✝ j, inst✝ i] (AlgEquiv.cast h).invFun

Tactic:
cases h

Goal state after:
case refl
R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i : ι
__spread✝⁻⁰ : A i ≃ₐ[R] A i := AlgEquiv.cast ⋯
⊢ Continuous[inst✝ i, inst✝ i] (AlgEquiv.cast ⋯).invFun
Module: Mathlib.Analysis.Complex.Basic

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

Tactic:
Complex.ext_iff

Goal state after:
z : ℂ
hz : ¬(z.re = re 0 ∧ z.im = im 0)
⊢ (0 < z.re ∨ z.im ≠ 0) ∨ 0 < (-z).re ∨ (-z).im ≠ 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ z * -I = -(z * I)

Tactic:
mul_neg

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ -(z * I) = -(z * I)
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ f (↑(toPartialHomeomorph f h).symm x) = x

Tactic:
by
  rw [← congr_fun (h.toPartialHomeomorph_apply f), PartialHomeomorph.right_inv]
  rwa [toPartialHomeomorph_target]

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F' : Type u_7
inst✝¹ : Norm E
inst✝ : SeminormedAddCommGroup F'
c : ℝ
f : α → E
g' : α → F'
l : Filter α
⊢ (IsBigOWith c l f fun x ↦ ‖g' x‖) ↔ IsBigOWith c l f g'

Tactic:
simp only [IsBigOWith_def, norm_norm]

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 : ℝ
g : α → F
f' : α → E'
l : Filter α
⊢ IsBigOWith c l (fun x ↦ ‖f' x‖) g ↔ IsBigOWith c l f' g

Tactic:
simp only [IsBigOWith_def, norm_norm]

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

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
intro c cpos

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₁ : f₁ =O[l] g₁
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₂ g₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x

Tactic:
intro c cpos

Goal state after:
α : Type u_1
R : Type u_13
inst✝² : SeminormedRing R
S : Type u_17
inst✝¹ : NormedRing S
inst✝ : NormMulClass S
l : Filter α
f₁ f₂ : α → R
g₁ g₂ : α → S
h₂ : f₂ =O[l] g₂
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f₁ g₁
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ f₁ x * f₂ x) fun x ↦ g₁ x * g₂ x
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 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
intro c cpos

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 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₁ : k₁ =O[l] k₂
h₂ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f' g'
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x
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 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
⊢ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x

Tactic:
intro c cpos

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 𝕜'
f' : α → E'
g' : α → F'
l : Filter α
inst✝³ : Module R E'
inst✝² : IsBoundedSMul R E'
inst✝¹ : Module 𝕜' F'
inst✝ : NormSMulClass 𝕜' F'
k₁ : α → R
k₂ : α → 𝕜'
h₂ : f' =O[l] g'
h₁ : ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l k₁ k₂
c : ℝ
cpos : 0 < c
⊢ IsBigOWith c l (fun x ↦ k₁ x • f' x) fun x ↦ k₂ x • g' x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
R : Type u_13
𝕜 : Type u_15
inst✝¹ : SeminormedRing R
inst✝ : NormedDivisionRing 𝕜
l : Filter α
ι : Type u_17
L : List ι
f : ι → α → R
g : ι → α → 𝕜
hf : ∀ i ∈ L, f i =O[l] g i
⊢ (fun x ↦ (List.map (fun x_1 ↦ f x_1 x) L).prod) =O[l] fun x ↦ (List.map (fun x_1 ↦ g x_1 x) L).prod

Tactic:
by
  induction L with
  | nil => simp [isBoundedUnder_const]
  | cons i L ihL =>
    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢
    exact hf.1.mul (ihL hf.2)

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

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ ∑ i ∈ range n, x ^ i / ↑i ! ≤ lim ⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩

Tactic:
refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)

Goal state after:
x : ℝ
hx : 0 ≤ x
n j : ℕ
hj : j ≥ n
⊢ ↑(const abs (∑ i ∈ range n, x ^ i / ↑i !)) j ≤ ↑⟨fun n ↦ (↑(exp' ↑x) n).re, ⋯⟩ j
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: x y : ℝ
h : x < y
⊢ 1 < y - x + 1

Tactic:
linarith

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

Goal state before:
pp: x y : ℝ
h : x < y
⊢ 0 ≤ y - x

Tactic:
linarith

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

Goal state before:
pp: x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + sinh x ^ 2) + sinh x * (2 * sinh x * cosh x) = 4 * cosh x ^ 3 - 3 * cosh x

Tactic:
rw [h2, sinh_sq]

Goal state after:
x : ℂ
h1 : x + 2 * x = 3 * x
h2 : sinh x * (2 * sinh x * cosh x) = 2 * cosh x * sinh x ^ 2
⊢ cosh x * (cosh x ^ 2 + (cosh x ^ 2 - 1)) + 2 * cosh x * (cosh x ^ 2 - 1) = 4 * cosh x ^ 3 - 3 * cosh x
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: case pos
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
C : ℝ
a : 𝕜
f g : α → 𝕜
l : Filter α
h : Tendsto (fun x ↦ g x / f x) l (𝓝 a)
hC : 0 < C
ha : C⁻¹ < ‖a‖
x : α
hf : f x = 0
hx : C ≤ 0
⊢ ‖f x‖ ≤ C * ‖g x‖

Tactic:
linarith

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

Goal state before:
pp: x : ℂ
⊢ (starRingEnd ℂ) (-(sin x * I)) = (starRingEnd ℂ) (sin x * -I)

Tactic:
mul_neg

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

Goal state before:
pp: x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := ⋯
hj : j = n + k
⊢ 2 * (‖x‖ / ↑n.succ - 1) ≤ -1

Tactic:
linarith

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

Goal state before:
pp: case hbc
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ - 1 < 0

Tactic:
linarith

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

Goal state before:
pp: case hbc.h
x : ℂ
n : ℕ
hx : ‖x‖ / ↑n.succ ≤ 1 / 2
j : ℕ
hj✝ : j ≥ n
k : ℕ := j - n
hj : j = n + k
⊢ ‖x‖ / ↑n.succ ≠ 1

Tactic:
linarith

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

Goal state before:
pp: E'' : Type u_9
inst✝ : NormedAddCommGroup E''
f : ℕ → E''
⊢ (∃ C, ∀ (x : ℕ), ‖f x‖ ≤ C * ‖1‖) ↔ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C

Tactic:
simp only [norm_one, mul_one]

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

Goal state before:
pp: n : ℕ
x r : ℝ
⊢ expNear (n + 1) x r = expNear n x (1 + x / (↑n + 1) * r)

Tactic:
simp [expNear, range_add_one, mul_add, add_left_comm, add_assoc, pow_succ, div_eq_mul_inv,
    Nat.factorial]

Goal state after:
n : ℕ
x r : ℝ
⊢ x ^ n * x * ((↑n.factorial)⁻¹ * (↑n + 1)⁻¹) * r = x ^ n * (↑n.factorial)⁻¹ * (x * (↑n + 1)⁻¹ * r)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
⊢ a ^ n = -1 ↔ a = -1 ∧ Odd n

Tactic:
by
  simpa using zpow_eq_neg_zpow_iff₀ (α := α) one_ne_zero

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

Goal state before:
pp: x : ℝ
hx✝ : x ≠ 0
hx : x < 0
h' : -x < 1
⊢ 0 < x + 1

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx : 0 < x
hx' : x < 2
⊢ 0 < 2 - x

Tactic:
linarith

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm✝ : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a < (k + (k + 1)) • ε - a

Tactic:
lt_sub_iff_add_lt,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
f : ℕ → α
a : α
m : ℕ
ham : ∀ n ≥ m, |f n| ≤ a
hnm✝ : ∀ n ≥ m, f n.succ ≤ f n
ε : α
ε0 : ε > 0
k : ℕ
hk : a ≤ k • ε
n : ℕ
hnm : n ≥ m
⊢ a + a < (k + (k + 1)) • ε
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB ((fun a ↦ ‖a‖) '' f '' s) (sInf ((fun a ↦ ‖a‖) '' f '' s))
w✝ : E
hnormCx : (fun a ↦ ‖a‖) w✝ = sInf ((fun a ↦ ‖a‖) '' f '' s)
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < sInf (Norm.norm '' f '' s)

Tactic:
← hnormCx,

Goal state after:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : TopologicalSpace α
s : Set α
f : α → E
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn f s
hC : ∀ i ∈ s, f i ≠ 0
c : F
x✝ : α
hx✝ : x✝ ∈ s
hs : IsCompact ((fun a ↦ ‖a‖) '' f '' s)
h_sInf : IsGLB ((fun a ↦ ‖a‖) '' f '' s) (sInf ((fun a ↦ ‖a‖) '' f '' s))
w✝ : E
hnormCx : (fun a ↦ ‖a‖) w✝ = sInf ((fun a ↦ ‖a‖) '' f '' s)
x : α
hx : x ∈ s
hCx : f x = w✝
⊢ 0 < (fun a ↦ ‖a‖) w✝
Module: Mathlib.Analysis.SpecialFunctions.Exp

Goal state before:
pp: n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : x ∈ Set.Ioi ↑N
⊢ rexp x / x ^ n ∈ Set.Ici C

Tactic:
rw [Set.mem_Ioi] at hx

Goal state after:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, ↑k ^ n < rexp ↑k / (rexp 1 * C)
x : ℝ
hx : ↑N < x
⊢ rexp x / x ^ n ∈ Set.Ici C
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ -(π / 2) < π - x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx₁ : π / 2 < x
hx₂ : x < π + π / 2
⊢ π - x < π / 2

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ -(π / 2) ≤ π - x

Tactic:
linarith

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

Goal state before:
pp: x : ℝ
hx₁ : π / 2 ≤ x
hx₂ : x ≤ π + π / 2
⊢ π - x ≤ π / 2

Tactic:
linarith

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

Goal state before:
pp: case left
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ -(π / 2) ≤ x / 2

Tactic:
linarith

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

Goal state before:
pp: case right
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ x / 2 ≤ π / 2

Tactic:
linarith

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

Goal state before:
pp: case h0x
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ 0 ≤ x / 2

Tactic:
linarith

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

Goal state before:
pp: case hxp
x : ℝ
hl : 0 ≤ x
hr : x ≤ 2 * π
⊢ x / 2 ≤ π

Tactic:
linarith

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

Goal state before:
pp: case hx0
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ x / 2 ≤ 0

Tactic:
linarith

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

Goal state before:
pp: case hpx
x : ℝ
hl : -(2 * π) ≤ x
hr : x ≤ 0
⊢ -π ≤ x / 2

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

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

Tactic:
linarith

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁸ : SeminormedAddCommGroup M
inst✝⁷ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Module R M
S T : Submodule R M
𝕜 : Type u_4
inst✝⁴ : SeminormedCommRing 𝕜
inst✝³ : Module 𝕜 M
inst✝² : IsBoundedSMul 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖a‖ - ‖mk a‖ < δ

Tactic:
linarith

Goal state after:
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 ≤ δ
x : E
⊢ s / closedBall x δ = x⁻¹ • cthickening δ s

Tactic:
by
  simp [div_eq_mul_inv, hs.mul_closedBall hδ]

Goal state after: