-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem cylinder_eq_empty_iff [h_nonempty : Nonempty (∀ i, α i)] (s : Finset ι)
    (S : Set (∀ i : s, α i)) :
    cylinder s S = ∅ ↔ S = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : S = ∅
⊢ cylinder s S = ∅

Tactic:
(rw [h]; exact cylinder_empty _)

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ False

Tactic:
have hf' : f' ∈ cylinder s S := by
  rw [mem_cylinder]
  simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
hf' : f' ∈ cylinder s S
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
hf' : f' ∈ cylinder s S
⊢ False

Tactic:
rw [h] at hf'

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
hf' : f' ∈ ∅
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
⊢ False

Tactic:
let f' : ∀ i, α i := fun i ↦ if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
⊢ False

Tactic:
let f := hS.some

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ f' ∈ cylinder s S

Tactic:
rw [mem_cylinder]

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ s.restrict f' ∈ S

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
⊢ False

Tactic:
have hf : f ∈ S := hS.choose_spec

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : ¬S = ∅
⊢ False

Tactic:
rw [← Ne, ← nonempty_iff_ne_empty] at hS

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
⊢ s.restrict f' ∈ S

Tactic:
simpa only [Finset.restrict_def, Finset.coe_mem, dif_pos, f']

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder s S = ∅ ↔ S = ∅

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by (rw [h]; exact cylinder_empty _)⟩

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
⊢ S = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ 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 not_mem_empty _ hf'

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
⊢ S = ∅

Tactic:
by_contra hS

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : ¬S = ∅
⊢ False

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : cylinder s S = ∅
hS : S.Nonempty
f : (i : { x // x ∈ s }) → α ↑i := hS.some
hf : f ∈ S
f' : (i : ι) → α i := fun i => if hi : i ∈ s then f ⟨i, hi⟩ else h_nonempty.some i
hf' : f' ∈ ∅
⊢ False

Tactic:
exact not_mem_empty _ hf'

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : S = ∅
⊢ cylinder s S = ∅

Tactic:
rw [h]

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : S = ∅
⊢ cylinder s ∅ = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
h : S = ∅
⊢ cylinder s ∅ = ∅

Tactic:
exact cylinder_empty _

Result:
no goals