mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
x✝ : (starRingEnd K) z = z
h : (starRingEnd K) z = z := x✝
⊢ 0 = 0

Tactic:
]

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 y : 𝕜
⊢ ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I -
      ↑(RCLike.im x) * ↑(RCLike.im y) =
    ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I +
      ↑(RCLike.im x) * ↑(RCLike.im y) * -1

Tactic:
]

Goal state after:
z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x y : 𝕜
⊢ ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I -
      ↑(RCLike.im x) * ↑(RCLike.im y) =
    ↑(RCLike.re x) * ↑(RCLike.re y) + ↑(RCLike.re x) * ↑(RCLike.im y) * I + ↑(RCLike.re y) * ↑(RCLike.im x) * I +
      ↑(RCLike.im x) * ↑(RCLike.im y) * -1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
F : ℂ →ₐ[ℝ] A
⊢ -1 = -1

Tactic:
]

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

Goal state before:
pp: 𝕜 : Type u_2
𝕜' : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
h : RCLike.im RCLike.I = 1
a : 𝕜
⊢ 0 ≤ RCLike.re ((RCLike.map 𝕜 𝕜') a) ∧ RCLike.im ((RCLike.map 𝕜 𝕜') a) = 0 ↔ 0 ≤ RCLike.re a ∧ RCLike.im a = 0

Tactic:
]

Goal state after:
𝕜 : Type u_2
𝕜' : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : RCLike 𝕜'
h : RCLike.im RCLike.I = 1
a : 𝕜
⊢ 0 ≤ RCLike.re ((RCLike.map 𝕜 𝕜') a) ∧ RCLike.im ((RCLike.map 𝕜 𝕜') a) = 0 ↔ 0 ≤ RCLike.re a ∧ RCLike.im a = 0
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
⊢ star z = z

Tactic:
]

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.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✝ : 𝕜
⊢ normSq
      ({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝) =
    RCLike.re x✝ * RCLike.re x✝ + RCLike.im x✝ * RCLike.im x✝

Tactic:
]

Goal state after:
z : ℂ
E : Type u_1
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
𝕜 : Type u_2
inst✝ : RCLike 𝕜
h : RCLike.im RCLike.I = 1
x✝ : 𝕜
⊢ normSq
      ({ toFun := (RCLike.complexRingEquiv h).toFun, map_add' := ⋯, map_smul' := ⋯,
          invFun := (RCLike.complexRingEquiv h).invFun, left_inv := ⋯, right_inv := ⋯ }
        x✝) =
    RCLike.re x✝ * RCLike.re x✝ + RCLike.im x✝ * RCLike.im x✝
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:
]

Goal state after:
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‖
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 : star z = z
⊢ (starRingEnd K) z = z

Tactic:
]

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.Analysis.Complex.Basic

Goal state before:
pp: z : ℝ
hz : 0 ≤ ↑z
⊢ ↑z = ↑z

Tactic:
]

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

Goal state before:
pp: x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x

Tactic:
]

Goal state after:
x : ℂ
hx : 0 ≤ x
⊢ ↑‖x‖ = x
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ RCLike.re x ↔ 0 ≤ x

Tactic:
]

Goal state after:
x : ℂ
hx : IsSelfAdjoint x
⊢ 0 ≤ RCLike.re x ↔ 0 ≤ x
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: x y : ℂ
h : RCLike.re x ≤ RCLike.re y ∧ RCLike.im x = RCLike.im y
⊢ x.re ≤ y.re

Tactic:
]

Goal state after:
x y : ℂ
h : RCLike.re x ≤ RCLike.re y ∧ RCLike.im x = RCLike.im y
⊢ x.re ≤ y.re
Module: Mathlib.Analysis.Complex.Basic

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
hx : IsSelfAdjoint x
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ normSq z ∧ ¬normSq z = 0 ↔ z ≠ 0

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 ≤ normSq z ∧ ¬normSq z = 0 ↔ z ≠ 0
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
x y : A
h₁ : ℜ x = ℜ y
h₂ : ℑ x = ℑ y
⊢ ↑(ℜ y) + I • ↑(ℑ y) = ↑(ℜ y) + I • ↑(ℑ y)

