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

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = univ
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
rw [hs]

Goal state after:
case inr.inr.inr.inr.inr.inr.inr.inr.inl
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s = univ
⊢ univ ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inr.inr.inr.inr.inr.inr.inr.inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s ∈ {∅}
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
rw [hs]

Goal state after:
case inr.inr.inr.inr.inr.inr.inr.inr.inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs✝ : s ∈ {s | IsPreconnected s}
hs : s ∈ {∅}
⊢ ∅ ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ NoncompactSpace α

Tactic:
rw [← not_compactSpace_iff, compactSpace_iff_isBounded_univ, isBounded_iff_ediam_ne_top,
    Classical.not_not]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (⇑e ⁻¹' Ioi a)

Tactic:
rw [e.preimage_Ioi]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen[inst✝³] (Ioi (e.symm a))
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x ↦ True) = liminf u f

Tactic:
by
  simp [bliminf_eq, liminf_eq]

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

Goal state before:
pp: x y : EReal
h1 : x ≠ ⊥ ∨ y ≠ ⊥
h2 : x ≠ ⊤ ∨ y ≠ ⊤
⊢ -(x - y) = -x + y

Tactic:
by
  rw [sub_eq_add_neg, neg_add _ _, sub_eq_add_neg, neg_neg] <;> simp_all

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y

Tactic:
refine ⟨fun h _ h' ↦ (eventually_lt_of_limsup_lt (h.trans_lt h') h₂).mono fun _ ↦ le_of_lt, ?_⟩
  rw [← forall_gt_iff_le]
  intro h y x_y
  obtain ⟨z, x_z, z_y⟩ := exists_between x_y
  exact (limsup_le_of_le h₁ (h z x_z)).trans_lt z_y

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

Goal state before:
pp: α : Type u_3
s : Finset α
⊢ ⋂ i, Ici {↑i} ⊆ Ici s

Tactic:
simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici,
    Finset.mem_singleton, Finset.subset_iff, forall_eq]

Goal state after:
α : Type u_3
s : Finset α
⊢ ∀ (x : Finset α), (∀ x_1 ∈ ↑s, x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x
Module: Mathlib.Topology.Order.LiminfLimsup

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

Tactic:
by_cases hn : b'' < u n r

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

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

Goal state before:
pp: case inl
ι : 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₂
i : ι
⊢ extend e f 1 (e i) ≤ g (e i)

Tactic:
rw [he.extend_apply]

Goal state after:
case inl
ι : 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₂
i : ι
⊢ f i ≤ g (e i)
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
K : Type u_4
inst✝² : CommGroupWithZero K
inst✝¹ : TopologicalSpace K
f g : α → K
inst✝ : SeparatelyContinuousMul K
c : K
hc : HasProd f c
s : Finset α
hs : ∀ a ∈ s, f a ≠ 0
hs' : ∀ a ∉ s, f a = g a
t : Finset α
ht : s ⊆ t
⊢ (∏ i ∈ t, f i) * ((∏ i ∈ s, g i) / ∏ i ∈ s, f i) = ((∏ i ∈ s, f i) * ∏ i ∈ t \ s, g i) * ?m.133

Tactic:
by
    conv_lhs => rw [← union_sdiff_of_subset ht, prod_union disjoint_sdiff,
      prod_congr rfl fun i hi ↦ hs' i (mem_sdiff.mp hi).2]

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

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
hf : f 0 = 1
n : ℕ
hn : n ∈ mulSupport f
h : n > 0
⊢ n ∈ Set.range PNat.val

Tactic:
· exact ⟨⟨n, h⟩, rfl⟩

Goal state after:
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 s ↦ ∏ b ∈ s, (fun x ↦ 1 + f x) b) (SummationFilter.unconditional ι).filter (nhds x)
a : α
ha : HasSum (fun i ↦ f i * ∏ j < i, (1 + f j)) a
⊢ 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j) = x

