mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x₁ x₂ : α
y : β
⊢ dist (x₁, y) (x₂, y) = dist x₁ x₂

Tactic:
simp [Prod.dist_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ ball x r ×ˢ ball y r ↔ z ∈ ball (x, y) r

Tactic:
simp [Prod.dist_eq]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α
y : β
r : ℝ
z : α × β
⊢ z ∈ closedBall x r ×ˢ closedBall y r ↔ z ∈ closedBall (x, y) r

Tactic:
simp [Prod.dist_eq]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
r : ℝ
hr : closedBall x r ⊆ s
⊢ IsCompact (closedBall x r)

Tactic:
exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

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

Goal state before:

Tactic:
Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
      _ = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Ioc a b)) :=
        closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
⊢ {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Ioi x) x}.Countable

Tactic:
apply (countable_image_lt_image_Ioi_within s f).mono
  rintro x ⟨xs, hx : ¬ContinuousWithinAt f (s ∩ Ioi x) x⟩
  dsimp only [mem_ofPred_eq]
  contrapose! hx
  refine tendsto_order.2 ⟨fun m hm => ?_, fun u hu => ?_⟩
  · filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy
    exact hm.trans_le (hf xs hy.1 (le_of_lt hy.2))
  rcases hx xs u hu with ⟨v, vs, xv, fvu⟩
  have : s ∩ Ioo x v ∈ 𝓝[s ∩ Ioi x] x := by simp [nhdsWithin_inter, mem_inf_of_left,
    self_mem_nhdsWithin, mem_inf_of_right, Ioo_mem_nhdsGT xv]
  filter_upwards [this] with y hy
  exact (hf hy.1 vs hy.2.2.le).trans_lt fvu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Af : Antitone f
bdd : BddAbove (range g)
⊢ f (⨆ i, g i) = ⨅ i, f (g i)

Tactic:
rw [iSup, Antitone.map_csSup_of_continuousAt Cf Af (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]

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

Goal state before:
pp: case refine_4
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 J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ (↑I').subtype.range ≤
    Submodule.map (↑I').subtype
      (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔ Submodule.comap (↑I').subtype ↑J')

Tactic:
Submodule.map_sup,

Goal state after:
case refine_4
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 J I' J' : FractionalIdeal R⁰ K
H✝ : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
H : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ (↑I').subtype.range ≤
    Submodule.map (↑I').subtype (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I)) ⊔
      Submodule.map (↑I').subtype (Submodule.comap (↑I').subtype ↑J')
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
h : ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact h

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
x y : E
⊢ ‖x⁻¹⁻¹ * y‖ = ‖(x⁻¹ * y⁻¹)⁻¹‖

Tactic:
mul_inv,

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
x y : E
⊢ ‖x⁻¹⁻¹ * y‖ = ‖x⁻¹⁻¹ * y⁻¹⁻¹‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖b / a‖ ≤ r

Tactic:
by
  rw [mem_closedBall, dist_eq_norm_div]

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

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b

Tactic:
exact norm_div_eq_zero_iff.not

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

Goal state before:
pp: ⊢ cofinite = atBot ⊔ atTop

Tactic:
by
  rw [← cocompact_eq_cofinite, cocompact_eq_atBot_atTop]

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: case some
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, b)

Tactic:
rcases b with (_ | b)

Goal state after:
case some.none
α : Type u
β : Type v
γ : Type w
a : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, none)

case some.some
α : Type u
β : Type v
γ : Type w
a b : ℝ≥0
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (some a, some b)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t

Tactic:
by simp [IsBounded]

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

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

Tactic:
obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)

Goal state after:
case inl
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop = ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))

case inr
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : atTop ≠ ⊥
⊢ Tendsto f atTop (𝓝 (⨆ i, f i))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case a
ι : Type u_6
R : Type u_7
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
w✝ : ι
h : w✝ ∈ a ⁻¹' {x | (fun n ↦ n ≤ b) x}
⊢ a w✝ ≤ b

Tactic:
exact h

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

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset β)
t : Finset β
H : ∀ (b : Finset β), t ⊆ b → b ∈ s
⊢ ∃ a, ∀ (b : Finset (α ⊕ β)), a ⊆ b → b.toRight ∈ s

