awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
rw :
  #(↑((s ∪ {∅} ∪ compl '' ⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) ∪
            range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
              ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(generateMeasurableRec s i) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
rw [generateMeasurableRec]

Premises used: MeasurableSpace.generateMeasurableRec
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h1 : #(↑s : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h1₁ : #(↑{∅} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h2 :
  #(↑(range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
            ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑((s ∪ {∅} ∪ compl '' ⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) ∪
            range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
              ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
apply_rules [(mk_union_le _ _).trans, add_le_of_le (aleph_one_le_continuum.trans A),
    mk_image_le.trans]

Premises used: Cardinal.add_le_of_le, Cardinal.mk_image_le, LE.le.trans, Cardinal.mk_union_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑s : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
(self_le_power _ one_le_aleph0).trans (power_le_power_right (le_max_left _ _))

Premises used: Cardinal.self_le_power, Cardinal.power_le_power_right, LE.le.trans, le_max_left, Cardinal.one_le_aleph0
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑s : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
exact (self_le_power _ one_le_aleph0).trans (power_le_power_right (le_max_left _ _))

Premises used: Cardinal.self_le_power, Cardinal.power_le_power_right, LE.le.trans, le_max_left, Cardinal.one_le_aleph0
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h1 : 1 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑{∅} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
rw [mk_singleton]

Premises used: Cardinal.mk_singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ 1 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
one_lt_aleph0.le.trans B

Premises used: Cardinal.one_lt_aleph0, LT.lt.le, LE.le.trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ 1 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
exact one_lt_aleph0.le.trans B

Premises used: Cardinal.one_lt_aleph0, LT.lt.le, LE.le.trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h2 : #(ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(range fun (f : ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ↦
            ⋃ (n : ℕ), (↑(f n) : Set α)) :
        Type u) ≤
    max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
apply mk_range_le.trans

Premises used: Cardinal.mk_range_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h2 : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(ℕ → (↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u)) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
simp only [mk_pi, prod_const, Cardinal.lift_uzero, mk_denumerable, lift_aleph0]

