-- Mathlib/Data/Set/Sigma.lean
theorem image_sigmaMk_preimage_sigmaMap {β : ι' → Type*} {f : ι → ι'} (hf : Function.Injective f)
    (g : ∀ i, α i → β (f i)) (i : ι) (s : Set (β (f i))) :
    Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) ⊆ Sigma.mk i '' (g i ⁻¹' s)

Tactic:
rintro ⟨j, x⟩ ⟨y, hys, hxy⟩

Result:
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : ⟨f i, y⟩ = Sigma.map f g ⟨j, x⟩
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Proof state:
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
y : β (f i)
hys : y ∈ s
x : α i
hxy : y = g i x
⊢ ⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Tactic:
subst y

Result:
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
x : α i
hys : g i x ∈ s
⊢ ⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Proof state:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.mk i '' (g i ⁻¹' s) = Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s)

Tactic:
refine (image_sigmaMk_preimage_sigmaMap_subset f g i s).antisymm ?_

Result:
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
⊢ Sigma.map f g ⁻¹' (Sigma.mk (f i) '' s) ⊆ Sigma.mk i '' (g i ⁻¹' s)

Proof state:
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : i = j ∧ HEq y (g j x)
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Tactic:
rcases hxy with ⟨rfl, hxy⟩

Result:
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
y : β (f i)
hys : y ∈ s
x : α i
hxy : HEq y (g i x)
⊢ ⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Proof state:
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : ⟨f i, y⟩ = Sigma.map f g ⟨j, x⟩
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Tactic:
simp only [hf.eq_iff, Sigma.map, Sigma.ext_iff] at hxy

Result:
case mk.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
j : ι
x : α j
y : β (f i)
hys : y ∈ s
hxy : i = j ∧ HEq y (g j x)
⊢ ⟨j, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Proof state:
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
x : α i
hys : g i x ∈ s
⊢ ⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Tactic:
exact ⟨x, hys, rfl⟩

Result:
no goals

Proof state:
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
y : β (f i)
hys : y ∈ s
x : α i
hxy : HEq y (g i x)
⊢ ⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)

Tactic:
rw [heq_iff_eq] at hxy

Result:
case mk.intro.intro.intro
ι : Type u_1
ι' : Type u_2
α : ι → Type u_3
β : ι' → Type u_4
f : ι → ι'
hf : Function.Injective f
g : (i : ι) → α i → β (f i)
i : ι
s : Set (β (f i))
y : β (f i)
hys : y ∈ s
x : α i
hxy : y = g i x
⊢ ⟨i, x⟩ ∈ Sigma.mk i '' (g i ⁻¹' s)