mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
s : Set α
h : μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x
⊢ SFinite (sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable α
s : Set α
h : μ = sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x
⊢ SFinite (sum fun x ↦ μ (measurableAtom ↑x) • dirac ↑x)
Module: Mathlib.Data.Complex.Basic

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

Tactic:
]

Goal state after:
a b₁ b₂ : ℝ
⊢ (fun y ↦ ↑a + ↑y * I) '' [[b₁, b₂]] = ⇑equivRealProd ⁻¹' {a} ×ˢ [[b₁, b₂]]
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν ∂μ

pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1) * φ) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (a : α), (f * fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) a ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν ∂μ

case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ f z.1) * φ) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun x ↦ ∫⁻ (y : β), φ (x, y) ∂ν) μ
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), f x * φ (x, a) ∂ν = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
hf : AEMeasurable f μ
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), f x * φ (x, a) ∂ν = ∫⁻ (y : β), ((fun z ↦ f z.1) * φ) (x, y) ∂ν
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i ↦ f i) i ≤ #s • a

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, f x ≤ a
⊢ ∑ i ∈ s, (fun i ↦ f i) i ≤ #s • a
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν ∂μ

pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ g z.2) * φ) (μ.prod ν)

pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ ∫⁻ (x : α), ∫⁻ (y : β), φ (x, y) ∂ν.withDensity g ∂μ = ∫⁻ (x : α), ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν ∂μ

case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable ((fun z ↦ g z.2) * φ) (μ.prod ν)

α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), (g * fun y ↦ φ (x, y)) a ∂ν = ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
g : β → ℝ≥0∞
hg : AEMeasurable g ν
φ : α × β → ℝ≥0∞
hφ : Measurable φ
x : α
⊢ ∫⁻ (a : β), (g * fun y ↦ φ (x, y)) a ∂ν = ∫⁻ (y : β), ((fun z ↦ g z.2) * φ) (x, y) ∂ν
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun i ↦ f i) i

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
a : α
hs : s.Nonempty
h : ∀ x ∈ s, a ≤ f x
⊢ #s • a ≤ ∑ i ∈ s, (fun i ↦ f i) i
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ (μ.prod ν).withDensity ((fun z ↦ f z.1) * fun z ↦ g z.2) = (μ.prod ν).withDensity fun z ↦ f z.1 * g z.2

pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)

pp: case hg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ (μ.prod ν).withDensity ((fun z ↦ f z.1) * fun z ↦ g z.2) = (μ.prod ν).withDensity fun z ↦ f z.1 * g z.2

case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ g z.2) (μ.prod ν)

case hg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝ : SFinite ν
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ AEMeasurable (fun z ↦ f z.1) (μ.prod ν)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ c • ∫⁻ (a : α), ν (Prod.mk a ⁻¹' s) ∂μ = c • ∫⁻ (x : α), ν (Prod.mk x ⁻¹' s) ∂μ

pp: case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)

Tactic:
]

Goal state after:
case hf
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
mβ : MeasurableSpace β
ν : Measure β
inst✝² : SFinite ν
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
s : Set (α × β)
hs : MeasurableSet s
A : ∀ (s : Set β), c • ν s = c • 1 * ν s
⊢ Measurable fun x ↦ ν (Prod.mk x ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ∞
hUf : U ⊆ {x_1 | (fun a ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, ↑(f a) ∂μ < ∞

Tactic:
]

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : OpensMeasurableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : α → ℝ≥0
hf : Continuous f
x : α
U : Set α
hμU : μ U < ∞
hUf : U ⊆ {x_1 | (fun a ↦ f a ≤ f x + 1) x_1}
hUx : U ∈ nhds x
hUo : IsOpen U
⊢ ∫⁻ (a : α) in U, ↑(f a) ∂μ < ∞
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: M : Type u_2
inst✝² : Monoid M
inst✝¹ : MeasurableSpace M
μ ν : Measure M
inst✝ : SFinite ν
s : ℝ≥0∞
⊢ s • map (fun x ↦ x.1 * x.2) (μ.prod ν) = s • map (fun x ↦ x.1 * x.2) (μ.prod ν)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, f x ≤ a
hlt : ∃ x ∈ s, f x < a
⊢ 𝔼 i ∈ s, f i < 𝔼 _i ∈ s, a

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, f x ≤ a
hlt : ∃ x ∈ s, f x < a
⊢ 𝔼 i ∈ s, f i < 𝔼 _i ∈ s, a
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, a ≤ f x
hlt : ∃ x ∈ s, a < f x
⊢ 𝔼 _i ∈ s, a < 𝔼 i ∈ s, f i

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
s : Finset ι
f : ι → α
a : α
hle : ∀ x ∈ s, a ≤ f x
hlt : ∃ x ∈ s, a < f x
⊢ 𝔼 _i ∈ s, a < 𝔼 i ∈ s, f i
Module: Mathlib.MeasureTheory.Measure.WithDensity

Goal state before:
pp: G : Type u_3
inst✝⁴ : Group G
mG : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
f g : G → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
φ : G → ℝ≥0∞
hφ : Measurable φ
x : G
⊢ ∫⁻ (y : G), ((fun z ↦ f z.1 * g z.2) * fun z ↦ φ (z.1 * z.2)) (x, y) ∂μ = ?m.96 x

Tactic:
apply (lintegral_mul_left_eq_self _ x⁻¹).symm

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : a ≤ 𝔼 i ∈ s, f i
⊢ a ≤ 𝔼 i ∈ s, f i

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : a ≤ 𝔼 i ∈ s, f i
⊢ a ≤ 𝔼 i ∈ s, f i
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : 𝔼 i ∈ s, f i ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedCancelAddMonoid α
inst✝¹ : Module ℚ≥0 α
inst✝ : PosSMulStrictMono ℚ≥0 α
a : α
s : Finset ι
f : ι → α
hs : s.Nonempty
h : 𝔼 i ∈ s, f i ≤ a
⊢ 𝔼 i ∈ s, f i ≤ a
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : 0 ≤ f
⊢ (∀ i ∈ univ, f i = 0) ↔ f = 0

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : 0 ≤ f
⊢ (∀ i ∈ univ, f i = 0) ↔ f = 0
Module: Mathlib.Algebra.Order.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ (∀ i ∈ univ, f i = 0) ↔ f = 0

Tactic:
]

Goal state after:
ι : Type u_1
α : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : AddCommMonoid α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Module ℚ≥0 α
f : ι → α
hf : f ≤ 0
⊢ (∀ i ∈ univ, f i = 0) ↔ f = 0
Module: Mathlib.Algebra.Star.MonoidHom

Goal state before:
pp: 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
e₁ : A ≃⋆* B
e₂ : B ≃⋆* C
a : A
⊢ star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f g : NormedAddGroupHom V₁ V₂
h : f.toAddMonoidHom = g.toAddMonoidHom
⊢ ⇑g.toAddMonoidHom = ⇑g.toAddMonoidHom

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: case pos
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ 0
h : ‖x‖ = 0
⊢ ‖f x‖ ≤ 0

Tactic:
]

