-- Mathlib/ModelTheory/Definability.lean
theorem Definable.image_comp_equiv {s : Set (β → M)} (h : A.Definable L s) (f : α ≃ β) :
    A.Definable L ((fun g : β → M => g ∘ f) '' s)

Proof state:
case h₂.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : α → M
a : α
⊢ (fun g => g ∘ ⇑f) ((fun g => g ∘ ⇑f.symm) i) a = i a

Tactic:
simp

Result:
no goals

Proof state:
case h₁
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : β → M
⊢ (fun g => g ∘ ⇑f.symm) ((fun g => g ∘ ⇑f) i) = i

Tactic:
ext b

Result:
case h₁.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : β → M
b : β
⊢ (fun g => g ∘ ⇑f.symm) ((fun g => g ∘ ⇑f) i) b = i b

Proof state:
case h₁.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : β → M
b : β
⊢ (fun g => g ∘ ⇑f.symm) ((fun g => g ∘ ⇑f) i) b = i b

Tactic:
simp only [Function.comp_apply, Equiv.apply_symm_apply]

Result:
no goals

Proof state:
case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : α → M
⊢ (fun g => g ∘ ⇑f) ((fun g => g ∘ ⇑f.symm) i) = i

Tactic:
ext a

Result:
case h₂.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : α → M
a : α
⊢ (fun g => g ∘ ⇑f) ((fun g => g ∘ ⇑f.symm) i) a = i a

Proof state:
case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.RightInverse (fun g => g ∘ ⇑f.symm) fun g => g ∘ ⇑f

Tactic:
intro i

Result:
case h₂
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : α → M
⊢ (fun g => g ∘ ⇑f) ((fun g => g ∘ ⇑f.symm) i) = i

Proof state:
case h₁
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.LeftInverse (fun g => g ∘ ⇑f.symm) fun g => g ∘ ⇑f

Tactic:
intro i

Result:
case h₁
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
i : β → M
⊢ (fun g => g ∘ ⇑f.symm) ((fun g => g ∘ ⇑f) i) = i

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ (fun g => g ∘ ⇑f.symm) ⁻¹' s = (fun g => g ∘ ⇑f) '' s

Tactic:
rw [image_eq_preimage_of_inverse]

Result:
case h₁
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable 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✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ Function.RightInverse (fun g => g ∘ ⇑f.symm) fun g => g ∘ ⇑f

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ A.Definable L ((fun g => g ∘ ⇑f) '' s)

Tactic:
refine (congr rfl ?_).mp (h.preimage_comp f.symm)

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
s : Set (β → M)
h : A.Definable L s
f : α ≃ β
⊢ (fun g => g ∘ ⇑f.symm) ⁻¹' s = (fun g => g ∘ ⇑f) '' s