M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ (fun g => g ∘ ↑f.symm) ⁻¹' s = (fun g => g ∘ ↑f) '' s
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Definable A L ((fun g => g ∘ ↑f) '' s)
refine' (congr rfl _).mp (h.preimage_comp f.symm)
case h₁
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Function.LeftInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f

case h₂
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Function.RightInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ (fun g => g ∘ ↑f.symm) ⁻¹' s = (fun g => g ∘ ↑f) '' s
rw [image_eq_preimage_of_inverse]
case h₁
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : β → M
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) = i
case h₁
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Function.LeftInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
intro i
case h₁.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : β → M
b : β
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) b = i b
case h₁
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : β → M
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) = i
ext b
no goals
case h₁.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : β → M
b : β
⊢ (fun g => g ∘ ↑f.symm) ((fun g => g ∘ ↑f) i) b = i b
simp only [Function.comp_apply, Equiv.apply_symm_apply]
case h₂
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : α → M
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) = i
case h₂
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
⊢ Function.RightInverse (fun g => g ∘ ↑f.symm) fun g => g ∘ ↑f
intro i
case h₂.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : α → M
a : α
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) a = i a
case h₂
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : α → M
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) = i
ext a
no goals
case h₂.h
M : Type w
A : Set M
L : Language
inst✝ : Structure L M
α : Type u₁
β : Type u_1
B : Set M
s✝ : Set (α → M)
s : Set (β → M)
h : Definable A L s
f : α ≃ β
i : α → M
a : α
⊢ (fun g => g ∘ ↑f) ((fun g => g ∘ ↑f.symm) i) a = i a
simp