awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (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)
h : y ∉ f '' F^[n] univ
refine_2 : g y ∈ g '' (f '' F^[n] univ)ᶜ
⊢ False

Tactic:
apply hx
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (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)
h : y ∉ f '' F^[n] univ
⊢ g y ∈ g '' (f '' F^[n] univ)ᶜ

Tactic:
⟨y, h, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
δ' : Type u_5
ι : Sort uι
s t u : Set α
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f_1 : α → β
g_1 : β → α
f : α → β
g : β → α
hf : MeasurableEmbedding f
hg : MeasurableEmbedding g
F : Set α → Set α := fun (A : Set α) ↦ (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)
h : y ∉ f '' F^[n] univ
⊢ g y ∈ g '' (f '' F^[n] univ)ᶜ

Tactic:
exact ⟨y, h, rfl⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
⊢ (hf.equivRange : (a : α) → (↑(range f) : Type u_2)) x = Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯

Tactic:
simp [MeasurableEmbedding.equivRange, MeasurableEquiv.cast, MeasurableEquiv.Set.univ,
    MeasurableEmbedding.equivImage]

Premises used: MeasurableEquiv.cast, MeasurableEmbedding.equivRange, MeasurableEquiv.Set.univ, MeasurableEmbedding.equivImage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
nth_rw :
  Eq.{u_1 + 1} (α := α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) : α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α)
        ((hf.equivRange : (a : α) → (↑(range f) : Type u_2)) x : (↑(range f) : Type u_2)) :
      α)
⊢ (hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) = x

Tactic:
nth_rw 3 [← hf.equivRange.symm_apply_apply x]

Premises used: MeasurableEmbedding.equivRange, MeasurableEquiv.symm_apply_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
x : α
rw rw₁ :
  Eq.{u_1 + 1} (α := α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) : α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) : α)
⊢ Eq.{u_1 + 1} (α := α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α) (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f x) ⋯) : α)
    ((hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α)
        ((hf.equivRange : (a : α) → (↑(range f) : Type u_2)) x : (↑(range f) : Type u_2)) :
      α)

Tactic:
rw [hf.equivRange_apply]

Premises used: MeasurableEmbedding.equivRange_apply
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
inst_2 : Nonempty α
hf : MeasurableEmbedding f
⊢ Measurable.{u_2, u_1} (α := (↑(range f) : Type u_2)) (β := α)
    (⇑hf.equivRange.symm : (a : (↑(range f) : Type u_2)) → α)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
inst_2 : Nonempty α
hf : MeasurableEmbedding f
x : α
⊢ hf.invFun (f x) = x

Tactic:
simp [MeasurableEmbedding.invFun]

Premises used: MeasurableEmbedding.invFun
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst : BooleanAlgebra β
h : Measurable.{u_2, u_2} (α := β) compl
f : α → β
rw : MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance
⊢ MeasurableSpace.comap.{u_1, u_2} (β := β) (fun (a : α) ↦ (f a)ᶜ) inferInstance = MeasurableSpace.comap f inferInstance

Tactic:
rw [← Function.comp_def, ← MeasurableSpace.comap_comp]

Premises used: MeasurableSpace.comap_comp, Function.comp_def
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst : BooleanAlgebra β
h : Measurable.{u_2, u_2} (α := β) compl
f : α → β
e_m : Eq.{u_2 + 1} (α := MeasurableSpace β) (MeasurableSpace.comap compl inferInstance) inferInstance
⊢ MeasurableSpace.comap f (MeasurableSpace.comap compl inferInstance) = MeasurableSpace.comap f inferInstance

Tactic:
congr
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst : BooleanAlgebra β
h : Measurable.{u_2, u_2} (α := β) compl
f : α → β
⊢ Eq.{u_2 + 1} (α := MeasurableSpace β) (MeasurableSpace.comap compl inferInstance) inferInstance

