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

Goal state before:
pp: 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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = spanSingleton R⁰ (mk' K n d)
hnd : mk' K n d = k
h : n = 0
⊢ False

Tactic:
h,

Goal state after:
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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
k : K
n : R := choose ⋯
d : ↥R⁰ := choose ⋯
hk : I = spanSingleton R⁰ (mk' K 0 d)
hnd : mk' K n d = k
h : n = 0
⊢ False
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: case inr.inl
p : ℝ≥0∞
hp : 0 < p
hpq : p ≤ ∞
⊢ p = 0 ∧ ∞ = 0 ∨
    p = 0 ∧ ∞ = ∞ ∨
      p = 0 ∧ 0 < ∞.toReal ∨ p = ∞ ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ ∞ = ∞ ∨ 0 < p.toReal ∧ 0 < ∞.toReal ∧ p.toReal ≤ ∞.toReal

Tactic:
simpa using p.trichotomy

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ (if x + y = 0 then 0 else 1) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
by_cases hx : x = 0
        · simp_rw [if_pos hx, hx, zero_add]
          exact le_max_of_le_right (le_refl _)
        · simp_rw [if_neg hx]
          split_ifs <;> simp

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ ↑y ∈ s.ordConnectedComponent (s.ordConnectedProj x)

Tactic:
h,

Goal state after:
case mp
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x y : ↑s
h : s.ordConnectedProj x = s.ordConnectedProj y
⊢ ↑y ∈ s.ordConnectedComponent (s.ordConnectedProj y)
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
i j k : ι
hk : f i + g j ≤ f k + g k
⊢ f i + g j ≤ ⨆ i, f i + g i

Tactic:
exact le_iSup_of_le k hk

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

Goal state before:
pp: case neg
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 I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I * I' = 0
⊢ count K v (I * I') = 0

Tactic:
h,

Goal state after:
case neg
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 I' : FractionalIdeal R⁰ K
inst✝ : Decidable (I ≠ 0 ∧ I' ≠ 0)
h : I * I' = 0
⊢ count K v 0 = 0
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ count K v (I ^ n) + count K v I = ↑(n + 1) * count K v I

Tactic:
h,

Goal state after:
case neg
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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ ↑n * count K v I + count K v I = ↑(n + 1) * count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
h : a * b = 1
⊢ a * b * b⁻¹ = b⁻¹

pp: a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞

Tactic:
h,

Goal state after:
a b : ℝ≥0∞
h : a * b = 1
⊢ 1 * b⁻¹ = b⁻¹

a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ a * b = c

Tactic:
h,

Goal state after:
a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ a * (c / a) = c
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case pos
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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑w.asIdeal = 1

Tactic:
h,

Goal state after:
case pos
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 w : HeightOneSpectrum R
inst✝ : Decidable (w = v)
h : w = v
⊢ count K v ↑v.asIdeal = 1
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case e'_2.h
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
v : HeightOneSpectrum R
hv : ↑v.asIdeal ^ exps v ≠ 1
h : v ∈ {x | (fun v ↦ exps v = 0) x}
⊢ False

Tactic:
h,

Goal state after:
case e'_2.h
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
v : HeightOneSpectrum R
hv : ↑v.asIdeal ^ 0 ≠ 1
h : v ∈ {x | (fun v ↦ exps v = 0) x}
⊢ False
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case ofNat.ofNat
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.ofNat b
⊢ x ^ a ≤ x ^ b

Tactic:
exact pow_right_mono₀ hx (Int.le_of_ofNat_le_ofNat h)

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

Goal state before:
pp: x : ℝ≥0∞
m : ℤ
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
obtain hx₀ | hx₀ := eq_or_ne x 0
  · obtain hm | hm | hm := lt_trichotomy m 0 <;>
      simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
  obtain hx | hx := eq_or_ne x ⊤
  · obtain hm | hm | hm := lt_trichotomy m 0 <;>
      simp_all [top_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]
  exact ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add hx₀ hx])

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

Goal state before:
pp: case inl
x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

pp: case inr
x : ℝ
hx : x ≤ 0
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹

Tactic:
· simp [ofReal_inv_of_pos hx]

Goal state after:
case inr
x : ℝ
hx : x ≤ 0
⊢ ENNReal.ofReal x⁻¹ ≤ (ENNReal.ofReal x)⁻¹
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ Bornology.IsBounded (range Subtype.val) ↔ Bornology.IsBounded {x | p x}

Tactic:
Subtype.range_coe_subtype

Goal state after:
α : Type u_1
inst✝ : Bornology α
p : α → Prop
⊢ Bornology.IsBounded {x | p x} ↔ Bornology.IsBounded {x | p x}
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated

Tactic:
exact isCountablyGenerated_pure

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

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : inst✝² = orderBornology
s : Set α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
h,

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : inst✝² = orderBornology
s : Set α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))

Tactic:
exacts [bddBelow_Icc, bddAbove_Icc]

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

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖

Tactic:
rw [mul_min_of_nonneg _ _ (by positivity)]
  refine le_min ?_ (norm_mul_sub_norm_div_le_two_mul u v)
  rw [norm_div_rev, mul_comm]
  exact norm_mul_sub_norm_div_le_two_mul _ _

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∀ (k : ℕ), ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k

Tactic:
intro k

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
k : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

Tactic:
simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩
  rw [ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)] at h
  exact h

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

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

Tactic:
by
  simp only [← ofReal_norm']
  refine ⟨fun h ↦ ?_, fun h ↦ by gcongr⟩
  rw [ENNReal.ofReal_le_ofReal_iff (norm_nonneg' _)] at h
  exact h

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x⌋₊ < ⌈↑x - r⌉₊

Tactic:
floor_natCast,

Goal state after:
x : ℕ
r : ℝ
hr : r < 0
⊢ x < ⌈↑x - r⌉₊
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u → ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
rintro ⟨b, hb⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
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
⊢ ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l f

Tactic:
rintro ⟨b, hb⟩

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 : ∀ᶠ (x : β) in map f l, (fun x1 x2 ↦ x1 ≤ x2) x b
⊢ False
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' univ)

Tactic:
← union_compl_self { x | f x ≤ b },

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x1 x2 ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' ({x | f x ≤ b} ∪ {x | f x ≤ b}ᶜ))
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: case inr
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x u
w : α
l_le_w : l ≤ w
w_le_u : w ≤ u
⊢ l' ≤ u

Tactic:
exact hl'.le.trans (l_le_w.trans w_le_u)

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ ∃ᶠ (x : ι) in f, (u * v) x ≤ U * V

Tactic:
apply (hV.and_eventually (hU.and (h₁.and h₃))).mono

Goal state after:
α : Type u_1
ι : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : Mul α
inst✝³ : Zero α
inst✝² : PosMulMono α
inst✝¹ : MulPosMono α
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun x1 x2 ↦ x2 ≤ x1) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ ∀ (x : ι), v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ ∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ ↑K * ediam s

Tactic:
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ ↑K * ediam s
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
x y : α
⊢ edist ((fun x ↦ b) x) ((fun x ↦ b) y) ≤ ↑0 * edist x y

Tactic:
simp only [edist_self, zero_le]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
K : ℝ≥0
x y : α
⊢ edist ((fun x ↦ b) x) ((fun x ↦ b) y) ≤ ↑K * edist x y

Tactic:
simp only [edist_self, zero_le]

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

Goal state before:
pp: a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ a + -b ≤ c ↔ a ≤ c - -b

Tactic:
refine (le_sub_iff_add_le ?_ ?_).symm

Goal state after:
case refine_1
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊥ ∨ c ≠ ⊥

case refine_2
a b c : EReal
h₁ : b ≠ ⊥ ∨ c ≠ ⊤
h₂ : b ≠ ⊤ ∨ c ≠ ⊥
⊢ -b ≠ ⊤ ∨ c ≠ ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = -(-x✝ * y✝)

Tactic:
h,

Goal state after:
case neg_left
x✝ y✝ : EReal
h : -x✝ * y✝ = -(x✝ * y✝)
⊢ - -x✝ * y✝ = - -(x✝ * y✝)
Module: Mathlib.Data.EReal.Operations

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

Tactic:
← neg_zero

Goal state after:
a b : EReal
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b
Module: Mathlib.Data.EReal.Operations

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

Tactic:
← neg_zero

Goal state after:
a b : EReal
⊢ a * b ≤ -0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: case mp
γ : Type u_3
β : Type u_4
f : γ ↪ β
s : Set (Finset γ)
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b.preimage ⇑f ⋯ ∈ s
⊢ ∃ a, ∀ (b : Finset γ), a ⊆ b → b ∈ s

Tactic:
refine ⟨t.preimage f (by simp), fun x hx ↦ ?_⟩
    simpa [Finset.union_eq_right.mpr hx] using ht (t ∪ x.map f) t.subset_union_left

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

Goal state before:
pp: a b : EReal
⊢ -(a * b) = ⊤ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤

Tactic:
← EReal.neg_mul,

Goal state after:
a b : EReal
⊢ -a * b = ⊤ ↔ a = ⊥ ∧ 0 < b ∨ 0 < a ∧ b = ⊥ ∨ a = ⊤ ∧ b < 0 ∨ a < 0 ∧ b = ⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
have B : ∀ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) =
                                Iic (⨅ (i : s (liminfReparam f s p j)), f i) := by
    intro j
    apply (Iic_ciInf _).symm
    change liminfReparam f s p j ∈ m
    by_cases Hj : j ∈ m
    · simpa only [m, liminfReparam, if_pos Hj] using Hj
    · simp only [m, liminfReparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ | hZ
      · exact hZ
      · exact (hZ j0 hj0).elim

Goal state after:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
A : ⋃ j, ⋂ i, Iic (f ↑i) = ⋃ j, ⋂ i, Iic (f ↑i)
B : ∀ (j : Subtype p), ⋂ i, Iic (f ↑i) = Iic (⨅ i, f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b' = (if b' = b then a / f b else 1) * f b'

Tactic:
h,

Goal state after:
case pos
α : Type u_1
β : Type u_2
L : SummationFilter β
inst✝⁴ : CommGroup α
inst✝³ : TopologicalSpace α
inst✝² : IsTopologicalGroup α
f : β → α
a₁ : α
inst✝¹ : L.LeAtTop
hf : HasProd f a₁ L
b : β
inst✝ : DecidableEq β
a : α
b' : β
h : b' = b
⊢ Function.update f b a b = (if b = b then a / f b else 1) * f b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.HasSupport
h : HasFiniteMulSupport f
⊢ Multipliable f L

Tactic:
apply multipliable_of_ne_finset_one (s := h.toFinset); simp

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

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
classical
  let : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
  have : IsUniformGroup G := isUniformGroup_of_commGroup
  exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
hf : HasFiniteMulSupport f
⊢ ∏'[L] (b : β), f b = ∏ᶠ (b : β), f b

Tactic:
simp [tprod_def, multipliable_of_hasFiniteMulSupport hf, show Set.Finite _ from hf,
    show L.HasSupport by infer_instance]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = Metric.eball (h.symm x) r

Tactic:
← h.isometry.preimage_eball (h.symm x) r,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ⇑h ⁻¹' Metric.eball x r = ⇑h ⁻¹' Metric.eball (h (h.symm x)) r
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
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s

Tactic:
rw [le_principal_iff] at hls

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 : s ∈ l
this : l.NeBot
V : ℕ → Set (X × X)
hV : (𝓤 X).HasAntitoneBasis V
W : ℕ → Set (X × X)
hW : ∀ (n : ℕ), W n ∈ 𝓤 X
hWV : ∀ (n : ℕ), SetRel.comp (W n) (W n) ⊆ V n
hWV' : ∀ (n : ℕ), W n ⊆ V n
⊢ ∀ (n : ℕ), ∃ t ∈ l, t ×ˢ t ⊆ W n ∧ t ⊆ s
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 : ℕ
hm : 2 * (take m L).sum ≤ L.sum
hLm : L.length ≤ m
⊢ False

Tactic:
take_of_length_le hLm,

Goal state after:
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 : ℕ
hm : 2 * L.sum ≤ L.sum
hLm : L.length ≤ m
⊢ False
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ Tendsto (fun n ↦ a - f n) l (𝓝 0) ↔ Tendsto (fun n ↦ f n) l (𝓝 a)

Tactic:
ENNReal.tendsto_nhds_zero,

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
⊢ (∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε) ↔ Tendsto (fun n ↦ f n) l (𝓝 a)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ f n ∈ Icc (a - ε) (a + ε)

Tactic:
refine ⟨?_, (hfa n).trans (le_add_right le_rfl)⟩

Goal state after:
α : Type u_1
l : Filter α
f : α → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
hfa : ∀ (n : α), f n ≤ a
h : ∀ ε > 0, ∀ᶠ (x : α) in l, a - f x ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : α
hn : a - f n ≤ ε
⊢ a - ε ≤ f n
Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝³ : SMul M X
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ p.1 • p.2

Tactic:
rw [(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).isQuotientMap.continuous_iff]
    exact continuous_mk.comp continuous_smul

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 ↦ pkg'.coe (f x)) (pkg.coe a) = g (pkg.coe a)

Tactic:
h,

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)