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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
⊢ count K v I⁻¹ = -count K v I

Tactic:
← zpow_neg_one,

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
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
⊢ count K v (I ^ (-1)) = -count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0∞
hr : r < x
⊢ r ≤ y

Tactic:
lift r to ℝ≥0 using ne_top_of_lt hr

Goal state after:
x y : ℝ≥0∞
h : ∀ (r : ℝ≥0), ↑r < x → ↑r ≤ y
r : ℝ≥0
hr : ↑r < x
⊢ ↑r ≤ y
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LT β
U : Filter (α × α)
z : β
D : α → α → β
H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s
s : Set (α × α)
⊢ s ∈ U ↔ ∃ i > z, {p | D p.1 p.2 < i} ⊆ s

Tactic:
simp only [H, subset_def, Prod.forall, mem_ofPred]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ ENNReal.ofReal (dist x y) = ↑(nndist x y)

Tactic:
dist_nndist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ ENNReal.ofReal ↑(nndist x y) = ↑(nndist x y)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = (dist x y).toNNReal

Tactic:
dist_nndist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = (↑(nndist x y)).toNNReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
⊢ dist y x ≤ ε - (ε - dist y x)

Tactic:
by rw [sub_sub_self]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ dist x y = 0

Tactic:
dist_nndist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = 0 ↔ ↑(nndist x y) = 0
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ IsClosed[inst✝¹] ↑(upperClosure s)

Tactic:
obtain rfl | h₁ := s.eq_empty_or_nonempty
  · simp
  by_cases h₂ : BddBelow s
  · exact upperClosure_eq_Ici_csInf h₁ h₂ hs ▸ isClosed_Ici
  · exact upperClosure_eq_bot h₂ ▸ isClosed_univ

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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 c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * 1 = c

Tactic:
refine ⟨algebraMap R K x / algebraMap R K (a.den.1 * c.den.1), ?_⟩

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✝
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 c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ a + FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x / (algebraMap R K) (↑a.den * ↑c.den)) * 1 = c
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ s) ∧ ∃ i, True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
intro ⟨⟨b, _, hb⟩, ⟨a, _, ha⟩⟩

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
⊢ BddBelow sᶜ ∧ BddAbove sᶜ
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ dist a 1 = ‖a‖

Tactic:
dist_eq_norm_inv_mul',

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ ‖1⁻¹ * a‖ = ‖a‖
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
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
by
  have := mem_image_of_mem f hc
  rw [h.image_Icc (hc.1.trans hc.2)] at this
  exact this.2

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht✝ : t₁ ∈ Icc a t₁
t : α
ht : t ∈ A
this : t ∈ Icc a t
⊢ t ∈ s

Tactic:
exact ht.2 this

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖

Tactic:
dist_eq_norm_inv_mul',

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖b⁻¹ * a‖ = ‖a / b‖
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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)

Tactic:
have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
this : Fact (s ≤ t)
⊢ StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ 1 ≤ g / a ^ k

Tactic:
simpa using nonneg

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

Goal state before:
pp: case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ∅ = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
Icc_eq_empty_of_lt

Goal state after:
case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ∅ = ∅

case inr
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊↑x + r⌋₊ < ⌈↑x - r⌉₊
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: x : EReal
h : x ≠ ⊥
⊢ ⊤ + x = ⊤

Tactic:
by
  induction x
  · exfalso; exact h (Eq.refl ⊥)
  · exact top_add_coe _
  · exact top_add_top

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

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

pp: case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)

Tactic:
· exact tendsto_bot

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : Filter β
u : β → α
a : α
hinf : a ≤ liminf u f
hsup : limsup u f ≤ a
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h' : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u
h✝ : f.NeBot
⊢ Tendsto u f (𝓝 a)
Module: Mathlib.Topology.EMetricSpace.Lipschitz

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn (fun y ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith K (fun x ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ Metric.eball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x ↑δ
hbt : (a, b).2 ∈ t
hby : (a, b).2 ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * ↑(3 * K) + ε / 2

Tactic:
push_cast; ring

Goal state after:
Module: Mathlib.Logic.Encodable.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Encodable β
f : β → Set α
C : Set α → Prop
H0 : C ∅
H1 : ∀ (b : β), C (f b)
n : ℕ
⊢ C (⋃ b ∈ none, f b)

Tactic:
simp only [Option.mem_def, iUnion_of_empty, iUnion_empty, reduceCtorEq]
    apply H0

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

Goal state before:
pp: a b : EReal
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
induction a, b using EReal.induction₂_symm with
  | symm h => simp [EReal.mul_comm, h, and_comm]
  | top_top => simp
  | top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
  | top_zero => simp
  | top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
  | top_bot => simp
  | pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
  | coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
  | zero_bot => simp
  | neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
  | bot_bot => simp

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
h : ∀ (x : β), ∀ᶠ (s : Finset β) in L.filter, x ∈ s
s : Set (Finset β)
hs : s ∈ atTop
t : Finset β
ht : ∀ (b : Finset β), t ⊆ b → b ∈ s
this : ⋂ i ∈ t, {x | (fun s ↦ i ∈ s) x} ∈ L.filter
r : Finset β
hr : r ∈ ⋂ i ∈ t, {x | (fun s ↦ i ∈ s) x}
⊢ t ⊆ r

Tactic:
by simpa using! hr

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)

Tactic:
have bddmax := IsBoundedUnder.sup h₃ h₄

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)

