mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ (ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi } =
    { re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r

Tactic:
ext

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ ((ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi }).re =
    ({ re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r).re

case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x✝ : ℂ
xr xi : ℝ
⊢ ((ofRealHom.comp (algebraMap R ℝ)) r * { re := xr, im := xi }).im =
    ({ re := xr, im := xi } * (ofRealHom.comp (algebraMap R ℝ)) r).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ r • x = (ofRealHom.comp (algebraMap R ℝ)) r * x

Tactic:
ext

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).re = ((ofRealHom.comp (algebraMap R ℝ)) r * x).re

case a
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).im = ((ofRealHom.comp (algebraMap R ℝ)) r * x).im
Module: Mathlib.Analysis.Complex.Basic

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

Tactic:
ext

Goal state after:
n : ℤ
⊢ ↑‖↑n‖₊ = ↑‖n‖₊
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ⊢ Tendsto (⇑normSq) (cocompact ℂ) atTop

Tactic:
by
  simpa [norm_mul_self_eq_normSq]
    using tendsto_norm_cocompact_atTop.atTop_mul_atTop₀ (tendsto_norm_cocompact_atTop (E := ℂ))

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
x✝ : (starRingEnd K) z = z
⊢ IsSelfAdjoint z

Tactic:
isSelfAdjoint_iff

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
x✝ : (starRingEnd K) z = z
⊢ star z = z
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
a : ℝ
b : ↥(skewAdjoint A)
⊢ ⟨-I • ↑(a • b), ⋯⟩ = (RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩

Tactic:
ext

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : ↥(skewAdjoint A)
⊢ ↑⟨-I • ↑(a • b), ⋯⟩ = ↑((RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩)
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
hz : IsSelfAdjoint z
⊢ (starRingEnd K) z = z

Tactic:
isSelfAdjoint_iff

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
hz : star z = z
⊢ (starRingEnd K) z = z
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
a : A
⊢ ℜ (I • a) = -ℑ a

Tactic:
ext

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℜ (I • a)) = ↑(-ℑ a)
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
a : A
⊢ ℑ (I • a) = ℜ a

Tactic:
ext

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : A
⊢ ↑(ℑ (I • a)) = ↑(ℜ a)
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
⊢ ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype = 0

Tactic:
ext

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x✝ : ↥(selfAdjoint.submodule ℝ A)
⊢ ↑((ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype) x✝) = ↑(0 x✝)
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
by rw [← ofReal_natCast, ofReal_re]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑↑n‖ = ↑n

Tactic:
exact norm_of_nonneg (Nat.cast_nonneg n)

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

Goal state before:
pp: A : Type u_1
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
⊢ ℜ 1 = 1

Tactic:
ext

Goal state after:
A : Type u_1
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
⊢ ↑(ℜ 1) = ↑1
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (e.source.domRestrict ↑e.toPartialEquiv) ∧ Injective (e.source.domRestrict ↑e.toPartialEquiv)

Tactic:
constructor

Goal state after:
case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing (e.source.domRestrict ↑e.toPartialEquiv)

case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (e.source.domRestrict ↑e.toPartialEquiv)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w ↔ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
constructor

Goal state after:
case mp
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ im z = im w) ∧ z ≠ w → (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

case mpr
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w → (re z ≤ re w ∧ im z = im w) ∧ z ≠ w
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ map K K = ContinuousLinearMap.id ℝ K

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : RCLike K
x✝ : K
⊢ (map K K) x✝ = (ContinuousLinearMap.id ℝ K) x✝
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ map K ℝ = reCLM

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : RCLike K
x✝ : K
⊢ (map K ℝ) x✝ = reCLM x✝
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ map ℝ K = ofRealCLM

Tactic:
ext

Goal state after:
K : Type u_1
inst✝ : RCLike K
⊢ (map ℝ K) 1 = ofRealCLM 1
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:
ext

Goal state after:
𝕜 : 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 𝕜)
x✝ : W
⊢ (α • e).symm x✝ = (α⁻¹ • e.symm) x✝
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
ext

