[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' F x' (cast (_ : E x = E x') b) = { proj := x, snd := b }
[PROOFSTEP]
subst h
[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
x : B
b : E x
⊢ mk' F x (cast (_ : E x = E x) b) = { proj := x, snd := b }
[PROOFSTEP]
rfl
[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
y y' : E b
⊢ mk' F b y = mk' F b y' ↔ y = y'
[PROOFSTEP]
simp [TotalSpace.ext_iff]
[GOAL]
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) = proj ⁻¹' {b}
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ range (mk b) ⊆ proj ⁻¹' {b}
[PROOFSTEP]
rintro _ ⟨x, rfl⟩
[GOAL]
case h₁.intro
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
x : E b
⊢ { proj := b, snd := x } ∈ proj ⁻¹' {b}
[PROOFSTEP]
rfl
[GOAL]
case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
b : B
⊢ proj ⁻¹' {b} ⊆ range (mk b)
[PROOFSTEP]
rintro ⟨_, x⟩ rfl
[GOAL]
case h₂.mk
B : Type u_1
F : Type u_2
E : B → Type u_3
proj✝ : B
x : E proj✝
⊢ { proj := proj✝, snd := x } ∈ range (mk { proj := proj✝, snd := x }.proj)
[PROOFSTEP]
exact ⟨x, rfl⟩