Tactic:
(MeasurableEquiv.ofInvolutive _ compl_involutive h).measurableEmbedding.comap_eq

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.ofInvolutive, compl_involutive, MeasurableEmbedding.comap_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
β : Type u_2
m' : MeasurableSpace β
inst : BooleanAlgebra β
h : Measurable.{u_2, u_2} (α := β) compl
f : α → β
⊢ Eq.{u_2 + 1} (α := MeasurableSpace β) (MeasurableSpace.comap compl inferInstance) inferInstance

Tactic:
exact (MeasurableEquiv.ofInvolutive _ compl_involutive h).measurableEmbedding.comap_eq

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.ofInvolutive, compl_involutive, MeasurableEmbedding.comap_eq
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
α : Type u_1
p : α → Prop
⊢ MeasurableSpace.comap (β := Prop) (fun (a : α) ↦ ¬p a) inferInstance = MeasurableSpace.comap p inferInstance

Tactic:
MeasurableSpace.comap_compl (fun _ _ ↦ measurableSet_top) _

Premises used: MeasurableSpace.comap_compl, MeasurableSpace.measurableSet_top
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Eq (α :=
    (a : (p : (i : ι) × κ i) → X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))) →
      (i : ι) → (j : κ i) → X i j)
    (⇑(piCurry (κ := κ) X) : (a : (p : (i : ι) × κ i) → X p.fst p.snd) → (i : ι) → (j : κ i) → X i j)
    (Sigma.curry (β := fun (i : ι) ↦ κ i) (γ := X))

Tactic:
rfl

Premises used: Sigma.curry, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
ι : Type u_6
κ : ι → Type u_7
X : (i : ι) → κ i → Type u_8
inst : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
⊢ Eq (α :=
    (a : (i : ι) → (j : κ i) → X i j) →
      (p : (i : ι) × κ i) → X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (⇑(symm (piCurry (κ := κ) X)) : (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
    (Sigma.uncurry (β := κ) (γ := X))

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
inst : MeasurableSpace X
⊢ Eq (α := (a : ι × κ → X) → ι → κ → X) (⇑(curry ι κ X) : (a : ι × κ → X) → ι → κ → X) Function.curry

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Embedding
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
inst : MeasurableSpace X
⊢ Eq (α := (a : ι → κ → X) → ι × κ → X) (⇑(symm (curry ι κ X)) : (a : ι → κ → X) → ι × κ → X) uncurry

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s_1 t : Set α
l : Filter α
inst : CountableInterFilter l
s : ℕ → Set α
hs : ∀ (i : ℕ), ∃ (t : Set α), MeasurableSet t ∧ s i =ᶠ[l] t
choose :
  ∀ (t : (i : ℕ) → Set α) (ht : ∀ (i : ℕ), MeasurableSet (t i)) (hts : ∀ (i : ℕ), s i =ᶠ[l] t i),
    ∃ (t : Set α), MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᶠ[l] t
⊢ ∃ (t : Set α), MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᶠ[l] t

Tactic:
choose t ht hts using hs
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s_1 t_1 : Set α
l : Filter α
inst : CountableInterFilter l
s t : (i : ℕ) → Set α
ht : ∀ (i : ℕ), MeasurableSet (t i)
hts : ∀ (i : ℕ), s i =ᶠ[l] t i
⊢ ∃ (t : Set α), MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᶠ[l] t

Tactic:
⟨⋃ i, t i, MeasurableSet.iUnion ht, .countable_iUnion hts⟩

Premises used: Filter.EventuallyEq.countable_iUnion, And.intro, Exists.intro, MeasurableSet.iUnion, Set.iUnion
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s_1 t_1 : Set α
l : Filter α
inst : CountableInterFilter l
s t : (i : ℕ) → Set α
ht : ∀ (i : ℕ), MeasurableSet (t i)
hts : ∀ (i : ℕ), s i =ᶠ[l] t i
⊢ ∃ (t : Set α), MeasurableSet t ∧ ⋃ (i : ℕ), s i =ᶠ[l] t

Tactic:
exact ⟨⋃ i, t i, MeasurableSet.iUnion ht, .countable_iUnion hts⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
l : Filter α
inst : CountableInterFilter l
hs : MeasurableSet s
⊢ EventuallyMeasurableSet m l s

Tactic:
⟨s, hs, EventuallyEq.refl _ _⟩

Premises used: MeasurableSet, Filter.EventuallyEq.refl, EventuallyMeasurableSet, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
l : Filter α
inst : CountableInterFilter l
⊢ m ≤ eventuallyMeasurableSpace m l

Tactic:
fun _ hs => hs.eventuallyMeasurableSet

Premises used: MeasurableSet.eventuallyMeasurableSet, EventuallyMeasurableSet
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s : Set α
l : Filter α
inst : CountableInterFilter l
hs : s ∈ l
⊢ EventuallyMeasurableSet m l s

Tactic:
⟨univ, MeasurableSet.univ, eventuallyEq_univ.mpr hs⟩

Premises used: Iff.mpr, MeasurableSet, Set.univ, EventuallyMeasurableSet, And.intro, Exists.intro, Filter.eventuallyEq_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst : CountableInterFilter l
ht : EventuallyMeasurableSet m l t
hst : s =ᶠ[l] t
rcases : ∀ (t' : Set α) (ht' : MeasurableSet t') (htt' : t =ᶠ[l] t'), EventuallyMeasurableSet m l s
⊢ EventuallyMeasurableSet m l s

Tactic:
rcases ht with ⟨t', ht', htt'⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst : CountableInterFilter l
hst : s =ᶠ[l] t
t' : Set α
ht' : MeasurableSet t'
htt' : t =ᶠ[l] t'
⊢ EventuallyMeasurableSet m l s

Tactic:
⟨t', ht', hst.trans htt'⟩

Premises used: Filter.EventuallyEq.trans, MeasurableSet, EventuallyMeasurableSet, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst : CountableInterFilter l
hst : s =ᶠ[l] t
t' : Set α
ht' : MeasurableSet t'
htt' : t =ᶠ[l] t'
⊢ EventuallyMeasurableSet m l s

Tactic:
exact ⟨t', ht', hst.trans htt'⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst : CountableInterFilter l
inst_1 : MeasurableSingletonClass α
⊢ MeasurableSingletonClass α

Tactic:
@MeasurableSingletonClass.mk _ (_) <| fun x => (MeasurableSet.singleton x).eventuallyMeasurableSet

Premises used: MeasurableSet.singleton, MeasurableSet.eventuallyMeasurableSet, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
l : Filter α
inst : CountableInterFilter l
β : Type u_2
inst_1 : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ EventuallyMeasurable m l f

Tactic:
hf.le le_eventuallyMeasurableSpace

Premises used: le_eventuallyMeasurableSpace, EventuallyMeasurable, Measurable.le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
l : Filter α
inst : CountableInterFilter l
β : Type u_2
γ : Type u_3
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
f : α → β
h : β → γ
hh : Measurable h
hf : EventuallyMeasurable m l f
⊢ EventuallyMeasurable m l (h ∘ f)

Tactic:
hh.comp hf

Premises used: Measurable.comp, EventuallyMeasurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
l : Filter α
inst : CountableInterFilter l
β : Type u_2
inst_1 : MeasurableSpace β
f g : α → β
hf : EventuallyMeasurable m l f
hgf : g =ᶠ[l] f
⊢ EventuallyMeasurable m l g

Tactic:
fun _ hs => EventuallyMeasurableSet.congr (hf hs)
    (hgf.preimage _)

Premises used: Measurable, EventuallyMeasurable, Filter.EventuallyEq.preimage, EventuallyMeasurableSet, EventuallyMeasurableSet.congr
-- Module: Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Goal:
α : Type u_1
m : MeasurableSpace α
l : Filter α
inst : CountableInterFilter l
β : Type u_2
inst_1 : MeasurableSpace β
f g : α → β
hf : Measurable f
hgf : g =ᶠ[l] f
⊢ EventuallyMeasurable m l g

Tactic:
hf.eventuallyMeasurable.congr hgf

Premises used: EventuallyMeasurable.congr, Measurable.eventuallyMeasurable
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
α : Type u_1
f : α → α
⊢ DiscreteMeasurableSpace (IterateMulAct f)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
⊢ MeasurableSingletonClass α

Tactic:
⟨fun i => ?_⟩

Premises used: MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
refine : ∀ (i : α), MeasurableSet (α := α) {i}
⊢ MeasurableSingletonClass α

Tactic:
refine ⟨fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ MeasurableSet.{u_1} (α := α) Set.univ

Tactic:
MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
h : Eq (α := Set α) {i} Set.univ
⊢ MeasurableSet (α := α) {i}

Tactic:
convert! MeasurableSet.univ

Premises used: MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ Eq (α := Set α) {i} Set.univ

Tactic:
simp [Set.eq_univ_iff_forall, eq_iff_true_of_subsingleton]

Premises used: Set.eq_univ_iff_forall, eq_iff_true_of_subsingleton
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ MeasurableSingletonClass Bool

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ MeasurableSingletonClass Prop

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ MeasurableSingletonClass ℕ

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ DiscreteMeasurableSpace ℕ∞

Tactic:
⟨fun _ ↦ trivial⟩

Premises used: trivial, DiscreteMeasurableSpace.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ MeasurableSingletonClass ℕ∞

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
n : ℕ
⊢ MeasurableSingletonClass (Fin n)

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
n : ℕ
⊢ MeasurableSingletonClass (ZMod n)

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ MeasurableSingletonClass ℤ

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Instances
Goal:
⊢ MeasurableSingletonClass ℚ

Tactic:
⟨fun _ => trivial⟩

Premises used: trivial, MeasurableSingletonClass.mk
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
⊢ (fun (s : Set α) ↦ f ⁻¹' s = s) ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → α
⊢ ∀ (s : Set α), (fun (s : Set α) ↦ f ⁻¹' s = s) s → (fun (s : Set α) ↦ f ⁻¹' s = s) sᶜ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
m : MeasurableSpace α
f_1 : α → α
f : ℕ → Set α
hf : ∀ (i : ℕ), (fun (s : Set α) ↦ f_1 ⁻¹' s = s) (f i)
⊢ (fun (s : Set α) ↦ f_1 ⁻¹' s = s) (⋃ (i : ℕ), f i)

Tactic:
simp [hf]
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
s : Set α
⊢ MeasurableSet s ↔ MeasurableSet s ∧ f ⁻¹' s = s

Tactic:
.rfl

Premises used: MeasurableSet, Iff.rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ invariants id = inst

Tactic:
ext fun _ ↦ ⟨And.left, fun h ↦ ⟨h, rfl⟩⟩

Premises used: And.left, And.intro, Iff.intro, MeasurableSpace.ext, rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
⊢ invariants f ≤ inst

Tactic:
fun _ ↦ And.left

Premises used: MeasurableSet, And.left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f g : α → α
s : Set α
hs : MeasurableSet s
rw : g ⁻¹' f ⁻¹' s = s
rw₁ : g ⁻¹' s = s
rw₂ rw₃ : s = s
⊢ f ∘ g ⁻¹' s = s

Tactic:
rw [preimage_comp, hs.1.2, hs.2.2]

Premises used: Set.preimage_comp, And.right, And.left
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
⊢ invariants f ≤ invariants f^[0]

Tactic:
simp [invariants_le]

Premises used: MeasurableSpace.invariants_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
n : ℕ
ihn : invariants f ≤ invariants f^[n]
⊢ invariants f ≤ invariants f^[n + 1]

Tactic:
le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

Premises used: le_rfl, le_inf, MeasurableSpace.inf_le_invariants_comp, le_trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
n : ℕ
ihn : invariants f ≤ invariants f^[n]
⊢ invariants f ≤ invariants f^[n + 1]

Tactic:
exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

Premises used: le_rfl, le_inf, MeasurableSpace.inf_le_invariants_comp, le_trans
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
f : α → α
n : ℕ
zero : invariants f ≤ invariants f^[0]
succ : ∀ (n : ℕ) (ihn : invariants f ≤ invariants f^[n]), invariants f ≤ invariants f^[n + 1]
⊢ invariants f ≤ invariants f^[n]

Tactic:
induction n with
  | zero => simp [invariants_le]
  | succ n ihn => exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

Premises used: MeasurableSpace.invariants_le
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
simp :
  (∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔
    ∀ (x : Set β) (x_1 : MeasurableSet x), MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x
⊢ Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ f ⁻¹' s = g ⁻¹' s

Tactic:
simp only [Measurable, ← forall_and]

Premises used: Measurable, forall_and
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
⊢ (∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔
    ∀ (x : Set β) (x_1 : MeasurableSet x), MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
fa : α → α
fb : β → β
g : α → β
hg : Measurable g
hfg : Semiconj g fa fb
s : Set β
hs : MeasurableSet s
rw : g ∘ fa ⁻¹' s = g ⁻¹' s
rw₁ : fb ∘ g ⁻¹' s = g ⁻¹' s
rw₂ : g ⁻¹' fb ⁻¹' s = g ⁻¹' s
rw₃ rw₄ : g ⁻¹' s = g ⁻¹' s
⊢ fa ⁻¹' g ⁻¹' s = g ⁻¹' s

Tactic:
rw [← preimage_comp, hfg.comp_eq, preimage_comp, hs.2]

Premises used: Function.Semiconj.comp_eq, Set.preimage_comp, And.right
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
h₁ : ∀ (x : α), (g ∘ f) x = g x
⊢ g ∘ f = g

Tactic:
funext x
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
this : x ∈ f ⁻¹' g ⁻¹' {g x}
⊢ (g ∘ f) x = g x

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
h₁ : x ∈ f ⁻¹' g ⁻¹' {g x}
⊢ (g ∘ f) x = g x

Tactic:
suffices x ∈ f ⁻¹' g ⁻¹' {g x} by simpa
-- Module: Mathlib.MeasureTheory.MeasurableSpace.Invariants
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_2
inst_1 : MeasurableSpace β
f : α → α
g : α → β
inst_2 : MeasurableSingletonClass β
h : Measurable g
x : α
h₁ : x ∈ g ⁻¹' {g x}
h₂ : Membership.mem (γ := Set β) {g x} (g x)
h₃ h₄ : g x = g x
⊢ x ∈ f ⁻¹' g ⁻¹' {g x}

Tactic:
rw [(h <| measurableSet_singleton (g x)).2, Set.mem_preimage, Set.mem_singleton_iff]

Premises used: MeasurableSingletonClass.measurableSet_singleton, Set.mem_singleton_iff, And.right, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
t : Set α
ht : Membership.mem (γ := Set (Set α)) {s} t
⊢ preimage (β := Prop) (fun (x : α) ↦ x ∈ s) {True} = t

Tactic:
simp [ht.symm]

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
refine : LE.le (α := MeasurableSpace α) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤) (generateFrom {s})
⊢ Eq (α := MeasurableSpace α) (generateFrom {s}) (MeasurableSpace.comap (β := Prop) (fun (x : α) ↦ x ∈ s) ⊤)

Tactic:
refine le_antisymm (generateFrom_le fun t ht => ⟨{True}, trivial, by simp [ht.symm]⟩) ?_
-- Module: Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Goal:
α : Type u_1
s : Set α
this : MeasurableSpace α := generateFrom {s}
u : Set Prop
⊢ MeasurableSet.{u_1} (α := α) ((fun (x : α) ↦ x ∈ s) ⁻¹' u)

Tactic:
(show MeasurableSet s from GenerateMeasurable.basic _ <| mem_singleton s).mem trivial

Premises used: MeasurableSet.mem, Set.mem_singleton, trivial, MeasurableSpace.GenerateMeasurable.basic