-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma congr_cylinder (hP : IsProjectiveMeasureFamily P)
    {S : Set (∀ i : I, α i)} {T : Set (∀ i : J, α i)} (hS : MeasurableSet S) (hT : MeasurableSet T)
    (h_eq : cylinder I S = cylinder J T) :
    P I S = P J T

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P (I ∪ J)) U = (P I) S ∧ (P (I ∪ J)) U = (P J) T

Tactic:
constructor

Result:
case left
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P (I ∪ J)) U = (P I) S

case right
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P (I ∪ J)) U = (P J) T

Proof state:
case right
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P (I ∪ J)) U = (P J) T

Tactic:
have h_eq_union : cylinder J T = cylinder (I ∪ J) U := by
  rw [← inter_cylinder, h_eq, inter_self]

Result:
case right
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
h_eq_union : cylinder J T = cylinder (I ∪ J) U
⊢ (P (I ∪ J)) U = (P J) T

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P I) S = (P J) T

Tactic:
suffices P (I ∪ J) U = P I S ∧ P (I ∪ J) U = P J T from this.1.symm.trans this.2

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P (I ∪ J)) U = (P I) S ∧ (P (I ∪ J)) U = (P J) T

Proof state:
case left
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
h_eq_union : cylinder I S = cylinder (I ∪ J) U
⊢ (P (I ∪ J)) U = (P I) S

Tactic:
exact hP.congr_cylinder_of_subset hS h_eq_union.symm Finset.subset_union_left

Result:
no goals

Proof state:
case left
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P (I ∪ J)) U = (P I) S

Tactic:
have h_eq_union : cylinder I S = cylinder (I ∪ J) U := by
  rw [← inter_cylinder, h_eq, inter_self]

Result:
case left
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
h_eq_union : cylinder I S = cylinder (I ∪ J) U
⊢ (P (I ∪ J)) U = (P I) S

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
⊢ (P I) S = (P J) T

Tactic:
let U := Finset.restrict₂ Finset.subset_union_left ⁻¹' S ∩
    Finset.restrict₂ Finset.subset_union_right ⁻¹' T

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ (P I) S = (P J) T

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
⊢ cylinder J T = cylinder (I ∪ J) U

Tactic:
rw [← inter_cylinder, h_eq, inter_self]

Result:
no goals

Proof state:
case right
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : { x // x ∈ I }) → α ↑i)
T : Set ((i : { x // x ∈ J }) → α ↑i)
hS : MeasurableSet S
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
U : Set ((i : { x // x ∈ I ∪ J }) → α ↑i) := Finset.restrict₂ ⋯ ⁻¹' S ∩ Finset.restrict₂ ⋯ ⁻¹' T
h_eq_union : cylinder J T = cylinder (I ∪ J) U
⊢ (P (I ∪ J)) U = (P J) T

Tactic:
exact hP.congr_cylinder_of_subset hT h_eq_union.symm Finset.subset_union_right

Result:
no goals