mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
this : μ (s i) < μ (s i) + ↑(ε' i)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) < μ (s i) + ↑(ε' i)
⊢ ∃ f, s i ⊆ ⋃ i, f i ∧ ∑' (i : ℕ), m (f i) < μ (s i) + ↑(ε' i)

Tactic:
exists t

Goal state after:
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
μ : Set α → ℝ≥0∞ := fun s ↦ ⨅ f, ⨅ (_ : s ⊆ ⋃ i, f i), ∑' (i : ℕ), m (f i)
s : ℕ → Set α
x✝ : Pairwise (Disjoint on s)
ε : ℝ≥0
hε : 0 < ε
hb : ∑' (i : ℕ), μ (s i) < ∞
ε' : ℕ → ℝ≥0
hε' : ∀ (i : ℕ), 0 < ε' i
hl : ∑' (i : ℕ), ↑(ε' i) < ↑ε
i : ℕ
this : μ (s i) < μ (s i) + ↑(ε' i)
t : ℕ → Set α
ht : ⨅ (_ : s i ⊆ ⋃ i, t i), ∑' (i : ℕ), m (t i) < μ (s i) + ↑(ε' i)
⊢ s i ⊆ ⋃ i, t i ∧ ∑' (i : ℕ), m (t i) < μ (s i) + ↑(ε' i)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case inl
α : Type u_3
f : Filter α
u v : α → EReal
a : EReal
ha : limsup u f < a
hb : limsup v f ≤ ⊤
⊢ limsup (u + v) f ≤ ⊤

Tactic:
exact le_top

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

Goal state before:
pp: r : ℝ≥0
hr' hr : ↑r < 1
⊢ Tendsto (fun n ↦ ↑r ^ n) atTop (𝓝 0)

Tactic:
rw [← ENNReal.coe_zero]

Goal state after:
r : ℝ≥0
hr' hr : ↑r < 1
⊢ Tendsto (fun n ↦ ↑r ^ n) atTop (𝓝 ↑0)
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case top.bot
h : (⊤, ⊥).1 ≠ ⊤ ∨ (⊤, ⊥).2 ≠ ⊥
h' : (⊤, ⊥).1 ≠ ⊥ ∨ (⊤, ⊥).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊥)

pp: case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

pp: case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)

Tactic:
· simp at h

Goal state after:
case top.coe
a✝ : ℝ
h : (⊤, ↑a✝).1 ≠ ⊤ ∨ (⊤, ↑a✝).2 ≠ ⊥
h' : (⊤, ↑a✝).1 ≠ ⊥ ∨ (⊤, ↑a✝).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ↑a✝)

case top.top
h : (⊤, ⊤).1 ≠ ⊤ ∨ (⊤, ⊤).2 ≠ ⊥
h' : (⊤, ⊤).1 ≠ ⊥ ∨ (⊤, ⊤).2 ≠ ⊤
⊢ ContinuousAt (fun p ↦ p.1 + p.2) (⊤, ⊤)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = (1 - r)⁻¹

Tactic:
tsub_eq_zero_iff_le.mpr hr,

Goal state after:
case inr
r : ℝ≥0∞
hr : 1 ≤ r
⊢ ∑' (n : ℕ), r ^ n = 0⁻¹
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
⊢ ∑ i ∈ Finset.range n, 1 ≤ ∑ i ∈ Finset.range n, r ^ i

Tactic:
gcongr

Goal state after:
case h
r : ℝ≥0∞
hr : 1 ≤ r
a : ℝ≥0∞
ha : a < ∞
n : ℕ
hn : a < ↑n
i : ℕ
a✝ : i ∈ Finset.range n
⊢ 1 ≤ r ^ i
Module: Mathlib.Topology.Instances.EReal.Lemmas

Goal state before:
pp: case h
x : ℝ
⊢ (∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2) ∧
    IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1) ∧ (⊤, ⊤) ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1

Tactic:
split_ands

Goal state after:
case h.refine_1
x : ℝ
⊢ ∀ y ∈ Ioi (max (↑x) 0) ×ˢ Ioi 1, ↑x < y.1 * y.2

case h.refine_2.refine_1
x : ℝ
⊢ IsOpen (Ioi (max (↑x) 0) ×ˢ Ioi 1)

case h.refine_2.refine_2.refine_1
x : ℝ
⊢ (⊤, ⊤).1 ∈ Ioi (max (↑x) 0)

case h.refine_2.refine_2.refine_2
x : ℝ
⊢ (⊤, ⊤).2 ∈ Ioi 1
Module: Mathlib.MeasureTheory.OuterMeasure.OfFunction

