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

Goal state before:
pp: α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
H : ∃ j, BddBelow (range fun i ↦ f ↑i)
⊢ liminf f v = ⨆ j, ⨅ i, f ↑i

Tactic:
rcases H with ⟨j0, hj0⟩
  let m : Set (Subtype p) := {j | BddBelow (range (fun (i : s j) ↦ f i))}
  have : ∀ (j : Subtype p), Nonempty (s j) := fun j ↦ Nonempty.coe_sort (hs j)
  have A : ⋃ (j : Subtype p), ⋂ (i : s j), Iic (f i) =
         ⋃ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) := by
    apply Subset.antisymm
    · apply iUnion_subset (fun j ↦ ?_)
      by_cases hj : j ∈ m
      · have : j = liminfReparam f s p j := by simp only [m, liminfReparam, hj, ite_true]
        conv_lhs => rw [this]
        apply subset_iUnion _ j
      · simp only [m, mem_ofPred_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj
        simp only [hj, empty_subset]
    · apply iUnion_subset (fun j ↦ ?_)
      exact subset_iUnion (fun (k : Subtype p) ↦ (⋂ (i : s k), Iic (f i))) (liminfReparam f s p j)
  have B : ∀ (j : Subtype p), ⋂ (i : s (liminfReparam f s p j)), Iic (f i) =
                                Iic (⨅ (i : s (liminfReparam f s p j)), f i) := by
    intro j
    apply (Iic_ciInf _).symm
    change liminfReparam f s p j ∈ m
    by_cases Hj : j ∈ m
    · simpa only [m, liminfReparam, if_pos Hj] using Hj
    · simp only [m, liminfReparam, if_neg Hj]
      have Z : ∃ n, (exists_surjective_nat (Subtype p)).choose n ∈ m ∨ ∀ j, j ∉ m := by
        rcases (exists_surjective_nat (Subtype p)).choose_spec j0 with ⟨n, rfl⟩
        exact ⟨n, Or.inl hj0⟩
      rcases Nat.find_spec Z with hZ | hZ
      · exact hZ
      · exact (hZ j0 hj0).elim
  simp_rw [hv.liminf_eq_sSup_iUnion_iInter, A, B, sSup_iUnion_Iic]

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

Goal state before:
pp: x y : EReal
hy : 0 ≤ y
⊢ (x * y).toENNReal = x.toENNReal * y.toENNReal

Tactic:
by
  rw [EReal.mul_comm, toENNReal_mul hy, mul_comm]

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

Goal state before:
pp: case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ finprod (L.support.mulIndicator fun b ↦ f b) = ∏ b ∈ ⋯.toFinset, f b

Tactic:
finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)

Goal state after:
case e'_6
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ ∏ i ∈ ⋯.toFinset, L.support.mulIndicator (fun b ↦ f b) i = ∏ b ∈ ⋯.toFinset, f b

case e'_6.h
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
h : L.HasSupport ∧ ((mulSupport fun b ↦ f b) ∩ L.support).Finite
⊢ mulSupport (L.support.mulIndicator fun b ↦ f b) ⊆ ↑⋯.toFinset
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:

Tactic:
f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
    _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
    _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

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

Goal state before:
pp: case refine_2
ι : 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
⊢ f = 1 → HasProd f 1 L

Tactic:
· rintro rfl
    exact hasProd_one

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

Goal state before:
pp: ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁷ : CommGroup α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedMonoid α
inst✝⁴ : TopologicalSpace α
inst✝³ : IsTopologicalGroup α
inst✝² : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
inst✝¹ : L.NeBot
inst✝ : L.LeAtTop
h : f ≤ g
hi : f i < g i
hf : HasProd f a₁ L
hg : HasProd g a₂ L
⊢ a₁ < a₂

Tactic:
classical
  have : update f i 1 ≤ update g i 1 := update_le_update_iff.mpr ⟨rfl.le, fun i _ ↦ h i⟩
  have : 1 / f i * a₁ ≤ 1 / g i * a₂ := hasProd_le this (hf.update i 1) (hg.update i 1)
  simpa only [one_div, mul_inv_cancel_left] using mul_lt_mul_of_lt_of_le hi this

Goal state after:
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:
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.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝⁵ : CommMonoid α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
hf : Multipliable f
⊢ ∏' (i : ι), f i ≠ 1 ↔ ∃ x, f x ≠ 1

