mathlib-initiative/mathlib-tactics huggingface dataset:
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 : t ∈ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
⊢ x ∈ t

Tactic:
contrapose h

Goal state after:
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}
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -(a' + b')

Tactic:
neg_add (.inr hb'.ne_top) (.inl ha'.ne_top)

Goal state after:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
a' : EReal
ha' : a' < -a
b' : EReal
hb' : b' < -b
⊢ c ≤ -a' - b'
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b : EReal
h : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0

Tactic:
cases a

Goal state after:
case bot
b : EReal
h : ⊥ ≠ 0 ∧ b ≠ 0
⊢ ⊥ * b ≠ 0

case coe
b : EReal
a✝ : ℝ
h : ↑a✝ ≠ 0 ∧ b ≠ 0
⊢ ↑a✝ * b ≠ 0

case top
b : EReal
h : ⊤ ≠ 0 ∧ b ≠ 0
⊢ ⊤ * b ≠ 0
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
⊢ liminf f v =
    if ∃ j, s ↑j = ∅ then sSup univ
    else if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i

Tactic:
if_neg H

Goal state after:
case neg
α : 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 : ι → α
H : ¬∃ j, s ↑j = ∅
⊢ liminf f v = if ∀ (j : Subtype p), ¬BddBelow (range fun i ↦ f ↑i) then sSup ∅ else ⨆ j, ⨅ i, f ↑i
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun x1 x2 ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) F
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
l : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ ∀ (x : R), m < x → f x ≤ f m

Tactic:
exact fun x hx ↦ f_decr hx.le

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 * ∏' (n : β), if n = b then 1 else f n

Tactic:
(hasProd_ite_div_hasProd hf.hasProd b).tprod_eq

Goal state after:
α : 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)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : ¬Multipliable f L
⊢ ¬Multipliable (fun i ↦ g (f i)) L

Tactic:
contrapose h

Goal state after:
case neg
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
h : Multipliable (fun i ↦ g (f i)) L
⊢ Multipliable f L
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
⊢ Multipliable f L → Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g

Tactic:
intro hf

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : CommMonoid α
inst✝⁵ : TopologicalSpace α
L : SummationFilter β
inst✝⁴ : CommMonoid γ
inst✝³ : TopologicalSpace γ
inst✝² : T2Space γ
G : Type u_4
inst✝¹ : FunLike G α γ
inst✝ : MonoidHomClass G α γ
g : G
hg : IsInducing ⇑g
f : β → α
hf : Multipliable f L
⊢ Multipliable (⇑g ∘ f) L ∧ ∏'[L] (i : β), g (f i) ∈ Set.range ⇑g
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case inl
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
a : β
⊢ m (⨆ b ∈ decode₂ β (encode a), s b) = extend encode (fun b ↦ m (s b)) 1 (encode a)

pp: case inr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range encode
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun b ↦ m (s b)) 1 n

Tactic:
· simp [encode_injective.extend_apply]

Goal state after:
case inr
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : TopologicalSpace M
α : Type u_3
β : Type u_4
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range encode
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun b ↦ m (s b)) 1 n
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
s t : Set β
hf₀ : ∀ b ∈ t, f b = 1
b : ↑s
hb : b ∉ Set.range (Set.inclusion ⋯)
⊢ ↑b ∈ t

Tactic:
by simpa using hb

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

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

Tactic:
rw [← tprod_subtype_eq_of_mulSupport_subset (s := {j})]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ ∏' (x : ↑{j}), (s ↑x).mulIndicator f i = f i

α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
s : γ → Set β
f : β → α
i : β
hi : i ∈ ⋃ d, s d
hs : Pairwise (Disjoint on fun j ↦ s j ∩ mulSupport f)
j : γ
hj : i ∈ s j
⊢ (mulSupport fun d ↦ (s d).mulIndicator f i) ⊆ {j}
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
s : ι
⊢ ∑ i ≤ s, f i * ∏ j ≤ s with j < i, (1 + f j) = ((fun s ↦ ∑ b ∈ s, (fun i ↦ f i * ∏ j < i, (1 + f j)) b) ∘ Iic) s

Tactic:
refine sum_congr rfl (fun i hi ↦ ?_)