Premises used: Cardinal.mk_pi, Cardinal.prod_const, Cardinal.lift_uzero, Cardinal.lift_aleph0, Cardinal.mk_denumerable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ (max (#(↑s : Type u)) 2 ^ ℵ₀) ^ ℵ₀

Tactic:
have := @power_le_power_right _ _ ℵ₀ C
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
i_1 i_2 i : Ordinal.{v}
IH :
  ∀ y < i,
    y ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1 →
      #(↑(generateMeasurableRec s y) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
hi : i ≤ (ω_ : (a : Ordinal.{v}) → Ordinal.{v}) 1
A : 𝔠 ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
B : ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
C : #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
this :
  #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ (max (#(↑s : Type u)) 2 ^ ℵ₀) ^ ℵ₀
h2 :
  ∀
    (this :
      #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤
        max (#(↑s : Type u)) 2 ^ (ℵ₀ * ℵ₀)),
    #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
h2₁ h2₂ h2₃ h2₄ :
  ∀
    (this :
      #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀),
    #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑(⋃ (j : Ordinal.{v}), ⋃ (_ : j < i), generateMeasurableRec s j) : Type u) ^ ℵ₀ ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
rwa [← power_mul, aleph0_mul_aleph0] at this

Premises used: Cardinal.power_mul, Cardinal.aleph0_mul_aleph0
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
rw : #(↑(generateMeasurableRec s ((ω_ : (a : Ordinal.{0}) → Ordinal.{0}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀
⊢ #(↑{t : Set α | GenerateMeasurable s t} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
rw [generateMeasurable_eq_rec.{u, 0}]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
⊢ #(↑(generateMeasurableRec s ((ω_ : (a : Ordinal.{0}) → Ordinal.{0}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
cardinal_generateMeasurableRec_le s _

Premises used: MeasurableSpace.cardinal_generateMeasurableRec_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
⊢ #(↑(generateMeasurableRec s ((ω_ : (a : Ordinal.{0}) → Ordinal.{0}) 1)) : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
exact cardinal_generateMeasurableRec_le s _

Premises used: MeasurableSpace.cardinal_generateMeasurableRec_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
⊢ #(↑{t : Set α | MeasurableSet t} : Type u) ≤ max (#(↑s : Type u)) 2 ^ ℵ₀

Tactic:
cardinal_generateMeasurable_le s

Premises used: MeasurableSet, setOf, MeasurableSpace.cardinal_generateMeasurable_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
hs : #(↑s : Type u) ≤ 𝔠
apply : max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠
⊢ #(↑{t : Set α | GenerateMeasurable s t} : Type u) ≤ 𝔠

Tactic:
apply (cardinal_generateMeasurable_le s).trans

Premises used: MeasurableSpace.cardinal_generateMeasurable_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
hs : #(↑s : Type u) ≤ 𝔠
rw : max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
⊢ max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠

Tactic:
rw [← continuum_power_aleph0]

Premises used: Cardinal.continuum_power_aleph0
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
hs : #(↑s : Type u) ≤ 𝔠
⊢ max (#(↑s : Type u)) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀

Tactic:
exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)

Premises used: Cardinal.power_le_power_right, Cardinal.nat_lt_continuum, LT.lt.le, max_le, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Card
Goal:
α : Type u
s : Set (Set α)
⊢ #(↑s : Type u) ≤ 𝔠 → #(↑{t : Set α | MeasurableSet t} : Type u) ≤ 𝔠

Tactic:
cardinal_generateMeasurable_le_continuum

Premises used: MeasurableSet, setOf, MeasurableSpace.cardinal_generateMeasurable_le_continuum
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
rw : MeasurableSet.{u_2} (α := β) (⋃ y ∈ s, f ⁻¹' {y})
⊢ MeasurableSet (f ⁻¹' s)

Tactic:
rw [← biUnion_preimage_singleton]

Premises used: Set.biUnion_preimage_singleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
⊢ MeasurableSet.{u_2} (α := β) (⋃ y ∈ s, f ⁻¹' {y})

Tactic:
MeasurableSet.iUnion fun y => MeasurableSet.iUnion fun hy => ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
refine : ∀ (y : α) (hy : y ∈ s), MeasurableSet (f ⁻¹' {y})
⊢ MeasurableSet.{u_2} (α := β) (⋃ y ∈ s, f ⁻¹' {y})

Tactic:
refine MeasurableSet.iUnion fun y => MeasurableSet.iUnion fun hy => ?_

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : α
hy : y ∈ s
pos : ∀ (hyf : y ∈ range f), MeasurableSet (f ⁻¹' {y})
neg : ∀ (hyf : y ∉ range f), MeasurableSet (f ⁻¹' {y})
⊢ MeasurableSet (f ⁻¹' {y})

Tactic:
by_cases hyf : y ∈ range f

Premises used: Set.range
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∈ range f
pos : ∀ (y : β) (hy : f y ∈ s), MeasurableSet (f ⁻¹' {f y})
⊢ MeasurableSet (f ⁻¹' {y})

Tactic:
rcases hyf with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : β
hy : f y ∈ s
⊢ MeasurableSet (f ⁻¹' {f y})

Tactic:
apply h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (y : β), MeasurableSet (f ⁻¹' {f y})
s : Set α
h_1 : MeasurableSet s
y : α
hy : y ∈ s
hyf : y ∉ range f
⊢ MeasurableSet (f ⁻¹' {y})

Tactic:
simp only [preimage_singleton_eq_empty.2 hyf, MeasurableSet.empty]

Premises used: Iff.mpr, MeasurableSet.empty, Set.preimage_singleton_eq_empty
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : Countable α
inst_2 : MeasurableSpace β
f : β → α
h : ∀ (x : α), MeasurableSet (f ⁻¹' {x})
⊢ Measurable f

Tactic:
measurable_to_countable fun y => h (f y)

Premises used: measurable_to_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
⊢ Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})

Tactic:
⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩

Premises used: MeasurableSingletonClass.measurableSet_singleton, Nat.cast, Iff.intro, measurable_to_countable'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
refine : ∀ (h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})) (n : ℕ∞), MeasurableSet (f ⁻¹' {n})
⊢ Measurable f ↔ ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})

Tactic:
refine ⟨fun hf n ↦ hf <| measurableSet_singleton _, fun h ↦ measurable_to_countable' fun n ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
top : MeasurableSet.{u_6} (α := α) (⋃ (i : ℕ), f ⁻¹' {some i})ᶜ
⊢ MeasurableSet (f ⁻¹' {⊤})

Tactic:
rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]

Premises used: Set.iUnion_singleton_eq_range, Set.compl_range_some, Set.preimage_iUnion, Set.preimage_compl, WithTop.none_eq_top
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
⊢ MeasurableSet.{u_6} (α := α) (⋃ (i : ℕ), f ⁻¹' {some i})ᶜ

Tactic:
.compl <| .iUnion h

Premises used: MeasurableSet.compl, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
⊢ MeasurableSet.{u_6} (α := α) (⋃ (i : ℕ), f ⁻¹' {some i})ᶜ

Tactic:
exact .compl <| .iUnion h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
n : ℕ
⊢ MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})

Tactic:
h n
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
n : ℕ
⊢ MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})

Tactic:
exact h n
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_6
inst : MeasurableSpace α
f : α → ℕ∞
h : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
n : ℕ∞
top : MeasurableSet (f ⁻¹' {⊤})
coe : ∀ (n : ℕ), MeasurableSet (f ⁻¹' {(↑n : ℕ∞)})
⊢ MeasurableSet (f ⁻¹' {n})

Tactic:
cases n with
  | top =>
    rw [← WithTop.none_eq_top, ← compl_range_some, preimage_compl, ← iUnion_singleton_eq_range,
      preimage_iUnion]
    exact .compl <| .iUnion h
  | coe n => exact h n

Premises used: Set.iUnion_singleton_eq_range, Set.compl_range_some, Set.preimage_iUnion, Set.preimage_compl, WithTop.none_eq_top
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
f : Unit → α
⊢ Measurable f

Tactic:
measurable_from_top

Premises used: measurable_from_top
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Measurable (α := ULift.{u_6, u_1} α) ULift.down

Tactic:
fun _ ↦ id

Premises used: MeasurableSet, Set.Mem, Measurable, setOf, id, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Measurable (α := α) ULift.up

Tactic:
fun _ ↦ id

Premises used: MeasurableSet, Measurable, setOf, id, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ MeasurableSet (ULift.down ⁻¹' s) ↔ MeasurableSet s

Tactic:
Iff.rfl

Premises used: MeasurableSet, Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set (ULift.{u_6, u_1} α)
⊢ MeasurableSet (ULift.up ⁻¹' s) ↔ MeasurableSet s

Tactic:
Iff.rfl

Premises used: MeasurableSet, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : ℕ → α
⊢ Measurable f

Tactic:
measurable_from_top

Premises used: measurable_from_top
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℕ
⊢ (∀ (y : α), MeasurableSet (f ⁻¹' {f y})) → Measurable f

Tactic:
measurable_to_countable

Premises used: measurable_to_countable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
h₁ : ∀ (x : Bool), MeasurableSet (f ⁻¹' {x})
⊢ Measurable f

Tactic:
apply measurable_to_countable'

Premises used: measurable_to_countable'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})ᶜ

Tactic:
h.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
h₁ : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
⊢ MeasurableSet (f ⁻¹' {false})

Tactic:
convert! h.compl

Premises used: MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
h₁ : f ⁻¹' {false} = f ⁻¹' {true}ᶜ
h₂ : f ⁻¹' {false} = f ⁻¹' {!true}
h₃ h₄ : f ⁻¹' {false} = f ⁻¹' {false}
⊢ f ⁻¹' {false} = (f ⁻¹' {true})ᶜ

Tactic:
rw [← preimage_compl, Bool.compl_singleton, Bool.not_true]

Premises used: Bool.compl_singleton, Set.preimage_compl, Bool.not_true
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})

Tactic:
h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Bool
h : MeasurableSet (f ⁻¹' {true})
⊢ MeasurableSet (f ⁻¹' {true})

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
⊢ Measurable f

Tactic:
measurable_to_countable' fun x => ?_

Premises used: measurable_to_countable'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
refine : ∀ (x : Prop), MeasurableSet (f ⁻¹' {x})
⊢ Measurable f

Tactic:
refine measurable_to_countable' fun x => ?_

Premises used: measurable_to_countable'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
pos : ∀ (hx : x), MeasurableSet (f ⁻¹' {x})
neg : ∀ (hx : ¬x), MeasurableSet (f ⁻¹' {x})
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
by_cases hx : x
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa [hx] using h
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → Prop
h : MeasurableSet (f ⁻¹' {True})
x : Prop
hx : ¬x
⊢ MeasurableSet (f ⁻¹' {x})

Tactic:
simpa only [hx, ← preimage_compl, Prop.compl_singleton, not_true, preimage_singleton_false]
      using h.compl

Premises used: Prop.compl_singleton, MeasurableSet.compl, Set.preimage_singleton_false, not_true, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | Nat.findGreatest (p x) N = k}
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.findGreatest (p x) N

Tactic:
measurable_to_nat fun _ => hN _ N.findGreatest_le

Premises used: measurable_to_nat, Nat.findGreatest, Nat.findGreatest_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.findGreatest (p x) N

Tactic:
measurable_findGreatest' fun k hk => ?_

Premises used: measurable_findGreatest'
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Constructions
Goal:
α : Type u_1
mα : MeasurableSpace α
p : α → ℕ → Prop
inst : (x : α) → DecidablePred (p x)
N : ℕ
hN : ∀ k ≤ N, MeasurableSet.{u_1} (α := α) {x : α | p x k}
refine : ∀ (k : ℕ) (hk : k ≤ N), MeasurableSet.{u_1} (α := α) {x : α | Nat.findGreatest (p x) N = k}
⊢ Measurable (β := ℕ) fun (x : α) ↦ Nat.findGreatest (p x) N

Tactic:
refine measurable_findGreatest' fun k hk => ?_

Premises used: measurable_findGreatest'