Goal state before:
pp: α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
hm : Monotone m
⊢ (map Subtype.val) (OuterMeasure.ofFunction (fun s_1 ↦ m (Subtype.val '' s_1)) ⋯) =
    OuterMeasure.ofFunction (fun t ↦ m (s ∩ t)) ⋯

Tactic:
simp only [map_ofFunction Subtype.coe_injective, Subtype.image_preimage_coe]

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

Goal state before:
pp: case h
a : ℝ
h : 0 < a
x : ℝ
⊢ (∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2) ∧
    IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)) ∧ (⊤, ↑a) ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2)

Tactic:
split_ands

Goal state after:
case h.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ ∀ y ∈ Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2), ↑x < y.1 * y.2

case h.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ IsOpen (Ioi ↑(2 * max (x + 1) 0 / a) ×ˢ Ioi ↑(a / 2))

case h.refine_2.refine_2.refine_1
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).1 ∈ Ioi ↑(2 * max (x + 1) 0 / a)

case h.refine_2.refine_2.refine_2
a : ℝ
h : 0 < a
x : ℝ
⊢ (⊤, ↑a).2 ∈ Ioi ↑(a / 2)
Module: Mathlib.Analysis.SpecificLimits.Basic

Goal state before:
pp: m : ℝ
f : ℕ → ℕ
hm : 1 < m
fi : ∀ (i : ℕ), i ≤ f i
⊢ Summable fun i ↦ 1 / m ^ f i

Tactic:
refine .of_nonneg_of_le (fun a ↦ by positivity) (fun a ↦ ?_)
      (summable_geometric_of_lt_one (one_div_nonneg.mpr (zero_le_one.trans hm.le))
        ((one_div_lt (zero_lt_one.trans hm) zero_lt_one).mpr (one_div_one.le.trans_lt hm)))
  rw [div_pow, one_pow]
  refine (one_div_le_one_div ?_ ?_).mpr (pow_right_mono₀ hm.le (fi a)) <;>
    exact pow_pos (zero_lt_one.trans hm) _

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

Goal state before:
pp: ⊢ ∀ᶠ (b : ℕ) in atTop, ↑b ! / ↑b ^ b ≤ 1 / ↑b

Tactic:
refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_

Goal state after:
n : ℕ
hn : 0 < n
⊢ ↑n ! / ↑n ^ n ≤ 1 / ↑n
Module: Mathlib.Order.SetDissipate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
⊢ ∀ (x : β), (∀ (i : α), x ∈ s i) → ∀ (i i_1 : α), i_1 ≤ i → x ∈ s i_1

Tactic:
· exact fun z h x' y hy ↦ h y

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert ∅ S

Tactic:
rcases hs with hs | hs

Goal state after:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S

case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
⊢ s ∩ t ∈ insert univ S

Tactic:
rcases hs with hs | hs

Goal state after:
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s = univ
⊢ s ∩ t ∈ insert univ S

case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : (s ∩ t).Nonempty
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
D : Set (Set β)
hC : IsPiSystem C
hD : IsPiSystem D
s₁ : Set α
hs₁ : s₁ ∈ C
t₁ : Set β
ht₁ : t₁ ∈ D
s₂ : Set α
hs₂ : s₂ ∈ C
t₂ : Set β
ht₂ : t₂ ∈ D
hst : (s₁ ∩ s₂).Nonempty ∧ (t₁ ∩ t₂).Nonempty
⊢ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) ∈ image2 (fun x1 x2 ↦ x1 ×ˢ x2) C D

Tactic:
exact mem_image2_of_mem (hC _ hs₁ _ hs₂ hst.1) (hD _ ht₁ _ ht₂ hst.2)

Goal state after:
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iic '' s)

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
  exact ⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩

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

Goal state before:
pp: case e'_3
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) = m (⋃ i, t ∩ s i)

Tactic:
simp [inter_iUnion]

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

Goal state before:
pp: α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
⊢ m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t

Tactic:
have hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i < n, s i) := by
    convert! measure_iUnion_le (μ := m) fun i => t ∩ s i using 1
    · simp [inter_iUnion]
    · simp [ENNReal.tsum_eq_iSup_nat, isCaratheodory_sum m h hd]

Goal state after:
α : Type u
m : OuterMeasure α
s : ℕ → Set α
h : ∀ (i : ℕ), m.IsCaratheodory (s i)
hd : Pairwise (Disjoint on s)
t : Set α
hp : m (t ∩ ⋃ i, s i) ≤ ⨆ n, m (t ∩ ⋃ i, ⋃ (_ : i < n), s i)
⊢ m (t ∩ ⋃ i, s i) + m (t \ ⋃ i, s i) ≤ m t
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ ∀ (i : P s₂), extend m s₁ ≤ m s₂ i

