[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
ι : Type u_1
M : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : AddCommMonoid M
inst✝³ : Algebra R A
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
b : Basis ι R M
h : Function.Bijective ↑(algebraMap R A)
c : R
x : M
⊢ ↑(RingEquiv.ofBijective (algebraMap R A) h) c • x = c • x
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : LinearIndependent R b
hc : LinearIndependent S c
⊢ LinearIndependent R fun p => b p.fst • c p.snd
[PROOFSTEP]
rw [linearIndependent_iff'] at hb hc 
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
⊢ LinearIndependent R fun p => b p.fst • c p.snd
[PROOFSTEP]
rw [linearIndependent_iff'']
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
⊢ ∀ (s : Finset (ι × ι')) (g : ι × ι' → R),
    (∀ (i : ι × ι'), ¬i ∈ s → g i = 0) → ∑ i in s, g i • b i.fst • c i.snd = 0 → ∀ (i : ι × ι'), g i = 0
[PROOFSTEP]
rintro s g hg hsg ⟨i, k⟩
[GOAL]
case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
⊢ g (i, k) = 0
[PROOFSTEP]
by_cases hik : (i, k) ∈ s
[GOAL]
case pos
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
⊢ g (i, k) = 0
[PROOFSTEP]
have h1 : ∑ i in s.image Prod.fst ×ˢ s.image Prod.snd, g i • b i.1 • c i.2 = 0 :=
  by
  rw [← hsg]
  exact
    (Finset.sum_subset Finset.subset_product fun p _ hp => show g p • b p.1 • c p.2 = 0 by rw [hg p hp, zero_smul]).symm
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
⊢ ∑ i in Finset.image Prod.fst s ×ˢ Finset.image Prod.snd s, g i • b i.fst • c i.snd = 0
[PROOFSTEP]
rw [← hsg]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
⊢ ∑ i in Finset.image Prod.fst s ×ˢ Finset.image Prod.snd s, g i • b i.fst • c i.snd = ∑ i in s, g i • b i.fst • c i.snd
[PROOFSTEP]
exact
  (Finset.sum_subset Finset.subset_product fun p _ hp => show g p • b p.1 • c p.2 = 0 by rw [hg p hp, zero_smul]).symm
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
p : ι × ι'
x✝ : p ∈ Finset.image Prod.fst s ×ˢ Finset.image Prod.snd s
hp : ¬p ∈ s
⊢ g p • b p.fst • c p.snd = 0
[PROOFSTEP]
rw [hg p hp, zero_smul]
[GOAL]
case pos
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
h1 : ∑ i in Finset.image Prod.fst s ×ˢ Finset.image Prod.snd s, g i • b i.fst • c i.snd = 0
⊢ g (i, k) = 0
[PROOFSTEP]
rw [Finset.sum_product_right] at h1 
[GOAL]
case pos
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
h1 : ∑ y in Finset.image Prod.snd s, ∑ x in Finset.image Prod.fst s, g (x, y) • b (x, y).fst • c (x, y).snd = 0
⊢ g (i, k) = 0
[PROOFSTEP]
simp_rw [← smul_assoc, ← Finset.sum_smul] at h1 
[GOAL]
case pos
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : (i, k) ∈ s
h1 : ∑ x in Finset.image Prod.snd s, (∑ i in Finset.image Prod.fst s, g (i, x) • b i) • c x = 0
⊢ g (i, k) = 0
[PROOFSTEP]
exact hb _ _ (hc _ _ h1 k (Finset.mem_image_of_mem _ hik)) i (Finset.mem_image_of_mem _ hik)
[GOAL]
case neg
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
b : ι → S
ι' : Type w₁
c : ι' → A
hb : ∀ (s : Finset ι) (g : ι → R), ∑ i in s, g i • b i = 0 → ∀ (i : ι), i ∈ s → g i = 0
hc : ∀ (s : Finset ι') (g : ι' → S), ∑ i in s, g i • c i = 0 → ∀ (i : ι'), i ∈ s → g i = 0
s : Finset (ι × ι')
g : ι × ι' → R
hg : ∀ (i : ι × ι'), ¬i ∈ s → g i = 0
hsg : ∑ i in s, g i • b i.fst • c i.snd = 0
i : ι
k : ι'
hik : ¬(i, k) ∈ s
⊢ g (i, k) = 0
[PROOFSTEP]
exact hg _ hik
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι × ι'
⊢ ↑(↑(smul b c).repr x) ij = ↑(↑b.repr (↑(↑c.repr x) ij.snd)) ij.fst
[PROOFSTEP]
simp [Basis.smul]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
⊢ ↑(smul b c) ij = ↑b ij.fst • ↑c ij.snd
[PROOFSTEP]
obtain ⟨i, j⟩ := ij
[GOAL]
case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
⊢ ↑(smul b c) (i, j) = ↑b (i, j).fst • ↑c (i, j).snd
[PROOFSTEP]
rw [Basis.apply_eq_iff]
[GOAL]
case mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
⊢ ↑(smul b c).repr (↑b (i, j).fst • ↑c (i, j).snd) = single (i, j) 1
[PROOFSTEP]
ext ⟨i', j'⟩
[GOAL]
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑(smul b c).repr (↑b (i, j).fst • ↑c (i, j).snd)) (i', j') = ↑(single (i, j) 1) (i', j')
[PROOFSTEP]
rw [Basis.smul_repr, LinearEquiv.map_smul, Basis.repr_self, Finsupp.smul_apply, Finsupp.single_apply]
[GOAL]
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑b.repr (↑b (i, j).fst • if (i, j).snd = (i', j').snd then 1 else 0)) (i', j').fst = ↑(single (i, j) 1) (i', j')
[PROOFSTEP]
dsimp only
[GOAL]
case mk.h.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ ↑(↑b.repr (↑b i • if j = j' then 1 else 0)) i' = ↑(single (i, j) 1) (i', j')
[PROOFSTEP]
split_ifs with hi
[GOAL]
case pos
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ ↑(↑b.repr (↑b i • 1)) i' = ↑(single (i, j) 1) (i', j')
[PROOFSTEP]
simp [hi, Finsupp.single_apply]
[GOAL]
case neg
R : Type u
S : Type v
A : Type w
B : Type u₁
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Algebra R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type v₁
ι' : Type w₁
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ ↑(↑b.repr (↑b i • 0)) i' = ↑(single (i, j) 1) (i', j')
[PROOFSTEP]
simp [hi]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
src✝ : Algebra B D := RingHom.toAlgebra ↑(restrictDomain B f)
⊢ OneHom.toFun (↑↑↑f) 1 = 1
[PROOFSTEP]
simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, map_one]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
src✝ : Algebra B D := RingHom.toAlgebra ↑(restrictDomain B f)
⊢ ∀ (x y : C),
    OneHom.toFun { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) } (x * y) =
      OneHom.toFun { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) } x *
        OneHom.toFun { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) } y
[PROOFSTEP]
simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, map_mul,
  MonoidHom.coe_coe, RingHom.coe_coe, forall_const]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
src✝ : Algebra B D := RingHom.toAlgebra ↑(restrictDomain B f)
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) },
          map_mul' := (_ : ∀ (a a_1 : C), ↑↑↑f (a * a_1) = ↑f a * ↑f a_1) })
      0 =
    0
