mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Prod.TProd

Goal state before:
pp: case fst
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.1 = w.1

pp: case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.2 = w.2

Tactic:
· rw [← elim_self v, hvw, elim_self]

Goal state after:
case snd
ι : Type u
α : ι → Type v
inst✝ : DecidableEq ι
i : ι
is : List ι
hl : (i :: is).Nodup
v w : TProd α (i :: is)
hvw : ∀ (i_1 : ι) (hi : i_1 ∈ i :: is), v.elim hi = w.elim hi
⊢ v.2 = w.2
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ DiscreteTopology 𝕜 ∨ Nonempty { h' // h'.toNormedField = h }

Tactic:
simp_rw [discreteTopology_iff_isOpen_singleton_zero, Metric.isOpen_singleton_iff, dist_eq_norm,
             sub_zero]

Goal state after:
case neg
𝕜 : Type u_4
h : NormedField 𝕜
H : ¬∃ x, x ≠ 0 ∧ ‖x‖ ≠ 1
⊢ (∃ ε > 0, ∀ (y : 𝕜), ‖y‖ < ε → y = 0) ∨ Nonempty { h' // h'.toNormedField = h }
Module: Mathlib.Analysis.Normed.Field.Lemmas

Goal state before:
pp: 𝕜 : Type u_4
inst✝ : NontriviallyNormedField 𝕜
n : ℤ
x : 𝕜
⊢ ContinuousAt (fun x ↦ x ^ n) x ↔ x ≠ 0 ∨ 0 ≤ n

Tactic:
refine ⟨?_, continuousAt_zpow₀ _ _⟩
  contrapose!
  rintro ⟨rfl, hm⟩ hc
  exact (hc.tendsto.mono_left nhdsWithin_le_nhds).not_tendsto (Metric.disjoint_nhds_cobounded _)
    (tendsto_zpow_nhdsNE_zero_cobounded hm)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort u_6
s t u : Set α
m : MeasurableSpace α
p : Set α → Prop
h : ∀ (s : Set α), p s ↔ MeasurableSet s
⊢ ∀ (f : ℕ → Set α), (∀ (i : ℕ), p (f i)) → p (⋃ i, f i)

Tactic:
by simpa only [h] using! m.measurableSet_iUnion

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert univ S) = generateFrom S

Tactic:
insert_eq,

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ generateFrom ({univ} ∪ S) = generateFrom S
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ generateFrom (insert ∅ S) = generateFrom S

Tactic:
insert_eq,

Goal state after:
α : Type u_1
S : Set (Set α)
⊢ generateFrom ({∅} ∪ S) = generateFrom S
Module: Mathlib.MeasureTheory.MeasurableSpace.Defs

Goal state before:
pp: α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s

Tactic:
rw [measurableSet_iSup]

Goal state after:
α : Type u_1
ι : Sort u_6
m : ι → MeasurableSpace α
s : Set α
⊢ GenerateMeasurable {s | ∃ i, MeasurableSet s} s ↔ MeasurableSet s
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
p : β → Prop
f : α → β
hf : Measurable f
h : ∀ (x : α), p (f x)
t : Set (Subtype p)
x✝ : MeasurableSet t
s : Set β
hs : MeasurableSet s ∧ Subtype.val ⁻¹' s = t
⊢ MeasurableSet ((fun x ↦ ⟨f x, ⋯⟩) ⁻¹' Subtype.val ⁻¹' s)

Tactic:
simp only [← preimage_comp, Function.comp_def, hf hs.1]

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

Goal state before:
pp: G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
n : ℕ
hn : C / ε < ↑n
hnpos : 0 < ↑n
⊢ n ≠ 0

Tactic:
rintro rfl

Goal state after:
G : Type u_6
H : Type u_7
inst✝² : SeminormedAddCommGroup G
inst✝¹ : SeminormedAddCommGroup H
inst✝ : NormedSpace ℝ H
s : Set G
f : G →+ H
hs : s ∈ 𝓝 0
hbounded : Bornology.IsBounded (⇑f '' s)
δ : ℝ
hδ : δ > 0
hUε : ball 0 δ ⊆ s
C ε : ℝ
hε : 0 < ε
hC : ∀ (a : G), ‖a‖ < δ → ‖f a‖ < C
hC₀ : 0 < C
hn : C / ε < ↑0
hnpos : 0 < ↑0
⊢ False
Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions

Goal state before:
pp: δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi t
⊢ MeasurableSet (s.pi t) ↔ ∀ i ∈ s, MeasurableSet (t i)

Tactic:
refine ⟨fun hst i hi => ?_, MeasurableSet.pi hs⟩

Goal state after:
δ : Type u_4
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
s : Set δ
t : (i : δ) → Set (X i)
hs : s.Countable
f : (i : δ) → X i
hf : f ∈ s.pi t
hst : MeasurableSet (s.pi t)
i : δ
hi : i ∈ s
⊢ MeasurableSet (t i)
Module: Mathlib.Data.Sign.Basic

Goal state before:
pp: case inl.a
z : ℤ
hz : Odd z
⊢ z ≠ 0

Tactic:
rintro rfl

Goal state after:
case inl.a
hz : Odd 0
⊢ False
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: α : Type u_1
ι : Type u_4
S : Set ι
f : α → ℝ≥0∞
t : ι → Set α
h : S.PairwiseDisjoint t
⊢ ∑' (x : ↑(⋃ i ∈ S, t i)), f ↑x = ∑' (i : ↑S) (x : ↑(t ↑i)), f ↑x

Tactic:
by
  simp [← ENNReal.tsum_sigma, ← (Set.biUnionEqSigmaOfDisjoint h).tsum_eq]

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

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

Tactic:
rintro rfl

Goal state after:
case mpr
x : EReal
⊢ x.abs = x.abs ∧ sign x = sign x
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:

Tactic:
#hf.toFinset * ε = ∑ _i ∈ hf.toFinset, ε := by rw [Finset.sum_const, nsmul_eq_mul]
    _ ≤ ∑ i ∈ hf.toFinset, a i := Finset.sum_le_sum fun i => hf.mem_toFinset.1
    _ ≤ ∑' i, a i := ENNReal.sum_le_tsum _
    _ ≤ c := tsum_le_c

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

Goal state before:
pp: β : Type u_2
f : β → ℝ≥0
⊢ ∑' (b : β), f b = (∑' (b : β), ↑(f b)).toNNReal

Tactic:
by_cases h : Summable f
  · rw [← ENNReal.coe_tsum h, ENNReal.toNNReal_coe]
  · have A := tsum_eq_zero_of_not_summable h
    simp only [← ENNReal.tsum_coe_ne_top_iff_summable, Classical.not_not] at h
    simp only [h, ENNReal.toNNReal_top, A]

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

Goal state before:
pp: 𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k ↦ a * (↑k)⁻¹ + c) atTop (𝓝 c)

pp: 𝕜 : Type u_4
inst✝⁵ : Semifield 𝕜
inst✝⁴ : CharZero 𝕜
inst✝³ : TopologicalSpace 𝕜
inst✝² : ContinuousSMul ℚ≥0 𝕜
inst✝¹ : IsTopologicalSemiring 𝕜
inst✝ : ContinuousInv₀ 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k ↦ b * (↑k)⁻¹ + d) atTop (𝓝 d)

Tactic:
all_goals
      apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
      apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
      exact tendsto_inv_atTop_nhds_zero_nat

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

Goal state before:
pp: α : Type u_3
f : Filter α
u v : α → EReal
inst✝ : f.NeBot
hu : 0 ≤ᶠ[f] u
hv : 0 ≤ᶠ[f] v
h₁ : limsup u f ≠ 0 ∨ liminf v f ≠ ⊤
h₂ : limsup u f ≠ ⊤ ∨ liminf v f ≠ 0
⊢ liminf (u * v) f ≤ limsup u f * liminf v f

Tactic:
by
  replace h₁ : 0 < limsup u f ∨ liminf v f ≠ ⊤ := by
    refine h₁.imp_left fun h ↦ lt_of_le_of_ne ?_ h.symm
    exact le_of_eq_of_le (limsup_const 0).symm (limsup_le_limsup hu)
  replace h₂ : limsup u f ≠ ⊤ ∨ 0 < liminf v f := by
    refine h₂.imp_right fun h ↦ lt_of_le_of_ne ?_ h.symm
    exact le_of_eq_of_le (liminf_const 0).symm (liminf_le_liminf hv)
  refine le_mul_of_forall_lt h₁ h₂ fun a a_u b b_v ↦ (liminf_le_iff).2 fun c c_ab ↦ ?_
  refine (((frequently_lt_of_liminf_lt) b_v).and_eventually <| (eventually_lt_of_limsup_lt a_u).and
    <| hu.and hv).mono fun x ⟨x_v, x_u, u_0, v_0⟩ ↦ ?_
  exact (mul_le_mul x_u.le x_v.le v_0 (u_0.trans x_u.le)).trans_lt c_ab

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

Goal state before:
pp: r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a ↦ ↑(r ^ a)) ↑(1 - r)⁻¹

Tactic:
push_cast

Goal state after:
r : ℝ≥0
hr : r < 1
⊢ HasSum (fun a ↦ ↑r ^ a) (↑(1 - r))⁻¹
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
⊢ (map f) (⨅ i, (comap f) (m i)) = ⨅ i, (map f) ((comap f) (m i))

Tactic:
refine (map_iInf_le _ _).antisymm fun s => ?_

Goal state after:
α : Type u_1
ι : Sort u_2
β : Type u_3
inst✝ : Nonempty ι
f : α → β
m : ι → OuterMeasure β
s : Set β
⊢ (⨅ i, (map f) ((comap f) (m i))) s ≤ ((map f) (⨅ i, (comap f) (m i))) s
Module: Mathlib.Topology.Semicontinuity.Basic

Goal state before:
pp: α : Type u_4
inst✝³ : TopologicalSpace α
β : Type u_5
f : α → β
s : Set α
inst✝² : PartialOrder β
inst✝¹ : CommGroup β
inst✝ : IsOrderedMonoid β
⊢ UpperSemicontinuousOn f⁻¹ s ↔ LowerSemicontinuousOn f s

Tactic:
by
  simp [← lowerSemicontinuousOn_inv_iff]

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

Goal state before:
pp: case refine_2
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (↑x + 1 + 1) * (↑k + 1)⁻¹ ≤ 1

Tactic:
refine (div_le_one <| mod_cast hn).mpr ?_
        norm_cast
        lia

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}

Tactic:
simp only [piiUnionInter, exists_prop, mem_union]

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ x ∈ t, f x ∈ π x) ∧ s = ⋂ x ∈ t, f x} ↔ s ∈ π i ∨ s ∈ {univ}
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i

Tactic:
ht1_eq,

