-- Mathlib/ModelTheory/Basic.lean
theorem coe_injective : @Function.Injective (M ↪[L] N) (M → N) (↑)
  | f, g, h => by
    cases f
    cases g
    congr
    ext x
    exact funext_iff.1 h x

Proof state:
case mk.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
⊢ { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }

Tactic:
congr

Result:
case mk.mk.e_toEmbedding
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
⊢ toEmbedding✝¹ = toEmbedding✝

Proof state:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ↪[L] N
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = ⇑g
⊢ { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g

Tactic:
cases g

Result:
case mk.mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
⊢ { toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ↪[L] N
h : ⇑f = ⇑g
⊢ f = g

Tactic:
cases f

Result:
case mk
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ↪[L] N
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = ⇑g
⊢ { toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ } = g

Proof state:
case mk.mk.e_toEmbedding
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
⊢ toEmbedding✝¹ = toEmbedding✝

Tactic:
ext x

Result:
case mk.mk.e_toEmbedding.h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
x : M
⊢ toEmbedding✝¹ x = toEmbedding✝ x

Proof state:
case mk.mk.e_toEmbedding.h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝¹.toFun (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), toEmbedding✝.toFun (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h :
  ⇑{ toEmbedding := toEmbedding✝¹, map_fun' := map_fun'✝¹, map_rel' := map_rel'✝¹ } =
    ⇑{ toEmbedding := toEmbedding✝, map_fun' := map_fun'✝, map_rel' := map_rel'✝ }
x : M
⊢ toEmbedding✝¹ x = toEmbedding✝ x

Tactic:
exact funext_iff.1 h x

Result:
no goals