[PROOFSTEP]
simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe,
  map_zero]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
src✝ : Algebra B D := RingHom.toAlgebra ↑(restrictDomain B f)
⊢ ∀ (x y : C),
    OneHom.toFun
        (↑{ toOneHom := { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) },
            map_mul' := (_ : ∀ (a a_1 : C), ↑↑↑f (a * a_1) = ↑f a * ↑f a_1) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) },
              map_mul' := (_ : ∀ (a a_1 : C), ↑↑↑f (a * a_1) = ↑f a * ↑f a_1) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := f.toFun, map_one' := (_ : ↑↑↑↑f 1 = 1) },
              map_mul' := (_ : ∀ (a a_1 : C), ↑↑↑f (a * a_1) = ↑f a * ↑f a_1) })
          y
[PROOFSTEP]
simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe,
  map_add, RingHom.coe_coe, forall_const]
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f✝ : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : C →ₐ[A] D
⊢ (fun fg =>
        let x := RingHom.toAlgebra ↑fg.fst;
        AlgHom.restrictScalars A fg.snd)
      ((fun f => { fst := AlgHom.restrictDomain B f, snd := AlgHom.extendScalars B f }) f) =
    f
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f✝ : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : C →ₐ[A] D
⊢ AlgHom.restrictScalars A (AlgHom.extendScalars B f) = f
[PROOFSTEP]
ext
[GOAL]
case H
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f✝ : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : C →ₐ[A] D
x✝ : C
⊢ ↑(AlgHom.restrictScalars A (AlgHom.extendScalars B f)) x✝ = ↑f x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
⊢ Function.RightInverse
    (fun fg =>
      let x := RingHom.toAlgebra ↑fg.fst;
      AlgHom.restrictScalars A fg.snd)
    fun f => { fst := AlgHom.restrictDomain B f, snd := AlgHom.extendScalars B f }
[PROOFSTEP]
rintro ⟨⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩, ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, hg⟩⟩
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f✝ : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } x * OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
commutes'✝ :
  ∀ (r : A),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap A B) r) =
      ↑(algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    OneHom.toFun { toFun := g, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := g, map_one' := map_one'✝ } x * OneHom.toFun { toFun := g, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : C),
    OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
hg :
  ∀ (r : B),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap B C) r) =
      ↑(algebraMap B D) r