Tactic:
exact ⟨.disjSum ∅ t, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

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

Goal state before:
pp: case coe.top
a✝ : ℝ
hx : 0 ≤ ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

Tactic:
rcases eq_or_lt_of_le hx with (hx | hx)

Goal state after:
case coe.top.inl
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 = ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal

case coe.top.inr
a✝ : ℝ
hx✝ : 0 ≤ ↑a✝
hx : 0 < ↑a✝
⊢ (↑a✝ * ⊤).toENNReal = (↑a✝).toENNReal * ⊤.toENNReal
Module: Mathlib.Data.EReal.Operations

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

Tactic:
simp [hx0]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, a < b
⊢ liminf f (𝓝[>] a) = ⨆ r, ⨆ (_ : r > a), f r

Tactic:
by
  rw [(nhdsGT_basis_of_exists_gt hb).liminf_eq_iSup_iInf]
  refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
  obtain ⟨b, hb⟩ := exists_between hr
  exact ⟨b, hb.1, iInf₂_le b hb⟩

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 : α
s : Set β
⊢ HasProd (s.mulIndicator f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a

Tactic:
hasProd_subtype_iff_of_mulSupport_subset Set.mulSupport_mulIndicator_subset

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set β
⊢ HasProd (s.mulIndicator f) a ↔ HasProd (s.mulIndicator f) a
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ c ∉ Set.range e, 1 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasProd (extend e f 1) a₁
hg : HasProd g a₂
c : κ
h : c ∉ Set.range e
⊢ 1 c ≤ g c

Tactic:
exact hs _ h

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

Goal state before:
pp: κ : Type u_4
γ : Type u_5
inst✝⁶ : CommGroup γ
inst✝⁵ : PartialOrder γ
inst✝⁴ : IsOrderedMonoid γ
inst✝³ : UniformSpace γ
inst✝² : IsUniformGroup γ
inst✝¹ : OrderClosedTopology γ
inst✝ : CompleteSpace γ
f : κ → γ
β : Set κ
h : ∀ (a : κ), 1 ≤ f a
hf : Multipliable f
⊢ ∀ (i : { x // x ∈ β }), f ↑i ≤ f ↑i

Tactic:
simp only [le_refl, implies_true]

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

Goal state before:
pp: β : Type u_2
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : CommGroup G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
a : G
⊢ ∏' (x : β), a = a ^ Nat.card β

Tactic:
by
  rcases finite_or_infinite β with hβ | hβ
  · let : Fintype β := Fintype.ofFinite β
    rw [tprod_eq_prod (s := univ) (fun x hx ↦ (hx (mem_univ x)).elim)]
    simp only [prod_const, Nat.card_eq_fintype_card, Fintype.card]
  · simp only [Nat.card_eq_zero_of_infinite, pow_zero]
    rcases eq_or_ne a 1 with rfl | ha
    · simp
    · apply tprod_eq_one_of_not_multipliable
      simpa [multipliable_const_iff] using ha

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 β
⊢ (if L.HasSupport ∧ ∅.Finite then 1 else 1) = 1

Tactic:
ite_self

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ 1 = 1
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable f
i : β → α
hi : Function.Injective i
⊢ Summable (f ∘ i)

Tactic:
rw [← summable_coe] at hf ⊢

Goal state after:
α : Type u_2
β : Type u_3
f : α → ℝ≥0
hf : Summable fun a ↦ ↑(f a)
i : β → α
hi : Function.Injective i
⊢ Summable fun a ↦ ↑((f ∘ i) a)
Module: Mathlib.Topology.MetricSpace.Antilipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (𝓝 (f x)) ≤ 𝓝 x

Tactic:
by
  simp only [nhds_eq_comap_uniformity]
  grw [← hf.comap_uniformity_le]
  simp [comap_comap, Function.comp_def]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace γ
inst✝ : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ ∀ (a : α), (Completion.extension f ∘ Completion.map g) ↑a = Completion.extension (f ∘ g) ↑a

Tactic:
by
    simp [hf, hg, hf.comp hg, map_coe, extension_coe]

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
⊢ m • n • x = n • m • x

Tactic:
have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl
    have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl
    rw [hmn, hnm, map_comp, map_comp]
    · exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))
    repeat' exact uniformContinuous_const_smul _

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

Goal state before:
pp: X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹

Tactic:
set d : X → X → ℝ≥0 := fun x y => if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0

Goal state after:
X : Type u_2
inst✝¹ : UniformSpace X
inst✝ : (𝓤 X).IsCountablyGenerated
U : ℕ → SetRel X X
hU_symm : ∀ (n : ℕ), (U n).IsSymm
hU_comp : ∀ ⦃m n : ℕ⦄, m < n → U n ○ (U n ○ U n) ⊆ U m
hB : (𝓤 X).HasAntitoneBasis U
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ ediam s

Tactic:
apply ENNReal.ofReal_le_of_le_toReal

Goal state after:
case inr.refine_2
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ (ediam s).toReal
Module: Mathlib.Topology.MetricSpace.Dilation

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ediam (⇑f '' s) / ↑(ratio f)

Tactic:
rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ↑(ratio f)⁻¹ * ediam (⇑f '' s)

α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ ratio f ≠ 0
Module: Mathlib.Data.ENNReal.Action

Goal state before:
pp: x : ℝ≥0
y : ℝ≥0∞
hx : x ≠ 0
⊢ x • y ≠ ∞ → y ≠ ∞

Tactic:
rintro h rfl; simp [smul_top (R := ℝ≥0), hx] at h

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

Goal state before:
pp: R : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Finite ι
inst✝³ : Finite ι'
F : Type u_8
inst✝² : FunLike F R ℝ
inst✝¹ : NonnegHomClass F R ℝ
inst✝ : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
⊢ ⨆ a, v (x a.1 * y a.2) = (⨆ i, v (x i)) * ⨆ j, v (y j)

Tactic:
simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
    Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]

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

Goal state before:
pp: α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
⊢ ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i

Tactic:
rcases isEmpty_or_nonempty ((a : α) → ι a) with h | h

Goal state after:
case inl
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
⊢ ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i

case inr
α : Type u_5
inst✝¹ : Fintype α
ι : α → Type u
inst✝ : ∀ (a : α), Finite (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ ⨆ i, ∏ a, f a (i a) = ∏ a, ⨆ i, f a i
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
⊢ (cobounded α)⁻¹ = 𝓝[≠] 0

Tactic:
rw [← comap_norm_atTop, ← Filter.comap_inv, ← comap_norm_nhdsGT_zero, ← inv_atTop₀,
    ← Filter.comap_inv]

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
⊢ comap Inv.inv (comap norm atTop) = comap norm (comap Inv.inv atTop)
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x ↦ x ^ (-m)) (𝓝[≠] 0) (cobounded α)

Tactic:
lift m to ℕ using by lia

Goal state after:
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : -↑m < 0
⊢ Tendsto (fun x ↦ x ^ (-↑m)) (𝓝[≠] 0) (cobounded α)
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
x✝ : MeasurableSet s
y : β
hy : f y ∈ s
⊢ MeasurableSet (f ⁻¹' {f y})

Tactic:
apply h

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

Goal state before:
pp: case true
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})

Tactic:
exact h

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
core : NormedSpace.Core 𝕜 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
core : NormedSpace.Core 𝕜 E
H : 𝓤 E = 𝓤 E
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
⊢ μ (⋃ i, s i) ≤ ∑' (i : ι), μ (s i)

Tactic:
refine rel_iSup_tsum μ measure_empty (· ≤ ·) (fun t ↦ ?_) _

Goal state after:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
inst✝ : Countable ι
s : ι → Set α
t : ℕ → Set α
⊢ μ (⨆ i, t i) ≤ ∑' (i : ℕ), μ (t i)
Module: Mathlib.Analysis.Normed.Module.Basic

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
T : TopologicalSpace E
core : NormedSpace.Core 𝕜 E
H : T = PseudoEMetricSpace.toUniformSpace.toTopologicalSpace
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h

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

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜' : Type u_2
E✝ : Type u_3
F : Type u_4
α : Type u_5
𝕜 : Type u_6
E : Type u_7
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Norm E
U : UniformSpace E
B : Bornology E
core : NormedSpace.Core 𝕜 E
HU : 𝓤 E = 𝓤 E
HB : ∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s
this : SeminormedAddCommGroup E := SeminormedAddCommGroup.ofCore ⋯
x y : E
h : dist x y = 0
⊢ ‖-x + y‖ = 0

Tactic:
exact h

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

Goal state before:
pp: case neg
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : ∀ (i : Set β), y ∈ i → MeasurableSet i → x ∈ i
hy : ∃ x_1, ∃ (_ : x ∈ x_1) (_ : MeasurableSet x_1), y ∉ x_1
⊢ False

Tactic:
obtain ⟨s, hxs, hs, hys⟩ := hy

Goal state after:
case neg
β : Type u_2
inst✝ : MeasurableSpace β
x y : β
hx : ∀ (i : Set β), y ∈ i → MeasurableSet i → x ∈ i
s : Set β
hxs : x ∈ s
hs : MeasurableSet s
hys : y ∉ s
⊢ False
Module: Mathlib.MeasureTheory.OuterMeasure.Operations

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
hf : Surjective f
m : OuterMeasure β
s : Set β
⊢ ((map f) ((comap f) m)) s = m s

Tactic:
by rw [map_apply, comap_apply, hf.image_preimage]

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

Goal state before:
pp: α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ MeasurableSpace.comap g MeasurableSpace.pi ≤ inst✝¹ ↔
    ∀ (a : δ), MeasurableSpace.comap (fun x ↦ g x a) (inst✝ a) ≤ inst✝¹

Tactic:
MeasurableSpace.pi,

Goal state after:
α : Type u_1
δ : Type u_4
X : δ → Type u_6
inst✝¹ : MeasurableSpace α
inst✝ : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
⊢ MeasurableSpace.comap g (⨆ a, MeasurableSpace.comap (fun b ↦ b a) (inst✝ a)) ≤ inst✝¹ ↔
    ∀ (a : δ), MeasurableSpace.comap (fun x ↦ g x a) (inst✝ a) ≤ inst✝¹
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance

Tactic:
MeasurableSpace.pi,

Goal state after:
β : Type u_2
δ : Type u_4
X✝ : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X✝ a)
X : (a : δ) → β → X✝ a
⊢ MeasurableSpace.comap (fun b a ↦ X a b) inferInstance = ⨆ a, MeasurableSpace.comap (X a) inferInstance
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case neg
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
j : δ
h : ¬j = a
⊢ Measurable fun x ↦ x.1 j

Tactic:
· exact measurable_pi_iff.1 measurable_fst _

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

Goal state before:
pp: f : ℕ → ℝ≥0
⊢ (¬Summable fun i ↦ ↑(f i)) ↔ Tendsto (fun n ↦ ∑ i ∈ range n, (fun i ↦ ↑(f i)) i) atTop atTop

Tactic:
simpa using mod_cast NNReal.not_summable_iff_tendsto_nat_atTop

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if -a < 0 then -1 else 0) = -if 0 < a then 1 else if a < 0 then -1 else 0

Tactic:
Right.neg_neg_iff

Goal state after:
α : Type u_1
inst✝³ : AddGroup α
inst✝² : Preorder α
inst✝¹ : DecidableLT α
inst✝ : AddRightStrictMono α
a : α
⊢ (if a < 0 then 1 else if 0 < a 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
a b : EReal
h : (a * b)⁻¹ = a⁻¹ * b⁻¹
⊢ (a * b)⁻¹ = a⁻¹ * b⁻¹

Tactic:
exact h

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

Goal state before:
pp: a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ b * (a / b) = a

Tactic:
rw [mul_comm, div_mul_cancel h₁ h₂ h₃]

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

Goal state before:
pp: a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a < c / b ↔ a * b < c

Tactic:
by
  nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' h.ne']
  rw [EReal.mul_div b a b, mul_comm a b]
  exact (strictMono_div_right_of_pos h h').lt_iff_lt

Goal state after: