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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : ¬Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
tprod_eq_one_of_not_multipliable hf

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : ¬Multipliable f L
⊢ 1 ≤ a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.Order

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
h : ∀ (i : ι), 1 ≤ g i
hg : Multipliable g L
hL : ¬L.NeBot
⊢ 1 ≤ ∏'[L] (i : ι), g i

Tactic:
simpa [tprod_bot hL] using one_le_finprod' h

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : ¬Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ 1

Tactic:
tprod_eq_one_of_not_multipliable hf

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
h : ∀ (i : ι), f i ≤ 1
hf : ¬Multipliable f L
⊢ 1 ≤ 1
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case e'_2
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
α : Type u_3
inst✝ : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
R : M → M → Prop
m_iSup : ∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))
s₁ s₂ : α
⊢ m s₁ * m s₂ = ∏' (b : Bool), m (bif b then s₁ else s₂)

Tactic:
· rw [tprod_fintype, Fintype.prod_bool, cond, cond]

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

Goal state before:
pp: case neg
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 | 0 ≤ n}
⊢ ∀ ⦃a : ℕ⦄, a ∈ t → a ∉ ↑s

Tactic:
· exact fun _ _ hs ↦ h ⟨_, hs⟩

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun n ↦ f ↑n * f (Int.negSucc n)) m

Tactic:
have : Injective Int.negSucc := @Int.negSucc.inj

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
⊢ HasProd (fun n ↦ f ↑n * f (Int.negSucc n)) m
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ tprod (f ∘ ⇑g) = ∏' (b : β), f b

Tactic:
tprod_eq_prod' hf_fin.coe_toFinset.ge,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : β → α
hf_fin : (mulSupport f).Finite
g : γ ↪ β
hf : mulSupport f ⊆ Set.range ⇑g
this : mulSupport f = ⇑g '' mulSupport (f ∘ ⇑g)
hfg_fin : (mulSupport (f ∘ ⇑g)).Finite
⊢ tprod (f ∘ ⇑g) = ∏ b ∈ hf_fin.toFinset, f b
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n

Tactic:
simpa [hf.tprod_eq_zero_mul] using tprod_pnat_eq_tprod_succ

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

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

Tactic:
by
  by_cases h₀ : i ∈ ⋃ d, s d
  · simp only [h₀, hs, Set.mulIndicator_of_mem, tprod_mulIndicator_of_disjoint_on_mulSupport_of_mem]
  · aesop

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

Goal state before:
pp: α : Type u_2
L : SummationFilter α
f : α → ℝ≥0
a : ℝ≥0
⊢ ↑(∑'[L] (x : α), f x * a) = ↑((∑'[L] (x : α), f x) * a)

Tactic:
simp only [coe_tsum, NNReal.coe_mul, tsum_mul_right]

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

Goal state before:
pp: α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : (fun x ↦ (f x).toReal) =ᶠ[l] fun x ↦ (g x).toReal
⊢ f =ᶠ[l] g

Tactic:
filter_upwards [hfi, hgi, hfg] with _ hfx hgx _
  rwa [← ENNReal.toReal_eq_toReal_iff' hfx hgx]

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

Goal state before:
pp: case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + min ε ↑δ < (a, b).2

Tactic:
grw [min_le_right]

Goal state after:
case inr.refine_1.refine_2
x : ℝ≥0∞
xt : x ≠ ∞
x0 : 0 < x
a b : ℝ≥0∞
ha : (a, b).1 < x
hb : x < (a, b).2
ε : ℝ≥0∞
ε0 : 0 < ε
hε : ε < x - (a, b).1
δ : ℝ≥0
δ0 : 0 < δ
hδ : x + ↑δ < (a, b).2
⊢ x + ↑δ < (a, b).2
Module: Mathlib.Topology.Algebra.InfiniteSum.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
⊢ ClusterPt a (Filter.map (fun s ↦ ∏ i ∈ s, f i) atTop)

Tactic:
simp only [← mapClusterPt_def, mapClusterPt_iff_frequently, frequently_atTop]

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformGroup α
γ : β → Type u_4
f : (b : β) × γ b → α
g : β → α
a : α
hf : ∀ (b : β), HasProd (fun c ↦ f ⟨b, c⟩) (g b)
hg : HasProd g a
h : CauchySeq fun s ↦ ∏ i ∈ s, f i
⊢ ∀ s ∈ 𝓝 a, ∀ (a : Finset ((b : β) × γ b)), ∃ b, a ⊆ b ∧ ∏ i ∈ b, f i ∈ s
Module: Mathlib.Analysis.Normed.Group.Continuity

Goal state before:
pp: E : Type u_4
inst✝ : SeminormedCommGroup E
x : E
⊢ Tendsto (fun a ↦ ‖a / x‖) (𝓝 x) (𝓝 0)

Tactic:
by
  simpa [dist_eq_norm_div] using
    tendsto_id.dist (tendsto_const_nhds : Tendsto (fun _a => (x : E)) (𝓝 x) _)

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

Goal state before:
pp: β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ Icc (a - ib) (a + ib)) ↔
    ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ∈ Icc (a - ε) (a + ε)

Tactic:
simp only [true_and]; rfl

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

Goal state before:
pp: β : Type u_2
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
⊢ (∀ (ib : ℝ≥0∞), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ Iic ib) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
simp only [true_and]; rfl

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

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ (((𝓤 α).lift' gen).lift' fun s ↦ s ○ s) = (𝓤 α).lift' fun s ↦ gen s ○ gen s

Tactic:
rw [lift'_lift'_assoc]
      · exact monotone_gen
      · exact monotone_id.relComp monotone_id

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

Goal state before:
pp: x y : ℝ≥0∞
hp : (x, y) ∈ {p | p ≠ (∞, ∞)}
⊢ ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} (x, y)

Tactic:
simp only [Ne, Set.mem_ofPred_eq, Prod.mk_inj] at hp

Goal state after:
x y : ℝ≥0∞
hp : ¬(x = ∞ ∧ y = ∞)
⊢ ContinuousWithinAt (fun p ↦ p.1 - p.2) {p | p ≠ (∞, ∞)} (x, y)
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
d : X → X → ℝ≥0 := fun x y ↦ if h : ∃ n, (x, y) ∉ U n then (1 / 2) ^ Nat.find h else 0
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹

Tactic:
have hd_symm x y : d x y = d y x := by simp only [d, (U _).comm]

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
hd₀ : ∀ {x y : X}, d x y = 0 ↔ Inseparable x y
hd_symm : ∀ (x y : X), d x y = d y x
⊢ ∃ I, PseudoMetricSpace.toUniformSpace = inst✝¹
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 α β
s : Set (α × β)
hs : IsBounded s
⊢ UniformContinuousOn (Function.uncurry fun x1 x2 ↦ x1 • x2) s

Tactic:
rcases hs.subset_ball_lt 0 0 with ⟨C, hC₀, hC⟩
  rw [Metric.uniformContinuousOn_iff_le]
  intro ε hε
  refine ⟨ε / (2 * C), by positivity, fun ⟨a, b⟩ hab ⟨x, y⟩ hxy h ↦ ?_⟩
  grw [hC, Metric.mem_ball, Prod.dist_eq, max_lt_iff] at hab hxy
  rw [Prod.dist_eq, max_le_iff] at h
  dsimp at hab hxy h ⊢
  grw [dist_triangle _ (a • y), dist_pair_smul, dist_smul_pair, hab.1, hxy.2, h.2, h.1]
  field_simp
  norm_num1

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

Goal state before:
pp: α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε

Tactic:
refine ⟨x + b, mt (Set.mem_singleton_iff.trans add_eq_left).1 <| norm_pos_iff.1 hb0, ?_⟩

Goal state after:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε
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 (⇑f '' s) = ↑(ratio f) * ediam s

Tactic:
by
  refine ((lipschitz f).ediam_image_le s).antisymm ?_
  apply ENNReal.mul_le_of_le_div'
  rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
  exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]

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

Goal state before:
pp: α : Type u_2
inst✝ : SeminormedRing α
a b c : α
ha : ‖a‖ ≤ 1
⊢ ‖c - a * b‖ ≤ ‖c - a‖ + ‖a * (1 - b)‖

Tactic:
by
        simpa [mul_one_sub] using norm_sub_le_norm_sub_add_norm_sub c a (a * b)

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

Goal state before:
pp: ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ TProd.elim' h ⁻¹' TProd.mk l ⁻¹' Set.tprod l t = Set.tprod l t

Tactic:
preimage_preimage

Goal state after:
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
l : List ι
hnd : l.Nodup
h : ∀ (i : ι), i ∈ l
t : (i : ι) → Set (α i)
h2 : {i | i ∈ l} = univ
⊢ (fun x ↦ TProd.mk l (TProd.elim' h x)) ⁻¹' Set.tprod l t = Set.tprod l t
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
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
⊢ ∀ᶠ (a : ι × X) in l ×ˢ 𝓝[s] x, (f a.2, F a.1 a.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ

Tactic:
filter_upwards [hF x hx (dist_mem_uniformity (half_pos hr₀)), tendsto_snd hUx] with y hy₁ hy₂

Goal state after:
α : Type u_1
inst✝¹ : NormedDivisionRing α
X : Type u_4
ι : Type u_5
inst✝ : TopologicalSpace X
s : Set X
F : ι → X → α
f : X → α
l : Filter ι
hF : ∀ x ∈ s, Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (l ×ˢ 𝓝[s] x) (𝓤 α)
hf : ∀ x ∈ s, Disjoint (map f (𝓝[s] x)) (𝓝 0)
x : X
hx : x ∈ s
U : Set X
hUx : U ∈ 𝓝[s] x
r : ℝ
hr₀ : 0 < r
hr : Disjoint (f '' id U) (ball 0 r)
y : ι × X
hy₁ : y ∈ (fun y ↦ (f y.2, F y.1 y.2)) ⁻¹' {p | dist p.1 p.2 < r / 2}
hy₂ : y ∈ Prod.snd ⁻¹' U
⊢ (f y.2, F y.1 y.2) ∈ (closedBall 0 (r / 2))ᶜ ×ˢ (closedBall 0 (r / 2))ᶜ
Module: Mathlib.MeasureTheory.MeasurableSpace.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet ((fun _a ↦ b) ⁻¹' s)

Tactic:
by_cases h : b ∈ s <;> simp [h]

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

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

Tactic:
by
  apply measurable_to_countable'
  rintro (- | -)
  · convert! h.compl
    rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]
  exact h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : OuterMeasure α
a : α
x✝¹ x✝ : Set α
h : x✝¹ ⊆ x✝
⊢ x✝¹.indicator (fun x ↦ 1) a ≤ x✝.indicator (fun x ↦ 1) a

Tactic:
grw [h]

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ CauchySeq f

Tactic:
apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)

Goal state after:
case hf
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ ∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)

case hd
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun i ↦ ↑(d i)) n
hd : Summable fun i ↦ ↑(d i)
⊢ Summable d
Module: Mathlib.Data.Sign.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h : (if 0 < a then 1 else if a < 0 then -1 else 0) = 0
⊢ a = 0

Tactic:
split_ifs at h with h_1 h_2

Goal state after:
case neg
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : α
h_1 : ¬0 < a
h_2 : ¬a < 0
h : 0 = 0
⊢ a = 0
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ min (-x) (-y) = -max x y

Tactic:
rcases le_total x y with (h | h)

Goal state after:
case inl
x y : EReal
h : x ≤ y
⊢ min (-x) (-y) = -max x y

case inr
x y : EReal
h : y ≤ x
⊢ min (-x) (-y) = -max x y
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: x y : EReal
⊢ max (-x) (-y) = -min x y

Tactic:
rcases le_total x y with (h | h)

Goal state after:
case inl
x y : EReal
h : x ≤ y
⊢ max (-x) (-y) = -min x y

case inr
x y : EReal
h : y ≤ x
⊢ max (-x) (-y) = -min x y
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: ⊢ ⨅ l, ⨅ (_ : l < ⊤), 𝓟 (Ioi l) = ⨅ a, ⨅ (_ : a ≠ ⊤), 𝓟 (Ioi a)

Tactic:
by simp only [lt_top_iff_ne_top]

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

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

Tactic:
unfold LowerSemicontinuousWithinAt at h

Goal state after:
case mp
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
x : α
γ : Type u_4
inst✝ : CompleteLinearOrder γ
f : α → γ
h : SemicontinuousWithinAt (fun x1 x2 ↦ f x1 > x2) s x
⊢ f x ≤ liminf f (𝓝[s] x)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inr
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
⊢ ∀ᶠ (a : α) in f, (u * v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v, hv]
    with x x_a x_b v_0

Goal state after:
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
⊢ (u * v) x < c
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u v : α → EReal
hu : ∃ᶠ (x : α) in f, 0 ≤ u x
hv : 0 ≤ᶠ[f] v
h✝ : f.NeBot
u_0 : 0 ≤ limsup u f
h₁ : 0 < limsup u f ∨ limsup v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ 0 < limsup v f
a : EReal
a_u : a > limsup u f
b : EReal
b_v : b > limsup v f
c : EReal
c_ab : c > a * b
x : α
x_a : u x < a
x_b : v x < b
v_0 : 0 x ≤ v x
hux : u x < 0
⊢ (u * v) x ≤ a * b

Tactic:
apply (mul_nonpos_iff.2 (.inr ⟨hux.le, v_0⟩)).trans
    exact mul_nonneg (u_0.trans a_u.le) (v_0.trans x_b.le)

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

Goal state before:
pp: case pos
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : x.2 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

pp: case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y

Tactic:
· simp [hx₂]

Goal state after:
case neg
x : EReal × EReal
y : EReal
hx₁ : ¬x.1 = ⊥
hx₂ : ¬x.2 = ⊥
⊢ (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x y →
    ∀ᶠ (x' : EReal × EReal) in 𝓝 x, (fun x1 x2 ↦ (fun p ↦ p.1 + p.2) x1 > x2) x' y
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: case cons
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
t✝ : Finset (Set α)
a : Set α
t : Finset (Set α)
hat : a ∉ t
t_ne : t.Nonempty
ih : (∀ s ∈ t, s ∈ S) → (⋂ s ∈ t, s).Nonempty → ⋂ s ∈ t, s ∈ S
ht : ∀ s ∈ Finset.cons a t hat, s ∈ S
h' : (⋂ s ∈ Finset.cons a t hat, s).Nonempty
⊢ ⋂ s ∈ Finset.cons a t hat, s ∈ S

Tactic:
| cons a t hat t_ne ih =>

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s₁ : Set α
⊢ m.IsCaratheodory s₁ → m.IsCaratheodory s₁ᶜ

Tactic:
by
  simp [IsCaratheodory, sdiff_eq, add_comm]

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

Goal state before:
pp: case a
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
P0 : P ∅
m0 : m ∅ P0 = 0
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s : Set α
⊢ ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht ≤ (inducedOuterMeasure m P0 m0) s

Tactic:
· refine le_iInf ?_
    intro f
    refine le_iInf ?_
    intro hf
    refine le_trans ?_ (extend_iUnion_le_tsum_nat' _ msU _)
    refine le_iInf ?_
    intro h2f
    exact iInf_le_of_le _ (iInf_le_of_le h2f <| iInf_le _ hf)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n ↦ {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ i ∈ S, m i

Tactic:
have hi' : i ∈ S := hpt hi

Goal state after:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n ↦ {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ i ∈ S, m i
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ (fun x ↦ x ∈ s) ⁻¹' x = ∅ ∨ (fun x ↦ x ∈ s) ⁻¹' x = s ∨ (fun x ↦ x ∈ s) ⁻¹' x = sᶜ ∨ (fun x ↦ x ∈ s) ⁻¹' x = univ

Tactic:
suffices x = univ by grind

Goal state after:
case pos
α : Type u_1
s : Set α
x : Set Prop
hT : True ∈ x
hF : False ∈ x
⊢ x = univ
Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort uι
inst✝¹ : MeasurableSpace α
f : ι → Filter α
inst✝ : ∀ (i : ι), (f i).IsMeasurablyGenerated
t : Set (PLift ι)
ht : t.Finite
V : ↑t → Set α
hVf : ∀ (i : ↑t), V i ∈ f (Equiv.plift ↑i)
U : ↑t → Set α
hUf : ∀ (i : ↑t), U i ∈ f (Equiv.plift ↑i)
hU : ∀ (i : ↑t), MeasurableSet (U i) ∧ U i ⊆ V i
⊢ MeasurableSet (⋂ i, U i)

Tactic:
have := ht.countable.toEncodable.countable
    exact MeasurableSet.iInter fun i => (hU i).1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), (μ i) t = (μ i).trim s

Tactic:
choose t hst ht hμt using fun i => (μ i).exists_measurable_superset_eq_trim s
  replace hst := subset_iInter hst
  replace ht := MeasurableSet.iInter ht
  refine ⟨⋂ i, t i, hst, ht, fun i => le_antisymm ?_ ?_⟩
  exacts [hμt i ▸ (μ i).mono (iInter_subset _ _), (measure_mono hst).trans_eq ((μ i).trim_eq ht)]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
m1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ : Measure α
s : Set β
⊢ (map f μ) s = μ (f ⁻¹' s)

Tactic:
refine le_antisymm ?_ (le_map_apply hf.measurable.aemeasurable s)
  set t := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
  have htm : MeasurableSet t :=
    (hf.measurableSet_image.2 <| measurableSet_toMeasurable _ _).union
      hf.measurableSet_range.compl
  have hst : s ⊆ t := by
    rw [subset_union_compl_iff_inter_subset, ← image_preimage_eq_inter_range]
    exact image_mono (subset_toMeasurable _ _)
  have hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s) := by
    rw [preimage_union, preimage_compl, preimage_range, compl_univ, union_empty,
      hf.injective.preimage_image]
  calc
    μ.map f s ≤ μ.map f t := by gcongr
    _ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable]

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s : Set X
b : X
⊢ ⇑ofDual ⁻¹' s ⊆ Iio (toDual b) ∧
      ((⇑ofDual ⁻¹' s).Nonempty → ∀ a < toDual b, (⇑ofDual ⁻¹' s ∩ Ioo a (toDual b)).Nonempty) ↔
    s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)

Tactic:
simp [← preimage_inter, ofDual.surjective]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : Countable ι
m : ι → Measure α
inst✝ : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Tactic:
· rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
    infer_instance

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝ : IsEmpty α
⊢ IsFiniteMeasure μ

Tactic:
eq_zero_of_isEmpty μ

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
m0 : MeasurableSpace α
mβ : MeasurableSpace β
μ ν ν₁ ν₂ : Measure α
s t : Set α
inst✝ : IsEmpty α
⊢ IsFiniteMeasure 0