mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.SeparationQuotient.Basic

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝³ : SMul M X
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] fun p ↦ p.1 • p.2

Tactic:
(IsOpenQuotientMap.id.prodMap isOpenQuotientMap_mk).isQuotientMap.continuous_iff

Goal state after:
M : Type u_1
X : Type u_2
inst✝³ : SMul M X
inst✝² : TopologicalSpace M
inst✝¹ : TopologicalSpace X
inst✝ : ContinuousSMul M X
⊢ Continuous[instTopologicalSpaceProd, _] ((fun p ↦ p.1 • p.2) ∘ Prod.map id mk)
Module: Mathlib.Topology.Algebra.UniformMulAction

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

Tactic:
have : _ = (_ : Completion X → Completion X) :=
      map_comp (uniformContinuous_const_smul m) (uniformContinuous_const_smul n)

Goal state after:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁷ : UniformSpace X
inst✝⁶ : UniformSpace Y
inst✝⁵ : SMul M X
inst✝⁴ : SMul N X
inst✝³ : SMul M N
inst✝² : UniformContinuousConstSMul M X
inst✝¹ : UniformContinuousConstSMul N X
inst✝ : IsScalarTower M N X
m : M
n : N
x : Completion X
this :
  ((Completion.map fun x ↦ m • x) ∘ Completion.map fun x ↦ n • x) = Completion.map ((fun x ↦ m • x) ∘ fun x ↦ n • x)
⊢ (m • n) • x = m • n • x
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
⊢ ∀ᶠ (a_1 : ι) in u, a ≤ f a_1

Tactic:
filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| lt_min (tsub_pos_of_lt hab) one_pos]
    with i hfg hg

Goal state after:
ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg✝ : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
b : ℝ≥0∞
hb : ∀ᶠ (n : ι) in u, b ≤ (f + g) n
a : ℝ≥0∞
hab : a < b
i : ι
hfg : b ≤ (f + g) i
hg : g i ≤ min (b - a) 1
⊢ a ≤ f i
Module: Mathlib.Topology.Instances.ENNReal.Lemmas

Goal state before:
pp: ι : Type u_4
u : Filter ι
g : ι → ℝ≥0∞
hg : Tendsto g u (𝓝 0)
f : ι → ℝ≥0∞
⊢ limsup (f + g) u = limsup f u

Tactic:
refine le_antisymm ?_ <| limsup_le_limsup <| .of_forall <| by simp
  refine le_limsup_of_le (by isBoundedDefault) fun b hb ↦ ?_
  rw [Filter.limsup_le_iff']
  rintro a hba
  filter_upwards [hb, ENNReal.tendsto_nhds_zero.1 hg _ <| tsub_pos_of_lt hba] with i hf hg
  calc f i + g i
    _ ≤ b + g i := by gcongr
    _ ≤ a := add_le_of_le_tsub_left_of_le hba.le hg

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

Goal state before:
pp: case refine_2
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
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ n ≤ d x.1 x.2 / 2 * 2

Tactic:
div_mul_cancel₀ _ two_ne_zero,

Goal state after:
case refine_2
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
hr : ↑0 < ↑(1 / 2) ∧ ↑(1 / 2) < ↑1
I : PseudoMetricSpace X := PseudoMetricSpace.ofPreNNDist d ⋯ hd_symm
hdist_le : ∀ (x y : X), dist x y ≤ ↑(d x y)
hle_d : ∀ {x y : X} {n : ℕ}, (1 / 2) ^ n ≤ d x y ↔ (x, y) ∉ U n
hd_le : ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
n : ℕ
x✝ : True
x : X × X
hx : x ∉ U n
⊢ (1 / 2) ^ n ≤ d x.1 x.2
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊓ c - c ⊓ d| ≤ |b - d|

Tactic:
inf_comm c

Goal state after:
case h₂
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |b ⊓ c - d ⊓ c| ≤ |b - d|
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ |a ⊓ b - c ⊓ d| ≤ |a - c| + |b - d|

Tactic:
calc
    |a ⊓ b - c ⊓ d| = |a ⊓ b - c ⊓ b + (c ⊓ b - c ⊓ d)| := by rw [sub_add_sub_cancel]
    _ ≤ |a ⊓ b - c ⊓ b| + |c ⊓ b - c ⊓ d| := abs_add_le _ _
    _ ≤ |a - c| + |b - d| := by
      gcongr ?_ + ?_
      · exact abs_inf_sub_inf_le_abs _ _ _
      · rw [inf_comm c, inf_comm c]
        exact abs_inf_sub_inf_le_abs _ _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Order.Lattice

Goal state before:
pp: α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
q : α × α
this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
⊢ Filter.Tendsto (fun e ↦ ‖e.1 ⊓ e.2 - (fun p ↦ p.1 ⊓ p.2) q‖) (nhds q) (nhds 0)

Tactic:
refine squeeze_zero (fun e => norm_nonneg _) this ?_

Goal state after:
α : Type u_1
inst✝³ : NormedAddCommGroup α
inst✝² : Lattice α
inst✝¹ : HasSolidNorm α
inst✝ : IsOrderedAddMonoid α
q : α × α
this : ∀ (p : α × α), ‖p.1 ⊓ p.2 - q.1 ⊓ q.2‖ ≤ ‖p.1 - q.1‖ + ‖p.2 - q.2‖
⊢ Filter.Tendsto (fun t ↦ ‖t.1 - q.1‖ + ‖t.2 - q.2‖) (nhds q) (nhds 0)
Module: Mathlib.Topology.MetricSpace.IsometricSMul

Goal state before:
pp: G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist b⁻¹ c⁻¹ = edist b c

Tactic:
edist_inv_inv

Goal state after:
G : Type v
inst✝³ : Group G
inst✝² : PseudoEMetricSpace G
inst✝¹ : IsIsometricSMul G G
inst✝ : IsIsometricSMul Gᵐᵒᵖ G
a b c : G
⊢ edist b c = edist b c
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ BddAbove (Set.range fun n ↦ ‖u n‖)

Tactic:
rw [bddAbove_def]

Goal state after:
G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∃ x, ∀ y ∈ Set.range fun n ↦ ‖u n‖, y ≤ x
Module: Mathlib.Analysis.Normed.Group.Uniform

Goal state before:
pp: G : Type u_4
inst✝ : SeminormedGroup G
u : ℕ → G
hu : CauchySeq u
C : ℝ
hC : ∀ (m n : ℕ), ‖(u m)⁻¹ * u n‖ < C
this : ∀ (n : ℕ), ‖u n‖ ≤ C + ‖u 0‖
⊢ ∀ y ∈ Set.range fun n ↦ ‖u n‖, y ≤ C + ‖u 0‖

Tactic:
by simpa using this

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

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
f : E → F
C : ℝ≥0
⊢ LipschitzWith C f ↔ ∀ (x y : E), ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Tactic:
by
  simp only [lipschitzWith_iff_dist_le_mul, dist_eq_norm_div]

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

Goal state before:
pp: 𝕜 : Type u_5
inst✝¹ : NormedDivisionRing 𝕜
inst✝ : DiscreteTopology 𝕜
x : 𝕜
⊢ ‖x‖ = 1 ↔ x ≠ 0

Tactic:
by
  constructor <;> intro hx
  · contrapose! hx
    simp [hx]
  · have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}
    simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this
    obtain ⟨ε, εpos, h'⟩ := this
    wlog! h : ‖x‖ < 1 generalizing 𝕜 with H
    · rcases h.eq_or_lt with h | h
      · rw [h]
      replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
      rw [← inv_inj, inv_one, ← norm_inv]
      exact H (by simpa) h' h
    obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h
    rw [← norm_pow] at hk
    specialize h' _ hk
    simp [hx] at h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (fun e ↦ ‖e.1 * e.2 - (fun p ↦ p.1 * p.2) x‖) (𝓝 x) (𝓝 0)

Tactic:
refine squeeze_zero (fun e => norm_nonneg _) this ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖
⊢ Tendsto (fun t ↦ ‖t.1‖ * ‖t.2 - x.2‖ + ‖t.1 - x.1‖ * ‖x.2‖) (𝓝 x) (𝓝 0)
Module: Mathlib.Analysis.Normed.Ring.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖↑↑z.natAbs‖ = ‖↑z‖

Tactic:
← norm_neg,

Goal state after:
case inr
α : Type u_2
inst✝ : SeminormedRing α
z : ℤ
hz : z = -↑z.natAbs
⊢ ‖-↑↑z.natAbs‖ = ‖↑z‖
Module: Mathlib.MeasureTheory.OuterMeasure.Basic

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

Tactic:
refine rel_iSup_tsum μ measure_empty (· ≤ ·) (fun t ↦ ?_) _
  calc
    μ (⋃ i, t i) = μ (⋃ i, disjointed t i) := by rw [iUnion_disjointed]
    _ ≤ ∑' i, μ (disjointed t i) :=
      OuterMeasureClass.measure_iUnion_nat_le _ _ (disjoint_disjointed _)
    _ ≤ ∑' i, μ (t i) := by gcongr; exact disjointed_subset ..

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

Goal state before:
pp: δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x ↦ (Equiv.piCongrLeft X f) x i

Tactic:
simp_rw [Equiv.piCongrLeft_apply_eq_cast]

Goal state after:
δ : Type u_4
δ' : Type u_5
X : δ → Type u_6
inst✝ : (a : δ) → MeasurableSpace (X a)
f : δ' ≃ δ
i : δ
⊢ Measurable fun x ↦ cast ⋯ (x (f.symm i))
Module: Mathlib.Topology.Algebra.InfiniteSum.Real

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

Tactic:
by
  rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]

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

Goal state before:
pp: n : ℤ
⊢ n.sign = ↑(SignType.sign n)

Tactic:
obtain (n | _) | _ := n

Goal state after:
case ofNat.zero
⊢ (ofNat 0).sign = ↑(SignType.sign (ofNat 0))

case ofNat.succ
n✝ : ℕ
⊢ (ofNat (n✝ + 1)).sign = ↑(SignType.sign (ofNat (n✝ + 1)))

case negSucc
a✝ : ℕ
⊢ -[a✝+1].sign = ↑(SignType.sign -[a✝+1])
Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal

Goal state before:
pp: f g : ℕ → ℝ≥0∞
h₁ : ∑' (i : ℕ), g i ≠ ∞
h₂ : g ≤ f
this : ∀ (i : ℕ), f i - g i + g i = f i
⊢ ∑' (i : ℕ), (f i - g i) + ∑' (i : ℕ), g i = ∑' (i : ℕ), f i

Tactic:
simp only [← ENNReal.tsum_add, this]

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

Goal state before:
pp: α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
⊢ HasSum (fun x ↦ ((fun i ↦ ↑(f i)) x).toReal) (∑' (x : α), ((fun i ↦ ↑(f i)) x).toReal)

Tactic:
simp only [coe_toReal, ← NNReal.coe_tsum, NNReal.hasSum_coe]

Goal state after:
α : Type u_1
f : α → ℝ≥0
hsum : ∑' (x : α), (fun i ↦ ↑(f i)) x ≠ ∞
⊢ HasSum f (∑' (a : α), f a)
Module: Mathlib.Data.EReal.Inv

Goal state before:
pp: a b c : EReal
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ b' ∈ Ioo 0 b, c < a * b'

Tactic:
by
  have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha
  simp_rw [mul_comm a] at h ⊢
  exact exists_lt_mul_left_of_nonneg hb.le hc h

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

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0∞
hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.edist ha) (mem_atTop_sets.2 ⟨n, fun m hnm => ?_⟩)
  change edist _ _ ≤ _
  refine le_trans (edist_le_Ico_sum_of_edist_le hnm fun _ _ => hf _) ?_
  rw [Finset.sum_Ico_eq_sum_range]
  exact ENNReal.summable.sum_le_tsum _ (fun _ _ => zero_le)

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

Goal state before:
pp: ⊢ (Ici 0).OrdConnected

Tactic:
exact ordConnected_Ici

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

Goal state before:
pp: case refine_1
α : Type u_1
m : Set α → ℝ≥0∞
β : Type u_2
f : β → α
h : (Monotone fun s ↦ m ↑s) ∨ Surjective f
⊢ (Monotone fun s ↦ ⨆ (_ : s.Nonempty), m s) ∨ Surjective f

Tactic:
refine h.imp (fun H s t hst => iSup_le fun hs => ?_) id
    have ht : t.Nonempty := hs.mono hst
    exact (@H ⟨s, hs⟩ ⟨t, ht⟩ hst).trans (le_iSup (fun _ : t.Nonempty => m t) ht)

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

Goal state before:
pp: a : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

Tactic:
rcases lt_or_gt_of_ne h with a_neg | a_pos

Goal state after:
case inl
a : ℝ
h : a ≠ 0
a_neg : a < 0
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)

case inr
a : ℝ
h : a ≠ 0
a_pos : 0 < a
⊢ ContinuousAt (fun p ↦ p.1 * p.2) (⊤, ↑a)
Module: Mathlib.MeasureTheory.OuterMeasure.Caratheodory

Goal state before:
pp: α : Type u
m : OuterMeasure α
s s₁ s₂ : Set α
f✝ : ℕ → Set α
x✝ : Pairwise (Disjoint on f✝)
hf : ∀ (i : ℕ), m.IsCaratheodory (f✝ i)
hn : Set α
⊢ m hn = m (hn ∩ ⋃ i, f✝ i) + m (hn \ ⋃ i, f✝ i)

Tactic:
apply isCaratheodory_iUnion m hf

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t

Tactic:
by
  rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure]

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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), m t

Tactic:
by
  simp +singlePass only [iInf_comm]
  exact
    inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => measure_iUnion_le f)
      (fun _ _ _ _ h => measure_mono h) s

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

Goal state before:
pp: case refine_2
α✝ : 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.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a

Tactic:
refine (Set.prod (range Sum.inr) univ).symm.measurable_comp_iff.1 ?_

Goal state after:
case refine_2
α✝ : 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.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inr) univ).symm)
Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding

Goal state before:
pp: case refine_2
α✝ : 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.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable ((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inr) univ).symm)

Tactic:
refine (prodCongr Set.rangeInr (Set.univ _)).symm.measurable_comp_iff.1 ?_

Goal state after:
case refine_2
α✝ : 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.23
β : Type ?u.25
γ : Type ?u.102
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
⊢ Measurable
    (((fun a ↦ (Equiv.sumProdDistrib α β γ) ↑a) ∘ ⇑(Set.prod (range Sum.inr) univ).symm) ∘
      ⇑(Set.rangeInr.prodCongr (Set.univ γ)).symm)
Module: Mathlib.MeasureTheory.OuterMeasure.Induced

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
i : ι
⊢ (μ i) (⋂ i, t i) ≤ (μ i).trim s

pp: case refine_2
α : Type u_1
inst✝¹ : MeasurableSpace α
ι : Sort u_2
inst✝ : Countable ι
μ : ι → OuterMeasure α
s : Set α
t : ι → Set α
hμt : ∀ (i : ι), (μ i) (t i) = (μ i).trim s
hst : s ⊆ ⋂ i, t i
ht : MeasurableSet (⋂ b, t b)
i : ι
⊢ (μ i).trim s ≤ (μ i) (⋂ i, t i)

Tactic:
exacts [hμt i ▸ (μ i).mono (iInter_subset _ _), (measure_mono hst).trans_eq ((μ i).trim_eq ht)]

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:
| succ n ih =>

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
R : Type u_4
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
μ : Measure α
f : α → β
c : ℝ≥0∞
hc : c ≠ 0
hf : ¬AEMeasurable f μ
⊢ map f (c • μ) = c • map f μ

Tactic:
· have hfc : ¬AEMeasurable f (c • μ) := by
      intro hfc
      exact hf ⟨hfc.mk f, hfc.measurable_mk, (ae_ennreal_smul_measure_iff hc).1 hfc.ae_eq_mk⟩
    simp [map_of_not_aemeasurable hf, map_of_not_aemeasurable hfc]

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 β
hs : NullMeasurableSet s (if hf : AEMeasurable f μ then (mapₗ (AEMeasurable.mk f hf)) μ else 0)
⊢ (if hf : AEMeasurable f μ then (mapₗ (AEMeasurable.mk f hf)) μ else 0) s = μ (f ⁻¹' s)

Tactic:
dif_pos hf,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((mapₗ (AEMeasurable.mk f hf)) μ)
⊢ ((mapₗ (AEMeasurable.mk f hf)) μ) s = μ (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Map

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

Tactic:
by
  simp [map_map e.symm.measurable e.measurable]

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

Goal state before:
pp: case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[k + 1] ⁻¹' s =ᵐ[μ] s

Tactic:
rw [iterate_succ, preimage_comp]

Goal state after:
case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' f^[k] ⁻¹' s =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Measure.Comap

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
⊢ (comap f μ) s ≤ μ (f '' s)

Tactic:
comap_apply₀ _ _ hf.1 hf.2 hs

Goal state after:
case pos
α : Type u_1
β : Type u_2
s : Set α
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hs : NullMeasurableSet s (comap f μ)
hf : Injective f ∧ ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
⊢ μ (f '' s) ≤ μ (f '' s)
Module: Mathlib.MeasureTheory.Measure.Restrict

Goal state before:
pp: α : Type u_2
_m0 : MeasurableSpace α
R : Type u_7
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
c : R
μ : Measure α
s : Set α
⊢ (c • μ).restrict s = c • μ.restrict s

Tactic:
simpa only [smul_one_smul] using! (restrictₗ s).map_smul (c • 1) μ

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

Goal state before:
pp: α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ μ.restrict (s ∩ t) = (μ.restrict s).restrict t

Tactic:
restrict_restrict' hs,

Goal state after:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ μ.restrict (s ∩ t) = μ.restrict (t ∩ s)
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: case pos.hf
α : Type u_1
m : MeasurableSpace α
μ : Measure α
ι : Type u_8
inst✝³ : LinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
s : ι → Set α
a : ι
hs : ∀ r > a, NullMeasurableSet (s r) μ
hm : ∀ (i j : ι), a < i → i ≤ j → s i ⊆ s j
hf : ∃ r > a, μ (s r) ≠ ∞
ha : Order.IsPredPrelimit a
this : atBot.IsCountablyGenerated
⊢ ∃ i, μ (s ↑i) ≠ ∞

Tactic:
simpa only [Subtype.exists, exists_prop]

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

Goal state before:
pp: case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (t ∩ u) = ν (t ∩ u)
this : μ (t ∩ u) + μ (t \ u) = μ (t ∩ u) + ν (t \ u)
⊢ μ (t ∩ uᶜ) = ν (t ∩ uᶜ)

Tactic:
ENNReal.add_right_inj

Goal state after:
case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (t ∩ u) = ν (t ∩ u)
this : μ (t \ u) = ν (t \ u)
⊢ μ (t ∩ uᶜ) = ν (t ∩ uᶜ)

case compl
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
S T : Set (Set α)
h_gen : m0 = generateFrom S
hc : T.Countable
h_inter : IsPiSystem S
hU : ⋃₀ T = univ
htop : ∀ t ∈ T, μ t ≠ ∞
ST_eq : ∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
T_eq : ∀ t ∈ T, μ t = ν t
t : Set α
ht : t ∈ T
u✝ u : Set α
hu : MeasurableSet u
ihu : μ (t ∩ u) = ν (t ∩ u)
this : μ (t ∩ u) + μ (t \ u) = μ (t ∩ u) + ν (t \ u)
⊢ μ (t ∩ u) ≠ ∞
Module: Mathlib.MeasureTheory.Measure.MeasureSpace

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
⊢ (measurableAtom '' s).Pairwise Disjoint

Tactic:
intro t ht t' ht' h_eq

Goal state after:
α : Type u_1
m : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (x : α), μ (measurableAtom x) = ν (measurableAtom x)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
t : Set α
ht : t ∈ measurableAtom '' s
t' : Set α
ht' : t' ∈ measurableAtom '' s
h_eq : t ≠ t'
⊢ Disjoint t t'
Module: Mathlib.Data.Set.MemPartition

Goal state before:
pp: case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
⊢ u ∈ memPartition f 0 → v ∈ memPartition f 0 → u ≠ v → Disjoint u v

Tactic:
hu

Goal state after:
case zero
α : Type u_1
f : ℕ → Set α
u v : Set α
hu : u ∈ memPartition f 0
⊢ v ∈ memPartition f 0 → u ≠ v → Disjoint u v