Tactic:
rw [Ne, hf.tprod_eq_one_iff, not_forall]

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

Goal state before:
pp: case pos
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
s : Finset ℕ
hs : ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
t : Set ℕ
h : s.Nonempty
ht : t ⊆ {n | s.max' h + 1 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

Tactic:
exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)

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

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

Tactic:
tprod_eq_prod (s := {b}),

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∏ b ∈ {b}, f b = f b

α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
L : SummationFilter β
inst✝ : L.LeAtTop
f : β → α
b : β
hf : ∀ (b' : β), b' ≠ b → f b' = 1
⊢ ∀ b_1 ∉ {b}, f b_1 = 1
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun a ↦ ↑(f (a + k))) ↑a ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)

Tactic:
hasSum_nat_add_iff (f := fun n => toReal (f n)) k

Goal state after:
f : ℕ → ℝ≥0
k : ℕ
a : ℝ≥0
⊢ HasSum (fun n ↦ ↑(f n)) (↑a + ∑ i ∈ Finset.range k, ↑(f i)) ↔ HasSum f (a + ∑ i ∈ Finset.range k, f i)
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (fun a ↦ ∑' (a_1 : { x // x ∉ a }), ↑(f ↑a_1)) atTop (𝓝 0)

Tactic:
exact tendsto_tsum_compl_atTop_zero fun a : α => (f a : ℝ)

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

Goal state before:
pp: α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (Filter.map (⇑sumEquiv) atTop) (𝓝 (a * b))

Tactic:
Finset.sumEquiv.map_atTop,

Goal state after:
α : Type u_4
β : Type u_5
M : Type u_6
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : α ⊕ β → M
a b : M
h₁ : HasProd (f ∘ Sum.inl) a
h₂ : HasProd (f ∘ Sum.inr) b
⊢ Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) atTop (𝓝 (a * b))
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: case refine_2.zero
E : Type u_4
inst✝ : SeminormedCommGroup E
a : E
s : Subgroup E
hg : a ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ↑s
b : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < b n
u : ℕ → E
u_in : ∀ (n : ℕ), u n ∈ s
lim_u : Tendsto u atTop (𝓝 a)
n₀ : ℕ
hn₀ : ∀ n ≥ n₀, ‖(u n)⁻¹ * a‖ < b 0
z : ℕ → E := fun n ↦ u (n + n₀)
lim_z : Tendsto z atTop (𝓝 a)
mem_𝓤 : ∀ (n : ℕ), {p | ‖p.1⁻¹ * p.2‖ < b (n + 1)} ∈ 𝓤 E
φ : ℕ → ℕ
φ_extr : StrictMono φ
hφ : ∀ (n : ℕ), ‖(z (φ (n + 1)))⁻¹ * z (φ n)‖ < b (n + 1)
w : ℕ → E := z ∘ φ
hw : Tendsto w atTop (𝓝 a)
v : ℕ → E := fun i ↦ if i = 0 then w 0 else (w (i - 1))⁻¹ * w i
⊢ v 0 ∈ s

Tactic:
change w 0 ∈ s
      apply u_in

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

Goal state before:
pp: case succ.refine_1
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
⊢ x ^ n ≠ 0 ∨ x ≠ ∞

Tactic:
by_cases H : x = 0

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

case neg
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ^ n ≠ 0 ∨ x ≠ ∞
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case succ.refine_2
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
⊢ x ≠ 0 ∨ x ^ n ≠ ∞

Tactic:
by_cases H : x = 0

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

case neg
n : ℕ
IH : Continuous fun a ↦ a ^ n
x : ℝ≥0∞
H : ¬x = 0
⊢ x ≠ 0 ∨ x ^ n ≠ ∞
Module: Mathlib.Order.Interval.Set.ProjIcc

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
⊢ IccExtend h (f ∘ Subtype.val) x = f x

Tactic:
rcases le_or_gt x b with hxb | hbx

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ IccExtend h (f ∘ Subtype.val) x = f x

case inr.inr
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hbx : b < x
⊢ IccExtend h (f ∘ Subtype.val) x = f x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
⊢ t.truncateToReal x = x.toReal

Tactic:
have x_lt_top : x < ∞ := lt_of_le_of_lt x_le t_ne_top.lt_top

Goal state after:
t x : ℝ≥0∞
t_ne_top : t ≠ ∞
x_le : x ≤ t
x_lt_top : x < ∞
⊢ t.truncateToReal x = x.toReal
Module: Mathlib.Topology.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n

Tactic:
rw [iterate_succ, mul_comm]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
f : ι → ℝ≥0∞
hf : Tendsto f u (𝓝 0)
g : ι → ℝ≥0∞
⊢ liminf (f + g) u = liminf g u

Tactic:
rw [add_comm, liminf_add_of_right_tendsto_zero hf]

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

Goal state before:
pp: case h₁
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊔ b - c ⊔ b| ≤ |a - c|

Tactic:
exact abs_sup_sub_sup_le_abs _ _ _

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊔ c - d ⊔ c| ≤ |b - d|

Tactic:
exact abs_sup_sub_sup_le_abs _ _ _

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

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), dist (u m) (u n) < C
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)

Tactic:
simp_rw [SeminormedGroup.dist_eq] at hC

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)
Module: Mathlib.Analysis.Normed.Field.Basic

Goal state before:
pp: 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
⊢ ∃ x, 1 < ‖x‖

Tactic:
rcases hx1.lt_or_gt with hlt | hlt

Goal state after:
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‖

case inr
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 : 1 < ‖x‖
⊢ ∃ x, 1 < ‖x‖
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f✝ : F
g : β →ᵈ γ
f : α →ᵈ β
x y : α
⊢ edist ((⇑g ∘ ⇑f) x) ((⇑g ∘ ⇑f) y) = ↑(ratio g * ratio f) * edist x y

Tactic:
Function.comp,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f✝ : F
g : β →ᵈ γ
f : α →ᵈ β
x y : α
⊢ edist (g (f x)) (g (f y)) = ↑(ratio g * ratio f) * edist x y
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) * edist x y = edist ((⇑g ∘ ⇑f) x) ((⇑g ∘ ⇑f) y)
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
Function.comp,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : ↑(ratio (g.comp f)) * edist x y = edist (g (f x)) (g (f y))
⊢ ratio (g.comp f) = ratio g * ratio f
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 g : X ≃ᵈ Y), ⇑e.toEquiv = ⇑g.toEquiv → ⇑e.symm = ⇑g.symm → e = g

Tactic:
by rintro ⟨⟩ ⟨⟩ h -; congr; exact DFunLike.ext' h

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:
n.cast_succ,

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑(n + 1) * ‖1‖
Module: Mathlib.Analysis.Normed.Ring.Basic

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

Tactic:
n.cast_succ,

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ (↑n + 1) * ‖1‖
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖-↑↑z.natAbs‖ = ‖↑z‖

Tactic:
← Int.cast_neg,

Goal state after:
case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑(-↑z.natAbs)‖ = ‖↑z‖
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 : {y | ‖y‖ < r} ⊆ sᶜ
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε

Tactic:
simp only [Set.subset_compl_comm (t := s), Set.compl_ofPred, not_lt] at hr

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
s : Set α
hs : sᶜ ∈ 𝓝 0
ε : ℝ
hε : ε > 0
r : ℝ
hr₀ : 0 < r
hr : s ⊆ {a | r ≤ ‖a‖}
⊢ ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist x⁻¹ y⁻¹ ≤ ε
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ‖k • e‖ < ‖e‖ ↔ k • e = 0

Tactic:
norm_zsmul ℚ k e,

Goal state after:
case inr
𝕜 : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
inst✝⁶ : NormedField 𝕜
inst✝⁵ : SeminormedAddCommGroup E✝
inst✝⁴ : SeminormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 E✝
inst✝² : NormedSpace 𝕜 F
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℚ E
e : E
this : IsAddTorsionFree E
he : e ≠ 0
k : ℤ
hx : k • e ∈ AddSubgroup.zmultiples e
⊢ ‖↑k‖ * ‖e‖ < ‖e‖ ↔ k • e = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
⊢ LawfulFunctor OuterMeasure

Tactic:
constructor <;> intros

Goal state after:
case map_const
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ : Type u_3
⊢ Functor.mapConst = Functor.map ∘ const β✝

case id_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ : Type u_3
x✝ : OuterMeasure α✝
⊢ id <$> x✝ = x✝

case comp_map
α : Type u_1
β : Type u_2
m : OuterMeasure α
α✝ β✝ γ✝ : Type u_3
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : OuterMeasure α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
⊢ Measurable fun p ↦ update p.1 a p.2