Goal state after:
ι : Type u_1
α : Type u_3
inst✝⁵ : CommSemiring α
inst✝⁴ : TopologicalSpace α
f : ι → α
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrderBot ι
inst✝¹ : T2Space α
inst✝ : ContinuousAdd α
h✝ : Nonempty ι
x : α
hx :
  Tendsto (fun x ↦ 1 + ∑ i ∈ x, f i * ∏ j ∈ x with j < i, (1 + f j)) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
s i : ι
hi : i ∈ Iic s
⊢ f i * ∏ j ≤ s with j < i, (1 + f j) = (fun i ↦ f i * ∏ j < i, (1 + f j)) i
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
⊢ Summable (fun a ↦ ↑(f a)) L ↔ Summable f L

Tactic:
rcases L.neBot_or_eq_bot with _ | hL
  · constructor
    · exact fun ⟨a, ha⟩ => ⟨⟨a, ha.nonneg fun x => (f x).2⟩, hasSum_coe.1 ha⟩
    · exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩
  · simp [Summable, HasSum, hL]

Goal state after:
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:
rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).ge_iff_eq']

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

Goal state before:
pp: case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ min 1 (ε / 2) < ε

Tactic:
refine (min_le_right _ _).trans_lt ?_

Goal state after:
case neg
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : f n ≤ min 1 (ε / 2)
hε_top : ¬ε = ∞
⊢ ε / 2 < ε
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 ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a

Tactic:
pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)

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 : α
⊢ (g ∘ pkg.coe) a = (g ∘ pkg.coe) a
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

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

Tactic:
simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
        not_false_iff, false_and]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case mp
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) → Nonempty α

Tactic:
rintro ⟨c⟩

Goal state after:
case mp
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
⊢ Nonempty α
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case mpr
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty α → Nonempty (CauchyFilter α)

Tactic:
rintro ⟨c⟩

Goal state after:
case mpr
α : Type u
inst✝ : UniformSpace α
c : α
⊢ Nonempty (CauchyFilter α)
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ∈ Icc a b
y : α
hy : y ∈ Icc a b
hxy : x < y
⊢ projIcc a b h x < projIcc a b h y

Tactic:
by
  simpa only [projIcc_of_mem, hx, hy]

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝² : PseudoEMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
s : β → α
b : β → ℝ≥0∞
b_bound : ∀ (n m N : β), N ≤ n → N ≤ m → edist (s n) (s m) ≤ b N
b_lim : Tendsto b atTop (𝓝 0)
ε : ℝ≥0∞
εpos : ε > 0
this : ∀ᶠ (n : β) in atTop, b n < ε
N : β
hN : b N < ε
m : β
hm : N ≤ m
n : β
hn : N ≤ n
⊢ edist (s m) (s n) < ε

Tactic:
calc edist (s m) (s n) ≤ b N := b_bound m n N hm hn
    _ < ε := hN

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

Goal state before:
pp: s : Set ℝ
h : Bornology.IsBounded s
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)

Tactic:
by
  rcases eq_empty_or_nonempty s with (rfl | hne)
  · simp
  refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_
  · exact Real.dist_le_of_mem_Icc (h.subset_Icc_sInf_sSup hx) (h.subset_Icc_sInf_sSup hy)
  · apply ENNReal.ofReal_le_of_le_toReal
    rw [← Metric.diam, ← Metric.diam_closure]
    calc sSup s - sInf s ≤ dist (sSup s) (sInf s) := le_abs_self _
    _ ≤ Metric.diam (closure s) := dist_le_diam_of_mem h.closure (csSup_mem_closure hne h.bddAbove)
        (csInf_mem_closure hne h.bddBelow)

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

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg✝ : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
hfg : b ≤ (f + g) i
hg : g i ≤ min (b - a) 1
⊢ a ≤ f i

Tactic:
exact ENNReal.le_of_add_le_add_right (hg.trans_lt <| by simp).ne <|
    (add_le_of_le_tsub_left_of_le hab.le <| hg.trans <| min_le_left ..).trans hfg

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

Goal state before:

