mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x y z t : EReal
h : x < y
h' : z ≤ t
hz : z ≠ ⊥
ht : t ≠ ⊤
⊢ -t ≠ ⊥

Tactic:
simp [ht]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
a✝ : β
h : a✝ ∈ s
⊢ s.piecewise u v a✝ = u a✝

Tactic:
simp [h]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteDistribLattice α
f : Filter β
u : β → α
s : Set β
inst✝ : DecidablePred fun x ↦ x ∈ s
v : β → α
a✝ : β
h : a✝ ∉ s
⊢ s.piecewise u v a✝ = v a✝

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * ↑(3 * K) + ε / 2

Tactic:
by push_cast; ring

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
hd : Pairwise (Disjoint on f)
i j : ℕ
ij : i ≠ j
x : α
this : ∀ (a : β), encode a = i → x ∈ f a → ∀ (b : β), encode b = j → x ∉ f b
⊢ x ∈ (fun i ↦ ⋃ b ∈ decode₂ β i, f b) i → x ∉ (fun i ↦ ⋃ b ∈ decode₂ β i, f b) j

Tactic:
simpa [decode₂_eq_some]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ (b : Finset α), t ⊆ b → b ∈ s
b : Finset (α ⊕ β)
hb : t.disjSum ∅ ⊆ b
⊢ t ⊆ b.toLeft

Tactic:
by simpa [← Finset.coe_subset, Set.subset_def] using hb

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ (b : Finset β), t ⊆ b → b ∈ s
b : Finset (α ⊕ β)
hb : ∅.disjSum t ⊆ b
⊢ t ⊆ b.toRight

Tactic:
by simpa [← Finset.coe_subset, Set.subset_def] using hb

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

Goal state before:
pp: case zero_top
⊢ -0 * ⊤ = -(0 * ⊤)

Tactic:
| zero_top =>

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

Goal state before:
pp: a b : EReal
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
L : SummationFilter β
inst✝ : L.HasSupport
f : β ↪ γ
h : L.filter = ⊥
⊢ ∀ᶠ (s : Finset γ) in (L.map f).filter, ↑s ⊆ (L.map f).support

Tactic:
simp [h]

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

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
hAtTop : atTop = pure Finset.univ
⊢ L = unconditional β

Tactic:
have hL := L.le_atTop

Goal state after:
β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
hAtTop : atTop = pure Finset.univ
hL : L.filter ≤ atTop
⊢ L = unconditional β
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
hx_nonneg : 0 ≤ x
hx_ne_top : x ≠ ⊤
y z : EReal
x✝ : x = 0 ∨ 0 < x
⊢ x * (y + z) = x * y + x * z

Tactic:
cases hx_nonneg.eq_or_lt' with

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

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
ha' : a ≠ ⊤
⊢ (b - c) * a = b * a - c * a

