mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
y₁ y₂ : β
⊢ edist (toLp p (0, y₁)) (toLp p (0, y₂)) = edist y₁ y₂

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Forall P ↔ ∀ (x : Matrix (Fin (m + 1)) (Fin n) α), P x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
P : Matrix (Fin (m + 1)) (Fin n) α → Prop
⊢ Exists P ↔ ∃ x, P x

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ A.transposeᵣ i j = Aᵀ i j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b

Tactic:
by
  simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
      Function.comp_apply]

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: l m n : ℕ
α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
A : Matrix (Fin l) (Fin m) α
B : Matrix (Fin m) (Fin n) α
⊢ A.mulᵣ B = A * B

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix (Fin l) (Fin m) α
v : Fin m → α
⊢ A.mulVecᵣ v = A *ᵥ v

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: l m : ℕ
α : Type u_1
inst✝ : NonUnitalNonAssocSemiring α
v : Fin l → α
A : Matrix (Fin l) (Fin m) α
⊢ vecMulᵣ v A = v ᵥ* A

Tactic:
by

Goal state after:
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin n) α
⊢ A.etaExpand = A

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
C : ℝ
Cpos : C > 0
hC : ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
y : F
x : E
xs : x ∈ s
fxy : f x = y
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ s
z : F
hz : z ∈ ball y (ε / C)
w : E
wim : f w = z - y
wnorm : ‖w‖ ≤ C * ‖z - y‖
this : f (x + w) = z
⊢ C * ‖z - y‖ < C * (ε / C)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ A * star A = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
⊢ A ∈ unitaryGroup n α ↔ star A * A = 1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det ∈ unitary α

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
f : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
surj : Surjective ⇑f
⊢ IsOpenMap ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i : ι
a : β i
⊢ (single p i a).ofLp i = a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i' ≠ i
a : β i
⊢ (single p i a).ofLp i' = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (β i)
i i' : ι
h : i ≠ i'
a : β i
⊢ (single p i a).ofLp i' = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f).range = ⊤
⊢ ∃ fsymm, 0 < fsymm.nnnorm

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero 𝕜
i : ι
a : 𝕜
j : ι
⊢ (single p i a).ofLp j = if j = i then a else 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁴ : RingHomInvPair σ σ'
inst✝³ : RingHomIsometric σ
inst✝² : RingHomIsometric σ'
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
f : E →SL[σ] F
hsurj : (↑f).range = ⊤
⊢ 0 < (f.nonlinearRightInverseOfSurjective hsurj).nnnorm

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
⊢ single p i (a + b) = single p i a + single p i b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
⊢ single p i (a - b) = single p i a - single p i b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a : β i
⊢ single p i (-a) = -single p i a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
inst✝³ : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module 𝕜 (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
this :
  LinearIndependent 𝕜 (⇑↑(WithLp.linearEquiv p 𝕜 ((j : η) → Ms j)).symm ∘ fun ji ↦ Pi.single ji.fst (v ji.fst ji.snd))
⊢ LinearIndependent 𝕜 fun ji ↦ single p ji.fst (v ji.fst ji.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
inst✝³ : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module 𝕜 (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
⊢ InjOn ⇑↑(WithLp.linearEquiv p 𝕜 ((j : η) → Ms j)).symm
    ↑(Submodule.span 𝕜 (range fun ji ↦ Pi.single ji.fst (v ji.fst ji.snd)))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
inst✝³ : Semiring 𝕜
η : Type u_5
ιs : η → Type u_6
Ms : η → Type u_7
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module 𝕜 (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent 𝕜 (v i)
⊢ LinearIndependent 𝕜 fun ji ↦ single p ji.fst (v ji.fst ji.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Ring 𝕜
this : LinearIndependent 𝕜 (⇑↑(WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm ∘ fun i ↦ Pi.single i 1)
⊢ LinearIndependent 𝕜 fun i ↦ single p i 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Ring 𝕜
⊢ InjOn ⇑↑(WithLp.linearEquiv p 𝕜 (ι → 𝕜)).symm ↑(Submodule.span 𝕜 (range fun i ↦ Pi.single i 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Ring 𝕜
⊢ LinearIndependent 𝕜 fun i ↦ single p i 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Ring 𝕜
inst✝³ : IsDomain 𝕜
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
this : LinearIndependent 𝕜 (⇑↑(WithLp.linearEquiv p 𝕜 (ι → M)).symm ∘ fun i ↦ Pi.single i (v i))
⊢ LinearIndependent 𝕜 fun i ↦ single p i (v i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ ∈ unitary (Matrix (n × m) (n × m) R)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring A
inst✝⁷ : Semiring B
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra R B
inst✝⁴ : StarRing A
inst✝³ : StarRing B
inst✝² : StarRing R
inst✝¹ : StarModule R A
inst✝ : StarModule R B
U : A
V : B
hU : U ∈ unitary A
hV : V ∈ unitary B
⊢ U ⊗ₜ[R] V ∈ unitary (A ⊗[R] B)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Ring 𝕜
inst✝³ : IsDomain 𝕜
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ InjOn ⇑↑(WithLp.linearEquiv p 𝕜 (ι → M)).symm ↑(Submodule.span 𝕜 (range fun i ↦ Pi.single i (v i)))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Ring 𝕜
inst✝³ : IsDomain 𝕜
M : Type u_5
inst✝² : AddCommGroup M
inst✝¹ : Module 𝕜 M
inst✝ : IsTorsionFree 𝕜 M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent 𝕜 fun i ↦ single p i (v i)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝¹³ : DecidableEq n
inst✝¹² : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Semiring A
inst✝⁹ : Semiring B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra R B
inst✝⁶ : StarRing A
inst✝⁵ : StarRing B
inst✝⁴ : StarRing R
inst✝³ : StarModule R A
inst✝² : StarModule R B
m : Type u_4
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : U ∈ unitary (Matrix m m A)
hV : V ∈ unitary (Matrix n n B)
⊢ U ⊗ₖₜ[R] V ∈ unitary (Matrix (m × n) (m × n) (A ⊗[R] B))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' A⁻¹ ∘ₗ toLin' A) x = (toLin' (A⁻¹ * A)) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' (A⁻¹ * A)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
⊢ edist f f = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' A ∘ₗ toLin' A⁻¹) x = (toLin' (A * A⁻¹)) x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
⊢ (toLin' (A * A⁻¹)) x = x

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
⊢ ↑(toGL 1) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A B : ↥(unitaryGroup n α)
⊢ ↑(toGL (A * B)) = ↑(toGL A * toGL B)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
⊢ edist f g = edist g f

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : Matrix n n α
⊢ Uᵀ ∈ unitaryGroup n α ↔ U ∈ unitaryGroup n α

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : Matrix n n α
⊢ U.map star ∈ unitaryGroup n α ↔ U ∈ unitaryGroup n α

Tactic:
simp [← conjTranspose_transpose, transpose_mem_unitaryGroup_iff, ← star_eq_conjTranspose]

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : Matrix n n α
⊢ U.map star ∈ unitaryGroup n α ↔ U ∈ unitaryGroup n α

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
⊢ (map_star U)⁻¹ = transpose U

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
e : E ≃ₛₗ[σ] F
h :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    ⇑e.symm

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
U : ↥(unitaryGroup n α)
⊢ (transpose U)⁻¹ = map_star U

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ star ↑A ∈ ↑(unitaryGroup n α)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A✝ : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ star ↑A ∈ ↑(MonoidHom.mker detMonoidHom)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl.inr
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ∞)
f g h : PiLp ∞ β
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (h.ofLp i) ≤ (⨆ i, edist (f.ofLp i) (g.ofLp i)) + ⨆ i, edist (g.ofLp i) (h.ofLp i)

Tactic:
refine
        iSup_le fun i => (edist_triangle _ (g i) _).trans <| add_le_add
            (le_iSup (fun k => edist (f k) (g k)) i) (le_iSup (fun k => edist (g k) (h k)) i)

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
f✝ : E →SL[σ] F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : Injective ⇑f
hclo : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f)
x : E
⊢ f x ∈ (↑f).range

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : Injective ⇑f
hclo : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f)
x : E
⊢ (equivRange hinj hclo).symm ⟨f x, ⋯⟩ = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ p.toReal
⊢ (∑ i, edist (f.ofLp i) (h.ofLp i) ^ p.toReal) ^ (1 / p.toReal) ≤
    (∑ i, (edist (f.ofLp i) (g.ofLp i) + edist (g.ofLp i) (h.ofLp i)) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
a b c d : R
⊢ !![a, b; c, d] ∈ specialOrthogonalGroup (Fin 2) R ↔ a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_5
F : Type u_6
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
f : E →L[𝕜] F
hf : Injective ⇑f
⊢ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f) ↔ ∃ K, AntilipschitzWith K ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
⊢ edist f h ≤ edist f g + edist g h

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
M : Matrix (Fin 2) (Fin 2) R
⊢ M ∈ specialOrthogonalGroup (Fin 2) R ↔ M 0 0 = M 1 1 ∧ M 0 1 = -M 1 0 ∧ M 0 0 ^ 2 + M 0 1 ^ 2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
f : WithLp p (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p✝)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ toLp p (WithLp.fst 0, 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
α : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ∞ α
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p✝)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ ∀ (x y : WithLp p (α × β)), toLp p ((x + y).fst, 0) = toLp p (x.fst, 0) + toLp p (y.fst, 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p✝)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ toLp p (0, WithLp.snd 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p✝ : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p✝)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ ∀ (x y : WithLp p (α × β)), toLp p (0, (x + y).snd) = toLp p (0, x.snd) + toLp p (0, y.snd)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ p.toReal
hp : ¬p = 0
h✝ : ¬p = ∞
i : ι
⊢ 0 i ≤ dist (f.ofLp i) (g.ofLp i) ^ p.toReal

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
x : WithLp p (α × β)
⊢ (idemFst + idemSnd) x = 1 x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: p : ℝ≥0∞
𝕜 : Type u_1
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
⊢ 0 ≤ dist f g

Tactic:
by

Goal state after: