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

Goal state before:
pp: case pos
ι : 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₂
y : M₂
hf : Summable f L
hL : L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

pp: case neg
ι : 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₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
·

Goal state after:
case pos
ι : 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₂
y : M₂
hf : Summable f L
hL : L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg
ι : 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₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
·

Goal state after:
case neg
ι : 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₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg
ι : 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₂
y : M₂
hf : ¬Summable f L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y

Tactic:
·

Goal state after:
case neg
ι : 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₂
y : M₂
hf : ¬Summable f L
⊢ ∑'[L] (z : ι), e (f z) = y ↔ ∑'[L] (z : ι), f z = e.symm y
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₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ 0 = y → 0 = e.symm y

pp: case neg.refine_2
ι : 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₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y

Tactic:
·

Goal state after:
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₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
⊢ 0 = y → 0 = e.symm y
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

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

Tactic:
·

Goal state after:
case neg.refine_2
ι : 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₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable (fun z ↦ e (f z)) L
H : 0 = e.symm y
⊢ 0 = y
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
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
g : Quotient (orbitRel α β) → R
⊢ automorphize (g ∘ Quotient.mk' • f) = g • automorphize f

Tactic:
by
  ext x
  induction x using Quotient.inductionOn with | _ b
  simp only [automorphize, Pi.smul_apply', comp_apply]
  set π : β → Quotient (MulAction.orbitRel α β) := Quotient.mk (MulAction.orbitRel α β)
  have H₁ : ∀ a : α, π (a • b) = π b := by
    intro a
    apply (@Quotient.eq _ (MulAction.orbitRel α β) (a • b) b).mpr
    use a
  change ∑' a : α, g (π (a • b)) • f (a • b) = g (π b) • ∑' a : α, f (a • b)
  simp_rw [H₁]
  exact tsum_const_smul'' _

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ r • 0 = 0

Tactic:
ext <;> simp [smul_re, smul_im, smul_zero]

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

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'

pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂

Tactic:
·

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (algebraMap ℝ A) (x₁ * x₂ - y₁ * y₂) = (algebraMap ℝ A) x₁ * (algebraMap ℝ A) x₂ + y₁ • I' * y₂ • I'
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) x₂

Tactic:
·

Goal state after:
case e_a
A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (x₁ * y₂ + y₁ * x₂) • I' = (algebraMap ℝ A) x₁ * y₂ • I' + y₁ • I' * (algebraMap ℝ A) 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
a : ↥(skewAdjoint A)
⊢ I • ↑(negISMul a) = ↑a

Tactic:
simp [smul_smul]

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 a) + ↑(RCLike.im a) * I‖ = ‖a‖

pp: case inr
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.im RCLike.I = 1
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_2
inst✝ : RCLike 𝕜
a : 𝕜
h : RCLike.I = 0
⊢ ‖↑(RCLike.re a) + ↑(RCLike.im a) * I‖ = ‖a‖
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
tfae_5_to_1 : IsSelfAdjoint z → (starRingEnd K) z = z
⊢ [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(re z) = z, im z = 0, IsSelfAdjoint z].TFAE

Tactic:
tfae_finish

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)⁻¹

pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ 0⁻¹ = (starRingEnd K) 0 * ↑(‖0‖ ^ 2)⁻¹
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h₀ : z ≠ 0
⊢ z⁻¹ = (starRingEnd K) z * ↑(‖z‖ ^ 2)⁻¹
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0

pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖0‖ = c * 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ ↑‖x‖ = c * x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0

pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : RCLike K
h : I = 0
⊢ I⁻¹ = -I

pp: case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I

Tactic:
·

Goal state after:
case pos
K : Type u_1
inst✝ : RCLike K
h : I = 0
⊢ I⁻¹ = -I
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I

Tactic:
·

Goal state after:
case neg
K : Type u_1
inst✝ : RCLike K
h : ¬I = 0
⊢ I⁻¹ = -I
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case refine_1
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
⊢ 0 ≤ ℜ a

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

Tactic:
·

Goal state after:
case refine_1
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
⊢ 0 ≤ ℜ a
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

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
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case refine_1
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
x✝ : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
⊢ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1

pp: case refine_2
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
x✝ : IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
hx : IsStarNormal x
h : ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
⊢ star x * x = 1 ∧ x * star x = 1

Tactic:
·

Goal state after:
case refine_1
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
x✝ : star x * x = 1 ∧ x * star x = 1
h : star x * x = 1
h' : x * star x = 1
⊢ IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case refine_2
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
x✝ : IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
hx : IsStarNormal x
h : ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
⊢ star x * x = 1 ∧ x * star x = 1

Tactic:
·

Goal state after:
case refine_2
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
x✝ : IsStarNormal x ∧ ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
hx : IsStarNormal x
h : ↑(ℜ x) ^ 2 + ↑(ℑ x) ^ 2 = 1
⊢ star x * x = 1 ∧ x * star x = 1
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.source.domRestrict ↑e.toPartialEquiv)

pp: case right
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
⊢ Injective (e.source.domRestrict ↑e.toPartialEquiv)

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.source.domRestrict ↑e.toPartialEquiv)
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.source.domRestrict ↑e.toPartialEquiv)

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 (e.source.domRestrict ↑e.toPartialEquiv)
Module: Mathlib.Analysis.RCLike.Basic

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

pp: case mpr
K : Type u_1
inst✝ : RCLike K
z w : K
⊢ (re z ≤ re w ∧ re z ≠ re w) ∧ im z = im w → (re z ≤ re w ∧ im z = im w) ∧ z ≠ w

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < z ↔ ∃ x > 0, ↑x = z

Tactic:
simp_rw [pos_iff (K := K), ext_iff (K := K)]

Goal state after:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ 0 < re z ∧ im z = 0 ↔ ∃ x > 0, re ↑x = re z ∧ im ↑x = im z
Module: Mathlib.Analysis.RCLike.Basic

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

Tactic:
rw [lt_iff_re_im]

Goal state after:
K : Type u_1
inst✝ : RCLike K
x y : ℝ
⊢ re ↑x < re ↑y ∧ im ↑x = im ↑y ↔ x < y
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
⊢ z = ↑‖z‖

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

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝ : RCLike K
z : K
h : ‖z‖ ≤ re z
⊢ z = ↑‖z‖
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:
·

Goal state after:
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: case 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.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:
·

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

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

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: case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 < ↑a' * (c - b)
⊢ 0 ≤ c - b

pp: case inr
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 = ↑a' * (c - b)
⊢ 0 ≤ c - b

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 < ↑a' * (c - b)
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 = ↑a' * (c - b)
⊢ 0 ≤ c - b

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
a : { x // 0 < x }
b c : K
a' : ℝ
ha1 : a' > 0
ha2 : ↑a' = ↑a
h : 0 = ↑a' * (c - b)
⊢ 0 ≤ c - b
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝ : RCLike K
z : K
h : I = 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝ : RCLike K
z : K
h : I = 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖
Module: Mathlib.Analysis.RCLike.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖

Tactic:
have : (I : K) ≠ 0 := fun _ ↦ by simp_all

Goal state after:
case inr
K : Type u_1
inst✝ : RCLike K
z : K
h : im I = 1
this : I ≠ 0
⊢ ‖z‖ ≤ im z ↔ z = I * ↑‖z‖
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.ofNat a✝) =Θ[l] fun x ↦ g x ^ Int.ofNat a✝

pp: case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.negSucc a✝) =Θ[l] fun x ↦ g x ^ Int.negSucc a✝

Tactic:
·

Goal state after:
case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.ofNat a✝) =Θ[l] fun x ↦ g x ^ Int.ofNat a✝
Module: Mathlib.Analysis.Asymptotics.Theta

Goal state before:
pp: case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.negSucc a✝) =Θ[l] fun x ↦ g x ^ Int.negSucc a✝

Tactic:
·

Goal state after:
case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x ↦ f x ^ Int.negSucc a✝) =Θ[l] fun x ↦ g x ^ Int.negSucc a✝
Module: Mathlib.Analysis.Asymptotics.Defs

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

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

Tactic:
·

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