⊢ (fun f => { fst := AlgHom.restrictDomain B f, snd := AlgHom.extendScalars B f })
      ((fun fg =>
          let x := RingHom.toAlgebra ↑fg.fst;
          AlgHom.restrictScalars A fg.snd)
        {
          fst :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                  map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
              commutes' := commutes'✝ },
          snd :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
                  map_zero' := map_zero'✝, map_add' := map_add'✝ },
              commutes' := hg } }) =
    {
      fst :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
          commutes' := commutes'✝ },
      snd :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ },
          commutes' := hg } }
[PROOFSTEP]
obtain rfl : f = fun x => g (algebraMap B C x) := by
  ext x
  exact (hg x).symm
[GOAL]
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f✝ : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } x * OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
commutes'✝ :
  ∀ (r : A),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap A B) r) =
      ↑(algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    OneHom.toFun { toFun := g, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := g, map_one' := map_one'✝ } x * OneHom.toFun { toFun := g, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : C),
    OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
hg :
  ∀ (r : B),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap B C) r) =
      ↑(algebraMap B D) r
⊢ f = fun x => g (↑(algebraMap B C) x)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f✝ : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f : B → D
map_one'✝¹ : f 1 = 1
map_mul'✝¹ :
  ∀ (x y : B),
    OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } x * OneHom.toFun { toFun := f, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : B),
    OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
commutes'✝ :
  ∀ (r : A),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap A B) r) =
      ↑(algebraMap A D) r
g : C → D
map_one'✝ : g 1 = 1
map_mul'✝ :
  ∀ (x y : C),
    OneHom.toFun { toFun := g, map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := g, map_one' := map_one'✝ } x * OneHom.toFun { toFun := g, map_one' := map_one'✝ } y
map_zero'✝ : OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 = 0
map_add'✝ :
  ∀ (x y : C),
    OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) y
hg :
  ∀ (r : B),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝ }, map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap B C) r) =
      ↑(algebraMap B D) r
x : B
⊢ f x = g (↑(algebraMap B C) x)
[PROOFSTEP]
exact (hg x).symm
[GOAL]
case mk.mk.mk.mk.mk.mk.mk.mk.mk
R : Type u
S : Type v
A : Type w
B : Type u₁
C : Type u_1
D : Type u_2
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
f : C →ₐ[A] D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
g : C → D
map_one'✝¹ : g 1 = 1
map_mul'✝¹ :
  ∀ (x y : C),
    OneHom.toFun { toFun := g, map_one' := map_one'✝¹ } (x * y) =
      OneHom.toFun { toFun := g, map_one' := map_one'✝¹ } x * OneHom.toFun { toFun := g, map_one' := map_one'✝¹ } y
map_zero'✝¹ : OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) 0 = 0
map_add'✝¹ :
  ∀ (x y : C),
    OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) (x + y) =
      OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) x +
        OneHom.toFun (↑{ toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ }) y
map_one'✝ : (fun x => g (↑(algebraMap B C) x)) 1 = 1
map_mul'✝ :
  ∀ (x y : B),
    OneHom.toFun { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ } (x * y) =
      OneHom.toFun { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ } x *
        OneHom.toFun { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ } y
map_zero'✝ :
  OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ }, map_mul' := map_mul'✝ }) 0 =
    0
map_add'✝ :
  ∀ (x y : B),
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ }, map_mul' := map_mul'✝ })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ }, map_mul' := map_mul'✝ })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ }, map_mul' := map_mul'✝ })
          y
commutes'✝ :
  ∀ (r : A),
    OneHom.toFun
        (↑↑{
              toMonoidHom :=
                { toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ },
                  map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ })
        (↑(algebraMap A B) r) =
      ↑(algebraMap A D) r
hg :
  ∀ (r : B),
    OneHom.toFun
        (↑↑{ toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ })
        (↑(algebraMap B C) r) =
      ↑(algebraMap B D) r
⊢ (fun f => { fst := AlgHom.restrictDomain B f, snd := AlgHom.extendScalars B f })
      ((fun fg =>
          let x := RingHom.toAlgebra ↑fg.fst;
          AlgHom.restrictScalars A fg.snd)
        {
          fst :=
            {
              toRingHom :=
                {
                  toMonoidHom :=
                    { toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ },
                      map_mul' := map_mul'✝ },
                  map_zero' := map_zero'✝, map_add' := map_add'✝ },
              commutes' := commutes'✝ },
          snd :=
            {
              toRingHom :=
                { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
                  map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
              commutes' := hg } }) =
    {
      fst :=
        {
          toRingHom :=
            {
              toMonoidHom :=
                { toOneHom := { toFun := fun x => g (↑(algebraMap B C) x), map_one' := map_one'✝ },
                  map_mul' := map_mul'✝ },
              map_zero' := map_zero'✝, map_add' := map_add'✝ },
          commutes' := commutes'✝ },
      snd :=
        {
          toRingHom :=
            { toMonoidHom := { toOneHom := { toFun := g, map_one' := map_one'✝¹ }, map_mul' := map_mul'✝¹ },
              map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ },
          commutes' := hg } }
[PROOFSTEP]
rfl
