Theorem: SciLean.bungeeDomain_preimage (SciLean/Core/Distribution/BungeeTest.lean)

State before:
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' bungeeDomain height = if x ∈ Icc 1 height then Icc 0 x else ∅
Tactic:
unfold bungeeDomain
State after:
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} = if x ∈ Icc 1 height then Icc 0 x else ∅

State before:
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x : R
⊢ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} = if x ∈ Icc 1 height then Icc 0 x else ∅
Tactic:
ext
State after:
case h
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x x✝ : R
⊢ x✝ ∈ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} ↔
    x✝ ∈ if x ∈ Icc 1 height then Icc 0 x else ∅

State before:
case h
R : Type u_1
inst✝⁵ : RealScalar R
W : Type ?u.9501
inst✝⁴ : SemiHilbert R W
X : Type ?u.9531
inst✝³ : SemiHilbert R X
Y : Type ?u.9555
inst✝² : SemiHilbert R Y
Z : Type ?u.9579
inst✝¹ : SemiHilbert R Z
inst✝ : MeasureSpace R
height x x✝ : R
⊢ x✝ ∈ (fun z => (x, z)) ⁻¹' {(x, z) | 1 ≤ x ∧ x ≤ height ∧ 0 ≤ z ∧ z ≤ x} ↔
    x✝ ∈ if x ∈ Icc 1 height then Icc 0 x else ∅
Tactic:
simp[and_assoc]
State after:
no goals