mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: case mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
g : A ≃⋆* B
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h : { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun = g.toFun
⊢ { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun = g.invFun →
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ } = g

Tactic:
;

Goal state after:
case mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
g : A ≃⋆* B
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h : { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun = g.toFun
⊢ { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun = g.invFun →
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ } = g
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
toMulEquiv✝¹ : A ≃* B
map_star'✝¹ : ∀ (a : A), toMulEquiv✝¹.toFun (star a) = star (toMulEquiv✝¹.toFun a)
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h :
  { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.toFun =
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun
⊢ { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.invFun =
      { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun →
    { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ } = { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }

Tactic:
;

Goal state after:
case mk.mk
F : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝⁷ : Mul A
inst✝⁶ : Mul B
inst✝⁵ : Mul C
inst✝⁴ : Mul D
inst✝³ : Star A
inst✝² : Star B
inst✝¹ : Star C
inst✝ : Star D
toMulEquiv✝¹ : A ≃* B
map_star'✝¹ : ∀ (a : A), toMulEquiv✝¹.toFun (star a) = star (toMulEquiv✝¹.toFun a)
toMulEquiv✝ : A ≃* B
map_star'✝ : ∀ (a : A), toMulEquiv✝.toFun (star a) = star (toMulEquiv✝.toFun a)
h :
  { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.toFun =
    { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.toFun
⊢ { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ }.invFun =
      { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }.invFun →
    { toMulEquiv := toMulEquiv✝¹, map_star' := map_star'✝¹ } = { toMulEquiv := toMulEquiv✝, map_star' := map_star'✝ }
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M ≤ max M 1

Tactic:
;

Goal state after:
case hbc
V : Type u_1
W : Type u_2
inst✝¹ : SeminormedAddCommGroup V
inst✝ : SeminormedAddCommGroup W
f : V → W
M : ℝ
h : ∀ (x : V), ‖f x‖ ≤ M * ‖x‖
x : V
⊢ M ≤ max M 1
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case mk
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✝ g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h : { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g

Tactic:
;

Goal state after:
case mk
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✝ g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h : { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case mk.mk
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₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ }.toFun =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }

Tactic:
;

Goal state after:
case mk.mk
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₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ }.toFun =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }.toFun
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H : ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = ⇑g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g

Tactic:
;

Goal state after:
case mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
g : NormedAddGroupHom V₁ V₂
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H : ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = ⇑g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case mk.mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H :
  ⇑{ toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }

Tactic:
;

Goal state after:
case mk.mk
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
toFun✝¹ : V₁ → V₂
map_add'✝¹ : ∀ (v₁ v₂ : V₁), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : V₁), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : V₁ → V₂
map_add'✝ : ∀ (v₁ v₂ : V₁), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : V₁), ‖toFun✝ v‖ ≤ C * ‖v‖
H :
  ⇑{ toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    ⇑{ toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case ha
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖

Tactic:
;

Goal state after:
case ha
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
c : ℝ
x : V₁
h : ‖x‖ ≤ c
⊢ 0 ≤ ‖f‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ max C 0

Tactic:
;

Goal state after:
case hbc
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : V₁ →+ V₂
C : ℝ
h : ∀ (x : V₁), ‖f x‖ ≤ C * ‖x‖
x : V₁
⊢ C ≤ max C 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : ‖x‖ / ‖x‖ ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖

Tactic:
div_self hx

Goal state after:
V : Type u_1
inst✝¹ : SeminormedAddCommGroup V
inst✝ : NontrivialTopology V
x : V
hx : ‖x‖ ≠ 0
this : 1 ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
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₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖

Tactic:
;

Goal state after:
case hbc
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₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
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₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖

Tactic:
;

Goal state after:
case hbc
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₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖f v‖ ≤ b * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case hbc
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₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖

Tactic:
;

Goal state after:
case hbc
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₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f v‖ ≤ ‖f‖ * ‖v‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case b0
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₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ 0 ≤ C₂

Tactic:
;

Goal state after:
case b0
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₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ 0 ≤ C₂
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ (incl s).toAddMonoidHom y ∈ s

Tactic:
;

Goal state after:
V₁ : Type u_3
inst✝ : SeminormedAddCommGroup V₁
s : AddSubgroup V₁
x : V₁
x✝ : x ∈ (incl s).range
y : ↥s
hy : (incl s).toAddMonoidHom y = x
⊢ (incl s).toAddMonoidHom y ∈ s
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ f.toAddMonoidHom.range = f.range

Tactic:
;

Goal state after:
V₁ : Type u_3
V₂ : Type u_4
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
⊢ f.toAddMonoidHom.range = f.range
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
x✝ : ↥(unitary R)
⊢ ↑((toUnits.comp (map f).toMonoidHom) x✝) = ↑(((Units.map f.toMonoidHom).comp toUnits) x✝)

Tactic:
;

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.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • f 1‖ ≤ ‖x‖ * ‖f 1‖

Tactic:
;

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Ring 𝕜₂
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : IsBoundedSMul 𝕜 E
f : 𝕜 →ₗ[𝕜] E
x : 𝕜
⊢ ‖x • f 1‖ ≤ ‖x‖ * ‖f 1‖
Module: Mathlib.Analysis.Normed.Operator.ContinuousLinearMap

Goal state before:
pp: 𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
⊢ (∀ (x : E), ‖f x‖ = a * ‖x‖) → ∀ (y : F), ‖f.symm y‖ = a⁻¹ * ‖y‖

Tactic:
intro hf y

Goal state after:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Ring 𝕜
inst✝⁶ : Ring 𝕜₂
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : Module 𝕜 E
inst✝² : Module 𝕜₂ F
σ : 𝕜 →+* 𝕜₂
σ₂₁ : 𝕜₂ →+* 𝕜
inst✝¹ : RingHomInvPair σ σ₂₁
inst✝ : RingHomInvPair σ₂₁ σ
a : ℝ
ha : 0 < a
f : E ≃ₛₗ[σ] F
hf : ∀ (x : E), ‖f x‖ = a * ‖x‖
y : F
⊢ ‖f.symm y‖ = a⁻¹ * ‖y‖
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst✝⁷ : UniformSpace E₁
inst✝⁶ : UniformSpace E₂
inst✝⁵ : Ring E₁
inst✝⁴ : IsUniformAddGroup E₁
inst✝³ : Algebra R E₁
inst✝² : Ring E₂
inst✝¹ : IsUniformAddGroup E₂
inst✝ : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑e
h₂ : Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm
⊢ Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
E₁ : Type u_5
E₂ : Type u_6
inst✝⁷ : UniformSpace E₁
inst✝⁶ : UniformSpace E₂
inst✝⁵ : Ring E₁
inst✝⁴ : IsUniformAddGroup E₁
inst✝³ : Algebra R E₁
inst✝² : Ring E₂
inst✝¹ : IsUniformAddGroup E₂
inst✝ : Algebra R E₂
e : E₁ ≃ₐ[R] E₂
h₁ : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁶.toTopologicalSpace] ⇑e
h₂ : Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm
⊢ Continuous[inst✝⁶.toTopologicalSpace, inst✝⁷.toTopologicalSpace] ⇑e.symm
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: case refl
R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i : ι
__spread✝⁻⁰ : A i ≃ₐ[R] A i := AlgEquiv.cast ⋯
⊢ Continuous[inst✝ i, inst✝ i] (AlgEquiv.cast ⋯).toFun

Tactic:
;

Goal state after:
case refl
R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i : ι
__spread✝⁻⁰ : A i ≃ₐ[R] A i := AlgEquiv.cast ⋯
⊢ Continuous[inst✝ i, inst✝ i] (AlgEquiv.cast ⋯).toFun
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: case refl
R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i : ι
__spread✝⁻⁰ : A i ≃ₐ[R] A i := AlgEquiv.cast ⋯
⊢ Continuous[inst✝ i, inst✝ i] (AlgEquiv.cast ⋯).invFun

Tactic:
;

Goal state after:
case refl
R : Type u_1
A✝ : Type u_2
B : Type u_3
C : Type u_4
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A✝
inst✝¹⁰ : TopologicalSpace A✝
inst✝⁹ : Semiring B
inst✝⁸ : TopologicalSpace B
inst✝⁷ : Semiring C
inst✝⁶ : TopologicalSpace C
inst✝⁵ : Algebra R A✝
inst✝⁴ : Algebra R B
inst✝³ : Algebra R C
ι : Type u_5
A : ι → Type u_6
inst✝² : (i : ι) → Semiring (A i)
inst✝¹ : (i : ι) → Algebra R (A i)
inst✝ : (i : ι) → TopologicalSpace (A i)
i : ι
__spread✝⁻⁰ : A i ≃ₐ[R] A i := AlgEquiv.cast ⋯
⊢ Continuous[inst✝ i, inst✝ i] (AlgEquiv.cast ⋯).invFun
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: n : ℤ
⊢ ↑‖↑n‖₊ = ↑‖n‖₊

Tactic:
;

Goal state after:
n : ℤ
⊢ ↑‖↑n‖₊ = ↑‖n‖₊
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ a ≤ b

Tactic:
;

Goal state after:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ a ≤ b
Module: Mathlib.Analysis.Complex.Basic

Goal state before:
pp: ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖

Tactic:
;

Goal state after:
ι : Type u_2
a b : ℝ
f : ι → ℂ
s : Finset ι
ha₀ : 0 ≤ a
ha : ↑a = ∑ i ∈ s, f i
hb : b = ∑ i ∈ s, ‖f i‖
⊢ ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: x : ℂ
hx : x ∈ ⊤
⊢ x ∈ ℝ[I]

Tactic:
;

Goal state after:
x : ℂ
hx : x ∈ ⊤
⊢ x ∈ ℝ[I]
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.im x) + ↑(RCLike.im y)) * I =
    ↑(RCLike.re x) + ↑(RCLike.im x) * I + (↑(RCLike.re y) + ↑(RCLike.im y) * I)

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

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✝¹ : ℝ
x✝ : 𝕜
⊢ ↑x✝¹ * ↑(RCLike.im x✝) * I = ↑x✝¹ * (↑(RCLike.im x✝) * I)
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 : ℝ
b : ↥(skewAdjoint A)
⊢ ↑⟨-I • ↑(a • b), ⋯⟩ = ↑((RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩)

Tactic:
;

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
a : ℝ
b : ↥(skewAdjoint A)
⊢ ↑⟨-I • ↑(a • b), ⋯⟩ = ↑((RingHom.id ℝ) a • ⟨-I • ↑b, ⋯⟩)
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✝ : ↥(selfAdjoint.submodule ℝ A)
⊢ ↑((ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype) x✝) = ↑(0 x✝)

Tactic:
;

Goal state after:
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
x✝ : ↥(selfAdjoint.submodule ℝ A)
⊢ ↑((ℑ ∘ₗ (selfAdjoint.submodule ℝ A).subtype) x✝) = ↑(0 x✝)
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: r : ℝ
⊢ ↑(ℑ ↑r) = ↑0

Tactic:
;

Goal state after:
r : ℝ
⊢ ↑(ℑ ↑r) = ↑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
q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q

Tactic:
;

Goal state after:
K : Type u_1
inst✝ : RCLike K
q : ℚ≥0
⊢ NNReal.mk ↑q ⋯ = ↑q
Module: Mathlib.LinearAlgebra.Complex.Module

Goal state before:
pp: A : Type u_1
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
⊢ ↑(ℜ 1) = ↑1

Tactic:
;

Goal state after:
A : Type u_1
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Module ℂ A
inst✝ : StarModule ℂ A
⊢ ↑(ℜ 1) = ↑1
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.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
⊢ IsHomeomorph ⇑(InjOn.toPartialEquiv f univ ⋯).toEquiv

Tactic:
rw [isHomeomorph_iff_isEmbedding_surjective]

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