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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ (Finite.toFinset hf).erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : Associated v.asIdeal w.asIdeal
⊢ False

Tactic:
associated_iff_eq

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ (Finite.toFinset hf).erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
hw_prime : Prime w.asIdeal
hvw : v.asIdeal = w.asIdeal
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2.refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ { q' // x < ↑q' }

pp: case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑?refine_2.refine_2 ≤ f ↑q

Tactic:
· exact ⟨y, hxy⟩

Goal state after:
case refine_2.refine_3
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
q : ↑(Ioi x)
hq : x < ↑q
y : ℚ
hxy : x < ↑y
hyq : ↑y < ↑q
⊢ f ↑↑⟨y, hxy⟩ ≤ f ↑q
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ⋂ r, Iic ↑r = ∅

Tactic:
by
  exact iInter_Iic_eq_empty_iff.mpr not_bddBelow_coe

Goal state after:
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 : Ideal R
hI : I ≠ 0
| ↑I

Tactic:
← Ideal.finprod_heightOneSpectrum_factorization hI

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 : Ideal R
hI : I ≠ 0
| ↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
hb : 0 ≤ b
⊢ a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b

Tactic:
lift a to ℝ≥0 using ha
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.le_toNNReal_iff_coe_le hb

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

Goal state before:
pp: x y : ℝ≥0
⊢ ofNNReal '' uIoc x y = uIoc ↑x ↑y

Tactic:
simp [uIoc]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁶ : Semifield 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup G
inst✝² : PartialOrder G
inst✝¹ : MulActionWithZero 𝕜 G
inst✝ : PosSMulStrictMono 𝕜 G
a : 𝕜
ha : 0 < a
b₁ b₂ : G
h : a • b₁ < a • b₂
⊢ b₁ < b₂