Goal state after:
α : Type u_3
ι : Type u_4
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ x ∈ p1, f1 x ∈ π x
ht1_eq : t1 = ⋂ x ∈ p1, f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ x ∈ p2, f2 x ∈ π x
ht2_eq : t2 = ⋂ x ∈ p2, f2 x
h_nonempty : (t1 ∩ t2).Nonempty
g : ι → Set α := fun n ↦ (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ (⋂ x ∈ p1, f1 x) ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i
Module: Mathlib.MeasureTheory.OuterMeasure.AE

Goal state before:
pp: case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
s : Set α
⊢ s = univ → μ sᶜ = 0

Tactic:
rintro rfl

Goal state after:
case refine_2
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
h : ∀ (a : α), ¬μ {a} = 0
⊢ μ univᶜ = 0
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case pos
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

pp: case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms

Tactic:
· simp only [hs]
    simp only [iInf_eq_top, ms] at hs
    exact ⟨univ, subset_univ s, MeasurableSet.univ, hs _ (subset_univ s) MeasurableSet.univ⟩

Goal state after:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs : ¬ms = ∞
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t = ms
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s✝ t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⇑(Equiv.Set.rangeInr α β) ⁻¹' s)

Tactic:
by
    refine ⟨_, hs.inr_image, Set.ext ?_⟩
    simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace γ
π : δ' → Type u_6
π' : δ' → Type u_7
inst✝³ : (x : δ') → MeasurableSpace (π x)
inst✝² : (x : δ') → MeasurableSpace (π' x)
α₁ : Type u_8
β₁ : Type u_9
α₂ : Type u_10
β₂ : Type u_11
inst✝¹ : MeasurableSpace β₁
inst✝ : MeasurableSpace β₂
hα : α₁ ≃ α₂
hβ : β₁ ≃ᵐ β₂
x✝ : Set (α₂ → β₂)
h : MeasurableSet x✝
⊢ MeasurableSet (⇑(hα.arrowCongr' ↑hβ) ⁻¹' x✝)

Tactic:
by
    exact MeasurableSet.preimage h <|
      measurable_pi_iff.mpr fun _ ↦ hβ.measurable.comp (measurable_pi_apply _)

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

Goal state before:
pp: case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet (F^[n + 1] univ)

Tactic:
Function.iterate_succ',

Goal state after:
case refine_1.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n : ℕ
ih : MeasurableSet (F^[n] univ)
⊢ MeasurableSet ((F ∘ F^[n]) univ)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2.a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ F^[n✝ + 1] univ

Tactic:
Function.iterate_succ',

Goal state after:
case refine_2.a.succ
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
n✝ : ℕ
⊢ F (iInter X) ⊆ (F ∘ F^[n✝]) univ
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ F^[n.succ] univ
⊢ y ∈ f '' F^[n] univ

Tactic:
Function.iterate_succ',

Goal state after:
case a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f✝ : α → β
g✝ : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun A ↦ (g '' (f '' A)ᶜ)ᶜ
Fmono : ∀ {A B : Set α}, A ⊆ B → F A ⊆ F B
X : ℕ → Set α := fun n ↦ F^[n] univ
y : β
hy : y ∈ (f '' iInter X)ᶜ
n : ℕ
hx : g y ∈ (F ∘ F^[n]) univ
⊢ y ∈ f '' F^[n] univ
Module: Mathlib.MeasureTheory.Measure.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : α ≃ᵐ β
μ : Measure α
⊢ Filter.map (⇑f) (ae μ) = ae (map (⇑f) μ)

Tactic:
by
  ext s
  simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply]

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t

Tactic:
by
  rw [← restrict_inter_add_sdiff₀ (s ∪ t) ht, union_inter_cancel_right, union_sdiff_right, ←
    restrict_inter_add_sdiff₀ s ht, add_comm, ← add_assoc, add_right_comm]

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

Goal state before:
pp: α : Type u_8
ι : Type u_9
x✝ : MeasurableSpace α
μ : Measure α
inst✝¹ : Countable ι
inst✝ : Preorder ι
f : ι → Set α
hm : ∀ (i : ι), NullMeasurableSet (f i) μ
hf : ∃ i, μ (f i) ≠ ∞
⊢ Tendsto (fun i ↦ μ (⋂ j, ⋂ (_ : j ≤ i), f j)) atTop (𝓝 (μ (⋂ i, f i)))

Tactic:
refine .of_neBot_imp fun hne ↦ ?_
  cases atTop_neBot_iff.mp hne
  rw [measure_iInter_eq_iInf_measure_iInter_le hm hf]
  exact tendsto_atTop_iInf
    fun i j hij ↦ measure_mono <| biInter_subset_biInter_left fun k hki ↦ le_trans hki hij

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

Goal state before:
pp: α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
⊢ μ = 0 → μ.toMeasure h = 0

Tactic:
rintro rfl

Goal state after:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
⊢ OuterMeasure.toMeasure 0 h = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
s : Set α
hs : MeasurableSet s
⊢ s = ∅ → μ₁ s ≤ μ₂ s

Tactic:
rintro rfl

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
hs : MeasurableSet ∅
⊢ μ₁ ∅ ≤ μ₂ ∅
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_1
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
⊢ x ∈ iUnion t'

pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
· by_cases hxt : x ∈ t
      · refine mem_iUnion.2 ⟨0, ?_⟩
        simp [hx, hxt]
      · refine mem_iUnion.2 ⟨1, ?_⟩
        simp [hx, hxt]

Goal state after:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ∑' (n : ℕ), ⨅ μ_1 ∈ toOuterMeasure '' {μ, ν}, μ_1 (t' n) ≤ μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ min (μ (t' 0)) (ν (t' 0)) +
      ((if 1 = 0 then 0 else min (μ (t' 1)) (ν (t' 1))) +
        ∑' (x : ℕ), if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) ≤
    μ (t ∩ s) + ν (tᶜ ∩ s)

Tactic:
if_neg zero_ne_one.symm,

Goal state after:
case refine_1.refine_2
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
x✝ : μ (t ∩ s) + ν (tᶜ ∩ s) ∈ {m | ∃ t, m = μ (t ∩ s) + ν (tᶜ ∩ s)}
t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ min (μ (t' 0)) (ν (t' 0)) +
      (min (μ (t' 1)) (ν (t' 1)) + ∑' (x : ℕ), if x = 1 then 0 else if x = 0 then 0 else min (μ (t' x)) (ν (t' x))) ≤
    μ (t ∩ s) + ν (tᶜ ∩ s)
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ ν : Measure α
s✝ t : Set α
a : α
μ : Measure α
inst✝ : SigmaFinite μ
s : Set α
i : ℕ
⊢ μ (spanningSets μ i ∩ s) < ∞

Tactic:
exact (measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ i)

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
⊢ AEMeasurable f (sum μ)

Tactic:
set g : α → β := (⋂ i, s i).piecewise (const α default) f

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
a✝ : Nontrivial β
inhabited_h : Inhabited β
s : ι → Set α := fun i ↦ toMeasurable (μ i) {x | f x ≠ mk f ⋯ x}
hsμ : ∀ (i : ι), (μ i) (s i) = 0
hsm : MeasurableSet (⋂ i, s i)
hs : ∀ (i : ι), ∀ x ∉ s i, f x = mk f ⋯ x
g : α → β := (⋂ i, s i).piecewise (const α default) f
⊢ AEMeasurable f (sum μ)
Module: Mathlib.MeasureTheory.Measure.AEMeasurable

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
inst✝ : Countable ι
μ : ι → Measure α
h : ∀ (i : ι), AEMeasurable f (μ i)
⊢ AEMeasurable f (sum μ)

Tactic:
by
  classical
  nontriviality β
  inhabit β
  set s : ι → Set α := fun i => toMeasurable (μ i) { x | f x ≠ (h i).mk f x }
  have hsμ : ∀ i, μ i (s i) = 0 := by
    intro i
    rw [measure_toMeasurable]
    exact (h i).ae_eq_mk
  have hsm : MeasurableSet (⋂ i, s i) :=
    MeasurableSet.iInter fun i => measurableSet_toMeasurable _ _
  have hs : ∀ i x, x ∉ s i → f x = (h i).mk f x := by
    intro i x hx
    contrapose! hx
    exact subset_toMeasurable _ _ hx
  set g : α → β := (⋂ i, s i).piecewise (const α default) f
  refine ⟨g, measurable_of_restrict_of_restrict_compl hsm ?_ ?_, ae_sum_iff.mpr fun i => ?_⟩
  · rw [domRestrict_piecewise]
    simp only [s]
    exact measurable_const
  · rw [domRestrict_piecewise_compl, compl_iInter]
    intro t ht
    refine ⟨⋃ i, (h i).mk f ⁻¹' t ∩ (s i)ᶜ, MeasurableSet.iUnion fun i ↦
      (measurable_mk _ ht).inter (measurableSet_toMeasurable _ _).compl, ?_⟩
    ext ⟨x, hx⟩
    simp only [mem_preimage, mem_iUnion, Set.domRestrict, mem_inter_iff,
      mem_compl_iff] at hx ⊢
    constructor
    · rintro ⟨i, hxt, hxs⟩
      rwa [hs _ _ hxs]
    · rcases hx with ⟨i, hi⟩
      rw [hs _ _ hi]
      exact fun h => ⟨i, h, hi⟩
  · refine measure_mono_null (fun x (hx : f x ≠ g x) => ?_) (hsμ i)
    contrapose hx
    refine (piecewise_eq_of_notMem _ _ _ ?_).symm
    exact fun h => hx (mem_iInter.1 h i)

Goal state after: