mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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:
simp

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
⊢ ∑'[L] (i : β), 0 • f i = 0 • ∑'[L] (i : β), f i

Tactic:
simp

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

Goal state before:
pp: case neg.refine_1
ι : 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₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ 0 = e.symm 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
⊢ ∑' (a : α), f (a • b₁) = ∑' (a : α), f (a • b₂)

Tactic:
rw [← ha]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
⊢ ∑' (a_1 : α), f (a_1 • a • b₂) = ∑' (a : α), f (a • b₂)
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:
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:
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:
simp

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

Goal state before:
pp: case «0»
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) ((fun i ↦ i) ⟨0, ⋯⟩) = c ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1»
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun z ↦ ![z.re, z.im]) ((fun c ↦ ↑(c 0) + c 1 • I) c) ((fun i ↦ i) ⟨1, ⋯⟩) = c ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «0».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «0».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨0, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1».«0»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨0, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
simp

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

Goal state before:
pp: case «1».«1»
⊢ (basisOneI.repr (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩))) ((fun i ↦ i) ⟨1, ⋯⟩) =
    (Finsupp.single ((fun i ↦ i) ⟨1, ⋯⟩) 1) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
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:
simp

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

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

Tactic:
simp

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:
simp

Goal state after:
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:
simp

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

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

Tactic:
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:
simp

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

Goal state before:
pp: case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re (↑(RCLike.re a) + ↑0 * RCLike.I)) + ↑(RCLike.im (↑(RCLike.re a) + ↑0 * RCLike.I)) * I‖ =
    ‖↑(RCLike.re a) + ↑0 * RCLike.I‖

Tactic:
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:
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:
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:
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:
simp

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

Goal state before:
pp: r : ℝ
⊢ 2⁻¹ • 2 • ↑r = ↑r

Tactic:
simp

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

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
⊢ 0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹

Tactic:
simp

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:
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:
simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : RCLike K
n : ℕ
inst✝ : n.AtLeastTwo
z : K
⊢ im (OfNat.ofNat n * z) = OfNat.ofNat n * im z

Tactic:
by
  rw [← ofReal_ofNat, im_ofReal_mul]

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:
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:
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:
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:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x ≤ re ↑y ∧ im ↑x = im ↑y ↔ x ≤ y

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x < re ↑y ∧ im ↑x = im ↑y ↔ x < y

Tactic:
simp

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : RCLike K
z : K
h : ‖z‖ ≤ re z
h' : ‖z‖ = re z
⊢ z = ↑‖z‖

Tactic:
rw [h', re_eq_self_of_le h]

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : RCLike K
z : K
h : z = ↑‖z‖
⊢ ‖↑‖z‖‖ ≤ re ↑‖z‖

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x = { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
exact h.smul_def'

Goal state after:
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
x✝ : V
⊢ ((α • e).trans f) x✝ = (α • e.trans f) x✝

Tactic:
simp

Goal state after:
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
x✝ : V
⊢ (e.trans (α • f)) x✝ = (α • e.trans f) x✝

Tactic:
simp

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
x✝ : α
⊢ f x✝ / g x✝ = (g x✝ / f x✝)⁻¹

Tactic:
simp

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

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

Tactic:
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 α
h : f =o[l] g
hg : ∀ᶠ (x : α) in l, 0 < ‖g x‖
⊢ 0 < 2⁻¹

Tactic:
simp

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:
simp

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
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
⊢ ∀ j ≥ max n i, abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε

Tactic:
intro j

Goal state after:
α : 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
i : ℕ
hi : ∀ j ≥ i, |(fun n ↦ ∑ i ∈ range n, a i) j - (fun n ↦ ∑ i ∈ range n, a i) i| < ε / 2
j : ℕ
⊢ j ≥ max n i → abv ((fun n ↦ ∑ i ∈ range n, f i) j - (fun n ↦ ∑ i ∈ range n, f i) (max n i)) < ε
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₂
toLinearMap✝¹ : E →ₛₗ[σ₁₂] E₂
norm_map'✝¹ : ∀ (x : E), ‖toLinearMap✝¹ x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
norm_map'✝ : ∀ (x : E), ‖toLinearMap✝ x‖ = ‖x‖
⊢ (fun f ↦ ⇑f) { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      (fun f ↦ ⇑f) { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ } →
    { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ }

Tactic:
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:
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:
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:
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:
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:
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:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ insert a s = Finset.cons a s h

Tactic:
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:
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:
simp

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

Goal state before:
pp: α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
c : ℝ
g' : α → F'
l : Filter α
hc : 0 ≤ c
x : α
⊢ x ∈ {x | (fun x ↦ ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
by simpa using mul_nonneg hc (norm_nonneg <| g' x)

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:
simp

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
⊢ 2 > 0

Tactic:
simp

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)
⊢ 0 < 4

Tactic:
simp

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'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
⊢ ∀ i ∈ s, C i * ‖B i x‖ ≤ sSup (C '' ↑s) * ‖B i x‖

Tactic:
intro j

Goal state after:
α : Type u_1
E' : Type u_6
inst✝ : SeminormedAddCommGroup E'
l : Filter α
ι : Type u_18
A : ι → α → E'
C : ι → ℝ
s : Finset ι
B : ι → α → ℝ
hs : s.Nonempty
hAB : ∀ i ∈ s, ∀ᶠ (x : α) in l, ‖A i x‖ ≤ C i * ‖B i x‖
x : α
hx : ∀ i ∈ s, ‖A i x‖ ≤ C i * ‖B i x‖
j : ι
⊢ j ∈ s → C j * ‖B j x‖ ≤ sSup (C '' ↑s) * ‖B j x‖
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:
simp

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

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

Tactic:
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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: x y : ℂ
⊢ ∀ (j : ℕ),
    ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
      ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)

Tactic:
intro j

Goal state after:
x y : ℂ
j : ℕ
⊢ ∑ m ∈ range j, (x + y) ^ m / ↑m.factorial =
    ∑ i ∈ range j, ∑ k ∈ range (i + 1), x ^ k / ↑k.factorial * (y ^ (i - k) / ↑(i - k).factorial)
Module: Mathlib.Analysis.Complex.Exponential

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

Tactic:
simp

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

Goal state before:
pp: x : ℂ
h : cexp x = 0
⊢ x + -x = 0 * cexp (-x)

Tactic:
simp

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

Goal state before:
pp: x : ℂ
⊢ cexp (x + -x) = cexp x * (cexp x)⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_17
inst✝³ : NormedField 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
h : Tendsto (fun x ↦ g x / f x) l atTop
x✝ : α
⊢ f x✝ / g x✝ = ((fun r ↦ r⁻¹) ∘ fun x ↦ g x / f x) x✝

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
hx : 0 ≤ 0
⊢ 0 + 1 ≤ rexp 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
n j : ℕ
hn : 0 < n
h₁ : ↑n.succ ≠ 1
h₂ : ↑n.succ ≠ 0
h₃ : ↑n.factorial * ↑n ≠ 0
⊢ ↑n.succ - 1 = ↑n

Tactic:
simp

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

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

Tactic:
by
  simp [sin, sub_eq_add_neg, exp_neg, (neg_div _ _).symm, add_mul]

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

Goal state before:
pp: x : ℂ
⊢ cosh (x * I ^ 2) = cosh x

Tactic:
simp

Goal state after: