mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = (‖f‖ + ‖g‖) * ‖v‖

Tactic:
add_mul

Goal state after:
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✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖
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₂
⊢ ∀ (v : V₁), ‖0 v‖ ≤ 0 * ‖v‖

Tactic:
by simp

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₂
⊢ ∀ (v : V), ‖(AddMonoidHom.id V) v‖ ≤ 1 * ‖v‖

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
inst✝ : SeminormedAddCommGroup V
x : V
⊢ ‖(id V) x‖ ≤ 1 * ‖x‖

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
x : ℝ
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
by simp

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

Goal state before:
pp: V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
hx : x ∈ s
⊢ (incl s).toAddMonoidHom ⟨x, hx⟩ = x

Tactic:
by simp

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

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
v : V₁
⊢ ‖0 v‖ ≤ ‖v‖

Tactic:
by simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : (i : ι) → R i
⊢ ⊥ ^ 2 = ⊥

Tactic:
by simp

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

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : { φ // f.comp φ = g.comp φ }
⊢ (fun ψ ↦ ⟨(ι f g).comp ψ, ⋯⟩) ((fun φ ↦ lift ↑φ ⋯) φ) = φ

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑reAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑reAddGroupHom).toFun x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).re = balance (re ∘ f) a

Tactic:
by
  simp [balance]

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑imAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑imAddGroupHom).toFun x

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).im = balance (im ∘ f) a

Tactic:
by
  simp [balance]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
a : α
⊢ (DistribSMul.toAddMonoidHom α g⁻¹) ((↑(DistribSMul.toAddMonoidHom α g)).toFun a) = a

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
a : α
⊢ (↑(DistribSMul.toAddMonoidHom α g)).toFun ((DistribSMul.toAddMonoidHom α g⁻¹) a) = a

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
z z' : ℂ
⊢ ![(z + z').re, (z + z').im] = ![z.re, z.im] + ![z'.re, z'.im]

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
c : ℝ
z : ℂ
⊢ ![(c • z).re, (c • z).im] = (RingHom.id ℝ) c • ![z.re, z.im]

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
z : ℂ
⊢ (fun c ↦ ↑(c 0) + c 1 • I) ((fun z ↦ ![z.re, z.im]) z) = z

Tactic:
by simp

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

Goal state before:
pp: ⊢ ∀ (m : ℝ) (x : ℂ), (m • x).re = (RingHom.id ℝ) m • x.re

Tactic:
by simp

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

Goal state before:
pp: ⊢ ∀ (m : ℝ) (x : ℂ), (m • x).im = (RingHom.id ℝ) m • x.im

Tactic:
by simp

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

Goal state before:
pp: r : ℝ
c : ℂ
⊢ equivRealProdAddHom.toFun (r • c) = (RingHom.id ℝ) r • equivRealProdAddHom.toFun c

Tactic:
by simp

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

Goal state before:
pp: ⊢ ↑↑conjCLE = conjAe.toLinearMap

Tactic:
by simp

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

Goal state before:
pp: x : ℂ
y : ℝ
hx : IsSelfAdjoint x
⊢ y = x.re ↔ ↑y = x

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

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

Goal state before:
pp: z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x : 𝕜
⊢ (fun x ↦ ↑x.re + ↑x.im * RCLike.I) ((fun x ↦ ↑(RCLike.re x) + ↑(RCLike.im x) * I) x) = x

Tactic:
by simp

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

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

Tactic:
neg_mul,

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ (I * z + -(I * (starRingEnd K) z)) / 2 = (I * z - I * (starRingEnd K) z) / 2
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI') I = I'

Tactic:
by simp

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

Goal state before:
pp: x : ℂ
⊢ I ∈ {I}

Tactic:
by simp

Goal state after:
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), ⋯⟩ = ⟨-I • ↑a, ⋯⟩ + ⟨-I • ↑b, ⋯⟩

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
L : SummationFilter α
f : α → ℝ
x✝ : ℝ
⊢ re ((algebraMap ℝ 𝕜) x✝) = x✝

Tactic:
by simp

Goal state after:
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
⊢ ‖imaginaryPart x‖ = ‖realPart (Complex.I • -x)‖

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
⊢ ∀ (x y : ↥(selfAdjoint ℂ)), (↑(x + y)).re = (↑x).re + (↑y).re

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
⊢ ∀ (m : ℝ) (x : ↥(selfAdjoint ℂ)), (↑(m • x)).re = (RingHom.id ℝ) m • (↑x).re

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
hz : ‖z‖ = 1
⊢ (starRingEnd K) z * z = 1

Tactic:
simp_rw [conj_mul, hz, algebraMap.coe_one, one_pow]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ ‖1‖ = 1 ∧ ↑‖0‖ = 1 * 0

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
⊢ ‖1‖ = 1 ∧ 1 * ↑‖0‖ = 0

Tactic:
by simp

Goal state after:
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
⊢ ∀ (x : ↑e.source), e.source.domRestrict (↑e.toPartialEquiv) x ∈ e.target

Tactic:
by simp

Goal state after:
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
⊢ range Subtype.val ⊆ e.source

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ∀ (a : ↑f.source), f.source.domRestrict (↑f) a ∈ f.target

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
Z : Type u_5
Z' : Type u_6
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace X'
inst✝³ : TopologicalSpace Y
inst✝² : TopologicalSpace Y'
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f : PartialEquiv X Y
h : IsHomeomorph ⇑f.toEquiv
⊢ ∀ (a : ↑f.target), f.target.domRestrict f.invFun a ∈ f.source

Tactic:
by simp

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

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝ : RCLike K
x : ℝ
z : K
hx : 0 < x
⊢ 0 < x * re z ∧ x * im z = 0 ↔ x < 0 ∧ re z < 0 ∧ im z = 0 ∨ 0 < x ∧ 0 < re z ∧ im z = 0

Tactic:
· simp only [mul_pos_iff, hx, true_and, not_lt_of_gt hx, false_and, or_false, mul_eq_zero,
      hx.ne', false_or]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖reLm x‖ ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖reLm x‖ ≤ ‖x‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖imLm x‖ ≤ 1 * ‖x‖

Tactic:
rw [one_mul]

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
x : K
⊢ ‖imLm x‖ ≤ ‖x‖
Module: Mathlib.Analysis.Complex.Asymptotics

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

Tactic:
by simp

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
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ 1 * ‖g x‖

Tactic:
rw [one_mul]

Goal state after:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
hfg : ∀ (x : α), ‖f x‖ ≤ ‖g x‖
x : α
⊢ ‖f x‖ ≤ ‖g x‖
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'
f : α → E
g' : α → F'
l : Filter α
⊢ (∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f fun x ↦ -g' x) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c l f g'

Tactic:
exact forall₂_congr fun _ _ => isBigOWith_neg_right

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
hg : IsCauSeq abs fun n ↦ ∑ i ∈ range n, a i
ε : α
ε0 : ε > 0
⊢ 0 < 2

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖f x‖ = ‖x‖

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖f x‖₊ = ‖x‖₊

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
f : E →ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖f x‖ₑ = ‖x‖ₑ

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖e x‖ = ‖x‖

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖e x‖₊ = ‖x‖₊

Tactic:
by simp

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
x : E
⊢ ‖e x‖ₑ = ‖x‖ₑ

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ ∅.sum f = ↑0

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.NormNum.BigOperators

Goal state before:
pp: β : Type u_1
α : Type u_2
inst✝ : CommSemiring β
f : α → β
⊢ ∅.prod f = ↑1

Tactic:
by simp

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'
g : α → F
l : Filter α
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ 0 * ‖g x‖) x}

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
E : Type u_3
F'' : Type u_10
inst✝¹ : Norm E
inst✝ : NormedAddCommGroup F''
c : E
c' : F''
hc' : c' ≠ 0
l : Filter α
⊢ IsBigOWith (‖c‖ / ‖c'‖) l (fun _x ↦ c) fun _x ↦ c'

Tactic:
simp only [IsBigOWith_def]
  apply univ_mem'
  intro x
  rw [mem_ofPred, div_mul_cancel₀ _ (norm_ne_zero_iff.mpr hc')]

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

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
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖

Tactic:
by
  rw [IsBigOWith_def, eventually_top]

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 g : ℕ → β
ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)
hb : IsCauSeq abv fun m ↦ ∑ n ∈ range m, g n
ε : α
ε0 : 0 < ε
P : α
hP : ∀ (i : ℕ), |∑ n ∈ range i, abv (f n)| < P
Q : α
hQ : ∀ (i : ℕ), abv (∑ n ∈ range i, g n) < Q
hP0 : 0 < P
hPε0 : 0 < ε / (2 * P)
N : ℕ
hN : ∀ j ≥ N, ∀ k ≥ N, abv (∑ n ∈ range j, g n - ∑ n ∈ range k, g n) < ε / (2 * P)
hQε0 : 0 < ε / (4 * Q)
M : ℕ
hM : ∀ j ≥ M, ∀ k ≥ M, |∑ n ∈ range j, abv (f n) - ∑ n ∈ range k, abv (f n)| < ε / (4 * Q)
K : ℕ
hK : K ≥ 2 * (max N M + 1)
h₁ : ∑ m ∈ range K, ∑ k ∈ range (m + 1), f k * g (m - k) = ∑ m ∈ range K, ∑ n ∈ range (K - m), f m * g n
⊢ (fun i ↦ ∑ k ∈ range (K - i), f i * g k) = fun i ↦ f i * ∑ k ∈ range (K - i), g k

Tactic:
simp [Finset.mul_sum]

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

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

Tactic:
by simp

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

Goal state before:
pp: ε : ℝ
ε0 : ε > 0
j : ℕ
ih : j + 1 ≥ 1 → ‖∑ m ∈ range (j + 1), 0 ^ m / ↑m.factorial - 1‖ = 0
hj : j + 1 + 1 ≥ 1
⊢ j + 1 ≥ 1

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_15
inst✝ : NormedDivisionRing 𝕜
l : Filter α
f g : α → 𝕜
h : f =o[l] g
⊢ (fun x ↦ f x / g x) =o[l] fun x ↦ g x / g x

Tactic:
by
        simpa only [div_eq_mul_inv] using h.mul_isBigO (isBigO_refl _ _)

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

Goal state before:
pp: x y : ℂ
⊢ cexp (Multiplicative.toAdd 1) = 1

Tactic:
by simp

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

Goal state before:
pp: x y : ℝ
⊢ rexp (Multiplicative.toAdd 1) = 1

Tactic:
by simp

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

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

Tactic:
neg_mul,

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ ‖cexp x - 1‖ = ‖cexp x - ∑ m ∈ range 1, x ^ m / ↑m.factorial‖

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑(Real.exp x) - 1 - ↑x‖ = ‖cexp ↑x - 1 - ↑x‖

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
hx : ‖x‖ ≤ 1
⊢ ‖↑x‖ ^ 2 = ‖x‖ ^ 2

Tactic:
by simp

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 4

Tactic:
by simp

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

Goal state before:
pp: x : ℂ
hx : ‖x‖ ≤ 1
⊢ 0 < 5

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ ↑(tan x)⁻¹ = ↑x.cot

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ ↑x.cot⁻¹ = ↑(tan x)

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ ↑(cosh (-x)) = ↑(cosh x)

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
⊢ 0 < 2

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
hx0 : 0 < x
hx : x ≤ 2
this : x / 2 ≤ 1
⊢ 0 < 2

Tactic:
by simp

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

Goal state before:
pp: ⊢ |1| ≤ 1

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ ‖cos ↑x + sin ↑x * I‖ = 1

Tactic:
norm_cos_add_sin_mul_I

Goal state after:
x : ℝ
⊢ 1 = 1
Module: Mathlib.Analysis.Complex.Exponential

Goal state before:
pp: n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |expNear n x (1 + x / (↑n + 1) * a₂) - expNear n x a₁| ≤
    |x| ^ n / ↑n.factorial * b₁

Tactic:
expNear_sub,

Goal state after:
n : ℕ
x a₁ b₁ a₂ b₂ : ℝ
e : |1 + x / ↑(n + 1) * a₂ - a₁| ≤ b₁ - |x| / ↑(n + 1) * b₂
h : |rexp x - expNear (n + 1) x a₂| ≤ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂
⊢ |x| ^ (n + 1) / ↑(n + 1).factorial * b₂ + |x ^ n / ↑n.factorial * (1 + x / (↑n + 1) * a₂ - a₁)| ≤
    |x| ^ n / ↑n.factorial * b₁
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n : ℤ
hn : Even n
a : α
⊢ 0 ≤ a ^ n

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
⊢ 0 ≤ a ^ (k + k)
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Even n
h : n ≠ 0
⊢ 0 < a ^ n ↔ a ≠ 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
k : ℤ
h : k + k ≠ 0
⊢ 0 < a ^ (k + k) ↔ a ≠ 0
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
n : ℤ
hn : Odd n
ha : a < 0
⊢ a ^ n < 0

Tactic:
obtain ⟨k, rfl⟩ := hn

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
k : ℤ
⊢ a ^ (2 * k + 1) < 0
Module: Mathlib.Algebra.Order.Field.Power

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
p : ℤ
⊢ |(-1) ^ p| = 1

Tactic:
by simp

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

Goal state before:
pp: case inl
t : ℝ
ht' : t ≤ ↑0
⊢ (1 - t / ↑0) ^ 0 ≤ rexp (-t)

pp: case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)

Tactic:
· simp
    rwa [Nat.cast_zero] at ht'

Goal state after:
case inr
n : ℕ
t : ℝ
ht' : t ≤ ↑n
hn : n ≠ 0
⊢ (1 - t / ↑n) ^ n ≤ rexp (-t)
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
by simp

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 • ε
h : ∃ l, ∀ n ≥ m, a - l • ε < f n
l : ℕ := Nat.find h
hl : ∀ n ≥ m, f n > a - l • ε
hl0 : l = 0
this : f m > a - l • ε
⊢ a < f m

Tactic:
simpa [hl0] using this

Goal state after: