mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (Int.negSucc n✝ • a✝).re = (-(↑n✝.succ • a✝)).re

pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (Int.negSucc n✝ • a✝).im = (-(↑n✝.succ • a✝)).im

Tactic:
<;>

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (Int.negSucc n✝ • a✝).re = (-(↑n✝.succ • a✝)).re

case a
n✝ : ℕ
a✝ : ℂ
⊢ (Int.negSucc n✝ • a✝).im = (-(↑n✝.succ • a✝)).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.re = -((↑n✝ + 1) * a✝.re)

pp: case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.im = -((↑n✝ + 1) * a✝.im)

Tactic:
<;>

Goal state after:
case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.re = -((↑n✝ + 1) * a✝.re)

case a
n✝ : ℕ
a✝ : ℂ
⊢ (-1 + -↑n✝) * a✝.im = -((↑n✝ + 1) * a✝.im)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (-a✝ + a✝).re = re 0

pp: case a
a✝ : ℂ
⊢ (-a✝ + a✝).im = im 0

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (-a✝ + a✝).re = re 0

case a
a✝ : ℂ
⊢ (-a✝ + a✝).im = im 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re

pp: case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).re = (b✝ + a✝).re

case a
a✝ b✝ : ℂ
⊢ (a✝ + b✝).im = (b✝ + a✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ a✝.re + b✝.re = b✝.re + a✝.re

pp: case a
a✝ b✝ : ℂ
⊢ a✝.im + b✝.im = b✝.im + a✝.im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ : ℂ
⊢ a✝.re + b✝.re = b✝.re + a✝.re

case a
a✝ b✝ : ℂ
⊢ a✝.im + b✝.im = b✝.im + a✝.im
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: case inl
α : Type u_1
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
ha : a ≤ 0
⊢ |q • a| = q • |a|

pp: case inr
α : Type u_1
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ |q • a| = q • |a|

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
ha : a ≤ 0
⊢ |q • a| = q • |a|

case inr
α : Type u_1
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : DistribMulAction ℚ≥0 α
inst✝ : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ |q • a| = q • |a|
Module: Mathlib.Algebra.Order.Module.Rat

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ q • a < q • b

Tactic:
by
    rw [NNRat.smul_def, NNRat.smul_def]; exact mul_lt_mul_of_pos_left hab <| NNRat.cast_pos.2 hq

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

Goal state before:
pp: case a
⊢ (↑0).re = re 0

pp: case a
⊢ (↑0).im = im 0

Tactic:
<;>

Goal state after:
case a
⊢ (↑0).re = re 0

case a
⊢ (↑0).im = im 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
x✝ : ℕ
⊢ (↑(x✝ + 1)).re = (↑x✝ + 1).re

pp: case a
x✝ : ℕ
⊢ (↑(x✝ + 1)).im = (↑x✝ + 1).im

Tactic:
<;>

Goal state after:
case a
x✝ : ℕ
⊢ (↑(x✝ + 1)).re = (↑x✝ + 1).re

case a
x✝ : ℕ
⊢ (↑(x✝ + 1)).im = (↑x✝ + 1).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).re = (↑x✝).re

pp: case a
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).im = (↑x✝).im

Tactic:
<;>

Goal state after:
case a
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).re = (↑x✝).re

case a
x✝ : ℕ
⊢ (IntCast.intCast ↑x✝).im = (↑x✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
x✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc x✝)).re = (-↑(x✝ + 1)).re

pp: case a
x✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc x✝)).im = (-↑(x✝ + 1)).im

Tactic:
<;>

Goal state after:
case a
x✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc x✝)).re = (-↑(x✝ + 1)).re

case a
x✝ : ℕ
⊢ (IntCast.intCast (Int.negSucc x✝)).im = (-↑(x✝ + 1)).im
Module: Mathlib.Analysis.Complex.Order

Goal state before:
pp: z w : ℂ
⊢ ¬z < w ↔ w.re ≤ z.re ∨ z.im ≠ w.im

Tactic:
by
  rw [lt_def, not_and_or, not_lt]

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

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).re = (a✝ * (b✝ * c✝)).re

case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * b✝ * c✝).im = (a✝ * (b✝ * c✝)).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)

pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im)

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.re - (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.im =
    a✝.re * (b✝.re * c✝.re - b✝.im * c✝.im) - a✝.im * (b✝.re * c✝.im + b✝.im * c✝.re)

case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re * b✝.re - a✝.im * b✝.im) * c✝.im + (a✝.re * b✝.im + a✝.im * b✝.re) * c✝.re =
    a✝.re * (b✝.re * c✝.im + b✝.im * c✝.re) + a✝.im * (b✝.re * c✝.re - b✝.im * c✝.im)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (1 * a✝).re = a✝.re

pp: case a
a✝ : ℂ
⊢ (1 * a✝).im = a✝.im

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (1 * a✝).re = a✝.re

case a
a✝ : ℂ
⊢ (1 * a✝).im = a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ * 1).re = a✝.re

pp: case a
a✝ : ℂ
⊢ (a✝ * 1).im = a✝.im

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (a✝ * 1).re = a✝.re

case a
a✝ : ℂ
⊢ (a✝ * 1).im = a✝.im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (0 * a✝).re = re 0

pp: case a
a✝ : ℂ
⊢ (0 * a✝).im = im 0

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (0 * a✝).re = re 0

case a
a✝ : ℂ
⊢ (0 * a✝).im = im 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ : ℂ
⊢ (a✝ * 0).re = re 0

pp: case a
a✝ : ℂ
⊢ (a✝ * 0).im = im 0

Tactic:
<;>

Goal state after:
case a
a✝ : ℂ
⊢ (a✝ * 0).re = re 0

case a
a✝ : ℂ
⊢ (a✝ * 0).im = im 0
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re

pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).re = (a✝ * b✝ + a✝ * c✝).re

case a
a✝ b✝ c✝ : ℂ
⊢ (a✝ * (b✝ + c✝)).im = (a✝ * b✝ + a✝ * c✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.re + c✝.re) - a✝.im * (b✝.im + c✝.im) = a✝.re * b✝.re - a✝.im * b✝.im + (a✝.re * c✝.re - a✝.im * c✝.im)

pp: case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.re + c✝.re) - a✝.im * (b✝.im + c✝.im) = a✝.re * b✝.re - a✝.im * b✝.im + (a✝.re * c✝.re - a✝.im * c✝.im)

case a
a✝ b✝ c✝ : ℂ
⊢ a✝.re * (b✝.im + c✝.im) + a✝.im * (b✝.re + c✝.re) = a✝.re * b✝.im + a✝.im * b✝.re + (a✝.re * c✝.im + a✝.im * c✝.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re

pp: case a
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).re = (a✝ * c✝ + b✝ * c✝).re

case a
a✝ b✝ c✝ : ℂ
⊢ ((a✝ + b✝) * c✝).im = (a✝ * c✝ + b✝ * c✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.re - (a✝.im + b✝.im) * c✝.im = a✝.re * c✝.re - a✝.im * c✝.im + (b✝.re * c✝.re - b✝.im * c✝.im)

pp: case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)

Tactic:
<;>

Goal state after:
case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.re - (a✝.im + b✝.im) * c✝.im = a✝.re * c✝.re - a✝.im * c✝.im + (b✝.re * c✝.re - b✝.im * c✝.im)

case a
a✝ b✝ c✝ : ℂ
⊢ (a✝.re + b✝.re) * c✝.im + (a✝.im + b✝.im) * c✝.re = a✝.re * c✝.im + a✝.im * c✝.re + (b✝.re * c✝.im + b✝.im * c✝.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ (a✝ * b✝).re = (b✝ * a✝).re

pp: case a
a✝ b✝ : ℂ
⊢ (a✝ * b✝).im = (b✝ * a✝).im

Tactic:
<;>

Goal state after:
case a
a✝ b✝ : ℂ
⊢ (a✝ * b✝).re = (b✝ * a✝).re

case a
a✝ b✝ : ℂ
⊢ (a✝ * b✝).im = (b✝ * a✝).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.re - a✝.im * b✝.im = b✝.re * a✝.re - b✝.im * a✝.im

pp: case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re

Tactic:
<;>

Goal state after:
case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.re - a✝.im * b✝.im = b✝.re * a✝.re - b✝.im * a✝.im

case a
a✝ b✝ : ℂ
⊢ a✝.re * b✝.im + a✝.im * b✝.re = b✝.re * a✝.im + b✝.im * a✝.re
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im }.re = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).re

pp: case a
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im }.im = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).im

Tactic:
<;>

Goal state after:
case a
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im }.re = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).re

case a
a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im }.im = ({ re := b.re, im := -b.im } * { re := a.re, im := -a.im }).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im

pp: case a
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)

Tactic:
<;>

Goal state after:
case a
a b : ℂ
⊢ a.re * b.re - a.im * b.im = b.re * a.re - b.im * a.im

case a
a b : ℂ
⊢ -(a.re * b.im) + -(a.im * b.re) = -(b.re * a.im) + -(b.im * a.re)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im }.re = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).re

pp: case a
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im }.im = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).im

Tactic:
<;>

Goal state after:
case a
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im }.re = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).re

case a
a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im }.im = ({ re := a.re, im := -a.im } + { re := b.re, im := -b.im }).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
z : ℂ
⊢ (↑(normSq z)).re = ((starRingEnd ℂ) z * z).re

pp: case a
z : ℂ
⊢ (↑(normSq z)).im = ((starRingEnd ℂ) z * z).im

Tactic:
<;>

Goal state after:
case a
z : ℂ
⊢ (↑(normSq z)).re = ((starRingEnd ℂ) z * z).re

case a
z : ℂ
⊢ (↑(normSq z)).im = ((starRingEnd ℂ) z * z).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case zero
r : ℝ
⊢ ↑(r ^ 0) = ↑r ^ 0

pp: case succ
r : ℝ
n✝ : ℕ
a✝ : ↑(r ^ n✝) = ↑r ^ n✝
⊢ ↑(r ^ (n✝ + 1)) = ↑r ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
r : ℝ
⊢ ↑(r ^ 0) = ↑r ^ 0

case succ
r : ℝ
n✝ : ℕ
a✝ : ↑(r ^ n✝) = ↑r ^ n✝
⊢ ↑(r ^ (n✝ + 1)) = ↑r ^ (n✝ + 1)
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
α : Type u_1
q : ℚ≥0
⊢ (↑q).re = (↑q.num / ↑q.den).re

pp: case a
α : Type u_1
q : ℚ≥0
⊢ (↑q).im = (↑q.num / ↑q.den).im

Tactic:
<;>

Goal state after:
case a
α : Type u_1
q : ℚ≥0
⊢ (↑q).re = (↑q.num / ↑q.den).re

case a
α : Type u_1
q : ℚ≥0
⊢ (↑q).im = (↑q.num / ↑q.den).im
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: case a
α : Type u_1
q : ℚ
⊢ (↑q).re = (↑q.num / ↑q.den).re

pp: case a
α : Type u_1
q : ℚ
⊢ (↑q).im = (↑q.num / ↑q.den).im

Tactic:
<;>

Goal state after:
case a
α : Type u_1
q : ℚ
⊢ (↑q).re = (↑q.num / ↑q.den).re

case a
α : Type u_1
q : ℚ
⊢ (↑q).im = (↑q.num / ↑q.den).im
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
obtain rfl | hs_nonempty := s.eq_empty_or_nonempty

Goal state after:
case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ ∅, p (f i)
⊢ m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)

case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module ℚ≥0 M
inst✝⁴ : AddCommMonoid N
inst✝³ : PartialOrder N
inst✝² : IsOrderedAddMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case h₁
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖

pp: case h₂
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g v‖ ≤ ‖g‖ * ‖v‖

Tactic:
<;>

Goal state after:
case h₁
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖

case h₂
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g v‖ ≤ ‖g‖ * ‖v‖
Module: Mathlib.Analysis.CStarAlgebra.Basic

Goal state before:
pp: case inl
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
h : ‖x.1‖ ≤ ‖x.2‖
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2

pp: case inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
h : ‖x.2‖ ≤ ‖x.1‖
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2

Tactic:
<;>

Goal state after:
case inl
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
h : ‖x.1‖ ≤ ‖x.2‖
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2

case inr
𝕜 : Type u_1
E : Type u_2
α : Type u_3
ι : Type u_4
R₁ : Type u_5
R₂ : Type u_6
R : ι → Type u_7
inst✝⁹ : NonUnitalNormedRing R₁
inst✝⁸ : StarRing R₁
inst✝⁷ : CStarRing R₁
inst✝⁶ : NonUnitalNormedRing R₂
inst✝⁵ : StarRing R₂
inst✝⁴ : CStarRing R₂
inst✝³ : (i : ι) → NonUnitalNormedRing (R i)
inst✝² : (i : ι) → StarRing (R i)
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), CStarRing (R i)
x : R₁ × R₂
h : ‖x.2‖ ≤ ‖x.1‖
⊢ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.1‖ ^ 2 ∨ max ‖x.1‖ ‖x.2‖ ^ 2 ≤ ‖x.2‖ ^ 2
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: case neg.mp
ι : 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
⊢ ∑ᶠ (z : ι), e (f z) = y → e (∑ᶠ (z : ι), f z) = y

pp: case neg.mpr
ι : 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
⊢ e (∑ᶠ (z : ι), f z) = y → ∑ᶠ (z : ι), e (f z) = y

Tactic:
<;>

Goal state after:
case neg.mp
ι : 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
⊢ ∑ᶠ (z : ι), e (f z) = y → e (∑ᶠ (z : ι), f z) = y

case neg.mpr
ι : 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
⊢ e (∑ᶠ (z : ι), f z) = y → ∑ᶠ (z : ι), e (f z) = y
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).re = (s • r • x).re

pp: case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).im = (s • r • x).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).re = (s • r • x).re

case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).im = (s • r • x).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).re = (r • s • x).re

pp: case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).im = (r • s • x).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).re = (r • s • x).re

case a
R : Type u_1
S : Type u_2
inst✝³ : SMul R S
inst✝² : SMul R ℝ
inst✝¹ : SMul S ℝ
inst✝ : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).im = (r • s • x).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).re = (r • x).re

pp: case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).im = (r • x).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).re = (r • x).re

case a
R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).im = (r • x).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).re = (r • s • x).re

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).im = (r • s • x).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).re = (r • s • x).re

case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).im = (r • s • x).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).re = x.re

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).im = x.im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).re = x.re

case a
R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ (1 • x).im = x.im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).re = re 0

pp: case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).im = im 0

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).re = re 0

case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ (r • 0).im = im 0
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).re = (r • x + r • y).re

pp: case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).im = (r • x + r • y).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).re = (r • x + r • y).re

case a
R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).im = (r • x + r • y).im
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).re = (r • x + s • x).re

pp: case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).im = (r • x + s • x).im

Tactic:
<;>

Goal state after:
case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).re = (r • x + s • x).re

case a
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).im = (r • x + s • x).im