Tactic:
by
  rw [measurable_pi_iff]
  intro j
  dsimp [update]
  split_ifs with h
  · subst h
    dsimp
    exact measurable_snd
  · exact measurable_pi_iff.1 measurable_fst _

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

Goal state before:
pp: case neg
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = neg
⊢ sign (∑ i ∈ s, f i) = neg

pp: case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos

Tactic:
· simp_rw [neg_eq_neg_one, sign_eq_neg_one_iff] at h ⊢
    exact Finset.sum_neg h hs

Goal state after:
case pos
α : Type u
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
ι : Type u_1
s : Finset ι
f : ι → α
hs : s.Nonempty
h : ∀ i ∈ s, sign (f i) = pos
⊢ sign (∑ i ∈ s, f i) = pos
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ sign a = 1

Tactic:
sign_apply,

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : 0 < a
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) = 1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ sign a = -1

Tactic:
sign_apply,

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
ha : a < 0
⊢ (if 0 < a then 1 else if a < 0 then -1 else 0) = -1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : sign a = 1
hn : ¬0 < a
⊢ False

Tactic:
sign_apply,

Goal state after:
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 1
hn : ¬0 < a
⊢ False
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
sign_apply,

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddLeftStrictMono α
a : α
⊢ (if 0 < -a then 1 else if -a < 0 then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ sign (-a) = -sign a

Tactic:
sign_apply,

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if 0 < -a then 1 else if -a < 0 then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: case symm
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (y✝ * x✝).abs = y✝.abs * x✝.abs

Tactic:
| symm h =>

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

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

Tactic:
| symm h =>

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

Goal state before:
pp: case mpr.inl
x y : EReal
h : sign x < sign y
⊢ x ≤ y

pp: case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ x ≤ y

pp: case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ x ≤ y

pp: case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ x ≤ y

Tactic:
· exact (sign.monotone.reflect_lt h).le

Goal state after:
case mpr.inr.inl
x y : EReal
h : sign x = neg ∧ sign y = neg ∧ y.abs ≤ x.abs
⊢ x ≤ y

case mpr.inr.inr.inl
x y : EReal
h : sign x = zero ∧ sign y = zero
⊢ x ≤ y

case mpr.inr.inr.inr
x y : EReal
h : sign x = pos ∧ sign y = pos ∧ x.abs ≤ y.abs
⊢ x ≤ y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: b : EReal
h : b ≤ 0
⊢ Antitone fun a ↦ a / b

Tactic:
intro a a' h'

Goal state after:
b : EReal
h : b ≤ 0
a a' : EReal
h' : a ≤ a'
⊢ (fun a ↦ a / b) a' ≤ (fun a ↦ a / b) a
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
⊢ ↑(ε' i) ≠ 0

Tactic:
by simpa using (hε' i).ne'

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
H : f x < f z
⊢ min (f z) (f x) ∈ u

Tactic:
simpa [H.le]

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

Goal state before:
pp: r : ℝ≥0
hr' hr : r < 1
⊢ Tendsto (HPow.hPow r) atTop (𝓝 0)

Tactic:
apply NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one hr

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

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : TopologicalSpace α
s : Set α
x : α
γ : Type u_5
inst✝⁴ : AddCommMonoid γ
inst✝³ : LinearOrder γ
inst✝² : IsOrderedAddMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousWithinAt f s x
hg : LowerSemicontinuousWithinAt g s x
hcont : ContinuousAt (fun p ↦ p.1 + p.2) (f x, g x)
y : γ
hy : (fun z ↦ f z + g z) x > y
u v : Set γ
u_open : IsOpen[inst✝¹] u
xu : f x ∈ u
v_open : IsOpen[inst✝¹] v
xv : g x ∈ v
h : u ×ˢ v ⊆ {p | y < p.1 + p.2}
hx₁ : ∃ l, l < f x
z₁ : γ
z₁lt : z₁ < f x
h₁ : Ioc z₁ (f x) ⊆ u
hx₂ : ∃ l, l < g x
z₂ : γ
z₂lt : z₂ < g x
h₂ : Ioc z₂ (g x) ⊆ v
z : α
h₁z : f z > z₁
h₂z : g z > z₂
A1 : min (f z) (f x) ∈ u
H : g x < g z
⊢ min (g z) (g x) ∈ v

Tactic:
simpa [H.le]

Goal state after: