mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ ⊤ ≤
    Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I))

Tactic:
Submodule.map_le_iff_le_comap,

Goal state after:
case refine_4
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ⊤ ≤
    Submodule.comap (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
        (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I)))
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖(a / b)⁻¹‖ₑ = ‖b / a‖ₑ

Tactic:
inv_div

Goal state after:
E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖b / a‖ₑ = ‖b / a‖ₑ
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr
α : 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
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty

Tactic:
union_comm s t

Goal state after:
case inr
α : 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 ⊆ t ∪ s
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Tactic:
have hex : ∀ g > 1, ∃ n : ℕ, g ∈ Ioc (a ^ n) (a ^ (n + 1)) := fun g hg => by
    rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩
    simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'
    lift m to ℕ
    · rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]
      exact hg.trans_le hm
    · simp only [← Nat.cast_succ, zpow_natCast] at hm hm'
      exact ⟨m, hm', hm⟩

Goal state after:
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hex : ∀ g > 1, ∃ n, g ∈ Ioc (a ^ n) (a ^ (n + 1))
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b
Module: Mathlib.Topology.UniformSpace.Real

Goal state before:
pp: u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := ⟨u, ⋯⟩
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ i, ∀ j ≥ i, |↑(c - CauSeq.const abs c.lim) j| < ε
⊢ s ∈ map u atTop

Tactic:
simp only [mem_map, mem_atTop_sets]

Goal state after:
u : ℕ → ℝ
hu : CauchySeq u
c : CauSeq ℝ abs := ⟨u, ⋯⟩
s : Set ℝ
h : s ∈ nhds c.lim
ε : ℝ
ε0 : ε > 0
hε : ball c.lim ε ⊆ s
this : ∃ i, ∀ j ≥ i, |↑(c - CauSeq.const abs c.lim) j| < ε
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → b ∈ u ⁻¹' s
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ ∀ b ∈ s, F b a ≤ s.sup' hs m

Tactic:
exact fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun i ↦ (I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))

Tactic:
rw [EquivLike.range_comp I e] at ih

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.top.inl
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
h : ↑a✝ < 0
⊢ ↑a✝ * ⊤ ≠ 0

Tactic:
simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]

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

Goal state before:
pp: case coe.top.inr
a✝ : ℝ
h✝ : ↑a✝ ≠ 0 ∧ ⊤ ≠ 0
h : 0 < ↑a✝
⊢ ↑a✝ * ⊤ ≠ 0

Tactic:
simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]

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

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
⊢ (Summable fun i ↦ f (i + k)) ↔ Summable f

Tactic:
by
  rw [← summable_coe, ← summable_coe]
  exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k

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 : l ≤ 𝓟 s
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
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
⊢ ball x (V N) ∈ l

Tactic:
refine mem_of_superset (htl n) fun y hy => hWV N ⟨u n, hn, htW N ?_⟩

Goal state after:
X : Type u_1
inst✝¹ : UniformSpace X
s : Set X
inst✝ : (𝓤 X).IsCountablyGenerated
hs : IsSeqCompact s
l : Filter X
hl : Cauchy l
hls : l ≤ 𝓟 s
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
t : ℕ → Set X
ht_anti : Antitone t
htl : ∀ (n : ℕ), t n ∈ l
htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n
hts : ∀ (n : ℕ), t n ⊆ s
u : ℕ → X
hu : ∀ (n : ℕ), u n ∈ t n
huc : CauchySeq u
x : X
hxs : x ∈ s
hx : Tendsto u atTop (𝓝 x)
N : ℕ
x✝ : True
n : ℕ
hNn : N ≤ n
hn : u n ∈ ball x (W N)
y : X
hy : y ∈ t n
⊢ (u n, y) ∈ t N ×ˢ t N
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case succ
n : ℕ
IH : Continuous fun a ↦ a ^ n
⊢ Continuous fun a ↦ a ^ n * a ^ 1

Tactic:
pow_one,

Goal state after:
case succ
n : ℕ
IH : Continuous fun a ↦ a ^ n
⊢ Continuous fun a ↦ a ^ n * a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

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

pp: case pos
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

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

Tactic:
· simp only [H, zero_ne_top, Ne, or_true, not_false_iff]

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

case pos
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

case neg
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case pos
a : ℝ≥0∞
a_infty : a = ∞
⊢ Continuous fun x ↦ x - a

pp: case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous fun x ↦ x - a

Tactic:
· simp [a_infty, continuous_const, tsub_eq_zero_of_le]

Goal state after:
case neg
a : ℝ≥0∞
a_infty : ¬a = ∞
⊢ Continuous fun x ↦ x - a
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
b x : α
hx : x ∈ Iic b
⊢ projIic b x = ⟨x, hx⟩

Tactic:
simpa [projIic]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] f

Tactic:
refine continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_
  rcases ENNReal.exists_nnreal_pos_mul_lt hC ε0.ne' with ⟨δ, δ0, hδ⟩
  rw [mul_comm] at hδ
  filter_upwards [Metric.closedEBall_mem_nhds x (ENNReal.coe_pos.2 δ0)] with y hy
  refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩ <;> grw [← hδ.le] <;> gcongr
  exacts [Metric.mem_closedEBall'.1 hy, Metric.mem_closedEBall.1 hy]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ edist p.1 p.2

Tactic:
apply continuous_of_le_add_edist 2 (by decide)

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
⊢ ∀ (x y : α × α), edist x.1 x.2 ≤ edist y.1 y.2 + 2 * edist x y
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:
simpa using hf.max (LipschitzWith.const a)

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

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0
hf : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ ↑(limsup u f) = limsup (fun i ↦ ↑(u i)) f

Tactic:
refine eq_of_forall_nnreal_le_iff fun r ↦ ?_
  rw [coe_le_coe, le_limsup_iff, le_limsup_iff]
  simp [forall_ennreal]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|

Tactic:
refine le_trans (abs_add_le (p.1 - q.1) (p.2 - q.2)) ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1| + |p.2 - q.2| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|

pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|

Tactic:
· exact abs_sup_sub_sup_le_abs _ _ _

Goal state after:
case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : SeminormedGroup E
inst✝ : TopologicalSpace α
f : α → E
hf : HasCompactMulSupport f
h'f : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ ∃ C, ∀ (x : α), ‖f x‖ ≤ C

Tactic:
by
  simpa using (hf.isCompact_range h'f).isBounded.exists_norm_le'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
by
  rcases hne with ⟨x, y, hα⟩
  have hgf := (edist_eq (g.comp f) x y).symm
  simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_left_inj hα.1 hα.2]
    at hgf
  rwa [← ENNReal.coe_inj, ENNReal.coe_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
a b : ℤ
⊢ ‖a * b‖ = ‖a‖ * ‖b‖

Tactic:
simp [← Int.norm_cast_real, abs_mul]

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ (TProd.mk is f).elim ⋯ = f j

Tactic:
elim_mk is

Goal state after:
case neg
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
f : (i : ι) → α i
j : ι
hj : j ∈ i :: is
hji : ¬j = i
⊢ f j = f j
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ ContinuousAt Inv.inv x

Tactic:
refine uniformContinuousOn_inv₀ (s := (Metric.closedBall x (‖x‖ / 2))) ?_
      |>.continuousOn |>.continuousAt ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ (closedBall x (‖x‖ / 2))ᶜ ∈ 𝓝 0

case refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NormedDivisionRing α
x : α
hx : x ≠ 0
⊢ closedBall x (‖x‖ / 2) ∈ 𝓝 x
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋃ i ∈ s, i)

Tactic:
exact .biUnion hs h

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ (cobounded E).NeBot

Tactic:
neBot_iff,

Goal state after:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ cobounded E ≠ ⊥
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ c • 0 = 0

Tactic:
← smul_one_mul c

Goal state after:
α : Type u_1
β : Type u_2
m✝ : OuterMeasure α
R : Type u_3
inst✝³ : SMul R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
R' : Type u_4
inst✝¹ : SMul R' ℝ≥0∞
inst✝ : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
c : R
m : OuterMeasure α
⊢ c • 1 * 0 = 0
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
k : ℕ
⊢ s ^ (2 * k) * s ^ 1 = s

Tactic:
pow_one,

Goal state after:
s : SignType
k : ℕ
⊢ s ^ (2 * k) * s = s
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case coe.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * (↑(↑a).abs)⁻¹ = (↑a)⁻¹

Tactic:
· rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul]
      simp only [abs_def a, coe_ennreal_ofReal, abs_nonneg, max_eq_left]
      congr
      exact abs_of_pos a_pos

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

Goal state before:
pp: b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
this : 0 ≤ -b
⊢ a * (-b)⁻¹ ≤ a' * (-b)⁻¹

Tactic:
exact div_le_div_right_of_nonneg this h'

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

Goal state before:
pp: a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * (a / b) ≤ c / b ↔ a * b ≤ c

Tactic:
mul_div b a b,

Goal state after:
a b c : EReal
h : b > 0
h' : b ≠ ⊤
⊢ b * a / b ≤ c / b ↔ a * b ≤ c
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case inr.inl
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : b ≤ 0
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

pp: case inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c

Tactic:
· obtain ⟨a', aa', a_top'⟩ := exists_between a_top
    exact ⟨a', mem_Ioo.2 ⟨aa', a_top'⟩, lt_of_le_of_lt (mul_le_mul_of_nonpos_right aa'.le b0) hc⟩

Goal state after:
case inr.inr
a b c : EReal
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ 0 < b
hc : a * b < c
a_top : a < ⊤
b0 : 0 < b
⊢ ∃ a' ∈ Ioo a ⊤, a' * b < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊥, ↑a)

Tactic:
simp only [ContinuousAt, tendsto_nhds_bot_iff_real, bot_add]
  refine fun r ↦ ((gt_mem_nhds (bot_lt_coe (r - (a + 1)))).prod_nhds
    (gt_mem_nhds <| EReal.coe_lt_coe_iff.2 <| lt_add_one _)).mono fun _ h ↦ ?_
  simpa only [← coe_add, _root_.sub_add_cancel] using add_lt_add h.1 h.2

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

Goal state before:
pp: x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ⊤), ↑x < a.1 * a.2

Tactic:
_root_.eventually_nhds_iff

Goal state after:
x : ℝ
⊢ ∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ⊤) ∈ t
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)

pp: case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

pp: case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1

Tactic:
· exact IsOpen.prod isOpen_Ioi isOpen_Ioi

Goal state after:
case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ᶠ (a : EReal × EReal) in 𝓝 (⊤, ↑a), ↑x < a.1 * a.2

Tactic:
_root_.eventually_nhds_iff

Goal state after:
a : ℝ
h : 0 < a
x : ℝ
⊢ ∃ t, (∀ y ∈ t, ↑x < y.1 * y.2) ∧ IsOpen t ∧ (⊤, ↑a) ∈ t
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

pp: case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

pp: case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)

Tactic:
· exact IsOpen.prod isOpen_Ioi isOpen_Ioi

Goal state after:
case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Type u_2
I : Set ι
hI : I.Nonempty
m : ι → OuterMeasure α
s : Set α
this : Nonempty ↑I
⊢ (⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, (m i) (t n)

Tactic:
simp only [← iInf_subtype'', iInf_apply]

Goal state after:
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
⊢ (∀ (n : ℕ), (s n).Nonempty) → ∀ (n : ℕ), (dissipate s n).Nonempty

Tactic:
intro h n

Goal state after:
α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
h : ∀ (n : ℕ), (s n).Nonempty
n : ℕ
⊢ (dissipate s n).Nonempty
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a - x⁻¹ ≤ ↑⌊a * x⌋₊ / x

Tactic:
simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul,
      inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']

Goal state after:
case hgf
R : Type u_4
inst✝⁵ : TopologicalSpace R
inst✝⁴ : Field R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : 1 ≤ x
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iio '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
  exact ⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩

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 : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ ↔ s ∪ t =ᵐ[μ] s ∪ univ

Tactic:
union_univ

Goal state after:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᵐ[μ] univ
⊢ s ∪ t =ᵐ[μ] univ ↔ s ∪ t =ᵐ[μ] univ
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)
x : α
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ

Tactic:
by_cases h : x ∈ s <;> simp [h]

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

Goal state before:
pp: case mpr
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ (∀ (t : Set α),
      P t →
        (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤
          (inducedOuterMeasure m P0 m0) t) →
    ∀ (t : Set α),
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t

Tactic:
· intro h u
    conv_rhs => rw [inducedOuterMeasure_eq_iInf _ msU m_mono]
    refine le_iInf ?_
    intro t
    refine le_iInf ?_
    intro ht
    refine le_iInf ?_
    intro h2t
    refine le_trans ?_ ((h t ht).trans_eq <| inducedOuterMeasure_eq' _ msU m_mono ht)
    gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
s : Set α
hs : s ∈ ⨅ x, f (Equiv.plift x)
⊢ ∃ t ∈ ⨅ i, f i, MeasurableSet t ∧ t ⊆ s

Tactic:
mem_iInf

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
s : Set α
hs : ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ f (Equiv.plift ↑i)) ∧ s = ⋂ i, V i
⊢ ∃ t ∈ ⨅ i, f i, MeasurableSet t ∧ t ⊆ s
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ⋂ i, U i ∈ ⨅ x, f (Equiv.plift x)

Tactic:
mem_iInf

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ ∃ I, I.Finite ∧ ∃ V, (∀ (i : ↑I), V i ∈ f (Equiv.plift ↑i)) ∧ ⋂ i, U i = ⋂ i, V i