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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ (if h : a ≤ c ∧ a ≠ 0 ∧ b ≠ 0 then ⋯.choose else 0) * b = c

Tactic:
dif_pos ⟨hac, ha, hb⟩

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
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
⊢ a + spanSingleton R⁰ ⋯.choose * b = c
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ |n|‖ = ‖a ^ n‖

Tactic:
rcases le_total 0 n with hn | hn <;> simp [hn, abs_of_nonneg, abs_of_nonpos]

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

Goal state before:
pp: case inr
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hn : ¬Nonempty α
⊢ SigmaCompactSpace α

Tactic:
· exact ⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
⊢ Icc a b ⊆ s

Tactic:
intro y

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
ha : a ∈ s
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
⊢ y ∈ Icc a b → y ∈ s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
⊢ Icc a b ⊆ s

Tactic:
intro y

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst✝²] (s ∩ Icc a b)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
⊢ y ∈ Icc a b → y ∈ s
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
⊢ Ioi (f a) ⊆ f '' Ioi a

Tactic:
intro y

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atTop
y : δ
⊢ y ∈ Ioi (f a) → y ∈ f '' Ioi a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atBot
⊢ Iio (f a) ⊆ f '' Ioi a

Tactic:
intro y

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Ici a)
htop : Tendsto f atTop atBot
y : δ
⊢ y ∈ Iio (f a) → y ∈ f '' Ioi a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
⊢ Iio (f a) ⊆ f '' Iio a

Tactic:
intro y

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
y : δ
⊢ y ∈ Iio (f a) → y ∈ f '' Iio a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
y : δ
hy : y ∈ Iio (f a)
⊢ y ∈ f '' Iio a

Tactic:
have := intermediate_value_Iic hf hbot (mem_Iic_of_Iio hy)

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atBot
y : δ
hy : y ∈ Iio (f a)
this : y ∈ f '' Iic a
⊢ y ∈ f '' Iio a
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
⊢ Ioi (f a) ⊆ f '' Iio a

Tactic:
intro y

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a : α
f : α → δ
hf : ContinuousOn f (Iic a)
hbot : Tendsto f atBot atTop
y : δ
⊢ y ∈ Ioi (f a) → y ∈ f '' Iio a
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
x✝² x✝¹ : ℝ
hr : x✝² ≤ x✝¹
x✝ : α
⊢ x✝ ∈ (closedBall c x✝¹)ᶜ → x✝ ∈ (closedBall c x✝²)ᶜ

Tactic:
by simpa using hr.trans_lt

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

Goal state before:
pp: n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
simp [Int.norm_eq_abs]

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

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
inst✝ : NoncompactSpace α
⊢ diam univ = 0

Tactic:
simp [diam]

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

Goal state before:
pp: case inr
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
refine ⟨t', fun ev ↦ ?_⟩

Goal state after:
case inr
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 ↦ x1 ≤ x2) x a) → (fun x1 x2 ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x ↦ t' ≤ x) x
⊢ False
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
⊢ ∀ b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a}, ⊤ ≤ b

Tactic:
simpa [eq_univ_iff_forall] using fun b hb => top_unique <| hb _

Goal state after:
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 : ℝ≥0∞
⊢ ∀ (y : EReal), ↑x = y → recENNReal coe neg_coe y ≍ coe x

Tactic:
intro y

Goal state after:
motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
y : EReal
⊢ ↑x = y → recENNReal coe neg_coe y ≍ coe x
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = 0 - ↑↑(-x).toNNReal

Tactic:
coe_nnreal_eq_coe_real,

Goal state after:
case inr
x : ℝ
h : x ≤ 0
⊢ ↑x = 0 - ↑↑(-x).toNNReal
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
a : α
⊢ LipschitzWith 1 (Prod.mk a)

Tactic:
simpa only [max_eq_right zero_le_one] using! (LipschitzWith.const a).prodMk LipschitzWith.id

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
⊢ ∀ ⦃c : β⦄, x < c → limsup u f < c

Tactic:
intro y

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y > x, ∀ᶠ (a : α) in f, u a < y
h' : ∀ y > x, ∃ z, x < z ∧ z < y
y : β
⊢ x < y → limsup u f < y
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg_bot
x✝ : ℝ
h : x✝ < 0
⊢ (↑x✝ * ⊥).toReal = (↑x✝).toReal * ⊥.toReal

Tactic:
| neg_bot _ h =>

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
⊢ ∀ ⦃c : β⦄, c < x → c < limsup u f

Tactic:
intro y

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
y : β
⊢ y < x → y < limsup u f
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r✝ : α
hr✝ : ∀ s ≥ r✝, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r✝ ≤ b''
n : ι
r : α
hr : u n r < b
h : c < u n r
⊢ (Set.Ioo c b).Nonempty

Tactic:
exact ⟨u n r, h, hr⟩

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
c : Set β
⊢ L.support ⊆ c ↔ (map SetLike.coe L.filter).limsInf ⊆ c

Tactic:
simpa [support, limsInf, ofPred_subset] using
    ⟨fun hL b hb x hx ↦ hL x <| hb.mp <| .of_forall fun c hc ↦ hc hx,
      fun hL x hx ↦ singleton_subset_iff.mp <| hL _ <| by simpa using hx⟩

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : b'' < u n r
⊢ u n v ≤ b''

pp: case neg
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : ¬b'' < u n r
⊢ u n v ≤ b''

Tactic:
· refine hrs n v ?_
    calc rs n
    _ = rs (⟨n, by simp [hn]⟩ : {n | b'' < u n r}) := rfl
    _ ≤ ⨆ n : {n | b'' < u n r}, rs n := by
      refine le_ciSup (f := fun (x : {n | b'' < u n r}) ↦ rs x) ?_
        (⟨n, by simp [hn]⟩ : {n | b'' < u n r})
      have : Finite {n | b'' < u n r} := by simpa using! hb''
      exact Finite.bddAbove_range _
    _ ≤ r ⊔ ⨆ n : {n | b'' < u n r}, rs n := le_sup_right
    _ ≤ v := hv

Goal state after:
case neg
ι : Type u_1
α : Type u_7
β : Type u_8
inst✝³ : ConditionallyCompleteLattice α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun r ↦ limsup (fun i ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun x ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun x ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : ι → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ n, rs ↑n ≤ v
n : ι
hn : ¬b'' < u n r
⊢ u n v ≤ b''
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 (g x) = ∏ b ∈ v', f b

Tactic:
· refine ⟨s.image g, fun t ht => ?_⟩
    simp only [← prod_preimage _ _ hg.injOn _ fun x _ => hf x]
    exact ⟨_, (image_subset_iff_subset_preimage _).1 ht, rfl⟩

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

Goal state before:
pp: 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
t' : Finset ↑t
⊢ ∏ x ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ t) t', f x ∈ o

Tactic:
apply hs

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
t' : Finset ↑t
⊢ ∀ ⦃a : β⦄, a ∈ Finset.map (Embedding.subtype fun x ↦ x ∈ t) t' → a ∉ s
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

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

Tactic:
by
  rw [hasProd_subtype_iff_mulIndicator] at *
  rw [Set.mulIndicator_union_of_disjoint hs]
  exact ha.mul hb

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

Goal state before:
pp: case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ e ∈ Filter.map (fun s ↦ ∏' (a : { x // x ∉ s }), f ↑a) atTop

Tactic:
simp only [Filter.mem_map, mem_atTop_sets, Set.mem_preimage]

Goal state after:
case pos
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
H : Multipliable f
e : Set G
he : e ∈ 𝓝 1
s : Finset α
hs : ∀ (t : Set α), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
⊢ ∃ a, ∀ (b : Finset α), a ⊆ b → ∏' (a : { x // x ∉ b }), f ↑a ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f ↑↑n) * ∏' (n : ℕ+), f (-↑↑n)

Tactic:
have h2 : Multipliable fun n : ℕ ↦ f (-n) :=
    (multipliable_int_iff_multipliable_nat_and_neg.mp hf2).2

Goal state after:
G : Type u_2
inst✝⁴ : CommGroup G
inst✝³ : UniformSpace G
inst✝² : IsUniformGroup G
inst✝¹ : CompleteSpace G
inst✝ : T2Space G
f : ℤ → G
hf2 : Multipliable f
h1 : Multipliable fun n ↦ f ↑n
h2 : Multipliable fun n ↦ f (-↑n)
⊢ ∏' (n : ℤ), f n = (f 0 * ∏' (n : ℕ+), f ↑↑n) * ∏' (n : ℕ+), f (-↑↑n)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun i ↦ |x i|
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

Tactic:
rw [isBoundedUnder_le_abs, not_and_or] at hbdd

Goal state after:
ι : Type u_4
l : Filter ι
x : ι → ℝ
hf : liminf (fun i ↦ ↑(Real.nnabs (x i))) l ≠ ∞
hbdd : ¬IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l x ∨ ¬IsBoundedUnder (fun x1 x2 ↦ x2 ≤ x1) l x
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
⊢ ∀ (b_1 : ℝ≥0∞), (∀ᶠ (n : ι) in f, b_1 ≤ u n) → b_1 ≤ b

Tactic:
intro y

Goal state after:
ι : Type u_4
f : Filter ι
u : ι → ℝ≥0∞
inst✝ : f.NeBot
b : ℝ≥0∞
b_ne_top : b ≠ ∞
le_b : ∀ᶠ (i : ι) in f, u i ≤ b
y : ℝ≥0∞
⊢ (∀ᶠ (n : ι) in f, y ≤ u n) → y ≤ b
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
⊢ CauchySeq fun n ↦ ∏ k ∈ range (n + 1), u k

Tactic:
let d : ℕ → E := fun n => ∏ k ∈ range (n + 1), u k / v k

Goal state after:
E : Type u_2
inst✝ : SeminormedCommGroup E
u v : ℕ → E
N : ℕ
huv : ∀ n ≥ N, u n = v n
hv : CauchySeq fun n ↦ ∏ k ∈ range (n + 1), v k
d : ℕ → E := fun n ↦ ∏ k ∈ range (n + 1), u k / v k
⊢ CauchySeq fun n ↦ ∏ k ∈ range (n + 1), u k
Module: Mathlib.Analysis.Normed.Group.Bounded

Goal state before:
pp: E : Type u_2
inst✝³ : SeminormedGroup E
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : DiscreteTopology X
inst✝ : ProperSpace E
e : X → E
he : Topology.IsClosedEmbedding e
⊢ Tendsto (norm ∘ e) Filter.cofinite atTop

Tactic:
rw [← Filter.cocompact_eq_cofinite X]
  apply tendsto_norm_cocompact_atTop'.comp (Topology.IsClosedEmbedding.tendsto_cocompact he)

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

Goal state before:
pp: α : Type u_1
inst✝² : SeminormedRing α
inst✝¹ : NormOneClass α
inst✝ : NormMulClass α
m : ℕ
hm : m ≠ 0
⊢ Tendsto (fun x ↦ x ^ m) (cobounded α) (cobounded α)

Tactic:
simpa [← tendsto_norm_atTop_iff_cobounded] using!
    (tendsto_pow_atTop hm).comp (tendsto_norm_cobounded_atTop (E := α))

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : Y), edist (e.symm.toFun x) (e.symm.toFun y) = ↑r * edist x y

Tactic:
by
    refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩
    simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]
    rw [← mul_assoc, ← ENNReal.coe_mul, inv_mul_cancel₀ (ratio_ne_zero e),
      ENNReal.coe_one, one_mul]

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

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

Tactic:
rw [dist_comm]

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
hs₀ : ∀ x ∈ s, x ≠ 0
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : dist x y ≤ ε * r ^ 2
⊢ ‖x‖⁻¹ * dist x y * ‖y‖⁻¹ ≤ r⁻¹ * (ε * r ^ 2) * r⁻¹
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 (⋂₀ s)

Tactic:
rw [sInter_eq_biInter]

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, MeasurableSet t
⊢ MeasurableSet (⋂ i ∈ s, i)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s t u : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h : univ ⊆ s ∪ t
hsu : MeasurableSet (Subtype.val ⁻¹' u)
htu : MeasurableSet (Subtype.val ⁻¹' u)
⊢ u = Subtype.val '' Subtype.val ⁻¹' u ∪ Subtype.val '' Subtype.val ⁻¹' u

Tactic:
simp [image_preimage_eq_inter_range, ← inter_union_distrib_left, univ_subset_iff.1 h]

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

Goal state before:
pp: β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
⊢ measurableAtom x ⊆ measurableAtom y

Tactic:
intro z hz
  simp only [measurableAtom, mem_iInter] at hz hx ⊢
  exact fun s hys hs ↦ hz s (hx s hys hs) hs

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

Goal state before:
pp: case pos
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : x ∈ measurableAtom y
hy : y ∈ measurableAtom x
⊢ measurableAtom y ⊆ measurableAtom x

Tactic:
exact measurableAtom_subset_of_mem hy

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

Goal state before:
pp: α : Type u_1
m : OuterMeasure α
s : ℕ → Set α
h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)
h0 : ∑' (k : ℕ), m (s (k + 1) \ s k) ≠ ∞
⊢ m (⋃ n, s n) = ⨆ n, m (s n)

Tactic:
refine measure_iUnion_of_tendsto_zero m atTop ?_
  refine tendsto_nhds_bot_mono' (ENNReal.tendsto_sum_nat_add _ h0) fun n => ?_
  refine (m.mono ?_).trans (measure_iUnion_le _)
  -- Current goal: `(⋃ k, s k) \ s n ⊆ ⋃ k, s (k + n + 1) \ s (k + n)`
  have h' : Monotone s := @monotone_nat_of_le_succ (Set α) _ _ h_mono
  simp only [sdiff_subset_iff, iUnion_subset_iff]
  intro i x hx
  have : ∃ i, x ∈ s i := by exists i
  rcases Nat.findX this with ⟨j, hj, hlt⟩
  clear hx i
  rcases le_or_gt j n with hjn | hnj
  · exact Or.inl (h' hjn hj)
  have : j - (n + 1) + n + 1 = j := by lia
  refine Or.inr (mem_iUnion.2 ⟨j - (n + 1), ?_, hlt _ ?_⟩)
  · rwa [this]
  · rw [← Nat.succ_le_iff, Nat.succ_eq_add_one, this]

Goal state after: