case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
⊢ F = G
cases' F with Ff Fr
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }
case mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
G : L →ᴸ L'
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = G.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = G.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = G
cases' G with Gf Gr
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ { onFunction := Ff, onRelation := Fr } = { onFunction := Gf, onRelation := Gr }
simp only [mk.injEq]
no goals
case mk.mk
L : Language
L' : Language
M : Type w
inst✝ : Structure L M
ϕ : L →ᴸ L'
L'' : Language
Ff : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Fr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
Gf : ⦃n : ℕ⦄ → Functions L n → Functions L' n
Gr : ⦃n : ℕ⦄ → Relations L n → Relations L' n
h_fun : { onFunction := Ff, onRelation := Fr }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr
exact And.intro h_fun h_rel