mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ ⇑e.symm '' S = ⇑e ⁻¹' S

Tactic:
e.symm.image_eq_preimage_symm,

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ ⇑e.symm.symm ⁻¹' S = ⇑e ⁻¹' S
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ ∀ (x y : ℂ),
    (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) (x * y) =
      (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) x *
        (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) y

Tactic:
rintro ⟨x₁, y₁⟩ ⟨x₂, y₂⟩

Goal state after:
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm)
      ({ re := x₁, im := y₁ } * { re := x₂, im := y₂ }) =
    (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₁, im := y₁ } *
      (Algebra.linearMap ℝ A ∘ₗ reLm + LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) { re := x₂, im := y₂ }
Module: Mathlib.Analysis.Complex.Basic

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

Tactic:
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.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‖ ≤ ‖x‖

Tactic:
by
  calc ‖imaginaryPart x‖ = ‖realPart (Complex.I • (-x))‖ := by simp
    _ ≤ ‖x‖ := by simpa only [smul_neg, map_neg, realPart_I_smul, neg_neg,
        AddSubgroupClass.coe_norm, norm_neg, norm_smul, Complex.norm_I, one_mul] using
        realPart.norm_le (Complex.I • (-x))

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

Goal state before:
pp: A : Type u_1
inst✝⁵ : NonUnitalNonAssocRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : StarModule ℂ A
x : A
hx : IsStarNormal x
⊢ ↑(ℜ x) * ↑(ℜ x) + ↑(ℑ x) * ↑(ℑ x) + I • (↑(ℜ x) * ↑(ℑ x) - ↑(ℑ x) * ↑(ℜ x)) = ↑(ℜ x) * ↑(ℜ x) + ↑(ℑ x) * ↑(ℑ x)

Tactic:
by simp [Commute.realPart_imaginaryPart x |>.eq]

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:
simp [realPart_apply_coe, ← two_smul ℝ]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖-1‖ = 1

Tactic:
norm_neg,

Goal state after:
K : Type u_1
inst✝ : RCLike K
hI : I ≠ 0
⊢ ‖1‖ = 1
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (↑e.toPartialEquiv ∘ Subtype.val)

Tactic:
toFun_eq_coe e,

Goal state after:
case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (↑e ∘ Subtype.val)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝ : RCLike K
z w : K
heq : z ≠ w
hr : re z ≤ re w
hi : im z = im w
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w

Tactic:
exact ⟨⟨hr, mt (fun hreq => ext hreq hi) heq⟩, hi⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] (range (e.source.domRestrict ↑e))

Tactic:
rw [range_domRestrict, image_source_eq_target]

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] e.target
Module: Mathlib.Topology.OpenPartialHomeomorph.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ IsOpen[inst✝] e.target

Tactic:
exact e.open_target

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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

case refine_2
K : Type u_1
inst✝ : RCLike K
z : K
h : z = ↑‖z‖
⊢ ‖z‖ ≤ re z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
hx : 0 ≤ re x ∧ im x = 0
y z : K
hyz : x * y < x * z
⊢ y < z

Tactic:
obtain ⟨r, rfl⟩ := ((is_real_TFAE x).out 3 1).1 hx.2

Goal state after:
K : Type u_1
inst✝ : RCLike K
y z : K
r : ℝ
hx : 0 ≤ re ↑r ∧ im ↑r = 0
hyz : ↑r * y < ↑r * z
⊢ y < z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
ha : 0 < a
r₁ r₂ : ℝ
hr : r₁ < r₂
hare : re 0 < re a
haim : im 0 = im a
⊢ r₁ • a < r₂ • a

Tactic:
simp_all [RCLike.lt_iff_re_im (K := K), smul_re, smul_im]

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

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

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 [hx, zero_mul, lt_self_iff_false, false_and, false_or]

Goal state after:
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
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (x y : ℝ), 0 ≤ x → x < y → ∃ a, x < ‖a‖ ∧ ‖a‖ < y
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ Function.Involutive star

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ Function.Involutive star
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r s : 𝕜), star (r * s) = star s * star r
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r s : 𝕜), star (r + s) = star r + star s
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ (algebraMap ℝ 𝕜) 1 = 1

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ (algebraMap ℝ 𝕜) 1 = 1
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x * y) = (algebraMap ℝ 𝕜) x * (algebraMap ℝ 𝕜) y

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x * y) = (algebraMap ℝ 𝕜) x * (algebraMap ℝ 𝕜) y
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ (algebraMap ℝ 𝕜) 0 = 0

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ (algebraMap ℝ 𝕜) 0 = 0
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x + y) = (algebraMap ℝ 𝕜) x + (algebraMap ℝ 𝕜) y

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (x y : ℝ), (algebraMap ℝ 𝕜) (x + y) = (algebraMap ℝ 𝕜) x + (algebraMap ℝ 𝕜) y
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
      x * { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
      x * { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜),
    r • x = { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
subst h''

Goal state after:
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
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r : ℝ) (x : 𝕜), ‖r • x‖ ≤ ‖r‖ * ‖x‖
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‖ ≤ ‖r‖ * ‖x‖

Tactic:
exact h.norm_smul_le

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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ {f : Filter 𝕜}, Cauchy f → ∃ x, f ≤ nhds x

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ {f : Filter 𝕜}, Cauchy f → ∃ x, f ≤ nhds x
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ 𝕜 →+ ℝ

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ 𝕜 →+ ℝ
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ (⋯ ▸
        let __spread.0 := h.toNormedField;
        re)
      I =
    0

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ (⋯ ▸
        let __spread.0 := h.toNormedField;
        re)
      I =
    0
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ I = 0 ∨ I * I = -1

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ I = 0 ∨ I * I = -1
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z : 𝕜),
    { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          ((⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z) +
        { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
            ((⋯ ▸
                let __spread.0 := h.toNormedField;
                im)
              z) *
          I =
      z

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
          ((⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z) +
        { toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
            ((⋯ ▸
                let __spread.0 := h.toNormedField;
                im)
              z) *
          I =
      z
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      r

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      r
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      0

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (r : ℝ),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ({ toFun := ⇑(algebraMap ℝ 𝕜), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r) =
      0
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w -
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w -
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z w : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        (z * w) =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ((starRingEnd 𝕜) z) =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        z

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        ((starRingEnd 𝕜) z) =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          re)
        z
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ((starRingEnd 𝕜) z) =
      -(⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        ((starRingEnd 𝕜) z) =
      -(⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ (starRingEnd 𝕜) I = -I

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ (starRingEnd 𝕜) I = -I
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z : 𝕜),
    ‖z‖ ^ 2 =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    ‖z‖ ^ 2 =
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z +
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z *
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z *
        (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          I =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        z

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ (z : 𝕜),
    (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          z *
        (⋯ ▸
            let __spread.0 := h.toNormedField;
            im)
          I =
      (⋯ ▸
          let __spread.0 := h.toNormedField;
          im)
        z
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 𝕜
hk : NormedField 𝕜
h'' : hk = h.toNormedField
⊢ ∀ {z w : 𝕜},
    z ≤ w ↔
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z ≤
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w ∧
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z =
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w

Tactic:
subst h''

Goal state after:
K : Type u_1
E : Type u_2
inst✝ : RCLike K
𝕜 : Type u_3
h : RCLike 𝕜
__spread✝⁻⁰ : NormedField 𝕜 := h.toNormedField
⊢ ∀ {z w : 𝕜},
    z ≤ w ↔
      (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            z ≤
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              re)
            w ∧
        (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            z =
          (⋯ ▸
              let __spread.0 := h.toNormedField;
              im)
            w
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'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ IsBigOWith c (𝓝[insert x s] x) g g' ↔ IsBigOWith c (𝓝[s] x) g g'

Tactic:
rw [isBigOWith_insert]

Goal state after:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝² : SeminormedAddCommGroup E'
inst✝¹ : SeminormedAddCommGroup F'
inst✝ : TopologicalSpace α
x : α
s : Set α
g : α → E'
g' : α → F'
h : g x = 0
c : ℝ
hc : 0 < c
⊢ ‖g x‖ ≤ c * ‖g' x‖