Tactic:
]

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
⊢ 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁴ : SeminormedAddCommGroup A
inst✝³ : StarAddMonoid A
inst✝² : NormedSpace ℂ A
inst✝¹ : StarModule ℂ A
inst✝ : NormedStarGroup A
x : A
⊢ 2⁻¹ * ‖x + star x‖ ≤ 2⁻¹ * (2 * ‖x‖)
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
x : A
⊢ ↑(ℜ x) + I • ↑(ℑ x) ∈ span ℂ ↑(selfAdjoint A)

Tactic:
]

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x : A
⊢ ↑(ℜ x) + I • ↑(ℑ x) ∈ span ℂ ↑(selfAdjoint A)
Module: Mathlib.LinearAlgebra.Complex.Module

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

Tactic:
]

Goal state after:
r : ℝ
⊢ 2⁻¹ • 2 • ↑r = ↑r
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑‖z‖ ^ 2 = ↑‖z‖ ^ 2

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ = ‖z‖

Tactic:
]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ 1 = 1

pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ ↑‖z‖ ^ 2 ≠ 0

Tactic:
]

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ ↑‖z‖ ^ 2 ≠ 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * re z = (‖z‖ ^ 2)⁻¹ * re z

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ (‖z‖ ^ 2)⁻¹ * -im z = (‖z‖ ^ 2)⁻¹ * -im z

Tactic:
]

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
⊢ ↑(ℜ x) * ↑(ℑ x) = ↑(ℑ x) * ↑(ℜ x) ↔ ↑(ℜ x) * ↑(ℑ x) = ↑(ℑ x) * ↑(ℜ x)

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
r : ℝ
⊢ r⁻¹ * re z = r⁻¹ * re z

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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
⊢ OfNat.ofNat n * re z = OfNat.ofNat n * re z

Tactic:
]

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
⊢ OfNat.ofNat n * im z = OfNat.ofNat n * im z

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
n : ℤ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ↑q = ↑q

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ ↑q = ↑q

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ ofScientific m s e = ofScientific m s e

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
m : ℕ
s : Bool
e : ℕ
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ ‖↑↑n‖ = ↑n
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
by
  rw [← ofReal_natCast]
  exact norm_of_nonneg (Nat.cast_nonneg n)

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

Goal state before:
pp: case refine_2
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ ℜ a ∧ ℑ a = 0
⊢ 0 ≤ ↑(ℜ a) + I • ↑0

Tactic:
]

Goal state after:
case refine_2
A : Type u_1
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
a : A
h : 0 ≤ ℜ a ∧ ℑ a = 0
⊢ 0 ≤ ↑(ℜ a) + I • ↑0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑↑q‖ = ↑q

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ ‖↑↑q‖ = ↑q
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ ‖z‖ * ‖z‖ = ‖z‖ * ‖z‖

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z * re z ≤ normSq z

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z * re z ≤ normSq z
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ star x * x = 1 ∧ x * star x = 1 ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

Tactic:
]

Goal state after:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : SMulCommClass ℂ A A
inst✝¹ : IsScalarTower ℂ A A
inst✝ : StarModule ℂ A
x : A
⊢ star x * x = 1 ∧ x * star x = 1 ↔ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ normSq z

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im z * im z ≤ normSq z
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
a : K
h : ‖a‖ ≤ re a
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / ‖z‖ ≤ 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |re z| / ‖z‖ ≤ 1
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / ‖z‖ ≤ 1

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ |im z| / ‖z‖ ≤ 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star (↑(ℜ x) + I • ↑(ℑ x))) = star (φ (↑(ℜ x) + I • ↑(ℑ x)))

Tactic:
]

