[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


[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ Linear k (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ AddCommGroup (CoeSort.coe V)
[PROOFSTEP]
change AddCommGroup ((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ AddCommGroup ↑((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ Module k (CoeSort.coe V)
[PROOFSTEP]
change Module k ((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ Module k ↑((forget₂ (FdRep k G) (FGModuleCat k)).obj V).obj
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ FiniteDimensional k (CoeSort.coe V)
[PROOFSTEP]
change FiniteDimensional k ((forget₂ (FdRep k G) (FGModuleCat k)).obj V)
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ FiniteDimensional k ↑((forget₂ (FdRep k G) (FGModuleCat k)).obj V)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ↑(ρ W) g = ↑(LinearEquiv.conj (isoToLinearEquiv i)) (↑(ρ V) g)
[PROOFSTEP]
erw [FdRep.isoToLinearEquiv, ← FGModuleCat.Iso.conj_eq_conj, Iso.conj_apply]
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ↑(ρ W) g =
    ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).inv ≫
      ↑(ρ V) g ≫ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom
[PROOFSTEP]
rw [Iso.eq_inv_comp ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)]
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V W : FdRep k G
i : V ≅ W
g : G
⊢ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom ≫ ↑(ρ W) g =
    ↑(ρ V) g ≫ ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i).hom
[PROOFSTEP]
exact (i.hom.comm g).symm
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
⊢ Rep.ρ ((forget₂ (FdRep k G) (Rep k G)).obj V) = ρ V
[PROOFSTEP]
ext g v
[GOAL]
case h.h
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
V : FdRep k G
g : G
v : CoeSort.coe ((forget₂ (FdRep k G) (Rep k G)).obj V)
⊢ ↑(↑(Rep.ρ ((forget₂ (FdRep k G) (Rep k G)).obj V)) g) v = ↑(↑(ρ V) g) v
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalCategory (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalPreadditive (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ MonoidalLinear k (FdRep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
⊢ HasKernels (FdRep k G)
[PROOFSTEP]
infer_instance
  -- Verify that Schur's lemma applies out of the box.
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝ : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y
⊢ (fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => Action.Hom.mk f.hom,
                map_add' :=
                  (_ :
                    ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                      (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
            map_smul' :=
              (_ :
                ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                  AddHom.toFun
                      { toFun := fun f => Action.Hom.mk f.hom,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                              (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                      (x • x_1) =
                    AddHom.toFun
                      { toFun := fun f => Action.Hom.mk f.hom,
                        map_add' :=
                          (_ :
                            ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                              (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                      (x • x_1)) }.toAddHom
        x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝¹ : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y
x✝ : ↑((forget₂ (FdRep k G) (Rep k G)).obj X).V
⊢ ↑((fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom))
            (AddHom.toFun
              {
                  toAddHom :=
                    { toFun := fun f => Action.Hom.mk f.hom,
                      map_add' :=
                        (_ :
                          ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                            (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
                  map_smul' :=
                    (_ :
                      ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                        AddHom.toFun
                            { toFun := fun f => Action.Hom.mk f.hom,
                              map_add' :=
                                (_ :
                                  ∀
                                    (x x_2 :
                                      (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                    (fun f => Action.Hom.mk f.hom) (x + x_2) =
                                      (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                            (x • x_1) =
                          AddHom.toFun
                            { toFun := fun f => Action.Hom.mk f.hom,
                              map_add' :=
                                (_ :
                                  ∀
                                    (x x_2 :
                                      (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                    (fun f => Action.Hom.mk f.hom) (x + x_2) =
                                      (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                            (x • x_1)) }.toAddHom
              x✝¹)).hom
      x✝ =
    ↑x✝¹.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝ : X ⟶ Y
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := fun f => Action.Hom.mk f.hom,
              map_add' :=
                (_ :
                  ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                    (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
          map_smul' :=
            (_ :
              ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                AddHom.toFun
                    { toFun := fun f => Action.Hom.mk f.hom,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                            (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                    (x • x_1) =
                  AddHom.toFun
                    { toFun := fun f => Action.Hom.mk f.hom,
                      map_add' :=
                        (_ :
                          ∀ (x x_2 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                            (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                    (x • x_1)) }.toAddHom
      ((fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom)) x✝) =
    x✝
[PROOFSTEP]
ext
[GOAL]
case h.w
k G : Type u
inst✝¹ : Field k
inst✝ : Monoid G
X Y : FdRep k G
x✝¹ : X ⟶ Y
x✝ : (forget (FGModuleCat k)).obj X.V
⊢ ↑(AddHom.toFun
            {
                toAddHom :=
                  { toFun := fun f => Action.Hom.mk f.hom,
                    map_add' :=
                      (_ :
                        ∀ (x x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                          (fun f => Action.Hom.mk f.hom) (x + x_1) = (fun f => Action.Hom.mk f.hom) (x + x_1)) },
                map_smul' :=
                  (_ :
                    ∀ (x : k) (x_1 : (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                      AddHom.toFun
                          { toFun := fun f => Action.Hom.mk f.hom,
                            map_add' :=
                              (_ :
                                ∀
                                  (x x_2 :
                                    (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                  (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                          (x • x_1) =
                        AddHom.toFun
                          { toFun := fun f => Action.Hom.mk f.hom,
                            map_add' :=
                              (_ :
                                ∀
                                  (x x_2 :
                                    (forget₂ (FdRep k G) (Rep k G)).obj X ⟶ (forget₂ (FdRep k G) (Rep k G)).obj Y),
                                  (fun f => Action.Hom.mk f.hom) (x + x_2) = (fun f => Action.Hom.mk f.hom) (x + x_2)) }
                          (x • x_1)) }.toAddHom
            ((fun f => Action.Hom.mk ((forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom)) x✝¹)).hom
      x✝ =
    ↑x✝¹.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Group G
⊢ RightRigidCategory (FdRep k G)
[PROOFSTEP]
change RightRigidCategory (Action (FGModuleCat k) (GroupCat.of G))
[GOAL]
k G : Type u
inst✝¹ : Field k
inst✝ : Group G
⊢ RightRigidCategory (Action (FGModuleCat k) ((forget₂ GroupCat MonCat).obj (GroupCat.of G)))
[PROOFSTEP]
infer_instance
[GOAL]
k G V : Type u
inst✝⁴ : Field k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
ρV : Representation k G V
W : FdRep k G
⊢ of (dual ρV) ⊗ W ≅ of (linHom ρV (ρ W))
[PROOFSTEP]
refine Action.mkIso (dualTensorIsoLinHomAux ρV W) ?_
[GOAL]
k G V : Type u
inst✝⁴ : Field k
inst✝³ : Group G
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : FiniteDimensional k V
ρV : Representation k G V
W : FdRep k G
⊢ ∀ (g : ↑(MonCat.of G)),
    ↑(of (dual ρV) ⊗ W).ρ g ≫ (dualTensorIsoLinHomAux ρV W).hom =
      (dualTensorIsoLinHomAux ρV W).hom ≫ ↑(of (linHom ρV (ρ W))).ρ g
[PROOFSTEP]
convert dualTensorHom_comm ρV W.ρ