[GOAL]
R : Type u_1
ι : Type u_2
n : ℕ
M : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : (i : Fin n) → AddCommMonoid (M i)
inst✝² : (i : Fin n) → Module R (M i)
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f g : MultilinearMap R M M₂
ι₁ : Fin n → Type u_6
e : (i : Fin n) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin n) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
⊢ f = g
[PROOFSTEP]
induction' n with m hm
[GOAL]
case zero
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
M : Fin Nat.zero → Type u_3
inst✝¹ : (i : Fin Nat.zero) → AddCommMonoid (M i)
inst✝ : (i : Fin Nat.zero) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin Nat.zero → Type u_6
e : (i : Fin Nat.zero) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin Nat.zero) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
⊢ f = g
[PROOFSTEP]
ext x
[GOAL]
case zero.H
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
M : Fin Nat.zero → Type u_3
inst✝¹ : (i : Fin Nat.zero) → AddCommMonoid (M i)
inst✝ : (i : Fin Nat.zero) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin Nat.zero → Type u_6
e : (i : Fin Nat.zero) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin Nat.zero) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
x : (i : Fin Nat.zero) → M i
⊢ ↑f x = ↑g x
[PROOFSTEP]
convert h finZeroElim
[GOAL]
case succ
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
⊢ f = g
[PROOFSTEP]
apply Function.LeftInverse.injective uncurry_curryLeft
[GOAL]
case succ.a
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
⊢ (fun x => curryLeft x) f = (fun x => curryLeft x) g
[PROOFSTEP]
refine' Basis.ext (e 0) _
[GOAL]
case succ.a
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
⊢ ∀ (i : ι₁ 0), ↑((fun x => curryLeft x) f) (↑(e 0) i) = ↑((fun x => curryLeft x) g) (↑(e 0) i)
[PROOFSTEP]
intro i
[GOAL]
case succ.a
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
⊢ ↑((fun x => curryLeft x) f) (↑(e 0) i) = ↑((fun x => curryLeft x) g) (↑(e 0) i)
[PROOFSTEP]
apply hm (Fin.tail e)
[GOAL]
case succ.a
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
⊢ ∀ (v : (i : Fin m) → ι₁ (Fin.succ i)),
    (↑(↑((fun x => curryLeft x) f) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (v i)) =
      ↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (v i)
[PROOFSTEP]
intro j
[GOAL]
case succ.a
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) f) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) =
    ↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)
[PROOFSTEP]
convert h (Fin.cons i j)
[GOAL]
case h.e'_2
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) f) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑f fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
iterate 2
  rw [curryLeft_apply]
  congr 1 with x
  refine' Fin.cases rfl (fun x => _) x
  dsimp [Fin.tail]
  rw [Fin.cons_succ, Fin.cons_succ]
[GOAL]
case h.e'_2
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) f) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑f fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
rw [curryLeft_apply]
[GOAL]
case h.e'_2
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ ↑f (Fin.cons (↑(e 0) i) fun i => ↑(Fin.tail e i) (j i)) = ↑f fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
congr 1 with x
[GOAL]
case h.e'_2.h.e_6.h.h
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
x : Fin (m + 1)
⊢ Fin.cons (↑(e 0) i) (fun i => ↑(Fin.tail e i) (j i)) x = ↑(e x) (Fin.cons i j x)
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
refine' Fin.cases rfl (fun x => _) x
[GOAL]
case h.e'_2.h.e_6.h.h
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
x✝ : Fin (m + 1)
x : Fin m
⊢ Fin.cons (↑(e 0) i) (fun i => ↑(Fin.tail e i) (j i)) (Fin.succ x) = ↑(e (Fin.succ x)) (Fin.cons i j (Fin.succ x))
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
dsimp [Fin.tail]
[GOAL]
case h.e'_2.h.e_6.h.h
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
x✝ : Fin (m + 1)
x : Fin m
⊢ Fin.cons (↑(e 0) i) (fun i => ↑(e (Fin.succ i)) (j i)) (Fin.succ x) = ↑(e (Fin.succ x)) (Fin.cons i j (Fin.succ x))
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_succ]
[GOAL]
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ (↑(↑((fun x => curryLeft x) g) (↑(e 0) i)) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
rw [curryLeft_apply]
[GOAL]
case h.e'_3
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
⊢ ↑g (Fin.cons (↑(e 0) i) fun i => ↑(Fin.tail e i) (j i)) = ↑g fun i_1 => ↑(e i_1) (Fin.cons i j i_1)
[PROOFSTEP]
congr 1 with x
[GOAL]
case h.e'_3.h.e_6.h.h
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
x : Fin (m + 1)
⊢ Fin.cons (↑(e 0) i) (fun i => ↑(Fin.tail e i) (j i)) x = ↑(e x) (Fin.cons i j x)
[PROOFSTEP]
refine' Fin.cases rfl (fun x => _) x
[GOAL]
case h.e'_3.h.e_6.h.h
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
x✝ : Fin (m + 1)
x : Fin m
⊢ Fin.cons (↑(e 0) i) (fun i => ↑(Fin.tail e i) (j i)) (Fin.succ x) = ↑(e (Fin.succ x)) (Fin.cons i j (Fin.succ x))
[PROOFSTEP]
dsimp [Fin.tail]
[GOAL]
case h.e'_3.h.e_6.h.h
R : Type u_1
ι : Type u_2
n : ℕ
M✝ : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : (i : Fin n) → AddCommMonoid (M✝ i)
inst✝⁴ : (i : Fin n) → Module R (M✝ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
f✝ g✝ : MultilinearMap R M✝ M₂
ι₁✝ : Fin n → Type u_6
e✝ : (i : Fin n) → Basis (ι₁✝ i) R (M✝ i)
h✝ : ∀ (v : (i : Fin n) → ι₁✝ i), (↑f✝ fun i => ↑(e✝ i) (v i)) = ↑g✝ fun i => ↑(e✝ i) (v i)
m : ℕ
hm :
  ∀ {M : Fin m → Type u_3} [inst : (i : Fin m) → AddCommMonoid (M i)] [inst_1 : (i : Fin m) → Module R (M i)]
    {f g : MultilinearMap R M M₂} {ι₁ : Fin m → Type u_6} (e : (i : Fin m) → Basis (ι₁ i) R (M i)),
    (∀ (v : (i : Fin m) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)) → f = g
M : Fin (Nat.succ m) → Type u_3
inst✝¹ : (i : Fin (Nat.succ m)) → AddCommMonoid (M i)
inst✝ : (i : Fin (Nat.succ m)) → Module R (M i)
f g : MultilinearMap R M M₂
ι₁ : Fin (Nat.succ m) → Type u_6
e : (i : Fin (Nat.succ m)) → Basis (ι₁ i) R (M i)
h : ∀ (v : (i : Fin (Nat.succ m)) → ι₁ i), (↑f fun i => ↑(e i) (v i)) = ↑g fun i => ↑(e i) (v i)
i : ι₁ 0
j : (i : Fin m) → ι₁ (Fin.succ i)
x✝ : Fin (m + 1)
x : Fin m
⊢ Fin.cons (↑(e 0) i) (fun i => ↑(e (Fin.succ i)) (j i)) (Fin.succ x) = ↑(e (Fin.succ x)) (Fin.cons i j (Fin.succ x))
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_succ]
[GOAL]
R : Type u_1
ι : Type u_2
n : ℕ
M : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : (i : Fin n) → AddCommMonoid (M i)
inst✝³ : (i : Fin n) → Module R (M i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Finite ι
f g : MultilinearMap R (fun x => M₂) M₃
ι₁ : Type u_6
e : Basis ι₁ R M₂
h : ∀ (v : ι → ι₁), (↑f fun i => ↑e (v i)) = ↑g fun i => ↑e (v i)
⊢ f = g
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
ι : Type u_2
n : ℕ
M : Fin n → Type u_3
M₂ : Type u_4
M₃ : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : (i : Fin n) → AddCommMonoid (M i)
inst✝³ : (i : Fin n) → Module R (M i)
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Finite ι
f g : MultilinearMap R (fun x => M₂) M₃
ι₁ : Type u_6
e : Basis ι₁ R M₂
h : ∀ (v : ι → ι₁), (↑f fun i => ↑e (v i)) = ↑g fun i => ↑e (v i)
val✝ : Fintype ι
⊢ f = g
[PROOFSTEP]
exact (domDomCongr_eq_iff (Fintype.equivFin ι) f g).mp (Basis.ext_multilinear_fin (fun _ => e) fun i => h (i ∘ _))


[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ ker (subToSupQuotient p p')
[PROOFSTEP]
rw [LinearMap.ker_comp, Submodule.ofLe, comap_codRestrict, ker_mkQ, map_comap_subtype]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (Submodule.subtype p) (p ⊓ p') ≤ comap (Submodule.subtype p) ((p ⊔ p') ⊓ p')
[PROOFSTEP]
exact comap_mono (inf_le_inf_right _ le_sup_left)
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ Function.Injective ↑(quotientInfToSupQuotient p p')
[PROOFSTEP]
rw [← ker_eq_bot, quotientInfToSupQuotient, ker_liftQ_eq_bot]
[GOAL]
case h'
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ker (subToSupQuotient p p') ≤ comap (Submodule.subtype p) (p ⊓ p')
[PROOFSTEP]
rw [ker_comp, ker_mkQ]
[GOAL]
case h'
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ comap (ofLe (_ : p ≤ p ⊔ p')) (comap (Submodule.subtype (p ⊔ p')) p') ≤ comap (Submodule.subtype p) (p ⊓ p')
[PROOFSTEP]
exact fun ⟨x, hx1⟩ hx2 =>
  ⟨hx1, hx2⟩
    -- Porting note: breaking up original definition of quotientInfEquivSupQuotient to avoid timing out
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ Function.Surjective ↑(quotientInfToSupQuotient p p')
[PROOFSTEP]
rw [← range_eq_top, quotientInfToSupQuotient, range_liftQ, eq_top_iff']
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
⊢ ∀ (x : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'), x ∈ range (subToSupQuotient p p')
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mk.mk
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
x : M
hx : x ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := x, property := hx } ∈ range (subToSupQuotient p p')
[PROOFSTEP]
rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩
[GOAL]
case mk.mk.intro.intro.intro.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ Quot.mk Setoid.r { val := y + z, property := hx } ∈ range (subToSupQuotient p p')
[PROOFSTEP]
use⟨y, hy⟩
[GOAL]
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(subToSupQuotient p p') { val := y, property := hy } = Quot.mk Setoid.r { val := y + z, property := hx }
[PROOFSTEP]
apply (Submodule.Quotient.eq _).2
[GOAL]
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x✝ : { x // x ∈ p ⊔ p' } ⧸ comap (Submodule.subtype (p ⊔ p')) p'
y : M
hy : y ∈ p
z : M
hz : z ∈ p'
hx : y + z ∈ p ⊔ p'
⊢ ↑(ofLe (_ : p ≤ p ⊔ p')) { val := y, property := hy } - { val := y + z, property := hx } ∈
    comap (Submodule.subtype (p ⊔ p')) p'
[PROOFSTEP]
simp only [mem_comap, map_sub, coeSubtype, coe_ofLe, sub_add_cancel', neg_mem_iff, hz]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x : { x // x ∈ p ⊔ p' }
hx : ↑x ∈ p
⊢ Submodule.Quotient.mk x = ↑(quotientInfEquivSupQuotient p p') (Submodule.Quotient.mk { val := ↑x, property := hx })
[PROOFSTEP]
rw [quotientInfEquivSupQuotient_apply_mk, ofLe_apply]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
p p' : Submodule R M
x : { x // x ∈ p ⊔ p' }
⊢ Submodule.Quotient.mk x = ↑(quotientInfEquivSupQuotient p p') 0 ↔ ↑x ∈ p'
[PROOFSTEP]
rw [_root_.map_zero, Quotient.mk_eq_zero, mem_comap, Submodule.coeSubtype]
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
⊢ map (mkQ S) T ≤ LinearMap.ker (mapQ S T LinearMap.id h)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ ↑(mkQ S) x ∈ LinearMap.ker (mapQ S T LinearMap.id h)
[PROOFSTEP]
rw [LinearMap.mem_ker, mkQ_apply, mapQ_apply]
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h✝ h : S ≤ T
x : M
hx : x ∈ ↑T
⊢ Quotient.mk (↑LinearMap.id x) = 0
[PROOFSTEP]
exact (Quotient.mk_eq_zero _).mpr hx
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
x : M
⊢ ↑(quotientQuotientEquivQuotientAux S T h) (Quotient.mk (Quotient.mk x)) = Quotient.mk x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
src✝ : (M ⧸ S) ⧸ map (mkQ S) T →ₗ[R] M ⧸ T := quotientQuotientEquivQuotientAux S T h
x✝¹ : (M ⧸ S) ⧸ map (mkQ S) T
x✝ : M ⧸ S
x : M
⊢ ↑(mapQ T (map (mkQ S) T) (mkQ S) (_ : T ≤ comap (mkQ S) (map (mkQ S) T)))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(quotientQuotientEquivQuotientAux S T h),
                map_add' :=
                  (_ :
                    ∀ (x y : (M ⧸ S) ⧸ map (mkQ S) T),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : (M ⧸ S) ⧸ map (mkQ S) T),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        (Quotient.mk'' (Quotient.mk'' x))) =
    Quotient.mk'' (Quotient.mk'' x)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
S T : Submodule R M
h : S ≤ T
src✝ : (M ⧸ S) ⧸ map (mkQ S) T →ₗ[R] M ⧸ T := quotientQuotientEquivQuotientAux S T h
x✝ : M ⧸ T
x : M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(quotientQuotientEquivQuotientAux S T h),
              map_add' :=
                (_ :
                  ∀ (x y : (M ⧸ S) ⧸ map (mkQ S) T),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : (M ⧸ S) ⧸ map (mkQ S) T),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(mapQ T (map (mkQ S) T) (mkQ S) (_ : T ≤ comap (mkQ S) (map (mkQ S) T))) (Quotient.mk'' x)) =
    Quotient.mk'' x
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R M₂
inst✝³ : Module R M₃
f : M →ₗ[R] M₂
S✝ T✝ : Submodule R M
h : S✝ ≤ T✝
S T : Submodule R M
hST : T ≤ S
inst✝² : DecidablePred fun x => x ∈ map (mkQ T) S
inst✝¹ : Fintype (M ⧸ S)
inst✝ : Fintype (M ⧸ T)
⊢ Fintype.card { x // x ∈ map (mkQ T) S } * Fintype.card (M ⧸ S) = Fintype.card (M ⧸ T)
[PROOFSTEP]
rw [Submodule.card_eq_card_quotient_mul_card (map T.mkQ S),
  Fintype.card_eq.mpr ⟨(quotientQuotientEquivQuotient T S hST).toEquiv⟩]