Tactic:
conv at hx in fun _ ↦ _ => ext _; rw [prod_one_add_ordered]

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
⊢ 1 + ∑' (i : ι), f i * ∏ j < i, (1 + f j) = x
Module: Mathlib.Topology.MetricSpace.ProperSpace.Real

Goal state before:
pp: x : ℝ≥0
r : ℝ
emb : IsClosedEmbedding toReal
⊢ IsCompact (Metric.closedBall x r)

Tactic:
exact emb.isCompact_preimage (K := Metric.closedBall x r) (isCompact_closedBall _ _)

Goal state after:
Module: Mathlib.Topology.Sequences

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a : ℕ
⊢ ∃ b, a ≤ b ∧ ∃ n ≥ j, y n ∈ closure[inst✝¹] {x b}

Tactic:
have := (Filter.eventually_all_finite (by simp : (Iic a).Finite)).2 fun i hi => hm i

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
x : ℕ → X
inst✝ : SequentialSpace X
hx : ∀ (l : X) (φ : ℕ → ℕ), StrictMono φ → ¬Tendsto (x ∘ φ) atTop (𝓝 l)
y : ℕ → X
l : X
hy : ∀ (n : ℕ), y n ∈ ⋃ i, closure[inst✝¹] {x i}
hy' : Tendsto y atTop (𝓝 l)
hm : ∀ (m : ℕ), ∀ᶠ (x_1 : ℕ) in atTop, y x_1 ∉ closure[inst✝¹] {x m}
j a : ℕ
this : ∀ᶠ (x_1 : ℕ) in atTop, ∀ i ∈ Iic a, y x_1 ∉ closure[inst✝¹] {x i}
⊢ ∃ b, a ≤ b ∧ ∃ n ≥ j, y n ∈ closure[inst✝¹] {x b}
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
⊢ HasProd f (a * b)

