mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
U : Set E
hU : IsOpen U ∧ U ∩ ↑L = {0}
⊢ IsClosed (↑L \ {0})

pp: E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
⊢ ∃ U, IsOpen U ∧ U ∩ ↑L = {0}

Tactic:
·

Goal state after:
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
U : Set E
hU : IsOpen U ∧ U ∩ ↑L = {0}
⊢ IsClosed (↑L \ {0})
Module: Mathlib.MeasureTheory.Function.UnifTight

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : μ Eg < ∞
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : μ Ef < ∞
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : μ E < ∞
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun n ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (μ E < ∞)
hInner : ∀ ε > 0, ∃ N, ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
⊢ eLpNorm (Eᶜ.indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ

Tactic:
unfold E; rw [compl_union, inter_comm, ← indicator_indicator]

Goal state after:
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_1
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ Z (n + 1) ⊆ Z n

pp: case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ (Z n).Nonempty

Tactic:
·

Goal state after:
case refine_1
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ Z (n + 1) ⊆ Z n
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ (Z n).Nonempty

Tactic:
·

Goal state after:
case refine_2
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ (Z n).Nonempty
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case hinf
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ μ s ≠ ∞

pp: case bc
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal ((1 + ↑(u n)) ^ finrank ℝ E)

Tactic:
·

Goal state after:
case hinf
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯
K : ConvexBody E := ⋯
S : ℕ → ConvexBody E := ⋯
Z : ℕ → Set E := ⋯
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ μ s ≠ ∞
Module: Mathlib.MeasureTheory.Group.GeometryOfNumbers

Goal state before:
pp: case bc
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal (1 + ↑(u n)) ^ finrank ℝ E

Tactic:
refine one_lt_pow₀ ?_ (ne_of_gt finrank_pos)

Goal state after:
case bc
E : Type u_1
inst✝⁸ : MeasurableSpace E
μ : Measure E
F s : Set E
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : BorelSpace E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : Nontrivial E
inst✝² : μ.IsAddHaarMeasure
L : AddSubgroup E
inst✝¹ : Countable ↥L
inst✝ : DiscreteTopology ↥L
fund : IsAddFundamentalDomain (↥L) F μ
h_symm : ∀ x ∈ s, -x ∈ s
h_conv : Convex ℝ s
h_cpt : IsCompact s
h : μ F * 2 ^ finrank ℝ E ≤ μ s
h_mes : μ s ≠ 0
h_nemp : s.Nonempty
u : ℕ → ℝ≥0 := ⋯.choose
K : ConvexBody E := { carrier := s, convex' := h_conv, isCompact' := h_cpt, nonempty' := h_nemp }
S : ℕ → ConvexBody E := fun n ↦ (1 + u n) • K
Z : ℕ → Set E := fun n ↦ ↑(S n) ∩ (↑L \ {0})
h_zero : 0 ∈ K
h_clos : IsClosed (↑L \ {0})
n : ℕ
⊢ 1 < ENNReal.ofReal (1 + ↑(u n))
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : g 0 = 0
⊢ HasCompactSupport (g.comp ↑f).toFun

pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬g 0 = 0
⊢ HasCompactSupport (ContinuousMap.toFun 0)

Tactic:
·

Goal state after:
case pos
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : g 0 = 0
⊢ HasCompactSupport (g.comp ↑f).toFun
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬g 0 = 0
⊢ HasCompactSupport (ContinuousMap.toFun 0)

Tactic:
·

Goal state after:
case neg
F : Type u_1
α : Type u_2
β : Type u_3
γ✝ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : Zero β
γ : Type u_5
inst✝¹ : TopologicalSpace γ
inst✝ : Zero γ
g : C(β, γ)
f : α →C_c β
hg : ¬g 0 = 0
⊢ HasCompactSupport (ContinuousMap.toFun 0)
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun

pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ?refine_1 } = f₂

Tactic:
·

Goal state after:
case refine_1
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ HasCompactSupport (f₂.toContinuousMap - f₁.toContinuousMap).toFun
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ } = f₂

Tactic:
·