Tactic:
intro h₂

Goal state after:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ extend m s₁ ≤ m s₂ h₂
Module: Mathlib.MeasureTheory.PiSystem

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ d.Has ((⋃ i, f i) ∩ s)

Tactic:
rw [iUnion_inter]

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
d : DynkinSystem α
s : Set α
h : d.Has s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), d.Has (f i ∩ s)
⊢ d.Has (⋃ i, f i ∩ s)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case mpr
α : 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 α
h :
  ∀ (t : Set α),
    P t →
      (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s) ≤ (inducedOuterMeasure m P0 m0) t
u t : Set α
ht : P t
h2t : u ⊆ t
⊢ (inducedOuterMeasure m P0 m0) (u ∩ s) + (inducedOuterMeasure m P0 m0) (u \ s) ≤
    (inducedOuterMeasure m P0 m0) (t ∩ s) + (inducedOuterMeasure m P0 m0) (t \ s)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
⊢ ∀ (i : MeasurableSet s₂), extend m s₁ ≤ m s₂ i

Tactic:
intro h₂

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s₁ s₂ : Set α
h₁ : MeasurableSet s₁
hs : s₁ ⊆ s₂
h₂ : MeasurableSet s₂
⊢ extend m s₁ ≤ m s₂ h₂
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
ms : ℝ≥0∞ := ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t
hs✝ : ¬ms = ∞
r : ℝ≥0∞
hs : r > ms
t : Set α
hmt : MeasurableSet t
hin : s ⊆ t
hlt : m t < r
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ m t < r

Tactic:
exists t

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : μ s' = μ s
hs'm : NullMeasurableSet s' μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ μ (f ⁻¹' s) ≤ μ (f ⁻¹' toMeasurable (map f μ) s)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
⊢ s ⊆ toMeasurable (map f μ) s
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 β
t : Set β := f '' toMeasurable μ (f ⁻¹' s) ∪ (range f)ᶜ
htm : MeasurableSet t
hst : s ⊆ t
hft : f ⁻¹' t = toMeasurable μ (f ⁻¹' s)
⊢ (map f μ) s ≤ (map f μ) t

Tactic:
gcongr

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

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

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
inst✝ : Countable ι
μ : F
s : ι → Set α
hs : ∑' (i : ι), μ (s i) ≠ ∞
t : Finset ι
⊢ limsup s cofinite ⊆ ⋃ i, s ↑i
Module: Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving

Goal state before:
pp: case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
hs : ⇑e '' s =ᵐ[μ] s
k : ℕ
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s

Tactic:
replace hs : e ⁻¹' s =ᵐ[μ] s := by
      convert! he.preimage_ae_eq hs.symm
      rw [Equiv.preimage_image]

Goal state after:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
e : α ≃ α
he : QuasiMeasurePreserving (⇑e) μ μ
he' : QuasiMeasurePreserving (⇑e.symm) μ μ
k : ℕ
hs : ⇑e ⁻¹' s =ᵐ[μ] s
⊢ ⇑(e ^ k)⁻¹.symm ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ μ (⋃ b ∈ s, As b) ≤ μ (⋃ i, As i)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
b : ι
⊢ ⋃ (_ : b ∈ s), As b ⊆ As b
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ (s₁ ∩ s₂) + μ (s₁ \ s₂) ≤ μ s₂ + μ (s₁ \ s₂)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ ⊆ s₂
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (t \ s) = 0
⊢ s ∪ t ≤ᵐ[μ] s

Tactic:
ae_le_set,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (t \ s) = 0
⊢ μ ((s ∪ t) \ s) = 0
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
⊢ μ (⋃ i, s i) ≤ μ (⋃ i, t i)

Tactic:
gcongr

Goal state after:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Sort u_8
inst✝ : Countable ι
s t : ι → Set α
hsub : ∀ (i : ι), s i ⊆ t i
h_le : ∀ (i : ι), μ (t i) ≤ μ (s i)
i : ι
⊢ s i ⊆ t i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.Finite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst✝ : IsFiniteMeasure μ
hs : MeasurableSet s
ht : MeasurableSet t
ε : ℝ≥0∞
h : μ s ≤ μ t + ε
⊢ μ univ - μ s + μ s ≤ μ univ - μ s + (μ t + ε)

Tactic:
gcongr

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

Goal state before:
pp: case h
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 ↦ x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ∞
this : ∀ t ⊆ s k, μ t ≠ ∞
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ μ (s k \ s i) ≤ μ (s k \ s j)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ (μ s).toReal - (μ t).toReal = (μ (s \ t)).toReal - (μ (t \ s)).toReal

Tactic:
measure_sdiff' s ht ht',

Goal state after:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hs' : μ s ≠ ∞
ht' : μ t ≠ ∞
hst : μ (s \ t) ≠ ∞
hts : μ (t \ s) ≠ ∞
⊢ (μ s).toReal - (μ t).toReal = (μ (s ∪ t) - μ t).toReal - (μ (t \ s)).toReal
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Antitone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
refine measure_iInter_of_ae_monotone (ι := ιᵒᵈ) ?_ hsm hfin

Goal state after:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirectedOrder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : ∀ᵐ (ω : α) ∂μ, Antitone fun x ↦ ω ∈ s x
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ∞
⊢ ∀ᵐ (ω : α) ∂μ, Monotone fun x ↦ ω ∈ s x
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_8
ι : Type u_9
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
x✝ : MeasurableSpace α
μ : Measure α
f : ι → Set α
h : atTop.NeBot
this : IsDirectedOrder ι
i j : ι
hij : i ≤ j
⊢ μ (accumulate f i) ≤ μ (accumulate f j)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t

Tactic:
gcongr

Goal state after:
case h₂
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ s ⊆ f ⁻¹' t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
⊢ μ (t ∩ u) ≤ μ ((⋂ n, w n) ∩ u)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := fun n ↦ toMeasurable (m n) t
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ (m i) ((⋂ n, w n) ∩ u) ≤ (m i) (w i ∩ u)

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
w : ℕ → Set α := ⋯
T : t ⊆ ⋂ n, w n
M : MeasurableSet (⋂ n, w n)
u : Set α
hu : MeasurableSet u
i : ℕ
⊢ ⋂ n, w n ⊆ w i
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: case pos
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (ht.choose ∩ s) = μ (t ∩ s)

pp: case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)

Tactic:
· apply measure_congr
    exact ae_eq_set_inter ht.choose_spec.2.2 (ae_eq_refl _)

Goal state after:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
m : ℕ → Measure α
hv : ∀ (n : ℕ), (m n) t ≠ ∞
hμ : μ = sum m
A : ∃ t' ⊇ t, MeasurableSet t' ∧ ∀ (u : Set α), MeasurableSet u → μ (t' ∩ u) = μ (t ∩ u)
ht : ¬∃ t_1 ⊇ t, MeasurableSet t_1 ∧ t_1 =ᵐ[μ] t
⊢ μ (A.choose ∩ s) = μ (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
⊢ μ (t ∩ s) ≤ μ (u ∩ s)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : μ t = μ u
htu : t ⊆ u
ht_ne_top : μ u ≠ ∞
⊢ μ (t ∩ s) + μ (t \ s) ≤ μ (t ∩ s) + μ (u \ s)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
⊢ μ (t ∩ u) ≤ μ (t' ∩ u)

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
⊢ (μ.trim hm).restrict s = (μ.restrict s).trim hm

Tactic:
refine @Measure.ext _ m _ _ (fun t ht => ?_)

Goal state after:
α : Type u_1
m m0 : MeasurableSpace α
s : Set α
hm : m ≤ m0
μ : Measure α
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ((μ.trim hm).restrict s) t = ((μ.restrict s).trim hm) t
Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := fun n ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋃ n, toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ μ (t ∩ disjointed w n) ≤ μ (t ∩ w n)

Tactic:
gcongr

Goal state after:
case h₂
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ n, v n
h'v : ∀ (n : ℕ), μ (t ∩ v n) ≠ ∞
w : ℕ → Set α := ⋯
hw : ∀ (n : ℕ), μ (w n) < ∞
t' : Set α := ⋯
ht' : t' = ⋃ n, toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
u : Set α
hu : MeasurableSet u
n : ℕ
⊢ disjointed w n ⊆ w n
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : (μ + ν) t ≠ ∞
h' : s ⊆ t
h'' : (μ + ν) s = (μ + ν) t
⊢ μ s + ν s ≤ μ s + ν t

Tactic:
gcongr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝² : SMul R ℝ≥0∞
inst✝¹ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝ : CovariantClass R ℝ≥0∞ (fun x1 x2 ↦ x1 • x2) fun x1 x2 ↦ x1 ≤ x2
c : R
μ ν : Measure α
hμν : (fun x1 x2 ↦ x1 ≤ x2) μ ν
s : Set α
⊢ c • μ s ≤ c • ν s

Tactic:
gcongr

Goal state after: