awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)
have pos : MeasurableSet (α := α j) (cast sorry t)
Tactic: simp only [hji, eq_mpr_eq_cast, dif_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
j : ι
hji : j = i
⊢ MeasurableSet (α := α j) (cast ⋯ t)
have h₁ : α j = α i → HEq (α := Set (α j)) (cast sorry t) t
Tactic: convert! ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
⊢ ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S
have refine_1 : ∀ (j : ι), MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr sorry t else univ : Set (α j))) j)
Tactic: classical
  refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
  · by_cases hji : j = i
    · simp only [hji, eq_mpr_eq_cast, dif_pos]
      convert! ht
      simp only [cast_heq]
    · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
  · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
m : (i : ι) → MeasurableSpace (α i)
i : ι
S : Set ((x : ι) → α x)
t : Set (α i)
ht : MeasurableSet t
h : eval (β := α) i ⁻¹' t = S
refine_1 :
  ∀ (j : ι), MeasurableSet.{u_1} (α := α j) ((fun (j : ι) ↦ (if hji : j = i then Eq.mpr ⋯ t else univ : Set (α j))) j)
⊢ ∃ (x : (i : ι) → Set (α i)), (∀ (i : ι), MeasurableSet (x i)) ∧ eval (β := α) i ⁻¹' x i = S
have refine_2 : eval (β := α) i ⁻¹' (fun (j : ι) ↦ (if hji : j = i then Eq.mpr sorry t else univ : Set (α j))) i = S
Tactic: classical
  refine ⟨fun j ↦ if hji : j = i then by convert! t else univ, fun j ↦ ?_, ?_⟩
  · by_cases hji : j = i
    · simp only [hji, eq_mpr_eq_cast, dif_pos]
      convert! ht
      simp only [cast_heq]
    · simp only [hji, not_false_iff, dif_neg, MeasurableSet.univ]
  · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal.
    It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in the new
    canonicalizer; a minimization would help. The original proof was: `grind` -/
    simp [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ Eq (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))
have a : LE.le (α := MeasurableSpace ((i : ι) → α i))
  (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
  (MeasurableSpace.pi (X := α))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
a :
  LE.le (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))
⊢ Eq (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))
have a₁ : LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.pi (X := α))
  (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ LE.le (α := MeasurableSpace ((i : ι) → α i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (MeasurableSpace.pi (X := α))
have a : Subset (α := Set (Set ((i : ι) → α i))) (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
  {t : Set ((i : ι) → α i) | MeasurableSet t}
Tactic: rw [MeasurableSpace.generateFrom_le_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
s : Finset ι
t : (i : ι) → Set (α i)
h :
  Membership.mem (γ := Set ((i : ι) → Set (α i)))
    (Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}) t
⊢ Membership.mem (γ := Set (Set ((i : ι) → α i))) {t : Set ((i : ι) → α i) | MeasurableSet t}
    ((↑s : Set ι).pi (α := α) t)
have h₁ : ∀ (i : ι), MeasurableSet (t i)
Tactic: simp only [mem_univ_pi, mem_setOf_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
⊢ LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.pi (X := α))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
have a : ∀ (i : ι),
  LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
Tactic: refine iSup_le fun i ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ LE.le (α := MeasurableSpace ((i : ι) → α i)) (MeasurableSpace.comap (fun (b : (a : ι) → α a) ↦ b i) (inst i))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
have a : LE.le (α := MeasurableSpace ((x : ι) → α x))
  (generateFrom
    ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
  (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
Tactic: refine (comap_eval_le_generateFrom_squareCylinders_singleton α i).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ LE.le (α := MeasurableSpace ((x : ι) → α x))
    (generateFrom
      ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
        Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
    (generateFrom (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s}))
have a : Subset (α := Set (Set ((i : ι) → α i)))
  ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
    Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
  (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
Tactic: refine MeasurableSpace.generateFrom_mono ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_2
α : ι → Type u_1
inst : (i : ι) → MeasurableSpace (α i)
i : ι
⊢ Subset (α := Set (Set ((i : ι) → α i)))
    ((fun (t : (i : ι) → Set (α i)) ↦ Set.pi (α := α) {i} t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
    (squareCylinders (α := α) fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
have a : Subset (α := Set (Set ((i : ι) → α i)))
  ((fun (t : (i : ι) → Set (α i)) ↦ (↑{i} : Set ι).pi (α := α) t) ''
    Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
  (⋃ (s : Finset ι),
    (fun (t : (i : ι) → Set (α i)) ↦ (↑s : Set ι).pi (α := α) t) ''
      Set.pi (α := fun (i : ι) ↦ Set (α i)) univ fun (i : ι) ↦ {s : Set (α i) | MeasurableSet s})
Tactic: rw [← Finset.coe_singleton, squareCylinders_eq_iUnion_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅
have rw : Eq (α := Set ((i : ι) → α i)) (s.restrict (π := α) ⁻¹' ∅) ∅
Tactic: rw [cylinder, preimage_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
rw : Eq (α := Set ((i : ι) → α i)) (s.restrict (π := α) ⁻¹' ∅) ∅
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅
have rw₁ : Eq (α := Set ((i : ι) → α i)) ∅ ∅
Tactic: rw [cylinder, preimage_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s univ) univ
have rw : Eq (α := Set ((i : ι) → α i)) (s.restrict (π := α) ⁻¹' univ) univ
Tactic: rw [cylinder, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
rw : Eq (α := Set ((i : ι) → α i)) (s.restrict (π := α) ⁻¹' univ) univ
⊢ Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s univ) univ
have rw₁ : Eq (α := Set ((i : ι) → α i)) univ univ
Tactic: rw [cylinder, preimage_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : S = ∅
⊢ cylinder (α := α) s S = ∅
have rw : Eq (α := Set ((i : ι) → α i)) (cylinder (α := α) s ∅) ∅
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
⊢ cylinder (α := α) s S = ∅ ↔ S = ∅
have refine : ∀ (h : cylinder (α := α) s S = ∅), S = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by (rw [h]; exact cylinder_empty _)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
⊢ S = ∅
have by_contra : ∀ (hS : ¬S = ∅), False
Tactic: by_contra hS
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : ¬S = ∅
⊢ False
have hS₁ : S.Nonempty
Tactic: rw [← Ne, ← nonempty_iff_ne_empty] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
⊢ False
have hf : f ∈ S
Tactic: have hf : f ∈ S := hS.choose_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
⊢ f' ∈ cylinder (α := α) s S
have rw : s.restrict (π := α) f' ∈ S
Tactic: rw [mem_cylinder]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
⊢ False
have hf' : f' ∈ cylinder (α := α) s S
Tactic: have hf' : f' ∈ cylinder s S := by
    rw [mem_cylinder]
    simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
f' : (i : ι) → α i :=
  fun (i : ι) ↦ if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i
hf' : f' ∈ cylinder (α := α) s S
⊢ False
have hf'₁ : Membership.mem (γ := Set ((i : ι) → α i)) ∅ f'
Tactic: rw [h] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
let let₁ let₂ : False
⊢ False
have let₃ : let f' : (i : ι) → α i := fun (i : ι) ↦
  if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i;
∀ (hf' : f' ∈ cylinder (α := α) s S), False
Tactic: classical
  let f' : ∀ i, α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
  have hf' : f' ∈ cylinder s S := by
    rw [mem_cylinder]
    simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']
  rw [h] at hf'
  exact notMem_empty _ hf'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
h : cylinder (α := α) s S = ∅
hS : S.Nonempty
f : (i : ↥s) → α (↑i : ι) := hS.some (s := S)
hf : f ∈ S
let let₁ let₂ : False
let₃ :
  let f' : (i : ι) → α i := fun (i : ι) ↦
    if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i;
  ∀ (hf' : f' ∈ cylinder (α := α) s S), False
⊢ False
have let₄ : let f' : (i : ι) → α i := fun (i : ι) ↦
  if hi : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) else h_nonempty.some i;
∀ (hf' : Membership.mem (γ := Set ((i : ι) → α i)) ∅ f'), False
Tactic: classical
  let f' : ∀ i, α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
  have hf' : f' ∈ cylinder s S := by
    rw [mem_cylinder]
    simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']
  rw [h] at hf'
  exact notMem_empty _ hf'
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
⊢ (cylinder (α := α) s S)ᶜ = cylinder (α := α) s Sᶜ
have h : ∀ (f : (i : ι) → α i), f ∈ (cylinder (α := α) s S)ᶜ ↔ f ∈ cylinder (α := α) s Sᶜ
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α (↑i : ι))
⊢ cylinder (α := α) s S \ cylinder (α := α) s T = cylinder (α := α) s (S \ T)
have h : ∀ (f : (i : ι) → α i), f ∈ cylinder (α := α) s S \ cylinder (α := α) s T ↔ f ∈ cylinder (α := α) s (S \ T)
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
h_eq : cylinder (α := α) I S = cylinder (α := α) J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ (π := α) hJI ⁻¹' T
have rw : ∀ (h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder (α := α) I S ↔ x ∈ cylinder (α := α) J T) (hJI : J ⊆ I),
  S = Finset.restrict₂ (π := α) hJI ⁻¹' T
Tactic: rw [Set.ext_iff] at h_eq
Cleared hypotheses: h_eq, hJI
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder (α := α) I S ↔ x ∈ cylinder (α := α) J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ (π := α) hJI ⁻¹' T
have h_eq₁ : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
Tactic: simp only [mem_cylinder] at h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
⊢ S = Finset.restrict₂ (π := α) hJI ⁻¹' T
have h : ∀ (f : (i : ↥I) → α (↑i : ι)), f ∈ S ↔ f ∈ Finset.restrict₂ (π := α) hJI ⁻¹' T
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
⊢ f ∈ S ↔ f ∈ Finset.restrict₂ (π := α) hJI ⁻¹' T
have h : f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
Tactic: simp only [mem_preimage]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
⊢ f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
have h_eq₁ : (I.restrict (π := α) fun (i : ι) ↦
      if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
    S ↔
  (J.restrict (π := α) fun (i : ι) ↦
      if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
    T
Tactic: specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
f : (i : ↥I) → α (↑i : ι)
h_eq :
  (I.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      S ↔
    (J.restrict (π := α) fun (i : ι) ↦
        if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
      T
⊢ f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
have h_mem : ∀ (j : ↥J), (↑j : ι) ∈ I
Tactic: have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
⊢ f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
have h : ∀
  (h_eq :
    (I.restrict (π := α) fun (i : ι) ↦
          if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
        S ↔
      (J.restrict (π := α) fun (i : ι) ↦
          if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
        T),
  f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
Tactic: classical
  specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i
  have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop
  simpa only [Finset.restrict_def, Finset.coe_mem, dite_true, h_mem] using h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
T : Set ((i : ↥J) → α (↑i : ι))
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict (π := α) x ∈ S ↔ J.restrict (π := α) x ∈ T
f : (i : ↥I) → α (↑i : ι)
h :
  ∀
    (h_eq :
      (I.restrict (π := α) fun (i : ι) ↦
            if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
          S ↔
        (J.restrict (π := α) fun (i : ι) ↦
            if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
          T),
    f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
⊢ f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
have h₁ : ∀
  (h_eq :
    (I.restrict (π := α) fun (i : ι) ↦
          if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
        S ↔
      (J.restrict (π := α) fun (i : ι) ↦
          if hi : i ∈ I then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi) else h_nonempty.some i) ∈
        T)
  (h_mem : ∀ (j : ↥J), (↑j : ι) ∈ I), f ∈ S ↔ Finset.restrict₂ (π := α) hJI f ∈ T
Tactic: classical
  specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i
  have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop
  simpa only [Finset.restrict_def, Finset.coe_mem, dite_true, h_mem] using h_eq
Cleared hypotheses: h_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
I : Finset ι
S : Set ((i : ↥I) → α (↑i : ι))
J : Finset ι
⊢ cylinder (α := α) I S = cylinder (α := α) (I ∪ J) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)
have h : ∀ (f : (i : ι) → α i), f ∈ cylinder (α := α) I S ↔ f ∈ cylinder (α := α) (I ∪ J) (Finset.restrict₂ (π := α) sorry ⁻¹' S)
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
T : Set ((i : ↥t) → α (↑i : ι))
inst_1 : DecidableEq ι
⊢ Disjoint (cylinder (α := α) s S) (cylinder (α := α) t T) ↔
    Disjoint (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' T)
have simp_rw : cylinder (α := α) s S ∩ cylinder (α := α) t T ⊆ ∅ ↔
  Subset (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι)))
    (Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T) ∅
Tactic: simp_rw [Set.disjoint_iff, subset_empty_iff, inter_cylinder, cylinder_eq_empty_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.Cylinders (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Nonempty ((i : ι) → α i)
s t : Finset ι
S : Set ((i : ↥s) → α (↑i : ι))
T : Set ((i : ↥t) → α (↑i : ι))
inst_1 : DecidableEq ι
simp_rw :
  cylinder (α := α) s S ∩ cylinder (α := α) t T ⊆ ∅ ↔
    Subset (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι)))
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' S ∩ Finset.restrict₂ (π := α) ⋯ ⁻¹' T) ∅
⊢ Disjoint (cylinder (α := α) s S) (cylinder (α := α) t T) ↔
    Disjoint (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) ⋯ ⁻¹' S)
      (Finset.restrict₂ (π := α) ⋯ ⁻¹' T)
have simp_rw₁ : cylinder (α := α) s S ∩ cylinder (α := α) t T = ∅ ↔
  Eq (α := Set ((i : ↥(s ∪ t)) → α (↑i : ι))) (Finset.restrict₂ (π := α) sorry ⁻¹' S ∩ Finset.restrict₂ (π := α) sorry ⁻¹' T) ∅
Tactic: simp_rw [Set.disjoint_iff, subset_empty_iff, inter_cylinder, cylinder_eq_empty_iff]