Goal state after:
case refine_2
α : Type u_2
inst✝ : TopologicalSpace α
f₁ f₂ : α →C_c ℝ≥0
h : f₁ ≤ f₂
⊢ f₁ + { toContinuousMap := f₂.toContinuousMap - f₁.toContinuousMap, hasCompactSupport' := ⋯ } = f₂
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = a * max (f x) 0

pp: case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = a * max (f x) 0

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = a * max (f x) 0
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = a * max (f x) 0

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : 0 ≤ a
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = a * max (f x) 0
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

pp: case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

Tactic:
·

Goal state after:
case inl
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : 0 ≤ f x
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0

Tactic:
·

Goal state after:
case inr
α : Type u_2
inst✝ : TopologicalSpace α
f : α →C_c ℝ
a : ℝ
ha : a ≤ 0
x : α
hfx : f x ≤ 0
⊢ max (a * f x) 0 = max (-a) 0 * max (-f x) 0
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : 0 ≤ a
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

Tactic:
·

Goal state after:
case inl
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : 0 ≤ a
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < b

pp: case hx
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 ≤ b

pp: p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ 0 < p

Tactic:
·

Goal state after:
p q b : ℝ
hp : 0 < p
hq : -1 < q
hb : 0 < b
⊢ b ^ (p⁻¹ * -1 + -p⁻¹ * q) * (1 / p * Gamma ((q + 1) / p)) = b ^ (-(q + 1) / p) * (1 / p * Gamma ((q + 1) / p))
Module: Mathlib.Topology.ContinuousMap.CompactlySupported

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))

Tactic:
·

Goal state after:
case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : TopologicalSpace α
Λ : (α →C_c ℝ≥0) →ₗ[ℝ≥0] ℝ≥0
a : ℝ
f : α →C_c ℝ
ha : a ≤ 0
⊢ ↑(Λ (a • f).nnrealPart) - ↑(Λ (-(a • f)).nnrealPart) = (RingHom.id ℝ) a • (↑(Λ f.nnrealPart) - ↑(Λ (-f).nnrealPart))
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_2
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-x ^ p)

pp: case e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)

Tactic:
·

Goal state after:
case e'_2
p : ℝ
hp : 0 < p
⊢ ∫ (x : ℝ) in Ioi 0, rexp (-x ^ p) = ∫ (x : ℝ) in Ioi 0, x ^ 0 * rexp (-x ^ p)
Module: Mathlib.MeasureTheory.Integral.Gamma

Goal state before:
pp: case e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)

Tactic:
·

Goal state after:
case e'_3
p : ℝ
hp : 0 < p
⊢ Gamma (1 / p + 1) = 1 / p * Gamma ((0 + 1) / p)
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ (x : ι), Measurable ((As x).indicator 1)

pp: case refine_2
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, (As n).indicator 1 a ≤ B.indicator 1 a

pp: case refine_3
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

pp: case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ (x : ι), Measurable ((As x).indicator 1)
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, (As n).indicator 1 a ≤ B.indicator 1 a

pp: case refine_3
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

pp: case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᶠ (n : ι) in L, ∀ᵐ (a : α) ∂μ, (As n).indicator 1 a ≤ B.indicator 1 a
Module: Mathlib.MeasureTheory.Integral.Indicator

Goal state before:
pp: case refine_3
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞

pp: case refine_4
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ (As n).indicator 1 a) L (𝓝 (A.indicator 1 a))

Tactic:
·

Goal state after:
case refine_3
α : Type u_1
inst✝¹ : MeasurableSpace α
A : Set α
ι : Type u_2
L : Filter ι
inst✝ : L.IsCountablyGenerated
As : ι → Set α
μ : Measure α
A_mble : MeasurableSet A
As_mble : ∀ (i : ι), MeasurableSet (As i)
B : Set α
B_mble : MeasurableSet B
B_finmeas : μ B ≠ ∞
As_le_B : ∀ᶠ (i : ι) in L, As i ⊆ B
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ ∫⁻ (a : α), B.indicator 1 a ∂μ ≠ ∞