[GOAL]
a₀ a₁ a₂ : Type u
i : ℕ
⊢ lift #(Sequence₂ a₀ a₁ a₂ i) = #(Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) i)
[PROOFSTEP]
rcases i with (_ | _ | _ | i)
[GOAL]
case zero
a₀ a₁ a₂ : Type u
⊢ lift #(Sequence₂ a₀ a₁ a₂ Nat.zero) = #(Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) Nat.zero)
[PROOFSTEP]
simp only [Sequence₂, mk_uLift, mk_fintype, Fintype.card_of_isEmpty, Nat.cast_zero, lift_zero]
[GOAL]
case succ.zero
a₀ a₁ a₂ : Type u
⊢ lift #(Sequence₂ a₀ a₁ a₂ (Nat.succ Nat.zero)) = #(Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) (Nat.succ Nat.zero))
[PROOFSTEP]
simp only [Sequence₂, mk_uLift, mk_fintype, Fintype.card_of_isEmpty, Nat.cast_zero, lift_zero]
[GOAL]
case succ.succ.zero
a₀ a₁ a₂ : Type u
⊢ lift #(Sequence₂ a₀ a₁ a₂ (Nat.succ (Nat.succ Nat.zero))) =
    #(Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) (Nat.succ (Nat.succ Nat.zero)))
[PROOFSTEP]
simp only [Sequence₂, mk_uLift, mk_fintype, Fintype.card_of_isEmpty, Nat.cast_zero, lift_zero]
[GOAL]
case succ.succ.succ
a₀ a₁ a₂ : Type u
i : ℕ
⊢ lift #(Sequence₂ a₀ a₁ a₂ (Nat.succ (Nat.succ (Nat.succ i)))) =
    #(Sequence₂ (ULift a₀) (ULift a₁) (ULift a₂) (Nat.succ (Nat.succ (Nat.succ i))))
[PROOFSTEP]
simp only [Sequence₂, mk_uLift, mk_fintype, Fintype.card_of_isEmpty, Nat.cast_zero, lift_zero]
[GOAL]
a₀ a₁ a₂ : Type u
⊢ (sum fun i => #(Sequence₂ a₀ a₁ a₂ i)) = #a₀ + #a₁ + #a₂
[PROOFSTEP]
rw [sum_nat_eq_add_sum_succ, sum_nat_eq_add_sum_succ, sum_nat_eq_add_sum_succ]
[GOAL]
a₀ a₁ a₂ : Type u
⊢ #(Sequence₂ a₀ a₁ a₂ 0) +
      (#(Sequence₂ a₀ a₁ a₂ (0 + 1)) +
        (#(Sequence₂ a₀ a₁ a₂ (0 + 1 + 1)) + sum fun i => #(Sequence₂ a₀ a₁ a₂ (i + 1 + 1 + 1)))) =
    #a₀ + #a₁ + #a₂
[PROOFSTEP]
simp [add_assoc, Sequence₂]
[GOAL]
L : Language
L' : Language
⊢ card L = (sum fun l => lift #(Functions L l)) + sum fun l => lift #(Relations L l)
[PROOFSTEP]
simp [card, Symbols]
[GOAL]
L : Language
L' : Language
⊢ card Language.empty = 0
[PROOFSTEP]
simp [card_eq_card_functions_add_card_relations]
[GOAL]
L : Language
L' : Language
⊢ IsEmpty (Symbols Language.empty)
[PROOFSTEP]
simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]
[GOAL]
L : Language
L' : Language
⊢ (∀ (a : ℕ), IsEmpty (Functions Language.empty a)) ∧ ∀ (a : ℕ), IsEmpty (Relations Language.empty a)
[PROOFSTEP]
exact ⟨fun _ => inferInstance, fun _ => inferInstance⟩
[GOAL]
L : Language
L' : Language
i : ℕ
⊢ #(Functions (Language.sum L L') i) = lift #(Functions L i) + lift #(Functions L' i)
[PROOFSTEP]
simp [Language.sum]
[GOAL]
L : Language
L' : Language
i : ℕ
⊢ #(Relations (Language.sum L L') i) = lift #(Relations L i) + lift #(Relations L' i)
[PROOFSTEP]
simp [Language.sum]
[GOAL]
L : Language
L' : Language
⊢ card (Language.sum L L') = lift (card L) + lift (card L')
[PROOFSTEP]
simp only [card_eq_card_functions_add_card_relations, card_functions_sum, card_relations_sum, sum_add_distrib',
  lift_add, lift_sum, lift_lift]
[GOAL]
L : Language
L' : Language
⊢ ((sum fun i => lift #(Functions L i)) + sum fun i => lift #(Functions L' i)) +
      ((sum fun i => lift #(Relations L i)) + sum fun i => lift #(Relations L' i)) =
    ((sum fun i => lift #(Functions L i)) + sum fun i => lift #(Relations L i)) +
      ((sum fun i => lift #(Functions L' i)) + sum fun i => lift #(Relations L' i))
[PROOFSTEP]
simp only [add_assoc, add_comm (Cardinal.sum fun i => (#(L'.Functions i)).lift)]
[GOAL]
L : Language
L' : Language
c f₁ f₂ : Type u
r₁ r₂ : Type v
⊢ card (Language.mk₂ c f₁ f₂ r₁ r₂) = lift #c + lift #f₁ + lift #f₂ + lift #r₁ + lift #r₂
[PROOFSTEP]
simp [card_eq_card_functions_add_card_relations, add_assoc]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f g : M →[L] N
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
g : M →[L] N
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h : (mk toFun✝).toFun = g.toFun
⊢ mk toFun✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toFun✝¹ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), toFun✝¹ (funMap f x) = funMap f (toFun✝¹ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝¹ ∘ x)
toFun✝ : M → N
map_fun'✝ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
h : (mk toFun✝¹).toFun = (mk toFun✝).toFun
⊢ mk toFun✝¹ = mk toFun✝
[PROOFSTEP]
cases h
[GOAL]
case mk.mk.refl
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toFun✝ : M → N
map_fun'✝¹ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
map_fun'✝ : ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), toFun✝ (funMap f x) = funMap f (toFun✝ ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r x → RelMap r (toFun✝ ∘ x)
⊢ mk toFun✝ = mk toFun✝
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : Functions L n✝
x✝ : Fin n✝ → M
⊢ (↑hnp ∘ ↑hmn) (funMap x✝¹ x✝) = funMap x✝¹ ((↑hnp ∘ ↑hmn) ∘ x✝)
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : Functions L n✝
x✝ : Fin n✝ → M
⊢ funMap x✝¹ (↑hnp ∘ ↑hmn ∘ x✝) = funMap x✝¹ ((↑hnp ∘ ↑hmn) ∘ x✝)
[PROOFSTEP]
rfl
  -- Porting note: should be done by autoparam?
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f g : M ↪[L] N
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
g : M ↪[L] N
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : (fun f => f.toFun) (mk toEmbedding✝) = (fun f => f.toFun) g
⊢ mk toEmbedding✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝¹ (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : (fun f => f.toFun) (mk toEmbedding✝¹) = (fun f => f.toFun) (mk toEmbedding✝)
⊢ mk toEmbedding✝¹ = mk toEmbedding✝
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEmbedding
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝¹ (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : (fun f => f.toFun) (mk toEmbedding✝¹) = (fun f => f.toFun) (mk toEmbedding✝)
⊢ toEmbedding✝¹ = toEmbedding✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.e_toEmbedding.h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝¹ (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : (fun f => f.toFun) (mk toEmbedding✝¹) = (fun f => f.toFun) (mk toEmbedding✝)
x : M
⊢ ↑toEmbedding✝¹ x = ↑toEmbedding✝ x
[PROOFSTEP]
exact Function.funext_iff.1 h x
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f g : M ↪[L] N
h : ↑f = ↑g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
g : M ↪[L] N
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : ↑(mk toEmbedding✝) = ↑g
⊢ mk toEmbedding✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝¹ (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : ↑(mk toEmbedding✝¹) = ↑(mk toEmbedding✝)
⊢ mk toEmbedding✝¹ = mk toEmbedding✝
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEmbedding
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝¹ (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : ↑(mk toEmbedding✝¹) = ↑(mk toEmbedding✝)
⊢ toEmbedding✝¹ = toEmbedding✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.e_toEmbedding.h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEmbedding✝¹ : M ↪ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝¹ (funMap f x) = funMap f (toEmbedding✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝¹.toFun ∘ x) ↔ RelMap r x
toEmbedding✝ : M ↪ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun toEmbedding✝ (funMap f x) = funMap f (toEmbedding✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEmbedding✝.toFun ∘ x) ↔ RelMap r x
h : ↑(mk toEmbedding✝¹) = ↑(mk toEmbedding✝)
x : M
⊢ ↑toEmbedding✝¹ x = ↑toEmbedding✝ x
[PROOFSTEP]
exact Function.funext_iff.1 h x
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝⁴ : Structure L M
inst✝³ : Structure L N
P : Type u_1
inst✝² : Structure L P
Q : Type u_2
inst✝¹ : Structure L Q
inst✝ : IsAlgebraic L
f : M →[L] N
hf : Function.Injective ↑f
⊢ toHom (ofInjective hf) = f
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝⁴ : Structure L M
inst✝³ : Structure L N
P : Type u_1
inst✝² : Structure L P
Q : Type u_2
inst✝¹ : Structure L Q
inst✝ : IsAlgebraic L
f : M →[L] N
hf : Function.Injective ↑f
x✝ : M
⊢ ↑(toHom (ofInjective hf)) x✝ = ↑f x✝
[PROOFSTEP]
simp
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Function.Embedding.toFun { toFun := ↑hnp ∘ ↑hmn, inj' := (_ : Function.Injective (↑hnp ∘ ↑hmn)) } (funMap f x) =
      funMap f ({ toFun := ↑hnp ∘ ↑hmn, inj' := (_ : Function.Injective (↑hnp ∘ ↑hmn)) }.toFun ∘ x)
[PROOFSTEP]
intros
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : Functions L n✝
x✝ : Fin n✝ → M
⊢ Function.Embedding.toFun { toFun := ↑hnp ∘ ↑hmn, inj' := (_ : Function.Injective (↑hnp ∘ ↑hmn)) } (funMap f✝ x✝) =
    funMap f✝ ({ toFun := ↑hnp ∘ ↑hmn, inj' := (_ : Function.Injective (↑hnp ∘ ↑hmn)) }.toFun ∘ x✝)
[PROOFSTEP]
simp only [Function.comp_apply, map_fun]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : Functions L n✝
x✝ : Fin n✝ → M
⊢ funMap f✝ (↑hnp ∘ ↑hmn ∘ x✝) = funMap f✝ ((↑hnp ∘ ↑hmn) ∘ x✝)
[PROOFSTEP]
trivial
  -- Porting note: should be done by autoparam?
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M),
    RelMap r ({ toFun := ↑hnp ∘ ↑hmn, inj' := (_ : Function.Injective (↑hnp ∘ ↑hmn)) }.toFun ∘ x) ↔ RelMap r x
[PROOFSTEP]
intros
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
r✝ : Relations L n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ({ toFun := ↑hnp ∘ ↑hmn, inj' := (_ : Function.Injective (↑hnp ∘ ↑hmn)) }.toFun ∘ x✝) ↔ RelMap r✝ x✝
[PROOFSTEP]
rw [Function.comp.assoc, map_rel, map_rel]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ toHom (comp hnp hmn) = Hom.comp (toHom hnp) (toHom hmn)
[PROOFSTEP]
ext
[GOAL]
case h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ↪[L] P
hmn : M ↪[L] N
x✝ : M
⊢ ↑(toHom (comp hnp hmn)) x✝ = ↑(Hom.comp (toHom hnp) (toHom hmn)) x✝
[PROOFSTEP]
simp only [coe_toHom, comp_apply, Hom.comp_apply]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f g : M ≃[L] N
h₁ : (fun f => f.toFun) f = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) f = (fun f => f.invFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
g : M ≃[L] N
toEquiv✝ : M ≃ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝ (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ : (fun f => f.toFun) (mk toEquiv✝) = (fun f => f.toFun) g
h₂ : (fun f => f.invFun) (mk toEquiv✝) = (fun f => f.invFun) g
⊢ mk toEquiv✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝¹ (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝ (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ : (fun f => f.toFun) (mk toEquiv✝¹) = (fun f => f.toFun) (mk toEquiv✝)
h₂ : (fun f => f.invFun) (mk toEquiv✝¹) = (fun f => f.invFun) (mk toEquiv✝)
⊢ mk toEquiv✝¹ = mk toEquiv✝
[PROOFSTEP]
simp only [mk.injEq]
[GOAL]
case mk.mk
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝¹ (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝ (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ : (fun f => f.toFun) (mk toEquiv✝¹) = (fun f => f.toFun) (mk toEquiv✝)
h₂ : (fun f => f.invFun) (mk toEquiv✝¹) = (fun f => f.invFun) (mk toEquiv✝)
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
ext x
[GOAL]
case mk.mk.H
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
toEquiv✝¹ : M ≃ N
map_fun'✝¹ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝¹ (funMap f x) = funMap f (toEquiv✝¹.toFun ∘ x)
map_rel'✝¹ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝¹.toFun ∘ x) ↔ RelMap r x
toEquiv✝ : M ≃ N
map_fun'✝ :
  ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M), Equiv.toFun toEquiv✝ (funMap f x) = funMap f (toEquiv✝.toFun ∘ x)
map_rel'✝ : ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M), RelMap r (toEquiv✝.toFun ∘ x) ↔ RelMap r x
h₁ : (fun f => f.toFun) (mk toEquiv✝¹) = (fun f => f.toFun) (mk toEquiv✝)
h₂ : (fun f => f.invFun) (mk toEquiv✝¹) = (fun f => f.invFun) (mk toEquiv✝)
x : M
⊢ ↑toEquiv✝¹ x = ↑toEquiv✝ x
[PROOFSTEP]
exact Function.funext_iff.1 h₁ x
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
f' : Functions L n
x : Fin n → N
⊢ Equiv.toFun
      { toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (funMap f' x) =
    funMap f'
      ({ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.toFun ∘
        x)
[PROOFSTEP]
simp only [Equiv.toFun_as_coe]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
f' : Functions L n
x : Fin n → N
⊢ ↑f.symm (funMap f' x) = funMap f' (↑f.symm ∘ x)
[PROOFSTEP]
rw [Equiv.symm_apply_eq]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
f' : Functions L n
x : Fin n → N
⊢ funMap f' x = ↑f.toEquiv (funMap f' (↑f.symm ∘ x))
[PROOFSTEP]
refine' Eq.trans _ (f.map_fun' f' (f.toEquiv.symm ∘ x)).symm
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
f' : Functions L n
x : Fin n → N
⊢ funMap f' x = funMap f' (f.toFun ∘ ↑f.symm ∘ x)
[PROOFSTEP]
rw [← Function.comp.assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.comp.left_id]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
r : Relations L n
x : Fin n → N
⊢ RelMap r
      ({ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.toFun ∘
        x) ↔
    RelMap r x
[PROOFSTEP]
simp only [Equiv.toFun_as_coe]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
r : Relations L n
x : Fin n → N
⊢ RelMap r (↑f.symm ∘ x) ↔ RelMap r x
[PROOFSTEP]
refine' (f.map_rel' r (f.toEquiv.symm ∘ x)).symm.trans _
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
f : M ≃[L] N
src✝ : N ≃ M := f.symm
n : ℕ
r : Relations L n
x : Fin n → N
⊢ RelMap r (f.toFun ∘ ↑f.symm ∘ x) ↔ RelMap r x
[PROOFSTEP]
rw [← Function.comp.assoc, Equiv.toFun_as_coe, Equiv.self_comp_symm, Function.comp.left_id]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
x : M
⊢ ↑(refl L M) x = x
[PROOFSTEP]
simp [refl]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
x : M
⊢ ↑(mk (_root_.Equiv.refl M)) x = x
[PROOFSTEP]
rfl
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ≃[L] P
hmn : M ≃[L] N
src✝ : M ≃ P := hmn.trans hnp.toEquiv
⊢ ∀ {n : ℕ} (f : Functions L n) (x : Fin n → M),
    Equiv.toFun
        { toFun := ↑hnp ∘ ↑hmn, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
          right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        (funMap f x) =
      funMap f
        ({ toFun := ↑hnp ∘ ↑hmn, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.toFun ∘
          x)
[PROOFSTEP]
intros
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ≃[L] P
hmn : M ≃[L] N
src✝ : M ≃ P := hmn.trans hnp.toEquiv
n✝ : ℕ
f✝ : Functions L n✝
x✝ : Fin n✝ → M
⊢ Equiv.toFun
      { toFun := ↑hnp ∘ ↑hmn, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (funMap f✝ x✝) =
    funMap f✝
      ({ toFun := ↑hnp ∘ ↑hmn, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.toFun ∘
        x✝)
[PROOFSTEP]
simp only [Function.comp_apply, map_fun]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ≃[L] P
hmn : M ≃[L] N
src✝ : M ≃ P := hmn.trans hnp.toEquiv
n✝ : ℕ
f✝ : Functions L n✝
x✝ : Fin n✝ → M
⊢ funMap f✝ (↑hnp ∘ ↑hmn ∘ x✝) = funMap f✝ ((↑hnp ∘ ↑hmn) ∘ x✝)
[PROOFSTEP]
trivial
  -- Porting note: should be done by autoparam?
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ≃[L] P
hmn : M ≃[L] N
src✝ : M ≃ P := hmn.trans hnp.toEquiv
⊢ ∀ {n : ℕ} (r : Relations L n) (x : Fin n → M),
    RelMap r
        ({ toFun := ↑hnp ∘ ↑hmn, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
              right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.toFun ∘
          x) ↔
      RelMap r x
[PROOFSTEP]
intros
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
hnp : N ≃[L] P
hmn : M ≃[L] N
src✝ : M ≃ P := hmn.trans hnp.toEquiv
n✝ : ℕ
r✝ : Relations L n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝
      ({ toFun := ↑hnp ∘ ↑hmn, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }.toFun ∘
        x✝) ↔
    RelMap r✝ x✝
[PROOFSTEP]
rw [Function.comp.assoc, map_rel, map_rel]
[GOAL]
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
a : Structure Language.empty M
⊢ a = default
[PROOFSTEP]
ext _ f
[GOAL]
case funMap.h.h.h
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
a : Structure Language.empty M
x✝¹ : ℕ
f : Functions Language.empty x✝¹
x✝ : Fin x✝¹ → M
⊢ funMap f x✝ = funMap f x✝
[PROOFSTEP]
exact Empty.elim f
[GOAL]
case RelMap.h.h.h.a
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : Structure L M
inst✝² : Structure L N
P : Type u_1
inst✝¹ : Structure L P
Q : Type u_2
inst✝ : Structure L Q
a : Structure Language.empty M
x✝¹ : ℕ
f : Relations Language.empty x✝¹
x✝ : Fin x✝¹ → M
⊢ RelMap f x✝ ↔ RelMap f x✝
[PROOFSTEP]
exact Empty.elim f
[GOAL]
L : Language
M : Type u_1
N : Type u_2
inst✝ : Structure L M
e : M ≃ N
⊢ M ≃[L] N
[PROOFSTEP]
letI : L.Structure N := inducedStructure e
[GOAL]
L : Language
M : Type u_1
N : Type u_2
inst✝ : Structure L M
e : M ≃ N
this : Structure L N := inducedStructure e
⊢ M ≃[L] N
[PROOFSTEP]
exact
  { e with
    map_fun' := @fun n f x => by simp [← Function.comp.assoc e.symm e x]
    map_rel' := @fun n r x => by simp [← Function.comp.assoc e.symm e x] }
[GOAL]
L : Language
M : Type u_1
N : Type u_2
inst✝ : Structure L M
e : M ≃ N
this : Structure L N := inducedStructure e
n : ℕ
f : Functions L n
x : Fin n → M
⊢ toFun
      { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
        right_inv := (_ : Function.RightInverse e.invFun e.toFun) }
      (funMap f x) =
    funMap f
      ({ toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
            right_inv := (_ : Function.RightInverse e.invFun e.toFun) }.toFun ∘
        x)
[PROOFSTEP]
simp [← Function.comp.assoc e.symm e x]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
inst✝ : Structure L M
e : M ≃ N
this : Structure L N := inducedStructure e
n : ℕ
r : Relations L n
x : Fin n → M
⊢ RelMap r
      ({ toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
            right_inv := (_ : Function.RightInverse e.invFun e.toFun) }.toFun ∘
        x) ↔
    RelMap r x
[PROOFSTEP]
simp [← Function.comp.assoc e.symm e x]
[GOAL]
L : Language
M : Type u_1
N : Type u_2
inst✝ : Structure L M
e : M ≃ N
⊢ (a : N) → (fun x => M) a
[PROOFSTEP]
letI : L.Structure N := inducedStructure e
[GOAL]
L : Language
M : Type u_1
N : Type u_2
inst✝ : Structure L M
e : M ≃ N
this : Structure L N := inducedStructure e
⊢ (a : N) → (fun x => M) a
[PROOFSTEP]
exact FunLike.coe (@inducedStructureEquiv L M N _ e).symm