Goal state after:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
x✝ : V
⊢ ((α • e).trans f) x✝ = (α • e.trans f) x✝
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
ext

Goal state after:
𝕜 : Type u_3
V : Type u_4
W : Type u_5
G : Type u_6
inst✝⁶ : RCLike 𝕜
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : Module 𝕜 V
inst✝³ : SeminormedAddCommGroup W
inst✝² : NormedSpace 𝕜 W
inst✝¹ : SeminormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
α : ↥(unitary 𝕜)
e : V ≃ₗᵢ[𝕜] G
f : G ≃ₗᵢ[𝕜] W
x✝ : V
⊢ (e.trans (α • f)) x✝ = (α • e.trans f) x✝
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
l : Filter α
⊢ IsBigOWith c l f g ↔ ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
by rw [IsBigOWith_def]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_14
inst✝ : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
⊢ (fun x ↦ f x / g x) = fun x ↦ (g x / f x)⁻¹

Tactic:
ext

Goal state after:
α : Type u_1
𝕜 : Type u_14
inst✝ : NormedField 𝕜
l : Filter α
c : 𝕜
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l (𝓝 c)
hc : c ≠ 0
x✝ : α
⊢ f x✝ / g x✝ = (g x✝ / f x✝)⁻¹
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ f =o[l] g ↔ ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ f =o[l] g → ∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖

case mpr
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
⊢ (∀ (n : ℕ), ∀ᶠ (x : α) in l, ↑n * ‖f x‖ ≤ ‖g x‖) → f =o[l] g
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case mp.zero
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
h₀ : (∀ (x : α), 0 ≤ ‖f x‖) ∨ ∀ (x : α), 0 ≤ ‖g x‖
H : f =o[l] g
⊢ ∀ᶠ (x : α) in l, ↑0 * ‖f x‖ ≤ ‖g x‖

Tactic:
refine (H.def one_pos).mono fun x h₀' => ?_
      rw [Nat.cast_zero, zero_mul]
      refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x
      rwa [one_mul] at h₀'

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
l : Filter α
f₁ f₂ : α → E
g₁ g₂ : α → F
hf : f₁ =ᶠ[l] f₂
hg : g₁ =ᶠ[l] g₂
⊢ f₁ =O[l] g₁ ↔ f₂ =O[l] g₂

Tactic:
simp only [IsBigO_def]
  exact exists_congr fun c => isBigOWith_congr rfl hf hg

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.LinearIsometry

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E₂
inst✝² : Module R₂ E₂
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ⇑f
⊢ ⇑(ofSurjective f hfr) = ⇑f

Tactic:
ext

Goal state after:
R : Type u_1
R₂ : Type u_2
E₂ : Type u_6
F : Type u_9
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E₂
inst✝² : Module R₂ E₂
inst✝¹ : NormedAddCommGroup F
inst✝ : Module R F
f : F →ₛₗᵢ[σ₁₂] E₂
hfr : Surjective ⇑f
x✝ : F
⊢ (ofSurjective f hfr) x✝ = f x✝
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
⊢ IsNat n ! a

Tactic:
constructor

Goal state after:
n x : ℕ
h₁ : IsNat n x
a : ℕ
h₂ : ascFactorial 1 x = a
⊢ n ! = ↑a
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ IsNat (n.ascFactorial l) a

Tactic:
constructor

Goal state after:
n x l y : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
a : ℕ
p : x.ascFactorial y = a
⊢ n.ascFactorial l = ↑a
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : x = z + y
a : ℕ
p : (z + 1).ascFactorial y = a
⊢ IsNat (n.descFactorial l) a

Tactic:
constructor

Goal state after:
n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : x = z + y
a : ℕ
p : (z + 1).ascFactorial y = a
⊢ n.descFactorial l = ↑a
Module: Mathlib.Tactic.NormNum.NatFactorial

Goal state before:
pp: n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ IsNat (n.descFactorial l) 0

Tactic:
constructor

