awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')
h : IsEmpty ((i : ι) → α i)
⊢ (P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) (S' ∪ T') =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) S' : ℝ≥0∞)
      ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) T' : ℝ≥0∞)

Tactic:
simp [hP.eq_zero_of_isEmpty]

Premises used: MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')
h : Nonempty ((i : ι) → α i)
rw : Disjoint S' T'
⊢ (P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) (S' ∪ T') =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) S' : ℝ≥0∞)
      ((P (I ∪ J) : (a : Set ((j : ↥(I ∪ J)) → α (↑j : ι))) → ℝ≥0∞) T' : ℝ≥0∞)

Tactic:
rw [measure_union _ hT']

Premises used: MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')
h : Nonempty ((i : ι) → α i)
rwa :
  ∀ (hst : Disjoint (cylinder (α := α) I S) t) (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S) (J : Finset ι)
    (T : Set ((i : ↥J) → α (↑i : ι))) (hT : MeasurableSet T) (ht_eq : t = cylinder (α := α) J T),
    let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
    let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T;
    ∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T') (h_eq1 : s = cylinder (α := α) (I ∪ J) S')
      (h_eq2 : t = cylinder (α := α) (I ∪ J) T') (h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T'))
      (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
rwa₁ :
  ∀ (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S) (J : Finset ι) (T : Set ((i : ↥J) → α (↑i : ι)))
    (hst : Disjoint (cylinder (α := α) I S) (cylinder (α := α) J T)) (hT : MeasurableSet T)
    (ht_eq : t = cylinder (α := α) J T),
    let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
    let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T;
    ∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T') (h_eq1 : s = cylinder (α := α) (I ∪ J) S')
      (h_eq2 : t = cylinder (α := α) (I ∪ J) T') (h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T'))
      (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (hS : MeasurableSet S) (hs_eq : s = cylinder (α := α) I S) (J : Finset ι) (T : Set ((i : ↥J) → α (↑i : ι)))
    (hst : Disjoint (α := Set ((i : ↥(I ∪ J)) → α (↑i : ι))) (restrict₂ (π := α) ⋯ ⁻¹' S) (restrict₂ (π := α) ⋯ ⁻¹' T))
    (hT : MeasurableSet T) (ht_eq : t = cylinder (α := α) J T),
    let S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S;
    let T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T;
    ∀ (hS' : MeasurableSet S') (hT' : MeasurableSet T') (h_eq1 : s = cylinder (α := α) (I ∪ J) S')
      (h_eq2 : t = cylinder (α := α) (I ∪ J) T') (h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T'))
      (h : Nonempty ((i : ι) → α i)), Disjoint S' T'
⊢ Disjoint S' T'

Tactic:
rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst

Premises used: MeasureTheory.disjoint_cylinder_iff
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : Disjoint s t
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hS : MeasurableSet S
hs_eq : s = cylinder (α := α) I S
J : Finset ι
T : Set ((i : ↥J) → α (↑i : ι))
hT : MeasurableSet T
ht_eq : t = cylinder (α := α) J T
S' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' S
T' : Set ((i : ↥(I ∪ J)) → α (↑i : ι)) := restrict₂ (π := α) ⋯ ⁻¹' T
hS' : MeasurableSet S'
hT' : MeasurableSet T'
h_eq1 : s = cylinder (α := α) (I ∪ J) S'
h_eq2 : t = cylinder (α := α) (I ∪ J) T'
h_eq3 : s ∪ t = cylinder (α := α) (I ∪ J) (S' ∪ T')
⊢ IsEmpty ((i : ι) → α i) ∨ Nonempty ((i : ι) → α i)

Tactic:
cases isEmpty_or_nonempty (Π i, α i) with
  | inl h => simp [hP.eq_zero_of_isEmpty]
  | inr h =>
    rw [measure_union _ hT']
    rwa [hs_eq, ht_eq, disjoint_cylinder_iff] at hst

Premises used: isEmpty_or_nonempty, MeasureTheory.disjoint_cylinder_iff, MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
⊢ (projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s = projectiveFamilyFun (α := α) P s

Tactic:
rfl

Premises used: dite, MeasureTheory.projectiveFamilyFun, rfl
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hP : IsProjectiveMeasureFamily (α := α) P
s : Set ((i : ι) → α i)
hs_eq : s = cylinder (α := α) I S
hS : MeasurableSet S
rw : projectiveFamilyFun (α := α) P s = (P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)

Tactic:
rw [projectiveFamilyContent_eq,
    projectiveFamilyFun_congr hP ((mem_measurableCylinders s).mpr ⟨I, S, hS, hs_eq⟩) hs_eq hS]

Premises used: Iff.mpr, MeasureTheory.projectiveFamilyContent_eq, And.intro, Exists.intro, MeasureTheory.projectiveFamilyFun_congr, MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
hP : IsProjectiveMeasureFamily (α := α) P
hS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞)
    ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (cylinder (α := α) I S) : ℝ≥0∞)
    ((P I : (a : Set ((j : ↥I) → α (↑j : ι))) → ℝ≥0∞) S : ℝ≥0∞)

Tactic:
projectiveFamilyContent_congr _ _ rfl hS

Premises used: MeasureTheory.projectiveFamilyContent_congr, rfl
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hst : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
addContent_mono isSetSemiring_measurableCylinders hs ht hst

Premises used: MeasureTheory.isSetSemiring_measurableCylinders, MeasureTheory.addContent_mono
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
hP : IsProjectiveMeasureFamily (α := α) P
s : ℕ → Set ((i : ι) → α i)
hs : ∀ (n : ℕ), s n ∈ measurableCylinders α
n : ℕ
⊢ Eq (α := ℝ≥0∞)
    ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i) : ℝ≥0∞)
    ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (⋃ i ∈ range (n + 1), s i) : ℝ≥0∞)

Tactic:
simp only [mem_range_succ_iff]

Premises used: Finset.mem_range_succ_iff
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s : Set ((i : ι) → α i)
inst : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily (α := α) P
⊢ Ne (α := ℝ≥0∞)
    (if hs : s ∈ measurableCylinders α then
      (P (measurableCylinders.finset (α := α) (t := s) hs) :
          (a : Set ((j : ↥(measurableCylinders.finset hs)) → α (↑j : ι))) → ℝ≥0∞)
        (measurableCylinders.set (α := α) (t := s) hs)
    else 0)
    ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
      ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (s \ t)

Tactic:
le_addContent_diff (projectiveFamilyContent hP) isSetRing_measurableCylinders hs ht

Premises used: MeasureTheory.projectiveFamilyContent, MeasureTheory.isSetRing_measurableCylinders, MeasureTheory.le_addContent_diff
-- Module: Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
Goal:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α (↑j : ι))
s t : Set ((i : ι) → α i)
inst : ∀ (J : Finset ι), IsFiniteMeasure (P J)
hP : IsProjectiveMeasureFamily (α := α) P
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
hts : t ⊆ s
⊢ (projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) (s \ t) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) s : ℝ≥0∞)
      ((projectiveFamilyContent (α := α) hP : (a : Set ((i : ι) → α i)) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
addContent_diff_of_ne_top (projectiveFamilyContent hP) isSetRing_measurableCylinders
    (fun _ _ ↦ projectiveFamilyContent_ne_top hP) hs ht hts

Premises used: MeasureTheory.addContent_diff_of_ne_top, MeasureTheory.projectiveFamilyContent, MeasureTheory.isSetRing_measurableCylinders, MeasureTheory.projectiveFamilyContent_ne_top
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
Ω : Type u_2
m : MeasurableSpace Ω
G : Ω → SimpleGraph V
⊢ Measurable G ↔ ∀ (u v : V), Measurable (β := Prop) fun (ω : Ω) ↦ (G ω).Adj u v

Tactic:
simp [measurable_comap_iff, measurable_pi_iff]

Premises used: measurable_pi_iff, measurable_comap_iff
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
⊢ Measurable.{u_1, u_1} (α := SimpleGraph V) Adj

Tactic:
comap_measurable _

Premises used: comap_measurable
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
a : Sym2 V
u v : V
mk : Measurable (β := Prop) fun (x : SimpleGraph V) ↦ x.Adj u v
⊢ Measurable (β := Prop) fun (x : SimpleGraph V) ↦ Quot.mk (Sym2.Rel V) (u, v) ∈ x.edgeSet

Tactic:
simp only [mem_edgeSet]

Premises used: SimpleGraph.mem_edgeSet
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
a : Sym2 V
u v : V
⊢ Measurable (β := Prop) fun (x : SimpleGraph V) ↦ x.Adj u v

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
simp : ∀ (u v : V), Measurable (β := Prop) fun (ω : Set (Sym2 V)) ↦ s(u, v) ∈ ω ∧ ¬u = v
⊢ Measurable.{u_1, u_1} (α := Set (Sym2 V)) fromEdgeSet

Tactic:
simp only [measurable_iff_adj, fromEdgeSet_adj, ne_eq]

Premises used: SimpleGraph.fromEdgeSet_adj, ne_eq, SimpleGraph.measurable_iff_adj
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
⊢ ∀ (u v : V), Measurable (β := Prop) fun (ω : Set (Sym2 V)) ↦ s(u, v) ∈ ω ∧ ¬u = v

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
simp :
  Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦
    fromEdgeSet x ∈ s ∧ ∀ ⦃a : Sym2 V⦄, Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet a → a ∉ x
⊢ MeasurableSet (edgeSet '' s)

Tactic:
simp only [← measurable_mem, Set.mem_image, edgeSet_eq_iff, ↓existsAndEq, true_and,
      Set.disjoint_right]

Premises used: measurable_mem, Set.disjoint_right, SimpleGraph.edgeSet_eq_iff, Set.mem_image, ExistsAndEq.existsAndEq, true_and
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
⊢ Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦
    fromEdgeSet x ∈ s ∧ ∀ ⦃a : Sym2 V⦄, Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet a → a ∉ x

Tactic:
.and (hs.mem.comp measurable_fromEdgeSet) <| .forall fun e ↦ .imp ?_ ?_

Premises used: MeasurableSet.mem, Measurable.comp, SimpleGraph.measurable_fromEdgeSet, Measurable.and, Measurable.imp, Measurable.forall
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
refine_1 :
  ∀ (e : Sym2 V), Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet e
refine_2 : ∀ (e : Sym2 V), Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ e ∉ x
⊢ Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦
    fromEdgeSet x ∈ s ∧ ∀ ⦃a : Sym2 V⦄, Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet a → a ∉ x

Tactic:
refine .and (hs.mem.comp measurable_fromEdgeSet) <| .forall fun e ↦ .imp ?_ ?_
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
e : Sym2 V
⊢ Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ Membership.mem (γ := Set (Sym2 V)) Sym2.diagSet e

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.SimpleGraph
Goal:
V : Type u_1
inst : Countable V
s : Set (SimpleGraph V)
hs : MeasurableSet s
e : Sym2 V
⊢ Measurable (β := Prop) fun (x : Set (Sym2 V)) ↦ e ∉ x

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
inst_3 : MeasurableSpace M
inst_4 : DiscreteMeasurableSpace M
⊢ DiscreteMeasurableSpace.{u_2} (M ⧸ p)

Tactic:
Quotient.instDiscreteMeasurableSpace

Premises used: Quotient.instDiscreteMeasurableSpace
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
⊢ Eq (α := Measure (↑I : Type)) volume (comap (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) volume)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
rw : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (Icc 0 1) : ENNReal) (1 : ENNReal)
rw₁ : ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0) = 1
rw₂ : ENNReal.ofReal 1 = 1
rw₃ rw₄ : Eq (α := ENNReal) 1 1
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
rw [Measure.Subtype.volume_univ nullMeasurableSet_Icc, Real.volume_Icc, sub_zero,
      ENNReal.ofReal_one]

Premises used: nullMeasurableSet_Icc, sub_zero, Real.volume_Icc, ENNReal.ofReal_one, MeasureTheory.Measure.Subtype.volume_univ
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
s : Set (↑I : Type)
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) '' s) : ENNReal)

Tactic:
measurableEmbedding_coe.comap_apply ..

Premises used: MeasurableEmbedding.comap_apply, unitInterval.measurableEmbedding_coe
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
⊢ MeasurePreserving (α := { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I)) volume
    (Measure.restrict volume I)

Tactic:
measurePreserving_subtype_coe measurableSet_Icc

Premises used: MeasureTheory.measurePreserving_subtype_coe, measurableSet_Icc
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x : (↑I : Type)
⊢ Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) {x} : ENNReal) (0 : ENNReal)

Tactic:
simp [volume_apply]

Premises used: unitInterval.volume_apply
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
⊢ Measurable σ

Tactic:
continuous_symm.measurable

Premises used: Continuous.measurable, unitInterval.continuous_symm
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
⊢ symmMeasurableEquiv.symm = symmMeasurableEquiv

Tactic:
rfl

Premises used: MeasurableEquiv.symm, unitInterval.symmMeasurableEquiv, Equiv.symm, unitInterval.symm, rfl
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
⊢ (⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) = σ

Tactic:
rfl

Premises used: unitInterval.symm, rfl
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
h :
  ∀ (s : Set (↑I : Type)) (hs : MeasurableSet s),
    Eq (α := ENNReal) ((map σ volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
      ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
⊢ Eq (α := Measure (↑I : Type)) (map σ volume) volume

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
h :
  Eq (α := ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
      ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((map σ volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)

Tactic:
apply symmMeasurableEquiv.map_apply _ |>.trans

Premises used: MeasurableEquiv.map_apply, unitInterval.symmMeasurableEquiv, Eq.trans
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ 1 - x

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
rw : ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
| ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
    ENNReal)

Tactic:
rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm,
      ← map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs),
      volume.measurePreserving_sub_left 1 |>.map_eq, ← volume_apply]

Premises used: MeasureTheory.Measure.measurePreserving_sub_left, unitInterval.coe_symmMeasurableEquiv, unitInterval.volume_apply, MeasureTheory.Measure.map_apply, MeasureTheory.MeasurePreserving.map_eq, unitInterval.image_coe_preimage_symm, MeasurableSet.subtype_image, MeasureTheory.MeasureSpace.volume, measurableSet_Icc, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
s : Set (↑I : Type)
hs : MeasurableSet s
conv_lhs :
  Eq (α := ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
      ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
h :
  Eq (α := ENNReal) ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) ((⇑symmMeasurableEquiv : (a : (↑I : Type)) → (↑I : Type)) ⁻¹' s) :
      ENNReal)
    ((volume : (a : Set (↑I : Type)) → ENNReal) s : ENNReal)

Tactic:
conv_lhs => rw [coe_symmMeasurableEquiv, volume_apply, image_coe_preimage_symm,
      ← map_apply (by fun_prop) (measurableSet_Icc.subtype_image hs),
      volume.measurePreserving_sub_left 1 |>.map_eq, ← volume_apply]

Premises used: MeasureTheory.Measure.measurePreserving_sub_left, unitInterval.coe_symmMeasurableEquiv, unitInterval.volume_apply, MeasureTheory.Measure.map_apply, MeasureTheory.MeasurePreserving.map_eq, unitInterval.image_coe_preimage_symm, MeasurableSet.subtype_image, MeasureTheory.MeasureSpace.volume, measurableSet_Icc, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Iic x) = ENNReal.ofReal (↑x : ℝ)

Tactic:
simp only [volume_apply, image_subtype_val_Icc_Iic, Real.volume_Icc, sub_zero]

Premises used: unitInterval.volume_apply, sub_zero, Real.volume_Icc, Set.image_subtype_val_Icc_Iic
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Iio x) = ENNReal.ofReal (↑x : ℝ)

Tactic:
simp only [← volume_image_subtype_coe measurableSet_Icc, image_subtype_val_Icc_Iio,
    Real.volume_Ico, sub_zero]

Premises used: sub_zero, Real.volume_Ico, measurableSet_Icc, Set.image_subtype_val_Icc_Iio, volume_image_subtype_coe
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Ici x) = ENNReal.ofReal (1 - (↑x : ℝ))

Tactic:
simp only [volume_apply, image_subtype_val_Icc_Ici, Real.volume_Icc]

Premises used: unitInterval.volume_apply, Real.volume_Icc, Set.image_subtype_val_Icc_Ici
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Ioi x) = ENNReal.ofReal (1 - (↑x : ℝ))

Tactic:
simp only [volume_apply, image_subtype_val_Icc_Ioi, Real.volume_Ioc]

Premises used: unitInterval.volume_apply, Real.volume_Ioc, Set.image_subtype_val_Icc_Ioi
-- Module: Mathlib.MeasureTheory.Constructions.UnitInterval
Goal:
x y : (↑I : Type)
⊢ (volume : (a : Set (↑I : Type)) → ENNReal) (Icc x y) = ENNReal.ofReal ((↑y : ℝ) - (↑x : ℝ))

Tactic:
simp only [volume_apply, image_subtype_val_Icc, Real.volume_Icc]

Premises used: unitInterval.volume_apply, Real.volume_Icc, Set.image_subtype_val_Icc