mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
⊢ (∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b

Tactic:
← Finset.prod_sdiff ht₁,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
h✝ : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
d : Set α
hd : d ∈ 𝓝 1
hde : ∀ v ∈ d, ∀ w ∈ d, v / w ∈ e
s : Finset β
h : ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ d
t₁ t₂ : Finset β
ht₁ : (s, s).1 ⊆ (t₁, t₂).1
ht₂ : (s, s).2 ⊆ (t₁, t₂).2
⊢ (∏ b ∈ t₂, f b) / ((∏ x ∈ (t₁, t₂).1 \ (s, s).1, f x) * ∏ x ∈ (s, s).1, f x) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a a' : α
hf : HasProd f a L
b : β
x : α
hf' : HasProd (update f b x) a' L
⊢ a * x = a' * f b

Tactic:
by
  have : ∀ b', f b' * ite (b' = b) x 1 = update f b x b' * ite (b' = b) (f b) 1 := by
    intro b'
    split_ifs with hb'
    · simpa only [Function.update_apply, hb', eq_self_iff_true] using! mul_comm (f b) x
    · simp only [Function.update_apply, hb', if_false]
  have h := hf.mul (hasProd_ite_eq b x L)
  simp_rw [this] at h
  exact HasProd.unique h (hf'.mul (hasProd_ite_eq b (f b) L))

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
g : γ → β
hg : Injective g
f : β → α
hf : mulSupport f ⊆ Set.range g
this : mulSupport f = g '' mulSupport (f ∘ g)
hf_fin : ¬(mulSupport f).Finite
⊢ tprod (f ∘ g) = ∏' (b : β), f b

Tactic:
· have hf_fin' : ¬ Set.Finite (mulSupport (f ∘ g)) := by
      rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
    simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
      show (unconditional β).HasSupport by infer_instance,
      show (unconditional γ).HasSupport by infer_instance, true_and,
      if_neg hf_fin, if_neg hf_fin', Multipliable]
    simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]

Goal state after:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: ⊢ Filter.map Real.toNNReal atTop = atTop

Tactic:
← map_coe_atTop,

Goal state after:
⊢ Filter.map Real.toNNReal (Filter.map toReal atTop) = atTop
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inl
α : Type u_2
L : SummationFilter α
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
h✝ : L.NeBot
y : ℝ≥0
hy : HasSum f (↑y) L
⊢ HasSum (fun x ↦ (f x).toNNReal) (↑y).toNNReal L

Tactic:
lift f to α → ℝ≥0 using hf₀

Goal state after:
case inl
α : Type u_2
L : SummationFilter α
h✝ : L.NeBot
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i ↦ ↑(f i)) (↑y) L
⊢ HasSum (fun x ↦ ((fun i ↦ ↑(f i)) x).toNNReal) (↑y).toNNReal L
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h :
  ∀ (f : X → Prop) (a : X), (∀ (u : ℕ → X), Tendsto u atTop (𝓝 a) → Tendsto (f ∘ u) atTop (𝓝 (f a))) → ContinuousAt f a
⊢ FrechetUrysohnSpace X

Tactic:
refine ⟨fun s x hcx => ?_⟩
  by_cases hx : x ∈ s
  · exact subset_seqClosure hx
  · obtain ⟨u, hux, hus⟩ : ∃ u : ℕ → X, Tendsto u atTop (𝓝 x) ∧ ∃ᶠ x in atTop, u x ∈ s := by
      simpa only [ContinuousAt, hx, tendsto_nhds_true, (· ∘ ·), ← not_frequently, exists_prop,
        ← mem_closure_iff_frequently, hcx, imp_false, not_forall, not_not, not_false_eq_true,
        not_true_eq_false] using h (· ∉ s) x
    rcases extraction_of_frequently_atTop hus with ⟨φ, φ_mono, hφ⟩
    exact ⟨u ∘ φ, hφ, hux.comp φ_mono.tendsto_atTop⟩

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : s ∈ l
this✝ : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
this : ∀ (n : ℕ), W n ∩ s ×ˢ s ∈ l ×ˢ l
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s

Tactic:
simpa only [l.basis_sets.prod_self.mem_iff, true_imp_iff, subset_inter_iff,
        prod_self_subset_prod_self, and_assoc] using! this

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

Goal state before:
pp: ι : Type u_2
κ : Type u_3
G : Type u_6
inst✝ : SeminormedGroup G
f : ι → κ → G
s : Set κ
l : Filter ι
⊢ TendstoUniformlyOn f 1 l s ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ s, ‖f i x‖ < ε

Tactic:
simp only [tendstoUniformlyOn_iff, Pi.one_apply, dist_one_left]

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

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n

Tactic:
have lim_z : Tendsto z atTop (𝓝 a) := lim_u.comp (tendsto_add_atTop_nat n₀)

Goal state after:
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
⊢ ∃ v,
    Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a) ∧
      (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case mp
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
⊢ Nonempty α

Tactic:
have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c

Goal state after:
case mp
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
⊢ Nonempty α
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
refine ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, ?_, ?_⟩

Goal state after:
case inr.refine_1
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)

case inr.refine_2
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x ↦ max (f x) a

Tactic:
by
  simpa using hf.max (LipschitzWith.const a)

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ limsup (f + g) u = limsup f u

Tactic:
by
  refine le_antisymm ?_ <| limsup_le_limsup <| .of_forall <| by simp
  refine le_limsup_of_le (by isBoundedDefault) fun b hb ↦ ?_
  rw [Filter.limsup_le_iff']
  rintro a hba
  filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| tsub_pos_of_lt hba] with i hf hg
  calc f i + g i
    _ ≤ b + g i := by gcongr
    _ ≤ a := add_le_of_le_tsub_left_of_le hba.le hg

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖

Tactic:
rwa [norm_pow]

Goal state after:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
p : β
⊢ dist p (s • x) ≤ ‖s‖ * ε → ∃ x_1, dist x_1 x ≤ ε ∧ s • x_1 = p

Tactic:
refine fun h ↦ ⟨s⁻¹ • p, ?_, by simp [smul_smul, hs]⟩
    refine le_of_mul_le_mul_of_pos_left ?_ (norm_pos_iff.mpr hs)
    rw [← dist_smul₀]
    simpa [smul_smul, hs] using h

Goal state after:
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : NormSMulClass α β
s : α
hs : s ≠ 0
x : β
ε : ℝ
⊢ (fun x ↦ s • x) '' sphere x ε = sphere (s • x) (‖s‖ * ε)

Tactic:
by
  simp_rw [← Metric.closedBall_sdiff_ball, Set.image_sdiff (smul_right_injective β hs),
    smul_image_ball hs, smul_image_closedBall hs]

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet s

Tactic:
← insert_eq_of_mem ha

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α
s : Set α
h : MeasurableSet (insert a s)
ha : a ∈ s
⊢ MeasurableSet (insert a s)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ k = 0 ↔ k = 0 ∨ e = 0

Tactic:
or_iff_left he

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ k = 0 ↔ k = 0
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜 : Type u_1
𝕜' : Type u_2
E : Type u_3
F : Type u_4
α : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace 𝕜 F
s : 𝕜
x : E × F
⊢ ‖s • x‖ ≤ ‖s‖ * ‖x‖

Tactic:
simp only [norm_smul, Prod.norm_def, le_rfl]

Goal state after:
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0

Tactic:
simp [union_eq_iUnion, and_comm]

Goal state after:
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ s ^ (2 * k) * s = s

Tactic:
zpow_mul,

Goal state after:
case inr
s : SignType
hs : s ≠ 0
k : ℤ
⊢ (s ^ 2) ^ k * s = s
Module: Mathlib.Topology.Algebra.Algebra

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : s.topologicalClosure = ⊤
⊢ (map (↑f) s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
A : Type u_2
inst✝⁷ : Semiring A
inst✝⁶ : TopologicalSpace A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : IsSemitopologicalSemiring A
inst✝ : IsSemitopologicalSemiring B
f : A →A[R] B
hf' : DenseRange ⇑f
s : Subalgebra R A
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(map (↑f) s).topologicalClosure = ↑⊤
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ ∑ i ∈ s, f i + ∑' (i : ↑(↑s)ᶜ), f ↑i = ∑' (i : ι), f i

Tactic:
rw [tsum_subtype, sum_eq_tsum_indicator]
  simp [← ENNReal.tsum_add]

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

Goal state before:
pp: f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum f r ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)

Tactic:
← ENNReal.hasSum_coe,

Goal state after:
f : ℕ → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun a ↦ ↑(f a)) ↑r ↔ Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -(↑a✝)⁻¹

Tactic:
rw [← coe_inv _, ← coe_neg _⁻¹, ← coe_neg _, ← coe_inv (-_)]

Goal state after:
case coe
a✝ : ℝ
⊢ ↑(-a✝)⁻¹ = ↑(-a✝⁻¹)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha

Goal state after:
a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
by_cases h' : x' ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∈ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsOpen[inst✝²] s
hy : 0 ≤ y
x : α
z : β
h : x ∉ s
hz : z < 0
x' : α
h' : x' ∉ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
by_cases h' : x' ∈ s

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∈ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
h' : x' ∉ s
⊢ (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case refine_2
r : ℝ≥0∞
⊢ 1 < r → Tendsto (fun n ↦ r ^ n) atTop (𝓝 ∞)

Tactic:
· intro r_gt_one
    have obs := @Tendsto.inv ℝ≥0∞ ℕ _ _ _ (fun n ↦ (r⁻¹) ^ n) atTop 0
    simp only [ENNReal.tendsto_pow_atTop_nhds_zero_iff, inv_zero] at obs
    simpa [← ENNReal.inv_pow] using obs <| ENNReal.inv_lt_one.mpr r_gt_one

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

Goal state before:
pp: ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε

Tactic:
rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩

Goal state after:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst✝ : Countable ι
x : ℝ≥0
right✝ : ↑x < ε
h0r : 0 < ↑x
hrε : ↑x < ε
⊢ ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ↑(ε' i) < ε
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
⊢ f ⁻¹' v ∈ 𝓝[s] x

Tactic:
filter_upwards [h₂ u fxu] with a lfa

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f : α → γ
h₁ : LowerSemicontinuousWithinAt f s x
h₂ : UpperSemicontinuousWithinAt f s x
v : Set γ
hv : v ∈ 𝓝 (f x)
Hl : ∀ (l : γ), f x ≤ l
Hu : ∃ u, f x < u
u : γ
fxu : f x < u
hu : Ico (f x) u ⊆ v
a : α
lfa : f a < u
⊢ a ∈ f ⁻¹' v
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
n : ℕ
h : ∀ i < n + 1, m.IsCaratheodory (s i)
⊢ m.IsCaratheodory (⋃ i, ⋃ (_ : i < n + 1), s i)

Tactic:
by
    rw [biUnion_lt_succ]
    exact isCaratheodory_union m
            (isCaratheodory_iUnion_lt fun i hi => h i <| lt_of_lt_of_le hi <| Nat.le_succ _)
            (h n (le_refl (n + 1)))

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ d.Has (tᶜ ∩ s)

Tactic:
simp_rw [this]

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
t : Set α
hts : d.Has (t ∩ s)
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ d.Has ((t ∩ s)ᶜ \ sᶜ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : β → γ
e : α ≃ᵐ β
hfe : Measurable (f ∘ ⇑e)
this : Measurable (f ∘ ⇑(e.symm.trans e).toEquiv)
⊢ Measurable f

Tactic:
rwa [coe_toEquiv, symm_trans_self] at this

Goal state after:
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ univ ⊆ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

Tactic:
rintro ⟨a | b, c⟩

Goal state after:
case inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
a : α
⊢ (Sum.inl a, c) ∈ univ → (Sum.inl a, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ

case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α✝
inst✝⁵ : MeasurableSpace α✝
inst✝⁴ : MeasurableSpace β✝
inst✝³ : MeasurableSpace γ✝
α : Type ?u.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
c : γ
b : β
⊢ (Sum.inr b, c) ∈ univ → (Sum.inr b, c) ∈ range Sum.inl ×ˢ univ ∪ range Sum.inr ×ˢ univ
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ (s ∪ t) u ↔ AEDisjoint μ s u ∧ AEDisjoint μ t u

Tactic:
simp [union_eq_iUnion, and_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.AEDisjoint

Goal state before:
pp: α : Type u_2
m : MeasurableSpace α
μ : Measure α
s t u : Set α
⊢ AEDisjoint μ s (t ∪ u) ↔ AEDisjoint μ s t ∧ AEDisjoint μ s u

Tactic:
simp [union_eq_iUnion, and_comm]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.NullMeasurable

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

Tactic:
have : Prod.snd ⁻¹' {y} = ⋃ x : α, {(x, y)} := by ext y; simp [Prod.ext_iff, eq_comm]

Goal state after:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Countable α
μ : Measure (α × β)
y : β
this : Prod.snd ⁻¹' {y} = ⋃ x, {(x, y)}
⊢ μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ

pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : ¬AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ

Tactic:
· have hfc : AEMeasurable f (c • μ) :=
      ⟨hf.mk f, hf.measurable_mk, (ae_ennreal_smul_measure_iff hc).2 hf.ae_eq_mk⟩
    simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hfc, map_smulₛₗ,
      RingHom.id_apply]
    congr 1
    apply mapₗ_congr hfc.measurable_mk hf.measurable_mk
    exact .trans ((ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk.symm) hf.ae_eq_mk

Goal state after:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : ¬AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ
Module: Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
μ₁ μ₂ ν ν' : Measure α
h1 : μ₁ ≪ ν
h2 : μ₂ ≪ ν'
⊢ μ₁ + μ₂ ≪ ν + ν'

Tactic:
intro s hs
  simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢
  exact ⟨h1 hs.1, h2 hs.2⟩

Goal state after:
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) = μ (⋃ i, t i)

Tactic:
refine le_antisymm (by gcongr; apply hsub) ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, t i) ≤ μ (⋃ i, s i)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
γ : Type u_5
f g : α → γ
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hs_zero : μ s = 0
⊢ (fun x ↦ if x ∈ s then f x else g x) =ᵐ[μ] g

Tactic:
have h_ss : sᶜ ⊆ { a : α | ite (a ∈ s) (f a) (g a) = g a } := fun x hx => by
    simp [(Set.mem_compl_iff _ _).mp hx]
  refine measure_mono_null ?_ hs_zero
  conv_rhs => rw [← compl_compl s]
  rwa [Set.compl_subset_compl]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ univ = 0

Tactic:
← hU

Goal state after:
α : Type u_1
ι : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
U : ι → Set α
hU : ⋃ i, U i = univ
H : ∀ (i : ι), μ (U i) ≤ 0
⊢ μ (⋃ i, U i) = 0