Goal state after:
A✝ : Type u_1
F : Type u_2
E : Type u_3
A : Type u_4
inst✝¹⁴ : AddCommGroup E
inst✝¹³ : PartialOrder E
inst✝¹² : StarAddMonoid E
inst✝¹¹ : SelfAdjointDecompose E
inst✝¹⁰ : Module ℂ E
inst✝⁹ : StarModule ℂ E
inst✝⁸ : NonUnitalRing A
inst✝⁷ : PartialOrder A
inst✝⁶ : StarRing A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module ℂ A
inst✝³ : StarModule ℂ A
inst✝² : FunLike F E A
inst✝¹ : OrderHomClass F E A
inst✝ : LinearMapClass F ℂ E A
φ : F
x : E
⊢ φ (star (↑(ℜ x) + I • ↑(ℑ x))) = star (φ (↑(ℜ x) + I • ↑(ℑ x)))
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖

Tactic:
]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ re ↑(‖x‖ ^ 2) = ‖↑(‖x‖ ^ 2)‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ (2 * re x) ^ 2 = (2 * re x) ^ 2

Tactic:
]

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
x : K
⊢ re (x + (starRingEnd K) x) ^ 2 = re (x + (starRingEnd K) x) ^ 2

Tactic:
]

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
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ univ

Tactic:
]

Goal state after:
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
h : e.source = univ
h' : e.target = univ
x : X
⊢ x ∈ univ
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
h : e.source = univ
h' : e.target = univ
x : Y
⊢ x ∈ univ

Tactic:
]

Goal state after:
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
h : e.source = univ
h' : e.target = univ
x : Y
⊢ x ∈ univ
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:
]

Goal state after:
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)
Module: Mathlib.Topology.PartialHomeomorph.Basic

Goal state before:
pp: case left
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ IsInducing ⇑e.toEquiv

Tactic:
]

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.toEquiv
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 Subtype.val

Tactic:
]

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

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝ : RCLike K
z : K
r : ℤ
x : K
⊢ |↑r| * ‖x‖ = |↑r| * ‖x‖

Tactic:
]

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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.source.domRestrict ↑f) f.target ⋯)

Tactic:
]

Goal state after:
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.source.domRestrict ↑f) f.target ⋯)
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.target.domRestrict f.invFun) f.source ⋯)

Tactic:
]

Goal state after:
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype]
    (codRestrict (f.target.domRestrict f.invFun) f.source ⋯)
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'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv ∧ Surjective ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv

Tactic:
]

Goal state after:
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'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv ∧ Surjective ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv
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'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding
    (codRestrict ((InjOn.toPartialEquiv f univ ⋯).source.domRestrict ↑(InjOn.toPartialEquiv f univ ⋯))
      (InjOn.toPartialEquiv f univ ⋯).target ⋯)

Tactic:
]

Goal state after:
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'
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
⊢ IsEmbedding
    (codRestrict ((InjOn.toPartialEquiv f univ ⋯).source.domRestrict ↑(InjOn.toPartialEquiv f univ ⋯))
      (InjOn.toPartialEquiv f univ ⋯).target ⋯)
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
ι : Type u_3
s : Finset ι
f : ι → E
x✝¹ : ℕ
x✝ : E
⊢ (↑x✝¹)⁻¹ • ‖x✝‖ = (↑x✝¹)⁻¹ • ‖x✝‖

Tactic:
]

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
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ x = x

pp: case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ x ∈ (toPartialHomeomorph f h).source

Tactic:
]

Goal state after:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : X
⊢ x ∈ (toPartialHomeomorph f h).source
Module: Mathlib.Topology.PartialHomeomorph.Basic

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

pp: case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ x ∈ (toPartialHomeomorph f h).target

Tactic:
]

Goal state after:
case h
X : Type u_1
Y : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
h : IsEmbedding f
inst✝ : Nonempty X
x : Y
hx : x ∈ range f
⊢ x ∈ (toPartialHomeomorph f h).target