Tactic:
have cobddmax := isCoboundedUnder_le_max (v := v) (Or.inl h₁)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ max (u a) (v a)
⊢ limsup (fun a ↦ max (u a) (v a)) f = max (limsup u f) (limsup v f)
Module: Mathlib.Topology.Algebra.InfiniteSum.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
f : β → α
ha : Multipliable f L
⊢ HasProd f (∏'[L] (b : β), f b) L

Tactic:
by
  -- This is quite delicate because of the fiddly special-casing for finite products.
  classical
  rw [tprod_def, dif_pos ha]
  split_ifs with h h'
  · convert! hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
    · simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
      simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
      rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
      · exact Finset.prod_congr rfl (by simp_all)
      · simp
    · grind [Set.Finite.mem_toFinset, mem_mulSupport]
    · exact h.1
  · exact h'
  · exact ha.choose_spec

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun n ↦ if n = b then 1 else f n) a' L
⊢ HasProd (update f b 1) a' L

Tactic:
convert! hf'

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝⁶ : L.LeAtTop
inst✝⁵ : L.NeBot
α : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a L
b : β
a' : α
hf' : HasProd (fun n ↦ if n = b then 1 else f n) a' L
x✝ : β
⊢ update f b 1 x✝ = if x✝ = b then 1 else f x✝
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| Summable fun n ↦ ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
x✝ : A
| ∑' (b : ↑↑(antidiagonal x✝)), f (↑b).1 * g (↑b).2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f (↑x.snd).1 * g (↑x.snd).2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| ∑' (n : A), ∑ kl ∈ antidiagonal n, f kl.1 * g kl.2

Tactic:
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Goal state after:
case f
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
x✝ : A
| ∑' (b : ↑↑(antidiagonal x✝)), f (↑b).1 * g (↑b).2

case L
α : Type u_3
A : Type u_4
inst✝⁵ : AddCommMonoid A
inst✝⁴ : HasAntidiagonal A
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : A → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x ↦ f x.1 * g x.2
| SummationFilter.unconditional A
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case inr
α : Type u_2
L : SummationFilter α
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y L
hL : L.filter = ⊥
⊢ HasSum (fun x ↦ (f x).toNNReal) y.toNNReal L

Tactic:
· simp [HasSum, hL]

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

Goal state before:
pp: case inl.mpr
α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
h✝ : L.NeBot
⊢ Summable f L → Summable (fun a ↦ ↑(f a)) L

Tactic:
exact fun ⟨a, ha⟩ => ⟨a.1, hasSum_coe.2 ha⟩

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

Goal state before:
pp: ι : Type u_4
l : Filter ι
x : ι → ℝ
hx : liminf (fun n ↦ ↑(Real.nnabs (x n))) l ≠ ∞
h : ∀ (R : ℝ), ∀ᶠ (x_1 : ι) in l, R ≤ x x_1
r : ℝ≥0
⊢ ∀ᶠ (a : ι) in l, r ≤ Real.nnabs (x a)

Tactic:
filter_upwards [h r] with i hi using hi.trans (le_abs_self (x i))

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

Goal state before:
pp: ι : Type u_4
fi : Filter ι
f : ι → ℝ≥0
x : ℝ≥0
⊢ Tendsto (fun n ↦ ((fun i ↦ ↑(f i)) n).toReal) fi (𝓝 (↑x).toReal) ↔ Tendsto (fun i ↦ ↑(f i)) fi (𝓝 ↑x)

Tactic:
simp [tendsto_coe]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ≥0
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y
⊢ LipschitzOnWith K f s

Tactic:
simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h

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 : α
⊢ |c ⊔ b - c ⊔ d| ≤ |b - d|

Tactic:
rw [sup_comm c, sup_comm c]
        exact abs_sup_sub_sup_le_abs _ _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformly F f l
hG : TendstoLocallyUniformly G g l
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformly (F • G) (f • g) l

Tactic:
← tendstoLocallyUniformlyOn_univ

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : PseudoMetricSpace α
inst✝⁵ : PseudoMetricSpace β
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMul α β
inst✝¹ : IsBoundedSMul α β
X : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace X
F : ι → X → α
G : ι → X → β
f : X → α
g : X → β
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l univ
hG : TendstoLocallyUniformlyOn G g l univ
hf : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (f y) 0
hg : ∀ (x : X), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝 x) fun y ↦ dist (g y) 0
⊢ TendstoLocallyUniformlyOn (F • G) (f • g) l univ
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝² : Group G
inst✝¹ : PseudoMetricSpace G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun x ↦ x * a) ⁻¹' ball b r = ball (b / a) r

Tactic:
by
  rw [div_eq_mul_inv]
  exact preimage_smul_ball (MulOpposite.op a) b r

Goal state after:
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 𝕜
h : ∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ ∃ x, 1 < ‖x‖

Tactic:
rcases h with ⟨x, hx, hx1⟩
    rcases hx1.lt_or_gt with hlt | hlt
    · use x⁻¹
      rw [norm_inv]
      exact (one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt
    · exact ⟨x, hlt⟩

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

Goal state before:
pp: 𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst✝³ : SeminormedRing 𝕜₁
inst✝² : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomIsometric σ
x : 𝕜₂
⊢ ‖σ (σ' x)‖ = ‖x‖

Tactic:
RingHomInvPair.comp_apply_eq₂

Goal state after:
𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst✝³ : SeminormedRing 𝕜₁
inst✝² : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomIsometric σ
x : 𝕜₂
⊢ ‖x‖ = ‖x‖
Module: Mathlib.Analysis.Normed.Ring.Lemmas

Goal state before:
pp: 𝕜₁ : Type u_4
𝕜₂ : Type u_5
inst✝³ : SeminormedRing 𝕜₁
inst✝² : SeminormedRing 𝕜₂
σ : 𝕜₁ →+* 𝕜₂
σ' : 𝕜₂ →+* 𝕜₁
inst✝¹ : RingHomInvPair σ σ'
inst✝ : RingHomIsometric σ
x : 𝕜₂
⊢ ‖σ' x‖ = ‖x‖

Tactic:
by rw [← RingHomIsometric.norm_map (σ := σ), RingHomInvPair.comp_apply_eq₂]

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

Goal state before:
pp: r : ℝ≥0
s : ℝ≥0∞
⊢ (r • s).toReal = r • s.toReal

Tactic:
ENNReal.smul_def,

Goal state after:
r : ℝ≥0
s : ℝ≥0∞
⊢ (↑r • s).toReal = r • s.toReal
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖(a :: b :: l).prod‖ ≤ (map norm (a :: b :: l)).prod

Tactic:
by
    rw [List.map_cons, List.prod_cons, List.prod_cons (a := ‖a‖)]
    refine le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left ?_ (norm_nonneg _))
    exact List.norm_prod_le' (List.cons_ne_nil b l)

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

Goal state before:
pp: R : Type u_5
S : Type u_6
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A : Subalgebra R S
f : S → ℝ
hf_pm : IsPowMul f
x : ↥A
n : ℕ
hn : 1 ≤ n
⊢ (fun x ↦ f ↑x) (x ^ n) = (fun x ↦ f ↑x) x ^ n

Tactic:
simpa using hf_pm (↑x) hn

Goal state after:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i_1 : ι), i_1 = i ∨ i_1 ∈ l → f i_1 ∈ t i_1

Tactic:
forall_eq_or_imp,

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
h : TProd.mk l f ∈ Set.tprod l t ↔ ∀ (i : ι), i ∈ l → f i ∈ t i
⊢ f i ∈ t i ∧ TProd.mk l f ∈ Set.tprod l t ↔ f i ∈ t i ∧ ∀ (a : ι), a ∈ l → f a ∈ t a
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformly F f l
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ TendstoLocallyUniformly F⁻¹ f⁻¹ l

Tactic:
← tendstoLocallyUniformlyOn_univ

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
F : ι → X → α
f : X → α
l : Filter ι
hF : TendstoLocallyUniformlyOn F f l Set.univ
hf : ∀ (x : X), Disjoint (map f (𝓝 x)) (𝓝 0)
⊢ TendstoLocallyUniformlyOn F⁻¹ f⁻¹ l Set.univ