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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hd : Disjoint u (Ioi x)
⊢ IsMax x

Tactic:
by_contra hx

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
x : α
u : Set α
hu : u ∈ 𝓝 x
hd : Disjoint u (Ioi x)
hx : ¬IsMax x
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst✝³] (Ioo a b) = Icc a b

Tactic:
by
  apply Subset.antisymm
  · exact closure_minimal Ioo_subset_Icc_self isClosed_Icc
  · rcases hab.lt_or_gt with hab | hab
    · rw [← sdiff_subset_closure_iff, Icc_sdiff_Ioo_same hab.le]
      have hab' : (Ioo a b).Nonempty := nonempty_Ioo.2 hab
      simp only [insert_subset_iff, singleton_subset_iff]
      exact ⟨(isGLB_Ioo hab).mem_closure hab', (isLUB_Ioo hab).mem_closure hab'⟩
    · rw [Icc_eq_empty_of_lt hab]
      exact empty_subset _

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
⊢ ∃ r, 0 < r ∧ IsCompact (closedBall x r)

Tactic:
have : ∀ᶠ r in 𝓝[>] 0, IsCompact (closedBall x r) :=
    eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)
  simpa only [and_comm] using (this.and self_mem_nhdsWithin).exists

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ interior (Ioi a) ∩ interior (Iic b) = Ioo a b

Tactic:
interior_Ioi,

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioi a ∩ interior (Iic b) = Ioo a b
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Tactic:
exact isLUB_of_mem_nhds hsa (mem_principal_self s)

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
⊢ b ∈ upperBounds (f '' s)

Tactic:
rintro _ ⟨x, hx, rfl⟩

Goal state after:
α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
⊢ f x ≤ b
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 ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
by
  lift r to ℝ≥0 using hr.le
  simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb✝ : x ≤ b
hxb : x < b
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b

Tactic:
have : s ∩ Iio b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Iio_mem_nhds hxb)

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : Tendsto f (𝓝[s] x) (𝓝 (f x))
this✝ : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb✝ : x ≤ b
hxb : x < b
this : s ∩ Iio b ∈ 𝓝[s] x
⊢ ∀ᶠ (c : α) in 𝓝[s] x, f c ≤ f b
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
f : α → β
s : Set α
Cf : ContinuousWithinAt f s (sSup s)
Mf : MonotoneOn f s
fbot : f ⊥ = ⊥
h : s.Nonempty
⊢ f (sSup s) = sSup (f '' s)

Tactic:
· exact Mf.map_csSup_of_continuousWithinAt Cf h

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c

Tactic:
exact this.1

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

Goal state before:
pp: α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ ↑(nndist (s.mulIndicator f x) (t.mulIndicator f x)) = ↑‖(s ∆ t).mulIndicator f x‖₊

Tactic:
nndist_mulIndicator

Goal state after:
α : Type u_2
E : Type u_5
inst✝ : SeminormedGroup E
s t : Set α
f : α → E
x : α
⊢ ↑‖(s ∆ t).mulIndicator f x‖₊ = ↑‖(s ∆ t).mulIndicator f x‖₊
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ (normalizedFactors I ∩ normalizedFactors J).prod ≠ ⊥

Tactic:
exact prod_inter_normalizedFactors_ne_zero I J

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

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)

Tactic:
exact hK.isCompact_closure.inter_right hs

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioc (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, b < f b_1

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
· filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le
      (h_mono has hxs hxa)

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Module: Mathlib.Topology.Order.MonotoneContinuity

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b

Tactic:
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[≥] a
hfs : ∀ b > f a, ∃ c ∈ s, f c ∈ Ioo (f a) b
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[≥] a, f b_1 < b
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: ι : Type u_3
α : Type u_4
f : ι → α → ℝ≥0∞
s : Finset α
inst✝ : Nonempty ι
h : ∀ (t : Finset α) (i j : ι), ∃ k, ∀ a ∈ t, f k a ≤ f i a ∧ f k a ≤ f j a
⊢ ⨅ i, ∑ a ∈ s, f i a = ∑ a ∈ s, ⨅ i, f i a

Tactic:
induction s using Finset.cons_induction_on with

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

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

Tactic:
· exact imp_iff_not_or.2 (hf (by simp [hj]) (by simp) <| ne_of_mem_of_not_mem hj hi).symm hi₀

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

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

Tactic:
have hb' := (tendsto_atTop.mp hf) b'

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

Goal state before:
pp: case bot.bot
⊢ (⊥ + ⊥).toENNReal ≤ ⊥.toENNReal + ⊥.toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ (⊥ + ↑a✝).toENNReal ≤ ⊥.toENNReal + (↑a✝).toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case bot.top
⊢ (⊥ + ⊤).toENNReal ≤ ⊥.toENNReal + ⊤.toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ (↑a✝ + ⊥).toENNReal ≤ (↑a✝).toENNReal + ⊥.toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ (↑a✝¹ + ↑a✝).toENNReal ≤ (↑a✝¹).toENNReal + (↑a✝).toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ (↑a✝ + ⊤).toENNReal ≤ (↑a✝).toENNReal + ⊤.toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case top.bot
⊢ (⊤ + ⊥).toENNReal ≤ ⊤.toENNReal + ⊥.toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ (⊤ + ↑a✝).toENNReal ≤ ⊤.toENNReal + (↑a✝).toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case top.top
⊢ (⊤ + ⊤).toENNReal ≤ ⊤.toENNReal + ⊤.toENNReal

Tactic:
{· simp}

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

Goal state before:
pp: case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
iSup_option,

Goal state after:
case h_option
R : Type u_3
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝¹ : Finite ι
α✝ : Type u_4
inst✝ : Fintype α✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : Option α✝ → Ideal R
⊢ emultiplicity p.asIdeal (I none ⊔ ⨆ b, I (some b)) = ⨅ i, emultiplicity p.asIdeal (I i)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : EReal
hx : ¬0 ≤ x
H₁ : 0 < -x
⊢ x = -↑(-x).toENNReal

Tactic:
by rw [coe_toENNReal H₁.le, neg_neg]

Goal state after:
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
by
  simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]

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

Goal state before:
pp: a : EReal
b : ℝ
⊢ a + ↑b - ↑b = a

Tactic:
by
  cases a <;> norm_cast
  exact _root_.add_sub_cancel_right _ _

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}
t : Set α
h : x ∉ t
⊢ t ∉ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}

Tactic:
· exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩

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

Goal state before:
pp: case bot_bot
⊢ (⊥ * ⊥).toReal = ⊥.toReal * ⊥.toReal

Tactic:
| bot_bot =>

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

Goal state before:
pp: case bot_bot
⊢ 0 < ⊥ * ⊥ ↔ 0 < ⊥ ∧ 0 < ⊥ ∨ ⊥ < 0 ∧ ⊥ < 0

Tactic:
| bot_bot =>

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

Goal state before:

Tactic:
r
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_left
    _ ≤ v := hv

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

Goal state before:
pp: case bot_bot
⊢ ⊥ * ⊥ = ⊤ ↔ ⊥ = ⊥ ∧ ⊥ < 0 ∨ ⊥ < 0 ∧ ⊥ = ⊥ ∨ ⊥ = ⊤ ∧ 0 < ⊥ ∨ 0 < ⊥ ∧ ⊥ = ⊤

Tactic:
| bot_bot =>

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

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

Tactic:
| inr hx0 =>

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
⊢ ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f (g b)

Tactic:
refine ⟨s.preimage g hg.injOn, fun t ht => ?_⟩

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
⊢ ∃ u', s ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ t, f (g b)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

Tactic:
obtain ⟨s, hs⟩ := vanish e he
    refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
    split_ifs at ht with h
    · exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)
    · exact fun _ _ hs ↦ h ⟨_, hs⟩

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

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
⊢ HasProd g (c * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i))

Tactic:
refine (Tendsto.mul_const ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) hc).congr' ?_

Goal state after:
α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
⊢ (fun x ↦ (∏ b ∈ x, f b) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i)) =ᶠ[(SummationFilter.unconditional α).filter] fun s ↦
    ∏ b ∈ s, g b
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : Set β
f : β → α
⊢ ∏' (x : ↑s), f ↑x = ∏' (x : β), s.mulIndicator f x

Tactic:
rw [← tprod_subtype_eq_of_mulSupport_subset Set.mulSupport_mulIndicator_subset, tprod_congr]
  simp

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
i : β
h₀ : i ∈ ⋃ d, s d
⊢ (⋃ d, s d).mulIndicator f i = ∏' (d : γ), (s d).mulIndicator f i

Tactic:
simp only [h₀, hs, Set.mulIndicator_of_mem, tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem]

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

Goal state before:
pp: case succ
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ (fun x ↦ x ^ (n✝ + 1)) = ⇑(NNReal.powOrderIso (n✝ + 1) hn).withTopCongr

Tactic:
ext (_ | _)

Goal state after:
case succ.none
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
⊢ none ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr none

case succ.some
ι : Sort u_1
n n✝ : ℕ
hn : n✝ + 1 ≠ 0
val✝ : NNReal
⊢ some val✝ ^ (n✝ + 1) = (NNReal.powOrderIso (n✝ + 1) hn).withTopCongr (some val✝)
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
x y : X
l : List X
⊢ (zipWith d (l ++ [y]) (x :: l)).sum = (zipWith d (x :: l) (l ++ [y])).sum

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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length

Tactic:
zipWith_comm_of_comm dist_comm

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
x y : X
l : List X
⊢ (zipWith d (x :: l) (l ++ [y])).sum = (zipWith d (x :: l) (l ++ [y])).sum

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
x y : X
l : List X
⊢ (y :: l.reverse).length = (l.reverse ++ [x]).length
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedGroup E
x : E
⊢ x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] {1} ↔ ‖x‖ = 0

Tactic:
by
  rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
⊢ HasProd g a

Tactic:
classical
  refine (atTop_basis.tendsto_iff (closed_nhds_basis a)).mpr ?_
  rintro s ⟨hs, hsc⟩
  rcases mem_atTop_sets.mp (ha hs) with ⟨u, hu⟩
  use u.image Sigma.fst, trivial
  intro bs hbs
  simp only [Set.mem_preimage] at hu
  have : Tendsto (fun t : Finset (Σ b, γ b) ↦ ∏ p ∈ t with p.1 ∈ bs, f p) atTop
      (𝓝 <| ∏ b ∈ bs, g b) := by
    simp only [← sigma_preimage_mk, prod_sigma]
    refine tendsto_finsetProd _ fun b _ ↦ ?_
    change
      Tendsto (fun t ↦ (fun t ↦ ∏ s ∈ t, f ⟨b, s⟩) (preimage t (Sigma.mk b) _)) atTop (𝓝 (g b))
    exact (hf b).comp (tendsto_finset_preimage_atTop_atTop (sigma_mk_injective))
  refine hsc.mem_of_tendsto this (eventually_atTop.2 ⟨u, fun t ht ↦ hu _ fun x hx ↦ ?_⟩)
  exact mem_filter.2 ⟨ht hx, hbs <| mem_image_of_mem _ hx⟩

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Bornology α
inst✝¹ : Bornology β
inst✝ : Bornology γ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: case refine_3
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
hM_lt : M < L.length
hM_ltx : M < (x :: l).length
hM_lty : M < (l ++ [y]).length
⊢ d (l ++ [y])[M] y ≤ L.sum

Tactic:
rcases hMl.eq_or_lt with (rfl | hMl)
    · simp only [getElem_append_right le_rfl, getElem_singleton, dist_self, zero_le]
    rw [getElem_append_left hMl]
    have hlen : length (drop (M + 1) l) = length l - (M + 1) := length_drop
    have hlen_lt : length l - (M + 1) < length l := Nat.sub_lt_of_pos_le M.succ_pos hMl
    refine (ihn _ hlen_lt _ y _ hlen).trans ?_
    rw [cons_getElem_drop_succ]
    have hMs' : L.sum ≤ 2 * (L.take (M + 1)).sum :=
      not_lt.1 fun h => (hMs.2 h.le).not_gt M.lt_succ_self
    rw [← sum_take_add_sum_drop L (M + 1), two_mul, add_le_add_iff_left, ← add_le_add_iff_right,
      sum_take_add_sum_drop, ← two_mul] at hMs'
    convert! hMs'
    rwa [drop_zipWith, drop, drop_append_of_le_length]

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

Goal state before:
pp: X✝ : Type u_1
X : Type u_2
t : TopologicalSpace X
inst✝ : TopologicalSpace.PseudoMetrizableSpace X
⊢ PseudoMetricSpace.toUniformSpace = TopologicalSpace.pseudoMetrizableSpaceUniformity X

Tactic:
by
  with_reducible_and_instances rfl

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

Goal state before:
pp: X✝ : Type u_1
X : Type u_2
t : TopologicalSpace X
inst✝ : TopologicalSpace.MetrizableSpace X
⊢ (TopologicalSpace.metrizableSpaceMetric X).toPseudoMetricSpace = TopologicalSpace.pseudoMetrizableSpacePseudoMetric X

Tactic:
by
  with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b : α
h : b ⊓ -b ≤ a ⊓ -a
⊢ -(-a ⊓ a) ≤ - -b ⊔ -b

Tactic:
rwa [← neg_inf, neg_le_neg_iff, inf_comm _ b, inf_comm _ a]

Goal state after: