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

Goal state before:
pp: n✝ : ℕ
a✝ : ℂ
⊢ ↑n✝.succ • a✝ = ↑n✝ • a✝ + a✝

Tactic:
ext

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

case a
n✝ : ℕ
a✝ : ℂ
⊢ (↑n✝.succ • a✝).im = (↑n✝ • a✝ + a✝).im
Module: Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ ↔ HasFiniteIntegral f μ

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral (↑c • f) μ → HasFiniteIntegral f μ

case mpr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup β
𝕜 : Type u_7
inst✝² : NormedRing 𝕜
inst✝¹ : MulActionWithZero 𝕜 β
inst✝ : IsBoundedSMul 𝕜 β
f : α → β
c : 𝕜ˣ
⊢ HasFiniteIntegral f μ → HasFiniteIntegral (↑c • f) μ
Module: Mathlib.Data.Complex.Basic

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

Tactic:
ext

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: a✝ : ℂ
⊢ -a✝ + a✝ = 0

Tactic:
ext

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: a✝ b✝ : ℂ
⊢ a✝ + b✝ = b✝ + a✝

Tactic:
ext

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: ⊢ ↑0 = 0

Tactic:
ext

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

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

Goal state before:
pp: x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
ext

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: x✝ : ℕ
⊢ IntCast.intCast ↑x✝ = ↑x✝

Tactic:
ext

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: x✝ : ℕ
⊢ IntCast.intCast (Int.negSucc x✝) = -↑(x✝ + 1)

Tactic:
ext

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

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

Tactic:
ext

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: a✝ : ℂ
⊢ 1 * a✝ = a✝

Tactic:
ext

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: a✝ : ℂ
⊢ a✝ * 1 = a✝

Tactic:
ext

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: a✝ : ℂ
⊢ 0 * a✝ = 0

Tactic:
ext

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: a✝ : ℂ
⊢ a✝ * 0 = 0

Tactic:
ext

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: a✝ b✝ c✝ : ℂ
⊢ a✝ * (b✝ + c✝) = a✝ * b✝ + a✝ * c✝

Tactic:
ext

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: a✝ b✝ c✝ : ℂ
⊢ (a✝ + b✝) * c✝ = a✝ * c✝ + b✝ * c✝

Tactic:
ext

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: a✝ b✝ : ℂ
⊢ a✝ * b✝ = b✝ * a✝

Tactic:
ext

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: a b : ℂ
⊢ { re := (a * b).re, im := -(a * b).im } = { re := b.re, im := -b.im } * { re := a.re, im := -a.im }

Tactic:
ext

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: a b : ℂ
⊢ { re := (a + b).re, im := -(a + b).im } = { re := a.re, im := -a.im } + { re := b.re, im := -b.im }

Tactic:
ext

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: z : ℂ
⊢ ↑(normSq z) = (starRingEnd ℂ) z * z

Tactic:
ext

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: α : Type u_1
q : ℚ≥0
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext

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: α : Type u_1
q : ℚ
⊢ ↑q = ↑q.num / ↑q.den

Tactic:
ext

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

Goal state before:
pp: a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

Tactic:
constructor

Goal state after:
case mp
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]] → x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b}

case mpr
a₁ a₂ b : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' [[a₁, a₂]] ×ˢ {b} → x ∈ (fun x ↦ ↑x + ↑b * I) '' [[a₁, a₂]]
Module: Mathlib.Data.Complex.Basic

Goal state before:
pp: a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] ↔ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

Tactic:
constructor

Goal state after:
case mp
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] → x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]

case mpr
a b₁ b₂ : ℝ
x : ℂ
⊢ x ∈ ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]] → x ∈ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]]
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: 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✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
a✝ b✝ : NormedAddGroupHom V₁ V₂
⊢ g.comp (a✝ + b✝) = g.comp a✝ + g.comp b✝

Tactic:
ext

Goal state after:
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✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
a✝ b✝ : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ (g.comp (a✝ + b✝)) x✝ = (g.comp a✝ + g.comp b✝) x✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: 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 : NormedAddGroupHom V₁ V₂
a✝ b✝ : NormedAddGroupHom V₂ V₃
⊢ AddMonoidHom.mk' (fun f ↦ (a✝ + b✝).comp f) ⋯ =
    AddMonoidHom.mk' (fun f ↦ a✝.comp f) ⋯ + AddMonoidHom.mk' (fun f ↦ b✝.comp f) ⋯

Tactic:
ext

Goal state after:
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 : NormedAddGroupHom V₁ V₂
a✝ b✝ : NormedAddGroupHom V₂ V₃
x✝¹ : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ((AddMonoidHom.mk' (fun f ↦ (a✝ + b✝).comp f) ⋯) x✝¹) x✝ =
    ((AddMonoidHom.mk' (fun f ↦ a✝.comp f) ⋯ + AddMonoidHom.mk' (fun f ↦ b✝.comp f) ⋯) x✝¹) x✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
⊢ f.comp 0 = 0

Tactic:
ext

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ (f.comp 0) x✝ = 0 x✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
⊢ NormedAddGroupHom.comp 0 f = 0

Tactic:
ext

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ (NormedAddGroupHom.comp 0 f) x✝ = 0 x✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V₁
inst✝² : SeminormedAddCommGroup V₂
inst✝¹ : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst✝ : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V₁
inst✝² : SeminormedAddCommGroup V₂
inst✝¹ : SeminormedAddCommGroup V₃
V₄ : Type u_5
inst✝ : SeminormedAddCommGroup V₄
h : NormedAddGroupHom V₃ V₄
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ((h.comp g).comp f) x✝ = (h.comp (g.comp f)) x✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
⊢ (incl g.ker).comp (lift f g h) = f

Tactic:
ext

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : g.comp f = 0
x✝ : V₁
⊢ ((incl g.ker).comp (lift f g h)) x✝ = f x✝
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
⊢ ker 0 = ⊤

Tactic:
ext

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ x✝ ∈ ker 0 ↔ x✝ ∈ ⊤
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : ↥(unitary R)
⊢ star (star x) = x

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x : ↥(unitary R)
⊢ ↑(star (star x)) = ↑x
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x y : ↥(unitary R)
⊢ star (x * y) = star y * star x

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x y : ↥(unitary R)
⊢ ↑(star (x * y)) = ↑(star y * star x)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
⊢ ⟨φ (v₁ + v₂), ⋯⟩ = ⟨φ v₁, ⋯⟩ + ⟨φ v₂, ⋯⟩

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
v₁ v₂ : V₁
⊢ ↑⟨φ (v₁ + v₂), ⋯⟩ = ↑(⟨φ v₁, ⋯⟩ + ⟨φ v₂, ⋯⟩)
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
⊢ unitary Rˣ = Submonoid.comap (Units.coeHom R) (unitary R)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x✝ : Rˣ
⊢ x✝ ∈ unitary Rˣ ↔ x✝ ∈ Submonoid.comap (Units.coeHom R) (unitary R)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
W : Type u_2
V₁ : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : SeminormedAddCommGroup W
inst✝ : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
⊢ (ι f g).comp (lift φ h) = φ

Tactic:
ext

Goal state after:
V : Type u_1
W : Type u_2
V₁ : Type u_3
inst✝² : SeminormedAddCommGroup V
inst✝¹ : SeminormedAddCommGroup W
inst✝ : SeminormedAddCommGroup V₁
f g : NormedAddGroupHom V W
φ : NormedAddGroupHom V₁ V
h : f.comp φ = g.comp φ
x✝ : V₁
⊢ ((ι f g).comp (lift φ h)) x✝ = φ x✝
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : StarMul R
inst✝¹ : Monoid S
inst✝ : StarMul S
f : R →⋆* S
⊢ toUnits.comp (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits

Tactic:
ext

Goal state after:
R : Type u_2
S : Type u_3
inst✝³ : Monoid R
inst✝² : StarMul R
inst✝¹ : Monoid S
inst✝ : StarMul S
f : R →⋆* S
x✝ : ↥(unitary R)
⊢ ↑((toUnits.comp (map f).toMonoidHom) x✝) = ↑(((Units.map f.toMonoidHom).comp toUnits) x✝)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst✝ : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
⊢ map (id V₁) (id W₁) ⋯ ⋯ = id ↥(f₁.equalizer g₁)

Tactic:
ext

Goal state after:
V₁ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
W₁ : Type u_6
inst✝ : SeminormedAddCommGroup W₁
f₁ g₁ : NormedAddGroupHom V₁ W₁
x✝ : ↥(f₁.equalizer g₁)
⊢ ↑((map (id V₁) (id W₁) ⋯ ⋯) x✝) = ↑((id ↥(f₁.equalizer g₁)) x✝)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
⊢ (map φ' ψ' hf' hg').comp (map φ ψ hf hg) = map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯

Tactic:
ext

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
V₃ : Type u_5
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
W₁ : Type u_6
W₂ : Type u_7
W₃ : Type u_8
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
hg' : ψ'.comp g₂ = g₃.comp φ'
x✝ : ↥(f₁.equalizer g₁)
⊢ ↑(((map φ' ψ' hf' hg').comp (map φ ψ hf hg)) x✝) = ↑((map (φ'.comp φ) (ψ'.comp ψ) ⋯ ⋯) x✝)
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
⊢ ∑ᶠ (z : ι), e (f z) = y ↔ e (∑ᶠ (z : ι), f z) = y

Tactic:
constructor

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.Topology.Algebra.InfiniteSum.Module

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

Tactic:
ext

Goal state after:
case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R✝ : Type u_7
R₂ : Type u_8
M✝ : Type u_9
M₂ : Type u_10
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : Group α
inst✝ : MulAction α β
f : β → M
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
x✝ : α
⊢ f (x✝ • a • b₂) = f ((x✝ * a) • b₂)
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: 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 = s • r • x

Tactic:
ext

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: 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 = r • s • x

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝² : SMul R ℝ
inst✝¹ : SMul Rᵐᵒᵖ ℝ
inst✝ : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ MulOpposite.op r • x = r • x

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
r s : R
x : ℂ
⊢ (r * s) • x = r • s • x

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝¹ : Monoid R
inst✝ : MulAction R ℝ
x : ℂ
⊢ 1 • x = x

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
⊢ r • 0 = 0

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝ : DistribSMul R ℝ
r : R
x y : ℂ
⊢ r • (x + y) = r • x + r • y

Tactic:
ext

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: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r s : R
x : ℂ
⊢ (r + s) • x = r • x + s • x

Tactic:
ext

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Module R ℝ
r : ℂ
⊢ 0 • r = 0

Tactic:
ext

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

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