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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ s ∈ Filter.atTop → s ∈ cobounded α

Tactic:
Filter.atTop_basis.mem_iff,

Goal state after:
α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ s) → s ∈ cobounded α
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1

Tactic:
exact dist_nonneg

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u / v * v‖ = ‖u‖

Tactic:
rw [div_mul_cancel]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ a = 1 → ‖a‖₊ = 0

Tactic:
by
    rintro rfl
    exact nnnorm_one'

Goal state after:
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ ∀ (t t' : Set α),
    IsClosed[inst✝³] t →
      IsClosed[inst✝³] t' →
        Icc a b ⊆ t ∪ t' → (Icc a b ∩ t).Nonempty → (Icc a b ∩ t').Nonempty → (Icc a b ∩ (t ∩ t')).Nonempty

Tactic:
rintro s t hs ht hab ⟨x, hx⟩ ⟨y, hy⟩

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst✝³] s
ht : IsClosed[inst✝³] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
⊢ (Icc a b ∩ (s ∩ t)).Nonempty
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
⊢ StrictMono f

Tactic:
by
  intro a b hab
  by_contra! h
  have H : f b < f a := lt_of_le_of_ne h <| hf_i.ne hab.ne'
  by_cases! ha : f a ≤ f ⊥
  · obtain ⟨u, hu⟩ := intermediate_value_Ioc le_top hf_c.continuousOn ⟨H.trans_le ha, hf⟩
    have : u = ⊥ := hf_i hu.2
    simp_all
  · by_cases! hb : f ⊥ < f b
    · obtain ⟨u, hu⟩ := intermediate_value_Ioo bot_le hf_c.continuousOn ⟨hb, H⟩
      rw [hf_i hu.2] at hu
      exact (hab.trans hu.1.2).false
    · replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
      obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩
      have : u = ⊥ := hf_i hu.2
      simp_all

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
c : α
⊢ Bornology.IsCobounded s ↔ ∃ r, (closedBall c r)ᶜ ⊆ s

Tactic:
rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]
  apply exists_congr
  intro r
  rw [compl_subset_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (range f)

Tactic:
← image_union_image_compl_eq_range

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Bornology.IsBounded (f '' ?m.75 ∪ f '' ?m.75ᶜ)

α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Prod.map f f x ∈ {p | dist p.1 p.2 < 1}
⊢ Set β
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: case cons
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
⊢ (f i * ∏ i ∈ s, f i)⁻¹ = (f i)⁻¹ * (∏ i ∈ s, f i)⁻¹

Tactic:
refine ENNReal.mul_inv (not_or_of_imp fun hi₀ ↦ prod_ne_top fun j hj ↦ ?_)
    (not_or_of_imp fun hi₀ ↦ Finset.prod_ne_zero_iff.2 fun j hj ↦ ?_)

Goal state after:
case cons.refine_1
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = 0
j : ι
hj : j ∈ s
⊢ f j ≠ ∞

case cons.refine_2
ι : Type u_1
f : ι → ℝ≥0∞
s✝ : Finset ι
i : ι
s : Finset ι
hi : i ∉ s
ih : ((↑s).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞) → (∏ i ∈ s, f i)⁻¹ = ∏ i ∈ s, (f i)⁻¹
hf : (↑(Finset.cons i s hi)).Pairwise fun i j ↦ f i ≠ 0 ∨ f j ≠ ∞
hi₀ : f i = ∞
j : ι
hj : j ∈ s
⊢ f j ≠ 0
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ False

Tactic:
have : { x : α | f x ≤ b } ∩ { x : α | b' ≤ f x } = ∅ :=
    eq_empty_of_subset_empty fun x hx => (not_le_of_gt h) (le_trans hx.2 hx.1)

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x1 x2 ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
⊢ IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f

Tactic:
rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩
  · exact ⟨l, fun x _ ↦ lbot x⟩
  refine ⟨l', fun u hu ↦ ?_⟩
  obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists
  exact hl'.le.trans (l_le_w.trans w_le_u)

Goal state after:
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : ∀ (a : ι), IsLUB (range (s.domRestrict (eval a))) (f a)
⊢ Tendsto Subtype.val atTop (𝓝 f)

Tactic:
exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).domRestrict _) (h i)

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ sInf {a | ∀ᶠ (n : β) in f, u n ≤ a} ⊔ sInf {a | ∀ᶠ (n : β) in g, u n ≤ a}

Tactic:
sInf_sup_eq,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤
    ⨅ a ∈ {a | ∀ᶠ (n : β) in f, u n ≤ a}, a ⊔ sInf {a | ∀ᶠ (n : β) in g, u n ≤ a}
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : BoundedLENhdsClass α
inst✝ : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a✝ : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun x1 x2 ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ IsBounded (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x)

Tactic:
← @Prod.mk.eta _ _ x,

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : BoundedLENhdsClass α
inst✝ : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a✝ : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun x1 x2 ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ IsBounded (fun x1 x2 ↦ x1 ≤ x2) (𝓝 (x.1, x.2))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f fun x ↦ ¬p x) ⊔ blimsup u f p = limsup u f

Tactic:
simpa only [not_not] using blimsup_sup_not (p := (¬p ·))

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ max (edist ((fun x ↦ (f x, g x)) x).1 ((fun x ↦ (f x, g x)) y).1)
      (edist ((fun x ↦ (f x, g x)) x).2 ((fun x ↦ (f x, g x)) y).2) ≤
    max (↑Kf * edist x y) (↑Kg * edist x y)

Tactic:
exact max_le_max (hf x y) (hg x y)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
ι : Type x
inst✝ : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod

Tactic:
by
    simp only [List.map_cons, List.prod_cons]
    exact (h i).mul_end (LipschitzWith.list_prod f K h l)

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

Goal state before:
pp: case top
a c : EReal
hb : ⊤ ≠ ⊥ ∨ c ≠ ⊥
ht : ¬c = ⊤
h : a + ⊤ ≤ c
ha : ¬a = ⊥
⊢ False

Tactic:
exact (h.trans_lt (Ne.lt_top ht)).ne (add_top_iff_ne_bot.2 ha)

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

Goal state before:
pp: case pos
x y z t : EReal
h : x ≤ y
h' : z < t
hx_top : x ≠ ⊤
hy_bot : y ≠ ⊥
hy_top : ¬y = ⊤
hxy : x = y
⊢ x < y + (t - z)

Tactic:
rw [hxy]
    lift y to ℝ using ⟨hy_top, hy_bot⟩
    by_cases htz_top : t - z = ⊤
    · simp_all
    rw [← coe_toReal htz_top <| ne_bot_of_le_ne_bot (by simp) (sub_pos.mpr h').le]
    norm_cast
    refine lt_add_of_pos_right y ?_
    exact EReal.toReal_pos (sub_pos.mpr h') htz_top

Goal state after:
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, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
⊢ limsup u f ≤ x

pp: case neg
α : 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, u a < y
h' : ¬∀ y > x, ∃ z, x < z ∧ z < y
⊢ limsup u f ≤ x

Tactic:
· rw [← forall_gt_iff_le]
    intro y x_y
    rcases h' y x_y with ⟨z, x_z, z_y⟩
    exact (limsup_le_of_le h₁ ((h z x_z).mono (fun _ ↦ le_of_lt))).trans_lt z_y

Goal state after:
case neg
α : 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, u a < y
h' : ¬∀ y > x, ∃ z, x < z ∧ z < y
⊢ limsup u f ≤ x
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ a ∈ s, ContinuousOn (fun y ↦ f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith K (fun x ↦ f (x, b)) univ
⊢ ContinuousOn f (univ ×ˢ univ)

Tactic:
exact continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _)
    hs.closure_eq.ge K ha fun b _ => hb b

Goal state after:
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: case inr.refine_2
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ i, u i b_1 < b

Tactic:
have A (n) : ∃ r, ∀ s ≥ r, u n s ≤ b'' := by
    suffices ∀ᶠ r in atTop, u n r ≤ b' by
      simp only [eventually_atTop] at this
      rcases this with ⟨r, hr⟩
      exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩
    simp only [b']
    split_ifs with h
    · filter_upwards [(tendsto_order.1 (h_all n)).2 _ h.some_mem.1] with r hr
      exact hr.le
    · filter_upwards [(tendsto_order.1 (h_all n)).2 b hb] with r hr
      contrapose! h
      exact ⟨u n r, h, hr⟩

Goal state after:
case inr.refine_2
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
A : ∀ (n : ι), ∃ r, ∀ s ≥ r, u n s ≤ b''
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ i, u i b_1 < b
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case top.coe.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a < 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

pp: case top.coe.inr.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

pp: case top.coe.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

Tactic:
· simp_all [le_of_lt, top_mul_of_neg (EReal.coe_neg'.mpr ha)]

Goal state after:
case top.coe.inr.inl
hx : 0 ≤ ⊤
a : ℝ
ha : a = 0
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal

case top.coe.inr.inr
hx : 0 ≤ ⊤
a : ℝ
ha : 0 < a
⊢ (⊤ * ↑a).toENNReal = ⊤.toENNReal * (↑a).toENNReal
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalGroup α
f g : β → α
a₁ a₂ : α
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ HasProd (fun b ↦ f b / g b) (a₁ / a₂) L

Tactic:
simp only [div_eq_mul_inv]
  exact hf.mul hg.inv

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

Goal state before:
pp: case e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = m (bif true then s₁ else s₂) * m (bif false then s₁ else s₂)

Tactic:
cond,

Goal state after:
case e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = m s₁ * m (bif false then s₁ else s₂)
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalSemiring α
f : ι → α
inst✝¹ : T2Space α
inst✝ : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : ¬Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
· simp [tsum_eq_zero_of_not_summable hf]

Goal state after:
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 : α
inst✝ : T2Space α
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
by_cases ha : a = 0
  · simp [ha]
  · exact ((Homeomorph.mulRight₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulRight a)).symm

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

Goal state before:
pp: α : Type u_3
inst✝³ : Ring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalRing α
inst✝ : T2Space α
x : α
h : Summable fun x_1 ↦ x ^ x_1
⊢ Tendsto (fun n ↦ ∑ i ∈ range n, x ^ i * (1 - x)) atTop (nhds 1)

Tactic:
simpa [← Finset.sum_mul, geom_sum_mul_neg] using tendsto_const_nhds.sub h.tendsto_atTop_zero

Goal state after:
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun x ↦ g (pkg.coe x)) (pkg.coe a) = g (pkg.coe a)

Tactic:
← comp_apply (f := g)

Goal state after:
α : Type uα
inst✝¹ : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝ : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun x ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
this : {x | 0 ≤ x} = negPart ⁻¹' {0}
⊢ IsClosed (negPart ⁻¹' {0})

Tactic:
exact isClosed_singleton.preimage continuous_negPart

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

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
p : E
⊢ mk p = 1 ↔ ‖p‖ = 0

Tactic:
by
  rw [← norm_mk', norm_eq_zero']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : NonUnitalNormedRing α
inst✝ : NormMulClass α
a✝ a : α
ha : a ≠ 0
x y : α
⊢ edist (x * a) (y * a) = ↑‖a‖₊ * edist x y

Tactic:
by
    simp [edist_nndist, nndist_eq_nnnorm, ← sub_mul, ← mul_comm (‖a‖₊)]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
this : Countable ↑s
⊢ MeasurableSet (⋃ x, f ↑x)

Tactic:
exact MeasurableSet.iUnion (by simpa using h)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ b ∈ s, f b)

Tactic:
by
  rw [biUnion_eq_iUnion]
  have := hs.to_subtype
  exact MeasurableSet.iUnion (by simpa using h)

Goal state after:
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 • e, hx⟩‖ < ‖e‖ ↔ ⟨k • e, hx⟩ ∈ {0}

Tactic:
AddSubgroup.coe_mk,

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 • e‖ < ‖e‖ ↔ ⟨k • e, hx⟩ ∈ {0}
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 • e‖ < ‖e‖ ↔ ↑⟨k • e, hx⟩ = ↑0

Tactic:
AddSubgroup.coe_mk,

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 • e‖ < ‖e‖ ↔ k • e = ↑0
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
t : Set ↑s
hs : MeasurableSet s
⊢ MeasurableSet t → MeasurableSet (Subtype.val '' t)

Tactic:
rintro ⟨u, hu, rfl⟩
  rw [Subtype.image_preimage_coe]
  exact hs.inter hu

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ (j - (n + 1) + n).succ ≤ j

Tactic:
Nat.succ_eq_add_one,

Goal state after:
case inr.refine_2
α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
n : ℕ
h' : Monotone s
x : α
this✝ : ∃ i, x ∈ s i
j : ℕ
hj : x ∈ s j
hlt : ∀ m < j, x ∉ s m
hnj : n < j
this : j - (n + 1) + n + 1 = j
⊢ j - (n + 1) + n + 1 ≤ j
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
⊢ z ∈ measurableAtom x ∩ measurableAtom y ↔ z ∈ ∅

Tactic:
simp only [mem_inter_iff, mem_empty_iff_false, iff_false, not_and]

Goal state after:
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∉ measurableAtom y
z : β
⊢ z ∈ measurableAtom x → z ∉ measurableAtom y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ x ≤ y ↔
    sign x < sign y ∨
      sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs ∨
        sign x = zero ∧ sign y = zero ∨ sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs

Tactic:
by
  constructor
  · intro h
    refine (sign.monotone h).lt_or_eq.imp_right (fun hs => ?_)
    rw [← x.sign_mul_abs, ← y.sign_mul_abs] at h
    cases hy : sign y <;> rw [hs, hy] at h ⊢
    · simp
    · left; simpa using h
    · right; right; simpa using h
  · rintro (h | h | h | h)
    · exact (sign.monotone.reflect_lt h).le
    all_goals rw [← x.sign_mul_abs, ← y.sign_mul_abs]; simp [h]

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

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

Tactic:
← coe_inv (-_)

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

Goal state before:
pp: case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < a * ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤

Tactic:
rw [mul_top_of_pos ha] at h

Goal state after:
case right
a c : EReal
ha✝ : 0 ≤ a
hc : 0 ≤ c
h : c < ⊤
ha : 0 < a
a' : EReal
a0' : 0 < a'
aa' : a' < a
⊢ c < a' * ⊤
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case neg
x : ℝ
hx : ↑x < ⊤
hx_bot : ¬↑x = ⊥
⊢ ∃ i', Ico ↑i' ⊤ ⊆ Ici ↑x ∩ {⊤}ᶜ

Tactic:
refine ⟨x, fun x ⟨h1, h2⟩ ↦ ?_⟩

Goal state after:
case neg
x✝¹ : ℝ
hx : ↑x✝¹ < ⊤
hx_bot : ¬↑x✝¹ = ⊥
x : EReal
x✝ : x ∈ Ico ↑x✝¹ ⊤
h1 : ↑x✝¹ ≤ x
h2 : x < ⊤
⊢ x ∈ Ici ↑x✝¹ ∩ {⊤}ᶜ