Tactic:
g x ≤ f z + K * dist x z := ciInf_le (B x) _
    _ ≤ f z + K * dist y z + K * dist x y := by
      rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle

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

Goal state before:
pp: β : Type u_2
inst✝² : PseudoMetricSpace β
inst✝¹ : Monoid β
inst✝ : LipschitzMul β
⊢ ∀ (p q : β × β), dist (p.1 * p.2) (q.1 * q.2) ≤ ↑(LipschitzMul.C β) * dist p q

Tactic:
by
  rw [← lipschitzWith_iff_dist_le_mul]
  exact lipschitzWith_lipschitz_const_mul_edist

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

Goal state before:
pp: G : Type v
X : Type w
inst✝³ : PseudoMetricSpace X
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun x ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r

Tactic:
by rw [preimage_smul, smul_sphere]

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

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
𝕜 : Type u_5
h' : NormedField 𝕜
x : 𝕜
hx : x ≠ 0
hx1 : ‖x‖ ≠ 1
hlt : ‖x‖ < 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
use x⁻¹
      rw [norm_inv]
      exact (one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt

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

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
a a₁ a₂ b c : α
inst✝ : NonUnitalSeminormedRing β
x y : α × β
⊢ max (‖x.1‖ * ‖y.1‖) (‖y.2‖ * ‖x.2‖) ≤ max ‖x.1‖ ‖x.2‖ * max ‖y.2‖ ‖y.1‖

Tactic:
apply max_mul_mul_le_max_mul_max <;> simp [norm_nonneg]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖

Tactic:
exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.IterateAct

Goal state before:
pp: α : Type u_1
f : α → α
x✝ : IterateMulAct f
⊢ (1 * x✝).val = x✝.val

Tactic:
apply Nat.zero_add

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

Goal state before:
pp: case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ c < ‖r • x‖

Tactic:
rwa [norm_smul, ← div_lt_iff₀]

Goal state after:
case h
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
c : ℝ
x : E
hx : x ≠ 0
r : 𝕜
hr : c / ‖x‖ < ‖r‖
⊢ 0 < ‖x‖
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

Goal state before:
pp: α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
⊢ μ S ≤ ⨆ n, μ (s n)

Tactic:
set M := ⨆ n, μ (s n)

Goal state after:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k ↦ μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
⊢ μ S ≤ M
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ a = -1 ∨ a = 0 ∨ a = 1

Tactic:
cases a

Goal state after:
case zero
⊢ zero = -1 ∨ zero = 0 ∨ zero = 1

case neg
⊢ neg = -1 ∨ neg = 0 ∨ neg = 1

case pos
⊢ pos = -1 ∨ pos = 0 ∨ pos = 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a b : SignType
⊢ Decidable (a ≤ b)

Tactic:
cases a

Goal state after:
case zero
b : SignType
⊢ Decidable (zero ≤ b)

case neg
b : SignType
⊢ Decidable (neg ≤ b)

case pos
b : SignType
⊢ Decidable (pos ≤ b)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ 1 * a = a

Tactic:
cases a

Goal state after:
case zero
⊢ 1 * zero = zero

case neg
⊢ 1 * neg = neg

case pos
⊢ 1 * pos = pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ a * 1 = a

Tactic:
cases a

Goal state after:
case zero
⊢ zero * 1 = zero

case neg
⊢ neg * 1 = neg

case pos
⊢ pos * 1 = pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ 0 * a = 0

Tactic:
cases a

Goal state after:
case zero
⊢ 0 * zero = 0

case neg
⊢ 0 * neg = 0

case pos
⊢ 0 * pos = 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ a * 0 = 0

Tactic:
cases a

Goal state after:
case zero
⊢ zero * 0 = 0

case neg
⊢ neg * 0 = 0

case pos
⊢ pos * 0 = 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
ha : a ≠ 0
⊢ a * id a = 1

Tactic:
cases a

Goal state after:
case zero
ha : zero ≠ 0
⊢ zero * id zero = 1

case neg
ha : neg ≠ 0
⊢ neg * id neg = 1

case pos
ha : pos ≠ 0
⊢ pos * id pos = 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ a ≤ a

Tactic:
cases a

Goal state after:
case zero
⊢ zero ≤ zero

case neg
⊢ neg ≤ neg

case pos
⊢ pos ≤ pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a : SignType
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        a) =
    a

Tactic:
cases a

Goal state after:
case zero
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        zero) =
    zero

case neg
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        neg) =
    neg

case pos
⊢ (fun a ↦
        match a with
        | ⟨0, isLt⟩ => 0
        | ⟨1, isLt⟩ => 1
        | ⟨2, isLt⟩ => -1)
      ((fun a ↦
          match a with
          | zero => ⟨0, fin3Equiv._proof_7⟩
          | pos => ⟨1, fin3Equiv._proof_8⟩
          | neg => ⟨2, fin3Equiv._proof_9⟩)
        pos) =
    pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: a b : SignType
⊢ (match a * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match a with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

Tactic:
cases a

Goal state after:
case zero
b : SignType
⊢ (match zero * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match zero with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case neg
b : SignType
⊢ (match neg * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match neg with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩

case pos
b : SignType
⊢ (match pos * b with
    | zero => ⟨0, fin3Equiv._proof_7⟩
    | pos => ⟨1, fin3Equiv._proof_8⟩
    | neg => ⟨2, fin3Equiv._proof_9⟩) =
    (match pos with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩) *
      match b with
      | zero => ⟨0, fin3Equiv._proof_7⟩
      | pos => ⟨1, fin3Equiv._proof_8⟩
      | neg => ⟨2, fin3Equiv._proof_9⟩
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: case mpr
f : ℕ → ℝ≥0
hnat : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, f i) atTop atTop
r : ℝ≥0
hr : HasSum f r
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop hnat _ (hasSum_iff_tendsto_nat.1 hr)

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

Goal state before:
pp: m n : ℕ
⊢ ↑↑(m / n) ≤ ↑↑m / ↑↑n

Tactic:
← coe_div,

Goal state after:
m n : ℕ
⊢ ↑↑(m / n) ≤ ↑(↑m / ↑n)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑a.toReal / ↑a.toReal = 1

Tactic:
← coe_div,

Goal state after:
a : EReal
h₁ : a ≠ ⊥
h₂ : a ≠ ⊤
h₃ : ↑a.toReal ≠ 0
⊢ ↑(a.toReal / a.toReal) = 1
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s.Nonempty
a : α
left✝ : a ∈ s
has : IsMinOn f s a
⊢ BddBelow (f '' s)

Tactic:
exact has.bddBelow

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

Goal state before:
pp: a : EReal
ha : a ≠ ⊤
h'a : a ≠ ⊥
⊢ Tendsto toReal (𝓝 a) (𝓝 a.toReal)

Tactic:
by
  lift a to ℝ using ⟨ha, h'a⟩
  rw [nhds_coe, tendsto_map'_iff]
  exact tendsto_id

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
⊢ LowerSemicontinuousWithinAt f s x ↔ f x ≤ liminf f (𝓝[s] x)

Tactic:
constructor
  · intro h; unfold LowerSemicontinuousWithinAt at h
    by_contra! hf
    obtain ⟨z, ltz, y, ylt, h₁⟩ := hf.exists_disjoint_Iio_Ioi
    exact ltz.not_ge
      (le_liminf_of_le (by isBoundedDefault) ((h y ylt).mono fun _ h₂ =>
        le_of_not_gt fun h₃ => (h₁ _ h₃ _ h₂).false))
  exact fun hf y ylt => eventually_lt_of_lt_liminf (ylt.trans_le hf)

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
⊢ (∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x) →
    ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1

Tactic:
intro hf

Goal state after:
case mp
α : Type u_1
inst✝³ : TopologicalSpace α
γ : Type u_4
inst✝² : LinearOrder γ
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology γ
f : α → γ
s : Set α
hs : IsClosed[inst✝³] s
hf : ∀ x ∈ s, ∀ y < f x, ∀ᶠ (x : α) in 𝓝 x, x ∈ s → y < f x
⊢ ∀ (x : α × γ), (x.1 ∈ s → x.2 < f x.1) → ∀ᶠ (a : α × γ) in 𝓝 x, a.1 ∈ s → a.2 < f a.1