Goal state after:
n x l y z : ℕ
h₁ : IsNat n x
h₂ : IsNat l y
h₃ : y = z + x + 1
⊢ n.descFactorial l = ↑0
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:
constructor

Goal state after:
case mp
α : 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‖

case mpr
α : 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
⊢ (∃ b, 0 < b ∧ ∀ᶠ (x : α) in l, b ≤ ‖f' x‖) → (fun _x ↦ c) =O[l] f'
Module: Mathlib.Analysis.Asymptotics.Defs

Goal state before:
pp: case empty
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
s : Finset ι
B : ι → α → ℝ
hAB : ∀ i ∈ ∅, A i =o[l] B i
⊢ (fun H ↦ ∑ i ∈ ∅, A i H) =o[l] fun H ↦ ∑ i ∈ ∅, ‖B i H‖

Tactic:
simp [isLittleO_zero]

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v ↔ ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ IsBigOWith c l u v → ∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v

case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
c : ℝ
l : Filter α
u v : α → 𝕜
hc : 0 ≤ c
⊢ (∃ φ, (∀ᶠ (x : α) in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v) → IsBigOWith c l u v
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v ↔ ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =O[l] v → ∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v

case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l (norm ∘ φ) ∧ u =ᶠ[l] φ * v) → u =O[l] v
Module: Mathlib.Analysis.Asymptotics.Lemmas

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v ↔ ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ u =o[l] v → ∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v

case mpr
α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
u v : α → 𝕜
⊢ (∃ φ, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v) → u =o[l] v
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‖ ≤ max (C * ‖g'' x‖) (C' * ‖g'' x‖)

Tactic:
le_max_iff,

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
⊢ ‖f x‖ ≤ C * ‖g'' x‖ ∨ ‖f x‖ ≤ C' * ‖g'' x‖
Module: Mathlib.Analysis.Complex.Trigonometric

Goal state before:
pp: x : ℂ
⊢ tan (-x) = -tan x

Tactic:
simp [tan, neg_div]

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

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

Tactic:
rw [← sin_sq_add_cos_sq x, add_sub_cancel_right]

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

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

Tactic:
by
  rw [← cos_sq', sqrt_sq_eq_abs]

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

Goal state before:
pp: x : ℝ
⊢ rexp x - rexp (-x) < rexp x + rexp (-x)

Tactic:
grind [exp_pos]

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

Goal state before:
pp: x : ℝ
⊢ -(rexp x + rexp (-x)) < rexp x - rexp (-x)

Tactic:
grind [exp_pos]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
⊢ abv (f m) ≤ abv (f n.succ) * 0⁻¹ ^ n.succ * 0 ^ m

Tactic:
have m_pos := lt_of_lt_of_le (Nat.succ_pos n) hmn

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Field α
inst✝⁴ : LinearOrder α
inst✝³ : IsStrictOrderedRing α
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : Archimedean α
f : ℕ → β
n m : ℕ
hmn : n.succ ≤ m
hr0 : 0 ≤ 0
hr1 : 0 < 1
h : ∀ (m : ℕ), n ≤ m → abv (f m.succ) ≤ 0 * abv (f m)
har1 : |0| < 1
m_pos : 0 < m
⊢ abv (f m) ≤ abv (f n.succ) * 0⁻¹ ^ n.succ * 0 ^ m
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
constructor

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

case right
x : ℝ
hl : -π ≤ x
hr : x ≤ π
⊢ x / 2 ≤ π / 2
Module: Mathlib.Analysis.Normed.Group.Pointwise

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (thickening δ s)⁻¹ = thickening δ s⁻¹

Tactic:
simp_rw [thickening, ← infEDist_inv]

Goal state after:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | infEDist x s < ENNReal.ofReal δ}⁻¹ = {x | infEDist x⁻¹ s < ENNReal.ofReal δ}
Module: Mathlib.Analysis.Normed.Group.Quotient

Goal state before:
pp: case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ x ∈ S, f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖(lift S f.toAddMonoidHom hf) x‖ ≤ ‖f‖ * ‖x‖

Tactic:
rcases mk_surjective x with ⟨x, rfl⟩
    simpa [h] using le_opNorm f x

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 ≤ δ
⊢ closedBall 1 δ / s = cthickening δ s⁻¹

Tactic:
simp [div_eq_mul_inv, mul_comm, hs.inv.mul_closedBall_one hδ]

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ 2 + sqrtTwoAddSeries 0 n

Tactic:
· exact add_nonneg two_pos.le (sqrtTwoAddSeries_zero_nonneg _)

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
⊢ ⋃ c ∈ s, sphere 0 (‖c‖ * r) = (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s

Tactic:
ext

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
x✝ : E
⊢ x✝ ∈ ⋃ c ∈ s, sphere 0 (‖c‖ * r) ↔ x✝ ∈ (fun x ↦ ‖x‖) ⁻¹' (fun x ↦ ‖x‖ * r) '' s
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

Tactic:
by
  rw [show (6 : ℝ) = 3 * 2 by norm_num, div_mul_eq_div_div, cos_half, cos_pi_div_three, one_add_div,
    ← div_mul_eq_div_div, two_add_one_eq_three, sqrt_div, sqrt_mul_self] <;> linarith [pi_pos]

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

Goal state before:
pp: α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ HasSummableGeomSeries R

Tactic:
constructor

Goal state after:
α : Type u_1
R✝ : Type u_2
S : Type u_3
inst✝⁷ : Field R✝
inst✝⁶ : Field S
inst✝⁵ : LinearOrder S
v w : AbsoluteValue R✝ S
inst✝⁴ : TopologicalSpace S
inst✝³ : IsStrictOrderedRing S
inst✝² : Archimedean S
_i : OrderTopology S
R : Type u_4
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
⊢ ∀ (ξ : R), ‖ξ‖ < 1 → Summable fun n ↦ ξ ^ n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

Goal state before:
pp: ⊢ 4 * cos (π / 5) ^ 2 - 2 * cos (π / 5) - 1 = 0

Tactic:
by
  set θ := π / 5 with hθ
  set c := cos θ
  set s := sin θ
  suffices 2 * c = 4 * c ^ 2 - 1 by simp [this]
  have hs : s ≠ 0 := by
    rw [ne_eq, sin_eq_zero_iff, hθ]
    push Not
    intro n hn
    replace hn : n * 5 = 1 := by field_simp at hn; norm_cast at hn
    lia
  suffices s * (2 * c) = s * (4 * c ^ 2 - 1) from mul_left_cancel₀ hs this
  calc s * (2 * c) = 2 * s * c := by rw [← mul_assoc, mul_comm 2]
                 _ = sin (2 * θ) := by rw [sin_two_mul]
                 _ = sin (π - 2 * θ) := by rw [sin_pi_sub]
                 _ = sin (2 * θ + θ) := by congr; linarith
                 _ = sin (2 * θ) * c + cos (2 * θ) * s := sin_add (2 * θ) θ
                 _ = 2 * s * c * c + cos (2 * θ) * s := by rw [sin_two_mul]
                 _ = 2 * s * c * c + (2 * c ^ 2 - 1) * s := by rw [cos_two_mul]
                 _ = s * (2 * c * c) + s * (2 * c ^ 2 - 1) := by linarith
                 _ = s * (4 * c ^ 2 - 1) := by linarith

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

Goal state before:
pp: c : ℝ := cos (π / 5)
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ π / 5 ∈ Icc (-(π / 2)) (π / 2)

Tactic:
constructor

Goal state after:
case left
c : ℝ := ⋯
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ -(π / 2) ≤ π / 5

case right
c : ℝ := ⋯
this : 4 * (c * c) + -2 * c + -1 = 0
hd : discrim 4 (-2) (-1) = 2 * √5 * (2 * √5)
h : c = (- -2 - 2 * √5) / (2 * 4)
⊢ π / 5 ≤ π / 2