Tactic:
by
  rw [sub_eq_add_neg, right_distrib_of_nonneg_of_ne_top ha ha']
  simp [← neg_mul, sub_eq_add_neg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ∏' (n : β), if n = b then 1 else f n

Tactic:
rw [(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
inst✝¹ : T2Space α
inst✝ : DecidableEq β
hf : Multipliable f
b : β
⊢ ∏' (n : β), f n = f b * ((∏' (b : β), f b) / f b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
⊢ (∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e) →
    ∀ s ∈ 𝓝 1, ∃ a, ∀ (b : Finset β × Finset β), a ≤ b → (∏ b ∈ b.2, f b) / ∏ b ∈ b.1, f b ∈ s

Tactic:
rintro h e he
    rcases exists_nhds_split_inv he with ⟨d, hd, hde⟩
    rcases h d hd with ⟨s, h⟩
    use (s, s)
    rintro ⟨t₁, t₂⟩ ⟨ht₁, ht₂⟩
    have : ((∏ b ∈ t₂, f b) / ∏ b ∈ t₁, f b) = (∏ b ∈ t₂ \ s, f b) / ∏ b ∈ t₁ \ s, f b := by
      rw [← Finset.prod_sdiff ht₁, ← Finset.prod_sdiff ht₂, mul_div_mul_right_eq_div]
    simp only [this]
    exact hde _ (h _ Finset.sdiff_disjoint) _ (h _ Finset.sdiff_disjoint)

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℕ → M
h : HasProd (fun n ↦ f (n + 1)) m
⊢ HasProd f (f 0 * m)

Tactic:
by
  simpa only [prod_range_one] using h.prod_range_mul

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd ((s ∪ t).mulIndicator f) (a * b)

Tactic:
Set.mulIndicator_union_of_disjoint hs

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a b : α
inst✝ : ContinuousMul α
s t : Set β
hs : Disjoint s t
ha : HasProd (s.mulIndicator f) a
hb : HasProd (t.mulIndicator f) b
⊢ HasProd (fun a ↦ s.mulIndicator f a * t.mulIndicator f a) (a * b)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
      ext1 i
      rw [div_eq_iff_eq_mul, mul_comm, hf.prod_mul_tprod_nat_add i]

Goal state after:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i ↦ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' (k : ℕ), f (k + i)
⊢ Tendsto (fun i ↦ ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : n = b
⊢ f n = f n * update f b 1 n

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : T2Space α
inst✝³ : ContinuousMul α
inst✝² : DecidableEq β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
f : β → α
b : β
hf : Multipliable (update f b 1) L
n : β
h : ¬n = b
⊢ f n = 1 * update f b 1 n

Tactic:
simp [h]

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

Goal state before:
pp: case inr
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (E i)
inst✝ : (i : ι) → Zero (E i)
i : ι
x y : E i
j : ι
h : i ≠ j
⊢ j ∈ Finset.univ → edist (Pi.single i x j) (Pi.single i y j) ≤ edist x y

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ Tendsto (fun x ↦ ↑(f x)) l (𝓝 ∞) ↔ Tendsto f l atTop

Tactic:
rw [tendsto_nhds_top_iff_nnreal, atTop_basis_Ioi.tendsto_right_iff]

Goal state after:
α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
Module: Mathlib.Topology.UniformSpace.AbstractCompletion

Goal state before:
pp: α : Type uα
inst✝² : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst✝¹ : UniformSpace β
f : α → β
inst✝ : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (⋯.extend f)

Tactic:
exact pkg.isDenseInducing.isUniformInducing_extend pkg.isUniformInducing h

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₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n : ℕ
⊢ ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n

Tactic:
apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)

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)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
n k : ℕ
hk : k < n
⊢ (v 0)⁻¹ * w (k + 1) = (v 0)⁻¹ * w k * v (k + 1)
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_1
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)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ Tendsto (fun n ↦ ∏ i ∈ range (n + 1), v i) atTop (𝓝 a)

Tactic:
apply hw.congr (fun n ↦ ?_)
    rw [Finset.prod_range_succ']
    have : ∏ k ∈ range n, v (k + 1) = (v 0)⁻¹ * w n := by
      apply prod_range_induction _ _ (by simp [v]) _ (fun k hk ↦ ?_)
      simp only [↓reduceIte, Nat.add_eq_zero_iff, one_ne_zero, and_false, add_tsub_cancel_right, v]
      group
    simp [this]

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
this : IsTrans X fun x y ↦ d x y = 0
x y : X
l : List X
ihn : ∀ m < l.length, ∀ (x y : X) (l : List X), l.length = m → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum
L : List ℝ≥0 := zipWith d (x :: l) (l ++ [y])
hL_len : L.length = l.length + 1
hd₀ : d x y ≠ 0
s : Set ℕ := {m | 2 * (take m L).sum ≤ L.sum}
hs₀ : 0 ∈ s
hsne : s.Nonempty
M : ℕ
hMl : M < l.length
hMs : IsGreatest s (M + 1)
hM_lt : M + 1 < L.length
hM_ltx : M + 1 < (x :: l).length
hM_lty : M + 1 < (l ++ [y]).length
hMl' : (take M l).length = M
⊢ zipWith d (x :: take M l) (take M l ++ [(x :: l)[M + 1]]) = take (M + 1) L

Tactic:
rw [take_zipWith, take, take_add_one, getElem?_append_left hMl, getElem?_eq_getElem hMl,
        ← Option.coe_def, Option.toList_some, take_append_of_le_length hMl.le, getElem_cons_succ]

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

Goal state before:
pp: case insert.ha
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ a a✝ ≠ 0 ∨ ∏ c ∈ s✝, a c ≠ ∞

pp: case insert.hmb
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ Tendsto (fun a ↦ ∏ c ∈ s✝, f c a) x (𝓝 (∏ c ∈ s✝, a c))

pp: case insert.hb
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ ∏ c ∈ s✝, a c ≠ 0 ∨ a a✝ ≠ ∞

Tactic:
· right
      exact prod_ne_top fun i hi => h' _ (Finset.mem_insert_of_mem hi)

Goal state after:
case insert.hmb
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ Tendsto (fun a ↦ ∏ c ∈ s✝, f c a) x (𝓝 (∏ c ∈ s✝, a c))

case insert.hb
α : Type u_1
ι : Type u_4
f : ι → α → ℝ≥0∞
x : Filter α
a : ι → ℝ≥0∞
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, Tendsto (f i) x (𝓝 (a i))) → (∀ i ∈ s✝, a i ≠ ∞) → Tendsto (fun b ↦ ∏ c ∈ s✝, f c b) x (𝓝 (∏ c ∈ s✝, a c))
h : ∀ i ∈ insert a✝ s✝, Tendsto (f i) x (𝓝 (a i))
h' : ∀ i ∈ insert a✝ s✝, a i ≠ ∞
⊢ ∏ c ∈ s✝, a c ≠ 0 ∨ a a✝ ≠ ∞
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case neg
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

Tactic:
· simp only [H, true_or, Ne, not_false_iff]

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

Goal state before:
pp: case inl
a b : ℝ
h : b ≤ a
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
simp [h]

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

Goal state before:
pp: case inl
a b : ℝ
h : a ≤ b
⊢ ENNReal.ofReal (b - sInf (Icc a b)) = ENNReal.ofReal (b - a)

Tactic:
csInf_Icc h

Goal state after:
case inl
a b : ℝ
h : a ≤ b
⊢ ENNReal.ofReal (b - a) = ENNReal.ofReal (b - a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
obs : min t x ≠ ∞
⊢ t.truncateToReal x = x.toReal

Tactic:
exact (ENNReal.toReal_eq_toReal_iff' obs x_lt_top.ne).mpr (min_eq_right x_le)

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

Goal state before:
pp: t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
⊢ t.truncateToReal x = x.toReal

Tactic:
by
  have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top
  have obs : min t x ≠ ∞ := by
    simp_all only [ne_eq, min_eq_top, false_and, not_false_eq_true]
  exact (ENNReal.toReal_eq_toReal_iff' obs x_lt_top.ne).mpr (min_eq_right x_le)

Goal state after:
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ ↑(1 / 2) ^ (n + 1) ≤ ↑(d x.1 x.2) / ↑2

Tactic:
← NNReal.coe_div,

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ ↑(1 / 2) ^ (n + 1) ≤ ↑(d x.1 x.2 / 2)
Module: Mathlib.Algebra.Order.GroupWithZero.Finset

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

Tactic:
by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp [bot_eq_zero]
  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_div₀ (ha := ha)]

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y

Tactic:
refine ⟨r, hne, fun x y => ?_⟩

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
inst✝² : FunLike F α✝ β✝
α : Type ?u.16
β : Type ?u.18
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ edist (f x) (f y) = ↑r * edist x y
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: ⊢ LipschitzWith 2 fun p ↦ p.1 - p.2

Tactic:
← NNReal.isometry_coe.lipschitzWith_iff

Goal state after:
⊢ LipschitzWith 2 (toReal ∘ fun p ↦ p.1 - p.2)
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
i : ι
⊢ i ∈ {i | i ∈ l} ↔ i ∈ univ

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ dist x⁻¹ y⁻¹ = ‖x‖⁻¹ * dist y x * ‖y‖⁻¹

Tactic:
by
      simp [dist_eq_norm, inv_sub_inv' (hs₀ x hx) (hs₀ y hy)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l s
hG : TendstoLocallyUniformlyOn G g l s
hf : ContinuousOn f s
hg : ContinuousOn g s
hg₀ : ∀ x ∈ s, g x ≠ 0
⊢ TendstoLocallyUniformlyOn (F / G) (f / g) l s

Tactic:
by
  simp only [div_eq_mul_inv]
  exact hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

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

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F G : ι → X → α
f g : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
hg₀ : ∀ (x : X), g x ≠ 0
⊢ TendstoLocallyUniformly (F / G) (f / g) l

Tactic:
by
  simp only [div_eq_mul_inv]
  exact hF.mul₀ (hG.inv₀ hg hg₀) hf <| hg.inv₀ hg₀

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

Goal state before:
pp: case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
⊢ ∃ a, Tendsto u atTop (𝓝 a)

Tactic:
have hu' : CauchySeq ((· / x) ∘ u) := (uniformContinuous_div_const' x).comp_cauchySeq hu

Goal state after:
case mpr.inr
K : Type u_4
val✝ : NontriviallyNormedField K
h : IsComplete (closedBall 0 1)
u : ℕ → K
hu : CauchySeq u
k : ℝ
hk : k ∈ upperBounds (Set.range fun n ↦ ‖u n‖)
kpos : 0 ≤ k
x : K
hx : k < ‖x‖
hu' : CauchySeq ((fun x_1 ↦ x_1 / x) ∘ u)
⊢ ∃ a, Tendsto u atTop (𝓝 a)
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∈ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
simp [h]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
h : b ∉ s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
⊢ MeasurableSpace.comap (fun _a ↦ b) m ≤ ⊥

Tactic:
rintro _ ⟨s, -, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace β
b : β
s : Set β
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ x✝ ^ 0 = 1

Tactic:
by ext; apply Nat.zero_mul

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:
rw [compl_iInter₂]

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, MeasurableSet (f b)
⊢ MeasurableSet (⋃ i ∈ s, (f i)ᶜ)
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 α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ ∑' (i : ℕ), μ (disjointed t i) ≤ ∑' (i : ℕ), μ (t i)

Tactic:
gcongr; exact disjointed_subset ..

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 α
ht : μ t = 0
⊢ μ t + μ (s \ t) = μ (s \ t)

Tactic:
simp [ht]

Goal state after: