mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
⊢ y < x → y < limsup u f

Tactic:
y_x

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
y_x : y < x
⊢ y < limsup u f
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
⊢ atTop = ⨅ x, 𝓟 (Ici {x})

Tactic:
refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_
  refine
    le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_
  simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici,
    Finset.mem_singleton, Finset.subset_iff, forall_eq]
  exact fun t => id

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
⊢ y < x → y < limsup u f

Tactic:
y_x

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
y_x : y < x
⊢ y < limsup u f
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: γ : Type u_3
β : Type u_4
f : γ ↪ β
⊢ { filter := Filter.map (fun s ↦ s.preimage ⇑f ⋯) atTop } = { filter := atTop }

Tactic:
congr 1 with s

Goal state after:
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
⊢ s ∈ Filter.map (fun s ↦ s.preimage ⇑f ⋯) atTop ↔ s ∈ atTop
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case bot
y : EReal
hx : 0 ≤ ⊥
⊢ (⊥ * y).toENNReal = ⊥.toENNReal * y.toENNReal

Tactic:
induction y

Goal state after:
case bot.bot
hx : 0 ≤ ⊥
⊢ (⊥ * ⊥).toENNReal = ⊥.toENNReal * ⊥.toENNReal

case bot.coe
hx : 0 ≤ ⊥
a✝ : ℝ
⊢ (⊥ * ↑a✝).toENNReal = ⊥.toENNReal * (↑a✝).toENNReal

case bot.top
hx : 0 ≤ ⊥
⊢ (⊥ * ⊤).toENNReal = ⊥.toENNReal * ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * y).toENNReal = (↑a✝).toENNReal * y.toENNReal

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊥).toENNReal = (↑a✝).toENNReal * ⊥.toENNReal

case coe.coe
a✝¹ : ℝ
hx : 0 ≤ ↑a✝¹
a✝ : ℝ
⊢ (↑a✝¹ * ↑a✝).toENNReal = (↑a✝¹).toENNReal * (↑a✝).toENNReal

case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top
y : EReal
hx : 0 ≤ ⊤
⊢ (⊤ * y).toENNReal = ⊤.toENNReal * y.toENNReal

Tactic:
induction y

Goal state after:
case top.bot
hx : 0 ≤ ⊤
⊢ (⊤ * ⊥).toENNReal = ⊤.toENNReal * ⊥.toENNReal

case top.coe
hx : 0 ≤ ⊤
a✝ : ℝ
⊢ (⊤ * ↑a✝).toENNReal = ⊤.toENNReal * (↑a✝).toENNReal

case top.top
hx : 0 ≤ ⊤
⊢ (⊤ * ⊤).toENNReal = ⊤.toENNReal * ⊤.toENNReal
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : CommGroup α
inst✝¹ : IsUniformGroup α
f : β → α
inst✝ : CompleteSpace α
i : γ → β
hf : Multipliable f
hi : Injective i
⊢ Multipliable (f ∘ i)

Tactic:
simpa only [Set.mulIndicator_range_comp] using
    (hi.multipliable_iff (fun x hx ↦ Set.mulIndicator_of_notMem hx _)).2
    (hf.mulIndicator (Set.range i))

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) = (∏ i ∈ s, g i) * ∏ i ∈ t \ s, g i

Tactic:
rw [← mul_div_assoc, ← div_mul_eq_mul_div, ← div_mul_eq_mul_div, div_self, one_mul, mul_comm]

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ ∏ i ∈ s, f i ≠ 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
⊢ Summable (fun i ↦ a / f i) L ↔ Summable (1 / f) L

Tactic:
simpa only [div_eq_mul_inv, one_mul] using! summable_mul_left_iff h

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
hf : ¬Multipliable f
⊢ ∏' (i : ι), f i ∈ s

Tactic:
simp [tprod_eq_one_of_not_multipliable hf, one_mem]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : TopologicalSpace α
L : SummationFilter β
inst✝¹ : Nonempty β
inst✝ : L.LeAtTop
⊢ HasProd (fun x ↦ 0) 0 L

Tactic:
obtain ⟨b⟩ := ‹Nonempty β›
  exact hasProd_zero_of_exists_eq_zero ⟨b, by simp⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (atTop ×ˢ atTop) (𝓝 (a * b))

Tactic:
convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))

Goal state after:
case e'_3
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ (fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm =
    (fun p ↦ p.1 * p.2) ∘ Prod.map (fun s ↦ ∏ b ∈ s, (f ∘ Sum.inl) b) fun s ↦ ∏ b ∈ s, (f ∘ Sum.inr) b
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ 0 ∨ b ≠ ∞
hb : b ≠ 0 ∨ a ≠ ∞
⊢ Tendsto (fun p ↦ p.1 * p.2) (𝓝 (a, b)) (𝓝 (a * b))

Tactic:
have ht : ∀ b : ℝ≥0∞, b ≠ 0 →
      Tendsto (fun p : ℝ≥0∞ × ℝ≥0∞ => p.1 * p.2) (𝓝 (∞, b)) (𝓝 ∞) := fun b hb => by
    refine tendsto_nhds_top_iff_nnreal.2 fun n => ?_
    rcases lt_iff_exists_nnreal_btwn.1 (pos_iff_ne_zero.2 hb) with ⟨ε, hε, hεb⟩
    have : ∀ᶠ c : ℝ≥0∞ × ℝ≥0∞ in 𝓝 (∞, b), ↑n / ↑ε < c.1 ∧ ↑ε < c.2 :=
      (lt_mem_nhds <| div_lt_top coe_ne_top hε.ne').prod_nhds (lt_mem_nhds hεb)
    refine this.mono fun c hc => ?_
    exact (ENNReal.div_mul_cancel hε.ne' coe_ne_top).symm.trans_lt (mul_lt_mul hc.1 hc.2)
  induction a with
  | top => simp only [ne_eq, or_false, not_true_eq_false] at hb; simp [ht b hb, top_mul hb]
  | coe a =>
    induction b with
    | top =>
      simp only [ne_eq, or_false, not_true_eq_false] at ha
      simpa [Function.comp_def, mul_comm, mul_top ha]
        using (ht a ha).comp (continuous_swap.tendsto (ofNNReal a, ∞))
    | coe b =>
      simp only [nhds_coe_coe, ← coe_mul, tendsto_coe, tendsto_map'_iff, Function.comp_def,
        tendsto_mul]

Goal state after:
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: M : Type u
G : Type v
X : Type w
Y : Type u_1
inst✝³ : PseudoEMetricSpace X
inst✝² : PseudoEMetricSpace Y
inst✝¹ : SMul M X
inst✝ : IsIsometricSMul M X
c : ULift.{u_2, u} M
⊢ Isometry fun x ↦ c • x

Tactic:
simpa only using! isometry_smul X c.down

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖b⁻¹‖ = ‖b‖

Tactic:
norm_inv'

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖b‖ = ‖b‖
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
a b c : E
⊢ dist a (b / c) = dist (a * c) b

Tactic:
by
  rw [← dist_mul_right _ _ c, div_mul_cancel]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

Goal state before:
pp: case inl
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
f : ι → G₀
⊢ ∅.sup f / a = ∅.sup fun i ↦ f i / a

pp: case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i ↦ f i / a

Tactic:
· simp [bot_eq_zero]

Goal state after:
case inr
ι : Type u_1
G₀ : Type u_3
inst✝ : LinearOrderedCommGroupWithZero G₀
a : G₀
ha : 0 ≤ a
s : Finset ι
f : ι → G₀
hs : s.Nonempty
⊢ s.sup f / a = s.sup fun i ↦ f i / a
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
⊢ A * ‖f i‖ * ‖g i‖ < ε

Tactic:
rcases le_total A 0 with hA | hA

Goal state after:
case inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : A ≤ 0
⊢ A * ‖f i‖ * ‖g i‖ < ε

case inr
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
f : α → E
g : α → F
l : Filter α
hf✝ : ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
op : E → F → G
A : ℝ
h_op : ∀ (x : E) (y : F), ‖op x y‖ ≤ A * ‖x‖ * ‖y‖
C : ℝ
hC : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) ((Norm.norm ∘ g) a) C
ε : ℝ
ε₀ : ε > 0
δ : ℝ
δ₀ : 0 < δ
hδ : A * C * δ < ε
i : α
hf : ‖f i‖ < δ
hg : (Norm.norm ∘ g) i ≤ C
hA : 0 ≤ A
⊢ A * ‖f i‖ * ‖g i‖ < ε
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(a :: b :: l).prod‖ ≤ (map norm (a :: b :: l)).prod

Tactic:
rw [List.map_cons, List.prod_cons, List.prod_cons (a := ‖a‖)]
    refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))
    exact List.norm_prod_le' (List.cons_ne_nil b l)

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a : α
x✝ : 0 < 1
⊢ ‖a ^ 1‖₊ ≤ ‖a‖₊ ^ 1

Tactic:
by simp only [pow_one, le_rfl]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)

Tactic:
apply measure_iUnion_le

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

Goal state before:
pp: β : Type u_2
f g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
hgf : ∀ (b : β), g b ≤ f b
hf : Summable f
⊢ Summable g

Tactic:
lift f to β → ℝ≥0 using fun b => (hg b).trans (hgf b)

Goal state after:
β : Type u_2
g : β → ℝ
hg : ∀ (b : β), 0 ≤ g b
f : β → ℝ≥0
hgf : ∀ (b : β), g b ≤ (fun i ↦ ↑(f i)) b
hf : Summable fun i ↦ ↑(f i)
⊢ Summable g
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝¹ : Nonempty α
x✝ : Nonempty ↑s
φ : β → Filter α := ⋯
ℱ : Filter α := ⋯
⊢ ∀ (i : ↑s), (φ (f ↑i)).NeBot

Tactic:
· intro x
      have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
      exact neBot_of_le this

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c

Tactic:
exact (strictMono_div_right_of_pos h h').lt_iff_lt

Goal state after:
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
h : 0 < c
h' : c ≠ ⊤
⊢ b / c < c * a / c ↔ b < c * a

Tactic:
exact (strictMono_div_right_of_pos h h').lt_iff_lt

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
⊢ False

Tactic:
suffices ∀ᶠ _ in 𝓝 a ⊓ ℱ, False by rwa [eventually_const] at this

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
f : α → β
inst✝ : LinearOrder β
s : Set α
ne_s : s.Nonempty
hs : IsCompact s
hf : LowerSemicontinuousOn f s
x✝² : Nonempty α
x✝¹ : Nonempty ↑s
φ : β → Filter α := fun b ↦ 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : ℱ.NeBot
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
x : α
hx : x ∈ s
hxa : f x < f a
x✝ : (𝓝 a ⊓ ℱ).NeBot := h
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
⊢ Tendsto (fun n ↦ (↑n)⁻¹) atTop (𝓝 0)

Tactic:
convert! NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜

Goal state after:
𝕜 : Type u_4
inst✝³ : DivisionSemiring 𝕜
inst✝² : CharZero 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : ContinuousSMul ℚ≥0 𝕜
x✝ : ℕ
⊢ (↑x✝)⁻¹ = (⇑(algebraMap ℚ≥0 𝕜) ∘ fun n ↦ (↑n)⁻¹) x✝
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case bot
y : EReal
h : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ ⊥
h' : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, y)

Tactic:
induction y

Goal state after:
case bot.bot
h : (⊥, ⊥).1 ≠ ⊤ ∨ (⊥, ⊥).2 ≠ ⊥
h' : (⊥, ⊥).1 ≠ ⊥ ∨ (⊥, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ⊥)

case bot.coe
a✝ : ℝ
h : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ ⊥
h' : (⊥, ↑a✝).1 ≠ ⊥ ∨ (⊥, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ↑a✝)

case bot.top
h : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ ⊥
h' : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ⊤)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ ⊥
h' : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, y)

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
h : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ ⊥
h' : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊥)

case coe.coe
a✝¹ a✝ : ℝ
h : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h' : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝¹, ↑a✝)

case coe.top
a✝ : ℝ
h : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ ⊥
h' : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (↑a✝, ⊤)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case top
y : EReal
h : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ ⊥
h' : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, y)

Tactic:
induction y

Goal state after:
case top.bot
h : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ ⊥
h' : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊥)

case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a ↦ ↑r ^ a) (↑(1 - r))⁻¹

Tactic:
NNReal.coe_sub (le_of_lt hr)

Goal state after:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a ↦ ↑r ^ a) (↑1 - ↑r)⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
rcases lt_or_ge r 1 with hr | hr

Goal state after:
case inl
r : ℝ≥0∞
hr : r < 1
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
c : ℝ≥0∞
hc : c ≠ ∞
⊢ c • OuterMeasure.ofFunction m m_empty = OuterMeasure.ofFunction (c • m) ⋯

Tactic:
ext1 s
  have : Nonempty { t : ℕ → Set α // s ⊆ ⋃ i, t i } := ⟨⟨fun _ => s, subset_iUnion (fun _ => s) 0⟩⟩
  simp only [smul_apply, ofFunction_apply, ENNReal.tsum_mul_left, Pi.smul_apply, smul_eq_mul,
  iInf_subtype']
  rw [ENNReal.mul_iInf fun h => (hc h).elim]

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

Goal state before:
pp: case bot
y : EReal
h₁ : (⊥, y).1 ≠ 0 ∨ (⊥, y).2 ≠ ⊥
h₂ : (⊥, y).1 ≠ 0 ∨ (⊥, y).2 ≠ ⊤
h₃ : (⊥, y).1 ≠ ⊥ ∨ (⊥, y).2 ≠ 0
h₄ : (⊥, y).1 ≠ ⊤ ∨ (⊥, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, y)

Tactic:
induction y

Goal state after:
case bot.bot
h₁ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊥
h₂ : (⊥, ⊥).1 ≠ 0 ∨ (⊥, ⊥).2 ≠ ⊤
h₃ : (⊥, ⊥).1 ≠ ⊥ ∨ (⊥, ⊥).2 ≠ 0
h₄ : (⊥, ⊥).1 ≠ ⊤ ∨ (⊥, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊥)

case bot.coe
a✝ : ℝ
h₁ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊥
h₂ : (⊥, ↑a✝).1 ≠ 0 ∨ (⊥, ↑a✝).2 ≠ ⊤
h₃ : (⊥, ↑a✝).1 ≠ ⊥ ∨ (⊥, ↑a✝).2 ≠ 0
h₄ : (⊥, ↑a✝).1 ≠ ⊤ ∨ (⊥, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ↑a✝)

case bot.top
h₁ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊥
h₂ : (⊥, ⊤).1 ≠ 0 ∨ (⊥, ⊤).2 ≠ ⊤
h₃ : (⊥, ⊤).1 ≠ ⊥ ∨ (⊥, ⊤).2 ≠ 0
h₄ : (⊥, ⊤).1 ≠ ⊤ ∨ (⊥, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊥, ⊤)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case coe
y : EReal
a✝ : ℝ
h₁ : (↑a✝, y).1 ≠ 0 ∨ (↑a✝, y).2 ≠ ⊥
h₂ : (↑a✝, y).1 ≠ 0 ∨ (↑a✝, y).2 ≠ ⊤
h₃ : (↑a✝, y).1 ≠ ⊥ ∨ (↑a✝, y).2 ≠ 0
h₄ : (↑a✝, y).1 ≠ ⊤ ∨ (↑a✝, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, y)

Tactic:
induction y

Goal state after:
case coe.bot
a✝ : ℝ
h₁ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊥
h₂ : (↑a✝, ⊥).1 ≠ 0 ∨ (↑a✝, ⊥).2 ≠ ⊤
h₃ : (↑a✝, ⊥).1 ≠ ⊥ ∨ (↑a✝, ⊥).2 ≠ 0
h₄ : (↑a✝, ⊥).1 ≠ ⊤ ∨ (↑a✝, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊥)

case coe.coe
a✝¹ a✝ : ℝ
h₁ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊥
h₂ : (↑a✝¹, ↑a✝).1 ≠ 0 ∨ (↑a✝¹, ↑a✝).2 ≠ ⊤
h₃ : (↑a✝¹, ↑a✝).1 ≠ ⊥ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
h₄ : (↑a✝¹, ↑a✝).1 ≠ ⊤ ∨ (↑a✝¹, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝¹, ↑a✝)

case coe.top
a✝ : ℝ
h₁ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊥
h₂ : (↑a✝, ⊤).1 ≠ 0 ∨ (↑a✝, ⊤).2 ≠ ⊤
h₃ : (↑a✝, ⊤).1 ≠ ⊥ ∨ (↑a✝, ⊤).2 ≠ 0
h₄ : (↑a✝, ⊤).1 ≠ ⊤ ∨ (↑a✝, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (↑a✝, ⊤)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case top
y : EReal
h₁ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊥
h₂ : (⊤, y).1 ≠ 0 ∨ (⊤, y).2 ≠ ⊤
h₃ : (⊤, y).1 ≠ ⊥ ∨ (⊤, y).2 ≠ 0
h₄ : (⊤, y).1 ≠ ⊤ ∨ (⊤, y).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, y)

Tactic:
induction y

Goal state after:
case top.bot
h₁ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊥
h₂ : (⊤, ⊥).1 ≠ 0 ∨ (⊤, ⊥).2 ≠ ⊤
h₃ : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ 0
h₄ : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊥)

case top.coe
a✝ : ℝ
h₁ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊥
h₂ : (⊤, ↑a✝).1 ≠ 0 ∨ (⊤, ↑a✝).2 ≠ ⊤
h₃ : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ 0
h₄ : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a✝)

case top.top
h₁ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊥
h₂ : (⊤, ⊤).1 ≠ 0 ∨ (⊤, ⊤).2 ≠ ⊤
h₃ : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ 0
h₄ : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ⊤)
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
β : Type u_4
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
⊢ IsPiSystem {s | ∃ t ∈ S, f ⁻¹' t = s}

Tactic:
by
  rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst
  rw [← Set.preimage_inter] at hst ⊢
  exact ⟨s ∩ t, h_pi s hs_mem t ht_mem (nonempty_of_nonempty_preimage hst), rfl⟩

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

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

Tactic:
univ_union

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : s =ᵐ[μ] univ
⊢ univ =ᵐ[μ] univ
Module: Mathlib.MeasureTheory.Measure.MeasureSpaceDef

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst✝ : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable (fun x ↦ g x a) μ

Tactic:
by
  constructor
  · exact AEMeasurable.eval
  · intro h
    use fun x a ↦ (h a).mk _ x, measurable_pi_lambda _ fun a ↦ (h a).measurable_mk
    exact (eventually_countable_forall.mpr fun a ↦ (h a).ae_eq_mk).mono fun _ h ↦ funext h

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ m (disjointed f i) ⋯ ≤ m (f i) ⋯

Tactic:
rw [← extend_eq m, ← extend_eq m]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
i : ℕ
⊢ extend m (disjointed f i) ≤ extend m (f i)
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)
⊢ Measurable f

Tactic:
have : Measurable (f ∘ (e.symm.trans e).toEquiv) := hfe.comp e.symm.measurable

Goal state after:
α : 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
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ g • s ∩ s = (fun x ↦ g₂⁻¹ • x) '' (g₁ • s ∩ g₂ • s)

Tactic:
image_smul,

Goal state after:
G : Type u_5
α : Type u_6
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
s : Set α
h_ae_disjoint : ∀ (g : G), g ≠ 1 → AEDisjoint μ (g • s) s
h_qmp : ∀ (g : G), QuasiMeasurePreserving (fun x ↦ g • x) μ μ
g₁ g₂ : G
g : G := g₂⁻¹ * g₁
hg : g ≠ 1
⊢ g • s ∩ s = g₂⁻¹ • (g₁ • s ∩ g₂ • s)