Tactic:
by simpa [ha.ne'] using smul_lt_smul_of_pos_left h <| inv_pos.2 ha

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

Goal state before:
pp: x : EReal
h : x ≠ ⊤
⊢ x ≤ ↑x.toReal

Tactic:
by
  by_cases h' : x = ⊥
  · simp only [h', bot_le]
  · simp only [le_refl, coe_toReal h h']

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

Goal state before:
pp: x z : EReal
h : x < z
a : EReal
ha₁ : x < a
ha₂ : a < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ⊤ = Ioi x

Tactic:
rw [← Ioi_inter_Iio]
  simp

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ⊥ ↑y = Iio y

Tactic:
rw [← Ioi_inter_Iio]
  simp

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Tactic:
rw [← Ioi_inter_Iio]
  simp

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

Goal state before:
pp: b c a : ℝ≥0∞
h0 : b ≠ 0 ∨ c ≠ 0
htop : b ≠ ∞ ∨ c ≠ ∞
⊢ a / b * c = a / (b / c)

Tactic:
by
  simp only [div_eq_mul_inv]
  rw [ENNReal.mul_inv, inv_inv]
  · ring
  · simpa
  · simpa

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

Goal state before:
pp: a b c : ℝ≥0∞
h : ∀ a' < a, ∀ b' < b, a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
by
  refine le_of_forall_lt_imp_le_of_dense fun d hd ↦ ?_
  obtain ⟨a', ha', hd⟩ := exists_lt_mul_left hd
  obtain ⟨b', hb', hd⟩ := exists_lt_mul_right hd
  exact le_trans hd.le <| h _ ha' _ hb'

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ eball x r ×ˢ eball y r ↔ z ∈ eball (x, y) r

Tactic:
by simp [Prod.edist_eq]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
y : β
r : ℝ≥0∞
z : α × β
⊢ z ∈ closedEBall x r ×ˢ closedEBall y r ↔ z ∈ closedEBall (x, y) r

Tactic:
by simp [Prod.edist_eq]

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α✝
γ : Type w
inst✝ : EMetricSpace γ
α : Type u
inst : PseudoEMetricSpace α
⊢ (uniformSpaceOfEDist edist ⋯ ⋯ ⋯).toTopologicalSpace ≤ toUniformSpace.toTopologicalSpace

Tactic:
rw [uniformSpace_edist]

Goal state after:
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddAbove s
⊢ sInf (a • s) = a • sSup s

Tactic:
· rw [Real.sInf_of_not_bddBelow (mt (bddBelow_smul_iff_of_neg ha').1 h),
        Real.sSup_of_not_bddAbove h, smul_zero]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
⊢ ∀ (x : ℝ), |x - x| = 0

Tactic:
by simp [abs_zero]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
isUniformEmbedding_iff,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ IsUniformInducing f ∧ Function.Injective f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ closure[inst✝³] (Ioi a) ⊆ Ici a

pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure[inst✝³] (Ioi a)

Tactic:
· exact closure_minimal Ioi_subset_Ici_self isClosed_Ici

Goal state after:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a ⊆ closure[inst✝³] (Ioi a)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case h₂.inr
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab✝ : a ≠ b
hab : b < a
⊢ ∅ ⊆ closure[inst✝³] (Ioo a b)

Tactic:
exact empty_subset _

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
⊢ dist f g ≤ ↑r ↔ ∀ (b : β), dist (f b) (g b) ≤ ↑r
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: q : ℚ≥0
⊢ ‖↑q‖₊ = ↑q

Tactic:
by
  simp [nnnorm]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
⊢ c = d

Tactic:
have : f (x c) = f (x d) := by simp [hcd]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
this : f (x c) = f (x d)
⊢ c = d
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ SecondCountableTopology α

Tactic:
suffices SigmaCompactSpace α from EMetric.secondCountable_of_sigmaCompact α
  rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn)
  · exact ⟨⟨fun n => closedBall x n, fun n => isCompact_closedBall _ _, iUnion_closedBall_nat _⟩⟩
  · exact ⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (closedBall x r)

Tactic:
closedBall_pi _ hr

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
h : ∀ (b : β), ProperSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ IsCompact (univ.pi fun b ↦ closedBall (x b) r)
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε

Tactic:
let u := { a : α × α | dist a.fst a.snd < ε }

Goal state after:
case mp
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : UniformCauchySeqOn F atTop s
ε : ℝ
hε : ε > 0
u : Set (α × α) := {a | dist a.1 a.2 < ε}
⊢ ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
⊢ UniformCauchySeqOn F atTop s

Tactic:
u

Goal state after:
case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
h : ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
u : Set (α × α)
⊢ u ∈ 𝓤 α → ∀ᶠ (m : β × β) in atTop ×ˢ atTop, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u
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.comap (↑I').subtype (Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I)) =
    ⊤

Tactic:
← top_le_iff,

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.map (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.comap (↑I').subtype (Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I))
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
hb : ∀ (n : ℕ), 0 < b n
⊢ ∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n

Tactic:
by
  rw [cauchySeq_iff] at hu
  have hu' : ∀ k, ∀ᶠ (n : ℕ) in atTop, ∀ m ≥ n, dist (u m) (u n) < b k := by
    intro k
    rw [eventually_atTop]
    obtain ⟨N, hN⟩ := hu (b k) (hb k)
    exact ⟨N, fun m hm r hr => hN r (hm.trans hr) m hm⟩
  exact Filter.extraction_forall_of_eventually hu'

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

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddBelow (closedBall 0 r)

Tactic:
simp [Int.closedBall_eq_Icc]

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

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddAbove (closedBall 0 r)

Tactic:
simp [Int.closedBall_eq_Icc]

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

Goal state before:
pp: case inl
r : ℝ
hr : 0 ≤ r
⊢ BddAbove (closedBall 0 r)

Tactic:
simp [closedBall_zero_eq_Icc, *]

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

Goal state before:
pp: case inr
r : ℝ
hr : r < 0
⊢ BddAbove (closedBall 0 r)

Tactic:
simp [closedBall_zero_eq_Icc, *]

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

Goal state before:
pp: a b : ℚ
⊢ TotallyBounded (Icc a b)

Tactic:
by
  simpa only [preimage_cast_Icc]
    using totallyBounded_preimage Rat.isUniformEmbedding_coe_real.isUniformInducing
      (totallyBounded_Icc (a : ℝ) b)

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

Goal state before:
pp: case inr
x y z t : EReal
h1 : x < y
h2 : z < t
hx : x ≠ ⊥
⊢ x + z < y + t

Tactic:
· lift x to ℝ using ⟨h1.ne_top, hx⟩
    calc (x : EReal) + z < x + t := add_lt_add_left_coe h2 _
    _ ≤ y + t := by gcongr

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_6
ι' : Type u_7
f : ι → α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
hv : v.HasBasis p s
⊢ liminf f v = sSup (⋃ j, ⋂ i, Iic (f ↑i))

Tactic:
by
  simp_rw [liminf_eq, hv.eventually_iff]
  congr 1
  ext x
  simp only [mem_ofPred_eq, iInter_coe_set, mem_iUnion, mem_iInter, mem_Iic, Subtype.exists,
    exists_prop]

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
u : β → α
a : α
hinf : a ≤ liminf u ⊥
hsup : limsup u ⊥ ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) ⊥ u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) ⊥ u
⊢ Tendsto u ⊥ (𝓝 a)

Tactic:
exact tendsto_bot

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

Goal state before:
pp: case coe
b a✝ : ℝ
⊢ a✝ + b - b = a✝

Tactic:
exact _root_.add_sub_cancel_right _ _

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

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

Tactic:
refine lt_add_of_pos_right y ?_

Goal state after:
case neg
x z t : EReal
h' : z < t
hx_top : x ≠ ⊤
y : ℝ
h : x ≤ ↑y
hy_bot : ↑y ≠ ⊥
hy_top : ¬↑y = ⊤
hxy : x = ↑y
htz_top : ¬t - z = ⊤
⊢ 0 < (t - z).toReal
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Preorder β
f : β → Finset α
h : Monotone f
h' : ∀ (x : α), ∃ n, x ∈ f n
⊢ Tendsto f atTop atTop

Tactic:
by
  simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
  intro a
  rcases h' a with ⟨b, hb⟩
  exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')

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:
by
  rw [← neg_eq_top_iff, ← EReal.neg_mul, mul_eq_top, neg_eq_bot_iff, neg_eq_top_iff,
    neg_lt_comm, lt_neg_comm, neg_zero]
  tauto

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

Goal state before:
pp: this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ Filter.map (fun x ↦ Finset.range (x + 1)) atTop = Filter.map Finset.range atTop

Tactic:
apply le_antisymm <;>
      rw [← Tendsto] <;>
      simp only [tendsto_atTop', mem_map, mem_atTop_sets, mem_preimage]

Goal state after:
case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ ∀ (s : Set (Finset ℕ)),
    (∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s) → ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s

case a
this : ∀ (n : ℕ), Finset.Iic n = Finset.range (n + 1)
⊢ ∀ (s : Set (Finset ℕ)),
    (∃ a, ∀ (b : ℕ), a ≤ b → Finset.range (b + 1) ∈ s) → ∃ a, ∀ (b : ℕ), a ≤ b → Finset.range b ∈ s
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
hL : ¬L.NeBot
f : β → α
a : α
this : L.filter = ⊥
⊢ Tendsto (fun s ↦ ∏ b ∈ s, f b) ⊥ (𝓝 a)

Tactic:
exact tendsto_bot

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

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

Tactic:
simp only [tprod_def, dif_pos (multipliable_bot hL f)]
  have : L.LeAtTop := L.leAtTop_of_not_NeBot hL
  rw [L.support_eq_univ, Set.inter_univ, Set.mulIndicator_univ]
  by_cases hf : (mulSupport f).Finite
  · rw [eq_true_intro hf, if_pos]
    simp only [and_true]
    infer_instance
  · rwa [if_neg (by tauto), if_pos (hasProd_bot hL _ _), finprod_of_infinite_mulSupport]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ b, b < a
⊢ liminf f (𝓝[<] a) = ⨆ r, ⨆ (_ : r < a), f r

Tactic:
rw [(nhdsLT_basis_of_exists_lt hb).liminf_eq_iSup_iInf]
  refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)
  obtain ⟨b, hb⟩ := exists_between hr
  exact ⟨b, hb.2, iInf₂_le b hb⟩

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 * ((∏' (b : β), f b) / f b)

Tactic:
exact (mul_div_cancel _ _).symm

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
⊢ ∏' (b : ↑t), f ↑b ∈ o

Tactic:
by_cases ht : Multipliable fun a : t ↦ f a

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : Multipliable fun a ↦ f ↑a
⊢ ∏' (b : ↑t), f ↑b ∈ o

case neg
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : CommGroup α
inst✝ : IsUniformGroup α
f : β → α
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ e
e : Set α
he : e ∈ 𝓝 1
o : Set α
ho : o ∈ 𝓝 1
o_closed : IsClosed[inst✝².toTopologicalSpace] o
oe : o ⊆ e
s : Finset β
hs : ∀ (t : Finset β), (∀ ⦃a : β⦄, a ∈ t → a ∉ s) → ∏ b ∈ t, f b ∈ o
t : Set β
hts : ∀ ⦃a : β⦄, a ∈ t → a ∉ ↑s
ht : ¬Multipliable fun a ↦ f ↑a
⊢ ∏' (b : ↑t), f ↑b ∈ o
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: ι : Type u_4
α : Type u_5
L : SummationFilter ι
inst✝⁶ : CommMonoid α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedMonoid α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
f : ι → α
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
hf : ∀ (i : ι), 1 ≤ f i
⊢ HasProd f 1 L ↔ f = 1

Tactic:
refine ⟨fun hf' ↦ ?_, ?_⟩
  · ext i
    exact (hf i).antisymm' (le_hasProd hf' _ fun j _ ↦ hf j)
  · rintro rfl
    exact hasProd_one

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ (∏ x ∈ s, f x) * ∏' (x : { x // x ∉ s }), f ↑x = (∏' (x : ↑↑s), f ↑x) * ∏' (x : ↑(↑s)ᶜ), f ↑x

Tactic:
simp only [Finset.tprod_subtype', mul_right_inj]

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : CommGroup α
inst✝² : IsUniformGroup α
inst✝¹ : CompleteSpace α
inst✝ : T2Space α
f : β → α
hf : Multipliable f
s : Finset β
⊢ ∏' (x : { x // x ∉ s }), f ↑x = ∏' (x : ↑(↑s)ᶜ), f ↑x
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ (∏'[L] (b' : β), if b' = b then a b' else 1) = a b

Tactic:
rw [tprod_eq_mulSingle b]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ (if b = b then a b else 1) = a b

α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
b : β
inst✝¹ : DecidablePred fun x ↦ x = b
a : β → α
L : SummationFilter β
inst✝ : L.LeAtTop
⊢ ∀ (b' : β), b' ≠ b → (if b' = b then a b' else 1) = 1