Tactic:
have : Tendsto ((∏ b ∈ ·, f b) ∘ sumEquiv.symm) (atTop.map sumEquiv) (nhds (a * b)) := by
    rw [Finset.sumEquiv.map_atTop, ← prod_atTop_atTop_eq]
    convert! (tendsto_mul.comp (nhds_prod_eq (x := a) (y := b) ▸ Tendsto.prodMap h₁ h₂))
    ext s
    simp

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
this : Tendsto ((fun x ↦ ∏ b ∈ x, f b) ∘ ⇑sumEquiv.symm) (Filter.map (⇑sumEquiv) atTop) (𝓝 (a * b))
⊢ HasProd f (a * b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → b ∈ (fun s ↦ ∏ b ∈ s, f b) ⁻¹' s
⊢ ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, ∏ b ∈ x, g b ∈ id s

Tactic:
use u.image Sigma.fst, trivial

Goal state after:
case right
α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : ContinuousMul α
inst✝ : RegularSpace α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
ha : HasProd f a
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
s : Set α
hs : s ∈ 𝓝 a
hsc : IsClosed[inst✝²] s
u : Finset ((b : β) × γ b)
hu : ∀ (b : Finset ((b : β) × γ b)), u ⊆ b → b ∈ (fun s ↦ ∏ b ∈ s, f b) ⁻¹' s
⊢ ∀ x ∈ Set.Ici (image Sigma.fst u), ∏ b ∈ x, g b ∈ id s
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : ↑f ≤ 𝓝 a
hb : ↑g ≤ 𝓝 b
⊢ Inseparable a b ↔ Inseparable f g

Tactic:
← tendsto_id'

Goal state after:
α : Type u
inst✝ : UniformSpace α
f g : CauchyFilter α
a b : α
ha : Tendsto id (↑f) (𝓝 a)
hb : Tendsto id (↑g) (𝓝 b)
⊢ Inseparable a b ↔ Inseparable f g
Module: Mathlib.Topology.UniformSpace.Completion

Goal state before:
pp: case refine_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion α
a : α
⊢ Completion.extension (lift' coe') (Completion.map SeparationQuotient.mk ↑a) = ↑a

Tactic:
rw [map_coe uniformContinuous_mk, extension_coe (uniformContinuous_lift' _),
      lift'_mk (uniformContinuous_coe _)]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) = edist x' y' + 2 * edist (x, y) (x', y')

Tactic:
← mul_two,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + edist (x, y) (x', y') * 2 = edist x' y' + 2 * edist (x, y) (x', y')
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖(↑a - 1) * (↑b - 1) - (↑b - 1) * (↑a - 1)‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖

Tactic:
simp_rw [sub_one_mul, mul_sub_one]

Goal state after:
α : Type u_2
inst✝ : SeminormedRing α
a b : αˣ
⊢ ‖↑a * ↑b - ↑b * ↑a‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ = ‖↑a * ↑b - ↑a - (↑b - 1) - (↑b * ↑a - ↑b - (↑a - 1))‖ * ‖↑a⁻¹‖ * ‖↑b⁻¹‖
Module: Mathlib.Analysis.Normed.MulAction

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x : αᵐᵒᵖ
y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Tactic:
simpa [sub_mul, dist_eq_norm, mul_comm] using! norm_mul_le (y₁ - y₂) x.unop

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

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

Tactic:
exact Finite.le_ciSup_of_le i le_rfl

Goal state after:
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

Tactic:
by_cases hj : j = i

Goal state after:
case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j

case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : (i_1 : ↥{i}) → π ↑i_1
j : ι
hj : ¬j = i
⊢ updateFinset x {i} y j = update x i (y ⟨i, ⋯⟩) j
Module: Mathlib.Data.Finset.Update

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
by_cases hj : j = i

Goal state after:
case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ TProd.mk l ⁻¹' Set.tprod l t ↔ f ∈ {x | x ∈ l}.pi t

Tactic:
mk_preimage_tprod l t

Goal state after:
ι : Type u
α : ι → Type v
i : ι
l : List ι
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ l}.pi t ↔ f ∈ {x | x ∈ l}.pi t
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
s : Set α
t : Set β
h : (s ×ˢ t).Nonempty
⊢ MeasurableSet (s ×ˢ t) ↔ MeasurableSet s ∧ MeasurableSet t ∨ s = ∅ ∨ t = ∅

Tactic:
simp [← not_nonempty_iff_eq_empty, prod_nonempty_iff.mp h, measurableSet_prod_of_nonempty h]

Goal state after:
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:
rw [map_apply, comap_apply, hf.image_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (restrict (range f)) ⊤ = ⊤

Tactic:
hf.range_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ (restrict univ) ⊤ = ⊤
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

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

Tactic:
dsimp [update]

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝¹ : (a : δ) → MeasurableSpace (X a)
a : δ
inst✝ : DecidableEq δ
j : δ
⊢ Measurable fun x ↦ if h : j = a then ⋯ ▸ x.2 else x.1 j
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
ι : Sort uι
inst✝¹ : MeasurableSpace α
inst✝ : Countable ι
p : ι → α → Prop
hp : ∀ (i : ι), Measurable (p i)
⊢ MeasurableSet {a | ∃ i, p i a}

Tactic:
rw [ofPred_exists]; exact MeasurableSet.iUnion fun i ↦ (hp i).setOf

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

Goal state before:
pp: ⊢ ∀ (x y : SignType), -x * y = -(x * y)

Tactic:
rintro ⟨_⟩ ⟨_⟩

Goal state after:
case zero.zero
⊢ -zero * zero = -(zero * zero)

case zero.neg
⊢ -zero * neg = -(zero * neg)

case zero.pos
⊢ -zero * pos = -(zero * pos)

case neg.zero
⊢ -neg * zero = -(neg * zero)

case neg.neg
⊢ -neg * neg = -(neg * neg)

case neg.pos
⊢ -neg * pos = -(neg * pos)

case pos.zero
⊢ -pos * zero = -(pos * zero)

case pos.neg
⊢ -pos * neg = -(pos * neg)

case pos.pos
⊢ -pos * pos = -(pos * pos)
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: ⊢ ∀ (x y : SignType), x * -y = -(x * y)

Tactic:
rintro ⟨_⟩ ⟨_⟩

Goal state after:
case zero.zero
⊢ zero * -zero = -(zero * zero)

case zero.neg
⊢ zero * -neg = -(zero * neg)

case zero.pos
⊢ zero * -pos = -(zero * pos)

case neg.zero
⊢ neg * -zero = -(neg * zero)

case neg.neg
⊢ neg * -neg = -(neg * neg)

case neg.pos
⊢ neg * -pos = -(neg * pos)

case pos.zero
⊢ pos * -zero = -(pos * zero)

case pos.neg
⊢ pos * -neg = -(pos * neg)

case pos.pos
⊢ pos * -pos = -(pos * pos)
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: s : SignType
k : ℕ
⊢ s ^ (2 * k) * s = s

Tactic:
pow_mul,

Goal state after:
s : SignType
k : ℕ
⊢ (s ^ 2) ^ k * s = s
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : 0 < b
⊢ 1 ≤ 1

Tactic:
try constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1

Tactic:
try constructor

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : b < 0
⊢ 1 ≤ -1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0

Tactic:
try constructor

Goal state after:
case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : 0 < a
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 1 ≤ 0
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_ : 0 < b
⊢ -1 ≤ 1

Tactic:
try constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : b < 0
⊢ -1 ≤ -1

Tactic:
try constructor

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

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : a < 0
_✝ : ¬0 < b
_ : ¬b < 0
⊢ -1 ≤ 0

Tactic:
try constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : 0 < b
⊢ 0 ≤ 1

Tactic:
try constructor

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1

Tactic:
try constructor

Goal state after:
case pos
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : b < 0
⊢ 0 ≤ -1
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: case neg
α : Type u_1
inst✝² : Zero α
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a✝ a b : α
h : a ≤ b
h₁ : ¬0 < a
h₄ : ¬a < 0
h₂ : ¬0 < b
h₃ : ¬b < 0
⊢ 0 ≤ 0

Tactic:
try constructor

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

Goal state before:
pp: case mp
x y : EReal
⊢ x.abs = y.abs ∧ sign x = sign y → x = y

pp: case mpr
x y : EReal
⊢ x = y → x.abs = y.abs ∧ sign x = sign y

Tactic:
· rintro ⟨habs, hsign⟩
    rw [← x.sign_mul_abs, ← y.sign_mul_abs, habs, hsign]

Goal state after:
case mpr
x y : EReal
⊢ x = y → x.abs = y.abs ∧ sign x = sign y
Module: Mathlib.Topology.Semicontinuity.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
x : α
s : Set α
t : Set β
ht : IsClosed[inst✝] t
⊢ (¬∀ᶠ (x' : α) in 𝓝[s] x, (f x' ∩ tᶜ).Nonempty) → ¬(f x ∩ tᶜ).Nonempty ↔ (∃ᶠ (x' : α) in 𝓝[s] x, f x' ⊆ t) → f x ⊆ t

Tactic:
simp [not_nonempty_iff_eq_empty, ← disjoint_iff_inter_eq_empty, disjoint_compl_right_iff_subset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → Set β
h : HasOpenCGraph f
⊢ HasOpenLowerSections f

Tactic:
intro x b hb
  have hopen : IsOpen {x' : α | b ∈ f x'} := by
    simpa using h.preimage (continuous_id.prodMk continuous_const)
  simpa [Filter.Eventually] using hopen.mem_nhds hb

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow (f '' s)

Tactic:
simp only [h, Set.image_empty]

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
f : α → β
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow ∅
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
s : Set α
y : β
inst✝¹ : Zero β
inst✝ : Preorder β
hs : IsClosed[inst✝²] s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, (fun x1 x2 ↦ s.indicator (fun _x ↦ y) x1 > x2) x' z

Tactic:
· filter_upwards [hs.isOpen_compl.mem_nhds h]
    simp +contextual [hz]

Goal state after: