-- Mathlib/ModelTheory/Fraisse.lean
theorem IsUltrahomogeneous.extend_embedding (M_homog : L.IsUltrahomogeneous M) {S : Type*}
    [L.Structure S] (S_FG : FG L S) {T : Type*} [L.Structure T] [h : Nonempty (T ↪[L] M)]
    (f : S ↪[L] M) (g : S ↪[L] T) :
    ∃ f' : T ↪[L] M, f = f'.comp g

Proof state:
case h.h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
⊢ f x = (t.toEmbedding.comp s) x

Tactic:
have eq' := congr_fun (congr_arg DFunLike.coe eq) ⟨s x, Hom.mem_range.2 ⟨x, rfl⟩⟩

Result:
case h.h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : (f.comp s.equivRange.symm.toEmbedding) ⟨s x, ⋯⟩ = (t.toEmbedding.comp s.toHom.range.subtype) ⟨s x, ⋯⟩
⊢ f x = (t.toEmbedding.comp s) x

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
⊢ ∃ f', f = f'.comp g

Tactic:
let ⟨r⟩ := h

Result:
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
⊢ ∃ f', f = f'.comp g

Proof state:
case h.h.a.a
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ ↑((r.comp g).equivRange x) = ↑((r.comp g).equivRange (s.equivRange.symm ⟨s x, ⋯⟩))

Tactic:
simp only [Equiv.apply_symm_apply, Embedding.equivRange_apply, s]

Result:
no goals

Proof state:
case h.h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : (f.comp s.equivRange.symm.toEmbedding) ⟨s x, ⋯⟩ = (t.toEmbedding.comp s.toHom.range.subtype) ⟨s x, ⋯⟩
⊢ f x = (t.toEmbedding.comp s) x

Tactic:
simp only [Embedding.comp_apply, Hom.comp_apply,
  Equiv.coe_toHom, Embedding.coe_toHom, coe_subtype] at eq'

Result:
case h.h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ f x = (t.toEmbedding.comp s) x

Proof state:
case h.h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ f x = (t.toEmbedding.comp s) x

Tactic:
simp only [Embedding.comp_apply, ← eq', Equiv.coe_toEmbedding, EmbeddingLike.apply_eq_iff_eq]

Result:
case h.h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
x : S
eq' : f (s.equivRange.symm.toEmbedding ⟨s x, ⋯⟩) = t.toEmbedding (s x)
⊢ x = s.equivRange.symm ⟨s x, ⋯⟩

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
⊢ ∃ f', f = f'.comp g

Tactic:
let s := r.comp g

Result:
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
⊢ ∃ f', f = f'.comp g

Proof state:
case h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
⊢ f = (t.toEmbedding.comp r).comp g

Tactic:
change _ = t.toEmbedding.comp s

Result:
case h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
⊢ f = t.toEmbedding.comp s

Proof state:
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
⊢ ∃ f', f = f'.comp g

Tactic:
use t.toEmbedding.comp r

Result:
case h
L : Language
M : Type w
inst✝² : L.Structure M
M_homog : L.IsUltrahomogeneous M
S : Type u_1
inst✝¹ : L.Structure S
S_FG : Structure.FG L S
T : Type u_2
inst✝ : L.Structure T
h : Nonempty (T ↪[L] M)
f : S ↪[L] M
g : S ↪[L] T
r : T ↪[L] M
s : S ↪[L] M := r.comp g
t : M ≃[L] M
eq : f.comp s.equivRange.symm.toEmbedding = t.toEmbedding.comp s.toHom.range.subtype
⊢ f = (t.toEmbedding.comp r).comp g