Goal state after:
case pos
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x : V₁
C : ℝ
_Cpos : 0 < C
hC : ‖f x‖ ≤ 0
h : ‖x‖ = 0
⊢ ‖f x‖ ≤ 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖f (x - y)‖ ≤ ↑⟨‖f‖, ⋯⟩ * ‖x - y‖

Tactic:
]

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖f (x - y)‖ ≤ ↑⟨‖f‖, ⋯⟩ * ‖x - y‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖ = ‖f‖ * ‖v‖ + ‖g‖ * ‖v‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0

Tactic:
]

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
x✝ : V₁
⊢ ‖0 x✝‖ = 0
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hn : ‖f‖ = 0
x : V₁
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_5
V₂ : Type u_6
inst✝¹ : NormedAddCommGroup V₁
inst✝ : NormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
hf : f = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
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 : 1 ≤ ‖id V‖
⊢ 1 ≤ ‖id V‖

Tactic:
]

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: 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₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖

Tactic:
]

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * b * ‖x‖
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * (b * ‖x‖)

Tactic:
]

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝¹¹ : SeminormedAddCommGroup V
inst✝¹⁰ : SeminormedAddCommGroup V₁
inst✝⁹ : SeminormedAddCommGroup V₂
inst✝⁸ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
R : Type u_5
R' : Type u_6
inst✝⁷ : MonoidWithZero R
inst✝⁶ : DistribMulAction R V₂
inst✝⁵ : PseudoMetricSpace R
inst✝⁴ : IsBoundedSMul R V₂
inst✝³ : MonoidWithZero R'
inst✝² : DistribMulAction R' V₂
inst✝¹ : PseudoMetricSpace R'
inst✝ : IsBoundedSMul R' V₂
r : R
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
x : V₁
this : ‖r • f x‖ ≤ dist r 0 * ‖f x‖
⊢ ‖(r • ⇑f) x‖ ≤ dist r 0 * (b * ‖x‖)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖n • f v‖ ≤ ↑n * (b * ‖v‖)

Tactic:
]

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
n : ℕ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖n • f v‖ ≤ ↑n * (b * ‖v‖)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z • f v‖ ≤ ‖z‖ * (b * ‖v‖)

Tactic:
]

Goal state after:
V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g : NormedAddGroupHom V₁ V₂
z : ℤ
f : NormedAddGroupHom V₁ V₂
b : ℝ
hb : ∀ (v : V₁), ‖f.toFun v‖ ≤ b * ‖v‖
v : V₁
⊢ ‖z • f v‖ ≤ ‖z‖ * (b * ‖v‖)
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V : Type u_1
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
f : NormedAddGroupHom V₁ V₂
v : V₁
⊢ ‖g‖ * (‖f‖ * ‖v‖) = ‖g‖ * (‖f‖ * ‖v‖)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ : ℝ
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g‖ * ‖f‖ ≤ C₂ * C₁

Tactic:
by gcongr; exact le_trans (norm_nonneg _) hg

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Hom

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₂ * C₁

Tactic:
]

Goal state after:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
C₁ C₂ C₃ : ℝ
h : C₃ = C₂ * C₁
hg : ‖g‖ ≤ C₂
hf : ‖f‖ ≤ C₁
⊢ ‖g.comp f‖ ≤ C₂ * C₁
Module: Mathlib.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U B : R
x✝¹ : U ∈ {U | star U * U = 1 ∧ U * star U = 1}
x✝ : B ∈ {U | star U * U = 1 ∧ U * star U = 1}
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ star B * star U * U * B = star B * star U * U * B

Tactic:
]

Goal state after: