mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
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)
i✝ j✝ : n × m
⊢ ∑ j, star U₂ i✝.2 j.2 * star U₁ i✝.1 j.1 * U₁ j.1 j✝.1 * U₂ j.2 j✝.2 = 1 i✝ j✝

pp: case right
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)
i✝ j✝ : n × m
⊢ ∑ j, U₁ i✝.1 j.1 * U₂ i✝.2 j.2 * star U₂ j.2 j✝.2 * star U₁ j.1 j✝.1 = 1 i✝ j✝

Tactic:
·

Goal state after:
case left
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)
i✝ j✝ : n × m
⊢ ∑ j, star U₂ i✝.2 j.2 * star U₁ i✝.1 j.1 * U₁ j.1 j✝.1 * U₂ j.2 j✝.2 = 1 i✝ j✝
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case right
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)
i✝ j✝ : n × m
⊢ ∑ j, U₁ i✝.1 j.1 * U₂ i✝.2 j.2 * star U₂ j.2 j✝.2 * star U₁ j.1 j✝.1 = 1 i✝ j✝

Tactic:
·

Goal state after:
case right
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)
i✝ j✝ : n × m
⊢ ∑ j, U₁ i✝.1 j.1 * U₂ i✝.2 j.2 * star U₂ j.2 j✝.2 * star U₁ j.1 j✝.1 = 1 i✝ j✝
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

pp: case inr
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 (α × β)
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : NormSMulClass 𝕜 α
inst✝ : NormSMulClass 𝕜 β
c : 𝕜
hp : Fact (1 ≤ ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
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 (α × β)
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊

Tactic:
·

Goal state after:
case inr
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 (α × β)
hp : 1 ≤ p.toReal
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

pp: case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ∞ β
⊢ edist f f = 0

pp: case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
·

Goal state after:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp 0 β
⊢ edist f f = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ∞ β
⊢ edist f f = 0

pp: case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < p.toReal
⊢ edist f f = 0

Tactic:
·

Goal state after:
case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ∞ β
⊢ edist f f = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

Tactic:
·

Goal state after:
case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < p.toReal
⊢ edist f f = 0
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

pp: case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ∞ β
⊢ edist f g = edist g f

pp: case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
·

Goal state after:
case inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ∞ β
⊢ edist f g = edist g f

pp: case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f

Tactic:
·

Goal state after:
case inr.inl
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ∞ β
⊢ edist f g = edist g f
Module: Mathlib.Analysis.Normed.Lp.PiLp

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

Tactic:
·

Goal state after:
case inr.inr
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < p.toReal
⊢ edist f g = edist g f
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : 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 ∞ β
⊢ edist f h ≤ edist f g + edist g h

pp: case inr
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
⊢ edist f h ≤ edist f g + edist g h

Tactic:
·

Goal state after:
case inl
𝕜 : 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 ∞ β
⊢ edist f h ≤ edist f g + edist g h
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl.inl
𝕜 : 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✝ : IsEmpty ι
⊢ ⨆ i, edist (f.ofLp i) (h.ofLp i) ≤ (⨆ i, edist (f.ofLp i) (g.ofLp i)) + ⨆ i, edist (g.ofLp i) (h.ofLp i)

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:
·

Goal state after:
case inl.inl
𝕜 : 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✝ : IsEmpty ι
⊢ ⨆ i, edist (f.ofLp i) (h.ofLp i) ≤ (⨆ i, edist (f.ofLp i) (g.ofLp i)) + ⨆ i, edist (g.ofLp i) (h.ofLp i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
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
⊢ edist f h ≤ edist f g + edist g h

Tactic:
·

Goal state after:
case inr
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
⊢ edist f h ≤ edist f g + edist g h
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 * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1

pp: R : Type v
inst✝ : CommRing R
a b c d : R
⊢ ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1 ↔
    a = d ∧ b = -c ∧ a ^ 2 + b ^ 2 = 1

Tactic:
·

Goal state after:
R : Type v
inst✝ : CommRing R
a b c d : R
⊢ !![a, b; c, d] ∈ specialOrthogonalGroup (Fin 2) R ↔
    ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
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 (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f.fst‖₊ ^ p.toReal + ‖(c • f).snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal

Tactic:
smul_snd,

Goal state after:
case inr
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 (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖c • f.fst‖₊ ^ p.toReal + ‖c • f.snd‖₊ ^ p.toReal = (‖c‖₊ * ‖f.fst‖₊) ^ p.toReal + (‖c‖₊ * ‖f.snd‖₊) ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : 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 : PiLp ∞ α
⊢ 0 ≤ dist f g

pp: case inr
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
⊢ 0 ≤ dist f g

Tactic:
·

Goal state after:
case inl
𝕜 : 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 : PiLp ∞ α
⊢ 0 ≤ dist f g
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
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
⊢ 0 ≤ dist f g

Tactic:
·

Goal state after:
case inr
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
⊢ 0 ≤ dist f g
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case pos
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
⊢ 0 ≤ ↑⋯.toFinset.card

pp: case pos
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 = ∞
⊢ 0 ≤ ⨆ i, dist (f.ofLp i) (g.ofLp i)

pp: case neg
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 = ∞
⊢ 0 ≤ (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
·

Goal state after:
case pos
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
⊢ 0 ≤ ↑⋯.toFinset.card
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✝
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
hf' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f)
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') ⇑f :=
  antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range f hf hf'
x : E
aux : ‖x‖ ≤ ↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') * ‖f x‖
⊢ ‖(↑f.rangeRestrict).leftInverse ⟨↑f x, ⋯⟩‖ ≤ ↑K * ‖⟨↑f x, ⋯⟩‖

Tactic:
convert! aux

Goal state after:
case e'_3.e'_3
𝕜 : 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✝
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
hf' : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Set.range ⇑f)
K : ℝ≥0 := f.antilipschitzConstant_of_injective_of_isClosed_range hf hf'
hfK : AntilipschitzWith (f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') ⇑f :=
  antilipschitz_antiLipschitzConstant_of_injective_of_isClosed_range f hf hf'
x : E
aux : ‖x‖ ≤ ↑(f.antilipschitzConstant_of_injective_of_isClosed_range hf hf') * ‖f x‖
⊢ (↑f.rangeRestrict).leftInverse ⟨↑f x, ⋯⟩ = x
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case pos
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 = ∞
⊢ 0 ≤ ⨆ i, dist (f.ofLp i) (g.ofLp i)

pp: case neg
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 = ∞
⊢ 0 ≤ (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
·

Goal state after:
case pos
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 = ∞
⊢ 0 ≤ ⨆ i, dist (f.ofLp i) (g.ofLp i)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case neg
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 = ∞
⊢ 0 ≤ (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)

Tactic:
·

Goal state after:
case neg
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 = ∞
⊢ 0 ≤ (∑ i, dist (f.ofLp i) (g.ofLp i) ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl
𝕜 : 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 : PiLp ∞ α
⊢ edist f g = ENNReal.ofReal (dist f g)

pp: case inr
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
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
·

Goal state after:
case inl
𝕜 : 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 : PiLp ∞ α
⊢ edist f g = ENNReal.ofReal (dist f g)
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ idemFst + idemSnd - idemFst = idemSnd

Tactic:
add_sub_cancel_left

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
p : ℝ≥0∞
⊢ idemSnd = idemSnd
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inl.inl
𝕜 : 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 : PiLp ∞ α
h✝ : IsEmpty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))

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 : PiLp ∞ α
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))

Tactic:
·

Goal state after:
case inl.inl
𝕜 : 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 : PiLp ∞ α
h✝ : IsEmpty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))
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 : PiLp ∞ α
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))

Tactic:
·

Goal state after:
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 : PiLp ∞ α
h✝ : Nonempty ι
⊢ ⨆ i, edist (f.ofLp i) (g.ofLp i) = ENNReal.ofReal (⨆ i, dist (f.ofLp i) (g.ofLp i))
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: case inr
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
⊢ edist f g = ENNReal.ofReal (dist f g)

Tactic:
·

Goal state after:
case inr
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
⊢ edist f g = ENNReal.ofReal (dist f g)
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case mp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f → Bijective ⇑f

pp: case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f

Tactic:
·

Goal state after:
case mp
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ IsUnit f → Bijective ⇑f
Module: Mathlib.Analysis.Normed.Operator.Banach

Goal state before:
pp: case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f

Tactic:
·

Goal state after:
case mpr
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : CompleteSpace E
f : E →L[𝕜] E
⊢ Bijective ⇑f → IsUnit f