mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a b : Rˣ
⊢ ↑a * ↑b⁻¹ ∈ unitary R ↔ star a * a = star b * b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a b : Rˣ
⊢ ↑a⁻¹ * ↑b ∈ unitary R ↔ a * star a = b * star b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

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

Tactic:
by

Goal state after:
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 φ
⊢ ∃ C, ∀ (v : V₁), ‖⟨φ v, ⋯⟩‖ ≤ C * ‖v‖

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

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

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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✝ : (i : ι) → R i
x y : NNReal
h : x ≤ y
⊢ (fun x ↦ x ^ 2) x ≤ (fun x ↦ x ^ 2) y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x u : R
hu : u ∈ unitary R
⊢ Commute u x ↔ star u * x * u = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
x u : R
hu : u ∈ unitary R
⊢ Commute u x ↔ u * x * star u = x

Tactic:
by

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

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

Goal state before:
pp: 𝕜 : 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 : (i : ι) → R i
⊢ ⊥ ^ 2 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : StarMul G
g : G
hg : g ∈ unitary G
⊢ g⁻¹ ∈ unitary G

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Monoid R
inst✝⁶ : Monoid A
inst✝⁵ : MulAction R A
inst✝⁴ : SMulCommClass R A A
inst✝³ : IsScalarTower R A A
inst✝² : StarMul R
inst✝¹ : StarMul A
inst✝ : StarModule R A
r : R
a : A
hr : r ∈ unitary R
ha : a ∈ unitary A
⊢ r • a ∈ unitary A

Tactic:
by

Goal state after:
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₁ ↥(f.equalizer g)
⊢ f.comp ((ι f g).comp ψ) = g.comp ((ι f g).comp ψ)

Tactic:
by

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

Goal state before:
pp: 𝕜 : 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 : (i : ι) → R i
⊢ ‖x‖ * ‖x‖ ≤ ‖x⋆ * x‖

Tactic:
by

Goal state after:
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₃
φ : { φ // f.comp φ = g.comp φ }
⊢ (fun ψ ↦ ⟨(ι f g).comp ψ, ⋯⟩) ((fun φ ↦ lift ↑φ ⋯) φ) = φ

Tactic:
by

Goal state after:
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 : Type u_5
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
r : R
hr : r ∈ unitary R
⊢ f r ∈ unitary S

Tactic:
by

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

Goal state after:
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₂
ψ : NormedAddGroupHom W₁ W₂
hf : ψ.comp f₁ = f₂.comp φ
hg : ψ.comp g₁ = g₂.comp φ
⊢ f₂.comp (φ.comp (ι f₁ g₁)) = g₂.comp (φ.comp (ι f₁ g₁))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U₁ U₂ : ↥(unitary R)
⊢ ↑(U₁ / U₂) = ↑U₁ / ↑U₂

Tactic:
by

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

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
U : ↥(unitary R)
z : ℤ
⊢ ↑(U ^ z) = ↑U ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : StarRing R
U : ↥(unitary R)
⊢ -↑U ∈ unitary R

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
⊢ ‖1‖ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝³ : CommSemiring R
inst✝² : Ring A
inst✝¹ : Algebra R A
inst✝ : StarMul A
a : A
U : ↥(unitary A)
⊢ spectrum R (star ↑U * a * ↑U) = spectrum R a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : StarRing R
inst✝¹ : TrivialStar R
inst✝ : NoZeroDivisors R
a : R
⊢ a ∈ unitary R ↔ a = 1 ∨ a = -1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_2
inst✝¹ : Ring R
inst✝ : StarRing R
p : R
hp : IsStarProjection p
⊢ 2 * p - 1 ∈ unitary R

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝³ : NormedRing E
inst✝² : StarRing E
inst✝¹ : CStarRing E
inst✝ : Nontrivial E
U : ↥(unitary E)
⊢ ‖↑U‖ = 1

Tactic:
by

Goal state after:
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₁ : NormedAddGroupHom V₁ W₁
f₂ : NormedAddGroupHom V₂ W₂
f₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : ψ.comp f₁ = f₂.comp φ
hf' : ψ'.comp f₂ = f₃.comp φ'
⊢ (ψ'.comp ψ).comp f₁ = f₃.comp (φ'.comp φ)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
U : ↥(unitary E)
A : E
⊢ ‖↑U * A‖ = ‖A‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
A : E
U : ↥(unitary E)
⊢ ‖A * ↑U‖ = ‖A‖

Tactic:
by

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

Goal state after:
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 : 𝕜
⊢ ‖f x‖ ≤ ‖f 1‖ * ‖x‖

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

Tactic:
by

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

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

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
e : E
he : IsStarProjection e
this : ‖e‖ * (‖e‖ - 1) = 0
⊢ ‖e‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝² : NonUnitalNormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
e : E
he : IsStarProjection e
⊢ ‖e‖ ≤ 1

Tactic:
by

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

Goal state before:
pp: 𝕜✝ : Type u_1
E : Type u_2
α : Type u_3
𝕜 : Type u_4
A : Type u_5
inst✝⁵ : NormedField 𝕜
inst✝⁴ : StarRing 𝕜
inst✝³ : SeminormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : StarModule 𝕜 A
S : StarSubalgebra 𝕜 A
⊢ NormedAlgebra 𝕜 ↥S

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℝ
a : α
⊢ ↑(balance f a) = balance (ofReal ∘ f) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑reAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑reAddGroupHom).toFun x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).re = balance (re ∘ f) a

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℂ
⊢ ∀ (m : ℚ≥0) (x : ℂ), (↑imAddGroupHom).toFun (m • x) = (RingHom.id ℚ≥0) m • (↑imAddGroupHom).toFun x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
f : α → ℂ
a : α
⊢ (balance f a).im = balance (im ∘ f) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: 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
f g : A ≃A[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
⊢ Function.Injective toAlgEquiv

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: 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
e₁ : A ≃A[R] B
e₂ : B ≃A[R] C
⊢ (↑e₂.toAlgEquiv).comp ↑e₁.toAlgEquiv = ↑↑(e₁.trans e₂)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : TopologicalSpace A
inst✝³ : Semiring B
inst✝² : TopologicalSpace B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃A[R] B
S : Set B
⊢ ⇑e.symm '' S = ⇑e ⁻¹' S

Tactic:
by

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: 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 j : ι
h : i = j
⊢ Continuous[inst✝ i, inst✝ j] (AlgEquiv.cast h).toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Equiv

Goal state before:
pp: 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 j : ι
h : i = j
⊢ Continuous[inst✝ j, inst✝ i] (AlgEquiv.cast h).invFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
a : α
⊢ (DistribSMul.toAddMonoidHom α g⁻¹) ((↑(DistribSMul.toAddMonoidHom α g)).toFun a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : Group γ
inst✝² : DistribMulAction γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
a : α
⊢ (↑(DistribSMul.toAddMonoidHom α g)).toFun ((DistribSMul.toAddMonoidHom α g⁻¹) a) = a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : AddCommMonoid α
f : β → α
L : SummationFilter β
γ : Type u_5
inst✝³ : DivisionSemiring γ
inst✝² : Module γ α
inst✝¹ : ContinuousConstSMul γ α
inst✝ : T2Space α
g : γ
⊢ ∑'[L] (i : β), g • f i = g • ∑'[L] (i : β), f i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : 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₂
L : SummationFilter ι
f : ι → M
φ : M →SL[σ] M₂
x : M
hf : HasSum f x L
⊢ HasSum (fun b ↦ φ (f b)) (φ x) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : 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 ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum (fun b ↦ e (f b)) y L
⊢ HasSum f (e.symm y) L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : 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 ι
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
h : HasSum f (e.symm y) L
⊢ HasSum (fun b ↦ e (f b)) y L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : 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 ι
f : ι → M
e : M ≃SL[σ] M₂
x : M
⊢ HasSum (fun b ↦ e (f b)) (e x) L ↔ HasSum f x L

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

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

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: ι : 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₂
⊢ e (∑'[L] (z : ι), f z) = ∑'[L] (z : ι), e (f z)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Module

Goal state before:
pp: α : 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
⊢ Quotient (orbitRel α β) → M

Tactic:
by

Goal state after:
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
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
⊢ ∀ (a : α), π (a • b) = π b

Tactic:
by

Goal state after: