-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem eq_of_cylinder_eq_of_subset [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

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
f : (i : { x // x ∈ I }) → α ↑i
h_eq :
  (I.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ S ↔
    (J.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ T
⊢ f ∈ S ↔ Finset.restrict₂ hJI f ∈ T

Tactic:
have h_mem : ∀ j : J, ↑j ∈ I := fun j ↦ hJI j.prop

Result:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
f : (i : { x // x ∈ I }) → α ↑i
h_eq :
  (I.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ S ↔
    (J.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ T
h_mem : ∀ (j : { x // x ∈ J }), ↑j ∈ I
⊢ f ∈ S ↔ Finset.restrict₂ hJI f ∈ T

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
f : (i : { x // x ∈ I }) → α ↑i
⊢ f ∈ S ↔ f ∈ Finset.restrict₂ hJI ⁻¹' T

Tactic:
simp only [mem_preimage]

Result:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
f : (i : { x // x ∈ I }) → α ↑i
⊢ f ∈ S ↔ Finset.restrict₂ hJI f ∈ T

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
f : (i : { x // x ∈ I }) → α ↑i
h_eq :
  (I.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ S ↔
    (J.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ T
h_mem : ∀ (j : { x // x ∈ J }), ↑j ∈ I
⊢ f ∈ S ↔ Finset.restrict₂ hJI f ∈ T

Tactic:
simpa only [Finset.restrict_def, Finset.coe_mem, dite_true, h_mem] using h_eq

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
f : (i : { x // x ∈ I }) → α ↑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

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder I S ↔ x ∈ cylinder J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Tactic:
simp only [mem_cylinder] at h_eq

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Tactic:
ext1 f

Result:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
f : (i : { x // x ∈ I }) → α ↑i
⊢ f ∈ S ↔ f ∈ Finset.restrict₂ hJI ⁻¹' T

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
h_eq : ∀ (x : (i : ι) → α i), I.restrict x ∈ S ↔ J.restrict x ∈ T
f : (i : { x // x ∈ I }) → α ↑i
⊢ f ∈ S ↔ Finset.restrict₂ hJI f ∈ T

Tactic:
specialize h_eq fun i ↦ if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i

Result:
case h
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hJI : J ⊆ I
f : (i : { x // x ∈ I }) → α ↑i
h_eq :
  (I.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ S ↔
    (J.restrict fun i => if hi : i ∈ I then f ⟨i, hi⟩ else h_nonempty.some i) ∈ T
⊢ f ∈ S ↔ Finset.restrict₂ hJI f ∈ T

Proof state:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ hJI ⁻¹' T

Tactic:
rw [Set.ext_iff] at h_eq

Result:
ι : Type u_1
α : ι → Type u_2
h_nonempty : Nonempty ((i : ι) → α i)
I J : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
h_eq : ∀ (x : (i : ι) → α i), x ∈ cylinder I S ↔ x ∈ cylinder J T
hJI : J ⊆ I
⊢ S = Finset.restrict₂ hJI ⁻¹' T