[GOAL]
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ (J l R)ᵀ = -J l R
[PROOFSTEP]
rw [J, fromBlocks_transpose, ← neg_one_smul R (fromBlocks _ _ _ _ : Matrix (l ⊕ l) (l ⊕ l) R), fromBlocks_smul,
  Matrix.transpose_zero, Matrix.transpose_one, transpose_neg]
[GOAL]
l : Type u_1
R : Type u_2
inst✝¹ : DecidableEq l
inst✝ : CommRing R
⊢ fromBlocks 0 1 (-1ᵀ) 0 = fromBlocks (-1 • 0) (-1 • -1) (-1 • 1) (-1 • 0)
[PROOFSTEP]
simp [fromBlocks]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * J l R = -1
[PROOFSTEP]
rw [J, fromBlocks_multiply]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (0 * 0 + -1 * 1) (0 * -1 + -1 * 0) (1 * 0 + 0 * 1) (1 * -1 + 0 * 0) = -1
[PROOFSTEP]
simp only [Matrix.zero_mul, Matrix.neg_mul, zero_add, neg_zero, Matrix.one_mul, add_zero]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ fromBlocks (-1) 0 0 (-1) = -1
[PROOFSTEP]
rw [← neg_zero, ← Matrix.fromBlocks_neg, ← fromBlocks_one]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (J l R)⁻¹ = -J l R
[PROOFSTEP]
refine' Matrix.inv_eq_right_inv _
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ J l R * -J l R = 1
[PROOFSTEP]
rw [Matrix.mul_neg, J_squared]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ - -1 = 1
[PROOFSTEP]
exact neg_neg 1
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ det (J l R) * det (J l R) = 1
[PROOFSTEP]
rw [← det_mul, J_squared, ← one_smul R (-1 : Matrix _ _ R), smul_neg, ← neg_smul, det_smul, Fintype.card_sum, det_one,
  mul_one]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ (-1) ^ (Fintype.card l + Fintype.card l) = 1
[PROOFSTEP]
apply Even.neg_one_pow
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ Even (Fintype.card l + Fintype.card l)
[PROOFSTEP]
exact even_add_self _
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a ∈ {A | A * J l R * Aᵀ = J l R}
hb : b ∈ {A | A * J l R * Aᵀ = J l R}
⊢ a * b ∈ {A | A * J l R * Aᵀ = J l R}
[PROOFSTEP]
simp only [Set.mem_setOf_eq, transpose_mul] at *
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * b * J l R * (bᵀ * aᵀ) = J l R
[PROOFSTEP]
rw [← Matrix.mul_assoc, a.mul_assoc, a.mul_assoc, hb]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
a b : Matrix (l ⊕ l) (l ⊕ l) R
ha : a * J l R * aᵀ = J l R
hb : b * J l R * bᵀ = J l R
⊢ a * J l R * aᵀ = J l R
[PROOFSTEP]
exact ha
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : CommRing R
inst✝ : Fintype l
⊢ 1 ∈
    { carrier := {A | A * J l R * Aᵀ = J l R},
        mul_mem' :=
          (_ :
            ∀ {a b : Matrix (l ⊕ l) (l ⊕ l) R},
              a ∈ {A | A * J l R * Aᵀ = J l R} →
                b ∈ {A | A * J l R * Aᵀ = J l R} → a * b ∈ {A | A * J l R * Aᵀ = J l R}) }.carrier
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ symplecticGroup l R ↔ A * J l R * Aᵀ = J l R
[PROOFSTEP]
simp [symplecticGroup]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ J l R ∈ symplecticGroup l R
[PROOFSTEP]
rw [mem_iff, J, fromBlocks_multiply, fromBlocks_transpose, fromBlocks_multiply]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks ((0 * 0 + -1 * 1) * 0ᵀ + (0 * -1 + -1 * 0) * (-1)ᵀ) ((0 * 0 + -1 * 1) * 1ᵀ + (0 * -1 + -1 * 0) * 0ᵀ)
      ((1 * 0 + 0 * 1) * 0ᵀ + (1 * -1 + 0 * 0) * (-1)ᵀ) ((1 * 0 + 0 * 1) * 1ᵀ + (1 * -1 + 0 * 0) * 0ᵀ) =
    fromBlocks 0 (-1) 1 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A ∈ symplecticGroup l R
⊢ -A ∈ symplecticGroup l R
[PROOFSTEP]
rw [mem_iff] at h ⊢
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
h : A * J l R * Aᵀ = J l R
⊢ -A * J l R * (-A)ᵀ = J l R
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ IsUnit (det A)
[PROOFSTEP]
rw [isUnit_iff_exists_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ ∃ b, det A * b = 1
[PROOFSTEP]
use A.det
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ det A * det A = 1
[PROOFSTEP]
refine' (isUnit_det_J l R).mul_left_cancel _
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ det (J l R) * (det A * det A) = det (J l R) * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
rw [mem_iff] at hA
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
apply_fun det at hA
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : det (A * J l R * Aᵀ) = det (J l R)
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
simp only [det_mul, det_transpose] at hA
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : det A * det (J l R) * det A = det (J l R)
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
rw [mul_comm A.det, mul_assoc] at hA
[GOAL]
case h
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : det (J l R) * (det A * det A) = det (J l R)
⊢ det (J l R) * (det A * det A) = det (J l R)
[PROOFSTEP]
exact hA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ Aᵀ ∈ symplecticGroup l R
[PROOFSTEP]
rw [mem_iff] at hA ⊢
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * Aᵀᵀ = J l R
[PROOFSTEP]
rw [transpose_transpose]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
⊢ Aᵀ * J l R * A = J l R
[PROOFSTEP]
have huA := symplectic_det hA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
⊢ Aᵀ * J l R * A = J l R
[PROOFSTEP]
have huAT : IsUnit Aᵀ.det := by
  rw [Matrix.det_transpose]
  exact huA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det Aᵀ)
[PROOFSTEP]
rw [Matrix.det_transpose]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
⊢ IsUnit (det A)
[PROOFSTEP]
exact huA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ * J l R * A = J l R
[PROOFSTEP]
calc
  Aᵀ * J l R * A = (-Aᵀ) * (J l R)⁻¹ * A := by
    rw [J_inv]
    simp
  _ = (-Aᵀ) * (A * J l R * Aᵀ)⁻¹ * A := by rw [hA]
  _ = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A := by simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
  _ = -(J l R)⁻¹ := by rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
  _ = J l R := by simp [J_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ * J l R * A = -Aᵀ * (J l R)⁻¹ * A
[PROOFSTEP]
rw [J_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ Aᵀ * J l R * A = -Aᵀ * -J l R * A
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -Aᵀ * (J l R)⁻¹ * A = -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A
[PROOFSTEP]
rw [hA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -Aᵀ * (A * J l R * Aᵀ)⁻¹ * A = -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A
[PROOFSTEP]
simp only [Matrix.mul_inv_rev, Matrix.mul_assoc, Matrix.neg_mul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -(Aᵀ * (Aᵀ⁻¹ * (J l R)⁻¹)) * A⁻¹ * A = -(J l R)⁻¹
[PROOFSTEP]
rw [mul_nonsing_inv_cancel_left _ _ huAT, nonsing_inv_mul_cancel_right _ _ huA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A * J l R * Aᵀ = J l R
huA : IsUnit (det A)
huAT : IsUnit (det Aᵀ)
⊢ -(J l R)⁻¹ = J l R
[PROOFSTEP]
simp [J_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ ∈ symplecticGroup l R
⊢ A ∈ symplecticGroup l R
[PROOFSTEP]
simpa using transpose_mem hA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ symplecticGroup l R ↔ Aᵀ * J l R * A = J l R
[PROOFSTEP]
rw [← transpose_mem_iff, mem_iff, transpose_transpose]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -(J l R * Aᵀ * J l R * A) = -J l R * (Aᵀ * J l R * A)
[PROOFSTEP]
simp only [Matrix.mul_assoc, Matrix.neg_mul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
[PROOFSTEP]
rw [mem_iff'] at hA
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ * J l R * A = J l R
⊢ -J l R * (Aᵀ * J l R * A) = -J l R * J l R
[PROOFSTEP]
rw [hA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * J l R = -1 • (J l R * J l R)
[PROOFSTEP]
simp only [Matrix.neg_mul, neg_smul, one_smul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • (J l R * J l R) = -1 • -1
[PROOFSTEP]
rw [J_squared]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -1 • -1 = 1
[PROOFSTEP]
simp only [neg_smul_neg, one_smul]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
A : { x // x ∈ symplecticGroup l R }
⊢ ↑A⁻¹ = (↑A)⁻¹
[PROOFSTEP]
refine' (coe_inv A).trans (inv_eq_left_inv _).symm
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
A : { x // x ∈ symplecticGroup l R }
⊢ -J l R * (↑A)ᵀ * J l R * ↑A = 1
[PROOFSTEP]
simp [inv_left_mul_aux, coe_inv]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ A : Matrix (l ⊕ l) (l ⊕ l) R
hA : A ∈ symplecticGroup l R
⊢ -J l R * Aᵀ * J l R * A = 1
[PROOFSTEP]
simp only [Matrix.neg_mul, inv_left_mul_aux hA]
[GOAL]
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
src✝¹ : Inv { x // x ∈ symplecticGroup l R } := hasInv
src✝ : Monoid { x // x ∈ symplecticGroup l R } := Submonoid.toMonoid (symplecticGroup l R)
A : { x // x ∈ symplecticGroup l R }
⊢ A⁻¹ * A = 1
[PROOFSTEP]
apply Subtype.ext
[GOAL]
case a
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
src✝¹ : Inv { x // x ∈ symplecticGroup l R } := hasInv
src✝ : Monoid { x // x ∈ symplecticGroup l R } := Submonoid.toMonoid (symplecticGroup l R)
A : { x // x ∈ symplecticGroup l R }
⊢ ↑(A⁻¹ * A) = ↑1
[PROOFSTEP]
simp only [Submonoid.coe_one, Submonoid.coe_mul, Matrix.neg_mul, coe_inv]
[GOAL]
case a
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A✝ : Matrix (l ⊕ l) (l ⊕ l) R
src✝¹ : Inv { x // x ∈ symplecticGroup l R } := hasInv
src✝ : Monoid { x // x ∈ symplecticGroup l R } := Submonoid.toMonoid (symplecticGroup l R)
A : { x // x ∈ symplecticGroup l R }
⊢ -(J l R * (↑A)ᵀ * J l R * ↑A) = 1
[PROOFSTEP]
exact inv_left_mul_aux A.2


[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V = ↑n
⊢ finrank K V = n
[PROOFSTEP]
apply_fun toNat at h
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ↑toNat (Module.rank K V) = ↑toNat ↑n
⊢ finrank K V = n
[PROOFSTEP]
rw [toNat_cast] at h
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ↑toNat (Module.rank K V) = n
⊢ finrank K V = n
[PROOFSTEP]
exact_mod_cast h
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V ≤ ↑n
⊢ finrank K V ≤ n
[PROOFSTEP]
rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_cast] at h
[GOAL]
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V ≤ ↑n
⊢ Module.rank K V < ℵ₀
[PROOFSTEP]
exact h.trans_lt (nat_lt_aleph0 n)
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V ≤ ↑n
⊢ ↑n < ℵ₀
[PROOFSTEP]
exact nat_lt_aleph0 n
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V < ↑n
⊢ finrank K V < n
[PROOFSTEP]
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_cast] at h
[GOAL]
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V < ↑n
⊢ Module.rank K V < ℵ₀
[PROOFSTEP]
exact h.trans (nat_lt_aleph0 n)
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V < ↑n
⊢ ↑n < ℵ₀
[PROOFSTEP]
exact nat_lt_aleph0 n
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < Module.rank K V
[PROOFSTEP]
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_cast]
[GOAL]
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < ℵ₀
[PROOFSTEP]
exact nat_lt_aleph0 n
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ Module.rank K V < ℵ₀
[PROOFSTEP]
contrapose! h
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ finrank K V ≤ n
[PROOFSTEP]
rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ 0 ≤ n
[PROOFSTEP]
exact n.zero_le
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
h : 1 < finrank K V
⊢ 1 < Module.rank K V
[PROOFSTEP]
simpa using lt_rank_of_lt_finrank h
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
h : lift (Module.rank K V) ≤ lift (Module.rank K V₂)
h' : Module.rank K V₂ < ℵ₀
⊢ finrank K V ≤ finrank K V₂
[PROOFSTEP]
simpa only [toNat_lift] using toNat_le_of_le_of_lt_aleph0 (lift_lt_aleph0.mpr h') h
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
n : ℕ
hn : finrank K V = Nat.succ n
⊢ 0 < finrank (?m.108424 hn) V
[PROOFSTEP]
rw [hn]
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
n : ℕ
hn : finrank K V = Nat.succ n
⊢ 0 < Nat.succ n
[PROOFSTEP]
exact n.succ_pos
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
h : Subsingleton V
⊢ finrank K V = 0
[PROOFSTEP]
by_contra h0
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
h : Subsingleton V
h0 : ¬finrank K V = 0
⊢ False
[PROOFSTEP]
obtain ⟨x, y, hxy⟩ := nontrivial_of_finrank_pos (Nat.pos_of_ne_zero h0)
[GOAL]
case mk.intro.intro
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
h : Subsingleton V
h0 : ¬finrank K V = 0
x y : V
hxy : x ≠ y
⊢ False
[PROOFSTEP]
exact hxy (Subsingleton.elim _ _)
[GOAL]
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
ι : Type w
b : Finset ι
h : Basis { x // x ∈ b } K V
⊢ finrank K V = Finset.card b
[PROOFSTEP]
rw [finrank_eq_card_basis h, Fintype.card_coe]
[GOAL]
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
⊢ Module.rank K K = ↑1
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
n : ℕ
⊢ finrank K (Fin n → K) = n
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Set V), Basis (↑s) K V → ¬Set.Finite s
⊢ finrank K V = 0
[PROOFSTEP]
obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set K V).mp ‹_›
[GOAL]
case intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Set V), Basis (↑s) K V → ¬Set.Finite s
w✝ : Set V
b : Basis (↑w✝) K V
⊢ finrank K V = 0
[PROOFSTEP]
exact dif_neg fun rank_lt => h _ b (b.finite_index_of_rank_lt_aleph0 rank_lt)
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ Basis (↑↑(Set.Finite.toFinset hs)) K V
[PROOFSTEP]
convert b
[GOAL]
case h.e'_1.h.e'_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ ↑(Set.Finite.toFinset hs) = s
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ finrank R M = finrank R M₂
[PROOFSTEP]
unfold finrank
[GOAL]
K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ ↑toNat (Module.rank R M) = ↑toNat (Module.rank R M₂)
[PROOFSTEP]
rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : Injective ↑f
⊢ finrank K { x // x ∈ range f } = finrank K V
[PROOFSTEP]
rw [(LinearEquiv.ofInjective f hf).finrank_eq]
[GOAL]
K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ finrank K { x // x ∈ ⊤ } = finrank K V
[PROOFSTEP]
unfold finrank
[GOAL]
K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ↑toNat (Module.rank K { x // x ∈ ⊤ }) = ↑toNat (Module.rank K V)
[PROOFSTEP]
simp [rank_top]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
s t : Submodule K V
le : s ≤ t
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ t }
h : s = t
⊢ finrank K { x // x ∈ s } = finrank K { x // x ∈ t }
[PROOFSTEP]
rw [h]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K V
⊢ s < ⊤
[PROOFSTEP]
rw [← finrank_top K V] at lt
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ ⊤ }
⊢ s < ⊤
[PROOFSTEP]
exact lt_of_le_of_finrank_lt_finrank le_top lt
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
⊢ Module.rank K { x // x ∈ span K s } ≤ ↑(Finset.card (Set.toFinset s))
[PROOFSTEP]
simpa using rank_span_le (K := K) s
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
⊢ Finset.card (Set.toFinset ↑s) = Finset.card s
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Set.finrank K (Set.range b) ≤ Fintype.card ι
[PROOFSTEP]
classical
refine (finrank_span_le_card _).trans ?_
rw [Set.toFinset_range]
exact Finset.card_image_le
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Set.finrank K (Set.range b) ≤ Fintype.card ι
[PROOFSTEP]
refine (finrank_span_le_card _).trans ?_
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Finset.card (Set.toFinset (Set.range b)) ≤ Fintype.card ι
[PROOFSTEP]
rw [Set.toFinset_range]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Finset.card (Finset.image b Finset.univ) ≤ Fintype.card ι
[PROOFSTEP]
exact Finset.card_image_le
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
[PROOFSTEP]
have : Module.rank K (span K (Set.range b)) = #(Set.range b) := rank_span hb
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
this : Module.rank K { x // x ∈ span K (Set.range b) } = #↑(Set.range b)
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
[PROOFSTEP]
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast, lift_eq_nat_iff] at this
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
[PROOFSTEP]
have : Module.rank K (span K s) = #s := rank_span_set hs
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
this : Module.rank K { x // x ∈ span K s } = #↑s
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
[PROOFSTEP]
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : LinearIndependent K Subtype.val
⊢ finrank K { x // x ∈ span K ↑s } = Finset.card s
[PROOFSTEP]
convert finrank_span_set_eq_card (s : Set V) hs
[GOAL]
case h.e'_3.h.e'_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : LinearIndependent K Subtype.val
⊢ s = Set.toFinset ↑s
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_2.a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : LinearIndependent K Subtype.val
a✝ : V
⊢ a✝ ∈ s ↔ a✝ ∈ Set.toFinset ↑s
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
⊢ g i = 0
[PROOFSTEP]
classical
by_contra gx_ne_zero
refine'
  not_le_of_gt (span_lt_top_of_card_lt_finrank (show (b '' (Set.univ \ { i })).toFinset.card < finrank K V from _)) _
·
  calc
    (b '' (Set.univ \ { i })).toFinset.card = ((Set.univ \ { i }).toFinset.image b).card := by
      rw [Set.toFinset_card, Fintype.card_ofFinset]
    _ ≤ (Set.univ \ { i }).toFinset.card := Finset.card_image_le
    _ = (Finset.univ.erase i).card := (congr_arg Finset.card (Finset.ext (by simp [and_comm])))
    _ < Finset.univ.card := (Finset.card_erase_lt_of_mem (Finset.mem_univ i))
    _ = finrank K V := card_eq
refine' spans.trans (span_le.mpr _)
rintro _
  ⟨j, rfl, rfl⟩
      -- The case that `j ≠ i` is easy because `b j ∈ b '' (univ \ {i})`.
by_cases j_eq : j = i
swap
· refine' subset_span ⟨j, (Set.mem_diff _).mpr ⟨Set.mem_univ _, _⟩, rfl⟩
  exact mt Set.mem_singleton_iff.mp j_eq
rw [j_eq, SetLike.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum fun j => g j • b j) from _]
· refine' neg_mem (smul_mem _ _ (sum_mem fun k hk => _))
  obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk
  refine' smul_mem _ _ (subset_span ⟨k, _, rfl⟩)
  simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff]
    -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum
        -- to have the form of the assumption `dependent`.
apply eq_neg_of_add_eq_zero_left
calc
  (b i + (g i)⁻¹ • (s.erase i).sum fun j => g j • b j) = (g i)⁻¹ • (g i • b i + (s.erase i).sum fun j => g j • b j) :=
    by rw [smul_add, ← mul_smul, inv_mul_cancel gx_ne_zero, one_smul]
  _ = (g i)⁻¹ • (0 : V) := (congr_arg _ ?_)
  _ = 0 :=
    smul_zero
      _
        -- And then it's just a bit of manipulation with finite sums.
rwa [← Finset.insert_erase i_mem_s, Finset.sum_insert (Finset.not_mem_erase _ _)] at dependent
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
⊢ g i = 0
[PROOFSTEP]
by_contra gx_ne_zero
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ False
[PROOFSTEP]
refine'
  not_le_of_gt (span_lt_top_of_card_lt_finrank (show (b '' (Set.univ \ { i })).toFinset.card < finrank K V from _)) _
[GOAL]
case refine'_1
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ Finset.card (Set.toFinset (b '' (Set.univ \ {i}))) < finrank K V
[PROOFSTEP]
calc
  (b '' (Set.univ \ { i })).toFinset.card = ((Set.univ \ { i }).toFinset.image b).card := by
    rw [Set.toFinset_card, Fintype.card_ofFinset]
  _ ≤ (Set.univ \ { i }).toFinset.card := Finset.card_image_le
  _ = (Finset.univ.erase i).card := (congr_arg Finset.card (Finset.ext (by simp [and_comm])))
  _ < Finset.univ.card := (Finset.card_erase_lt_of_mem (Finset.mem_univ i))
  _ = finrank K V := card_eq
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ Finset.card (Set.toFinset (b '' (Set.univ \ {i}))) = Finset.card (Finset.image b (Set.toFinset (Set.univ \ {i})))
[PROOFSTEP]
rw [Set.toFinset_card, Fintype.card_ofFinset]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ∀ (a : ι), a ∈ Set.toFinset (Set.univ \ {i}) ↔ a ∈ Finset.erase Finset.univ i
[PROOFSTEP]
simp [and_comm]
[GOAL]
case refine'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ⊤ ≤ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
refine' spans.trans (span_le.mpr _)
[GOAL]
case refine'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ Set.range b ⊆ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
rintro _
  ⟨j, rfl, rfl⟩
      -- The case that `j ≠ i` is easy because `b j ∈ b '' (univ \ {i})`.
[GOAL]
case refine'_2.intro.refl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
by_cases j_eq : j = i
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
swap
[GOAL]
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
refine' subset_span ⟨j, (Set.mem_diff _).mpr ⟨Set.mem_univ _, _⟩, rfl⟩
[GOAL]
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ ¬j ∈ {i}
[PROOFSTEP]
exact mt Set.mem_singleton_iff.mp j_eq
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
rw [j_eq, SetLike.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum fun j => g j • b j) from _]
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ -((g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j) ∈ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
refine' neg_mem (smul_mem _ _ (sum_mem fun k hk => _))
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ Finset.erase s i
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk
[GOAL]
case pos.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ Finset.erase s i
k_ne_i : k ≠ i
right✝ : k ∈ s
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
refine' smul_mem _ _ (subset_span ⟨k, _, rfl⟩)
[GOAL]
case pos.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ Finset.erase s i
k_ne_i : k ≠ i
right✝ : k ∈ s
⊢ k ∈ Set.univ \ {i}
[PROOFSTEP]
simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff]
  -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum
      -- to have the form of the assumption `dependent`.
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b i = -((g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j)
[PROOFSTEP]
apply eq_neg_of_add_eq_zero_left
[GOAL]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ (b i + (g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j) = 0
[PROOFSTEP]
calc
  (b i + (g i)⁻¹ • (s.erase i).sum fun j => g j • b j) = (g i)⁻¹ • (g i • b i + (s.erase i).sum fun j => g j • b j) :=
    by rw [smul_add, ← mul_smul, inv_mul_cancel gx_ne_zero, one_smul]
  _ = (g i)⁻¹ • (0 : V) := (congr_arg _ ?_)
  _ = 0 :=
    smul_zero
      _
        -- And then it's just a bit of manipulation with finite sums.
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ (b i + (g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j) =
    (g i)⁻¹ • (g i • b i + Finset.sum (Finset.erase s i) fun j => g j • b j)
[PROOFSTEP]
rw [smul_add, ← mul_smul, inv_mul_cancel gx_ne_zero, one_smul]
[GOAL]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ (g i • b i + Finset.sum (Finset.erase s i) fun j => g j • b j) = 0
[PROOFSTEP]
rwa [← Finset.insert_erase i_mem_s, Finset.sum_insert (Finset.not_mem_erase _ _)] at dependent
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b → Fintype.card ι = Set.finrank K (Set.range b)
[PROOFSTEP]
intro h
[GOAL]
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
h : LinearIndependent K b
⊢ Fintype.card ι = Set.finrank K (Set.range b)
[PROOFSTEP]
exact (finrank_span_eq_card h).symm
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Fintype.card ι = Set.finrank K (Set.range b) → LinearIndependent K b
[PROOFSTEP]
intro hc
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
⊢ LinearIndependent K b
[PROOFSTEP]
let f := Submodule.subtype (span K (Set.range b))
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
⊢ LinearIndependent K b
[PROOFSTEP]
let b' : ι → span K (Set.range b) := fun i => ⟨b i, mem_span.2 fun p hp => hp (Set.mem_range_self _)⟩
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ LinearIndependent K b
[PROOFSTEP]
have hs : ⊤ ≤ span K (Set.range b') := by
  intro x
  have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
  have hf : f '' Set.range b' = Set.range b := by
    ext x
    simp [Set.mem_image, Set.mem_range]
  rw [hf] at h
  have hx : (x : V) ∈ span K (Set.range b) := x.property
  conv at hx =>
    arg 2
    rw [h]
  simpa [mem_map] using hx
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ ⊤ ≤ span K (Set.range b')
[PROOFSTEP]
intro x
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
have hf : f '' Set.range b' = Set.range b := by
  ext x
  simp [Set.mem_image, Set.mem_range]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ ↑f '' Set.range b' = Set.range b
[PROOFSTEP]
ext x
[GOAL]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x✝ : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
x : V
⊢ x ∈ ↑f '' Set.range b' ↔ x ∈ Set.range b
[PROOFSTEP]
simp [Set.mem_image, Set.mem_range]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
rw [hf] at h
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
have hx : (x : V) ∈ span K (Set.range b) := x.property
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
conv at hx =>
  arg 2
  rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| ↑x ∈ span K (Set.range b)
[PROOFSTEP]
  arg 2
  rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| ↑x ∈ span K (Set.range b)
[PROOFSTEP]
  arg 2
  rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| ↑x ∈ span K (Set.range b)
[PROOFSTEP]
arg 2
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| span K (Set.range b)
[PROOFSTEP]
rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
simpa [mem_map] using hx
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
⊢ LinearIndependent K b
[PROOFSTEP]
have hi : LinearMap.ker f = ⊥ := ker_subtype _
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
hi : LinearMap.ker f = ⊥
⊢ LinearIndependent K b
[PROOFSTEP]
convert (linearIndependent_of_top_le_span_of_card_eq_finrank hs hc).map' _ hi
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (Set.range b)
[PROOFSTEP]
rw [linearIndependent_iff_card_eq_finrank_span, finrank_range_le_card.le_iff_eq]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V = 1
[PROOFSTEP]
haveI := nontrivial_of_invariantBasisNumber K
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V = 1
[PROOFSTEP]
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{u} PUnit).mpr ⟨v, n, h⟩
[GOAL]
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
b : Basis PUnit K V
⊢ finrank K V = 1
[PROOFSTEP]
rw [finrank_eq_card_basis b, Fintype.card_punit]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V ≤ 1
[PROOFSTEP]
haveI := nontrivial_of_invariantBasisNumber K
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V ≤ 1
[PROOFSTEP]
rcases eq_or_ne v 0 with (rfl | hn)
[GOAL]
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
⊢ finrank K V ≤ 1
[PROOFSTEP]
haveI :=
  subsingleton_of_forall_eq (0 : V) fun w => by
    obtain ⟨c, rfl⟩ := h w
    simp
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
w : V
⊢ w = 0
[PROOFSTEP]
obtain ⟨c, rfl⟩ := h w
[GOAL]
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
c : K
⊢ c • 0 = 0
[PROOFSTEP]
simp
[GOAL]
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ finrank K V ≤ 1
[PROOFSTEP]
rw [finrank_zero_of_subsingleton]
[GOAL]
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case inr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
hn : v ≠ 0
⊢ finrank K V ≤ 1
[PROOFSTEP]
exact (finrank_eq_one v hn h).le
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ⊤ }
[PROOFSTEP]
rw [← Algebra.top_toSubmodule]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ↑Subalgebra.toSubmodule ⊤ }
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ finrank F { x // x ∈ ⊤ } = finrank F { x // x ∈ ⊤ }
[PROOFSTEP]
rw [← Algebra.top_toSubmodule]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ finrank F { x // x ∈ ⊤ } = finrank F { x // x ∈ ↑Subalgebra.toSubmodule ⊤ }
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F E
[PROOFSTEP]
rw [subalgebra_top_rank_eq_submodule_top_rank]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F E
[PROOFSTEP]
exact _root_.rank_top F E
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
[PROOFSTEP]
letI := Module.nontrivial F E
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
[PROOFSTEP]
rw [rank_span_set]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ #↑{1} = 1
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ LinearIndependent F fun x => ↑x
[PROOFSTEP]
exacts [mk_singleton _, linearIndependent_singleton one_ne_zero]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F { x // x ∈ ⊥ } = ↑1
[PROOFSTEP]
simp


[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (↑(piQuotientLift p q f hf) fun i => Quotient.mk (x i)) = Quotient.mk (↑(↑(lsum R (fun i => Ms i) R) f) x)
[PROOFSTEP]
rw [piQuotientLift, lsum_apply, sum_apply, ← mkQ_apply, lsum_apply, sum_apply, _root_.map_sum]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
x : (i : ι) → Ms i
⊢ (Finset.sum Finset.univ fun d =>
      ↑(comp (mapQ (p d) q (f d) (_ : p d ≤ comap (f d) q)) (proj d)) fun i => Quotient.mk (x i)) =
    Finset.sum Finset.univ fun x_1 => ↑(mkQ q) (↑(comp (f x_1) (proj x_1)) x)
[PROOFSTEP]
simp only [coe_proj, mapQ_apply, mkQ_apply, comp_apply]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ ↑(piQuotientLift p q f hf) (Pi.single i x) = ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) x
[PROOFSTEP]
simp_rw [piQuotientLift, lsum_apply, sum_apply, comp_apply, proj_apply]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ (Finset.sum Finset.univ fun x_1 => ↑(mapQ (p x_1) q (f x_1) (_ : p x_1 ≤ comap (f x_1) q)) (Pi.single i x x_1)) =
    ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) x
[PROOFSTEP]
rw [Finset.sum_eq_single i]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) (Pi.single i x i) = ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) x
[PROOFSTEP]
rw [Pi.single_eq_same]
[GOAL]
case h₀
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ ∀ (b : ι), b ∈ Finset.univ → b ≠ i → ↑(mapQ (p b) q (f b) (_ : p b ≤ comap (f b) q)) (Pi.single i x b) = 0
[PROOFSTEP]
rintro j - hj
[GOAL]
case h₀
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
j : ι
hj : j ≠ i
⊢ ↑(mapQ (p j) q (f j) (_ : p j ≤ comap (f j) q)) (Pi.single i x j) = 0
[PROOFSTEP]
rw [Pi.single_eq_of_ne hj, _root_.map_zero]
[GOAL]
case h₁
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
⊢ ¬i ∈ Finset.univ → ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) (Pi.single i x i) = 0
[PROOFSTEP]
intros
[GOAL]
case h₁
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
a✝ : ¬i ∈ Finset.univ
⊢ ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) (Pi.single i x i) = 0
[PROOFSTEP]
have := Finset.mem_univ i
[GOAL]
case h₁
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
q : Submodule R N
f : (i : ι) → Ms i →ₗ[R] N
hf : ∀ (i : ι), p i ≤ comap (f i) q
i : ι
x : Ms i ⧸ p i
a✝ : ¬i ∈ Finset.univ
this : i ∈ Finset.univ
⊢ ↑(mapQ (p i) q (f i) (_ : p i ≤ comap (f i) q)) (Pi.single i x i) = 0
[PROOFSTEP]
contradiction
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
Ns : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (Ns i)
inst✝ : (i : ι) → Module R (Ns i)
p : (i : ι) → Submodule R (Ms i)
f : (i : ι) → Ms i →ₗ[R] Ns i
hf : ∀ (i : ι), p i ≤ ker (f i)
x : (i : ι) → Ms i
hx : x ∈ pi Set.univ p
⊢ ↑(LinearMap.pi fun i => comp (f i) (proj i)) x = 0
[PROOFSTEP]
ext i
[GOAL]
case h
ι : Type u_1
R : Type u_2
inst✝⁶ : CommRing R
Ms : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommGroup (Ms i)
inst✝⁴ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
Ns : ι → Type u_5
inst✝¹ : (i : ι) → AddCommGroup (Ns i)
inst✝ : (i : ι) → Module R (Ns i)
p : (i : ι) → Submodule R (Ms i)
f : (i : ι) → Ms i →ₗ[R] Ns i
hf : ∀ (i : ι), p i ≤ ker (f i)
x : (i : ι) → Ms i
hx : x ∈ pi Set.univ p
i : ι
⊢ ↑(LinearMap.pi fun i => comp (f i) (proj i)) x i = OfNat.ofNat 0 i
[PROOFSTEP]
simpa using hf i (mem_pi.mp hx i (Set.mem_univ i))
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk'' x')) = Quotient.mk'' x'
[PROOFSTEP]
rw [Quotient.mk''_eq_mk x']
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ invFun p (toFun p (Quotient.mk x')) = Quotient.mk x'
[PROOFSTEP]
dsimp only [toFun, invFun]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
x : ((i : ι) → Ms i) ⧸ pi Set.univ p
x' : (i : ι) → Ms i
⊢ ↑(piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))
      (↑(quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i)))) (Quotient.mk x')) =
    Quotient.mk x'
[PROOFSTEP]
rw [quotientPiLift_mk p, funext fun i => (mkQ_apply (p i) (x' i)), piQuotientLift_mk p, lsum_single, id_apply]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ Function.RightInverse (invFun p) (toFun p)
[PROOFSTEP]
dsimp only [toFun, invFun]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ Function.RightInverse
    ↑(piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))
    ↑(quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
[PROOFSTEP]
rw [Function.rightInverse_iff_comp, ← coe_comp, ← @id_coe R]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
⊢ ↑(comp (quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
        (piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p)))) =
    ↑LinearMap.id
[PROOFSTEP]
refine' congr_arg _ (pi_ext fun i x => Quotient.inductionOn' x fun x' => funext fun j => _)
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ ↑(comp (quotientPiLift p (fun i => mkQ (p i)) (_ : ∀ (i : ι), p i ≤ ker (mkQ (p i))))
          (piQuotientLift p (pi Set.univ p) single (_ : ∀ (x : ι), p x ≤ comap (single x) (pi Set.univ p))))
      (Pi.single i (Quotient.mk'' x')) j =
    ↑LinearMap.id (Pi.single i (Quotient.mk'' x')) j
[PROOFSTEP]
rw [comp_apply, piQuotientLift_single, Quotient.mk''_eq_mk, mapQ_apply, quotientPiLift_mk, id_apply]
[GOAL]
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
⊢ (fun i_1 => ↑(mkQ (p i_1)) (↑(single i) x' i_1)) j = Pi.single i (Quotient.mk x') j
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : i = j
⊢ (fun i_1 => ↑(mkQ (p i_1)) (↑(single i) x' i_1)) j = Pi.single i (Quotient.mk x') j
[PROOFSTEP]
simp only [mkQ_apply, coe_single]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : ¬i = j
⊢ (fun i_1 => ↑(mkQ (p i_1)) (↑(single i) x' i_1)) j = Pi.single i (Quotient.mk x') j
[PROOFSTEP]
simp only [mkQ_apply, coe_single]
[GOAL]
case pos
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : i = j
⊢ Quotient.mk (Pi.single i x' j) = Pi.single i (Quotient.mk x') j
[PROOFSTEP]
subst hij
[GOAL]
case pos
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
⊢ Quotient.mk (Pi.single i x' i) = Pi.single i (Quotient.mk x') i
[PROOFSTEP]
rw [Pi.single_eq_same, Pi.single_eq_same]
[GOAL]
case neg
ι : Type u_1
R : Type u_2
inst✝⁸ : CommRing R
Ms : ι → Type u_3
inst✝⁷ : (i : ι) → AddCommGroup (Ms i)
inst✝⁶ : (i : ι) → Module R (Ms i)
N : Type u_4
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
Ns : ι → Type u_5
inst✝³ : (i : ι) → AddCommGroup (Ns i)
inst✝² : (i : ι) → Module R (Ns i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
p : (i : ι) → Submodule R (Ms i)
i : ι
x : Ms i ⧸ p i
x' : Ms i
j : ι
hij : ¬i = j
⊢ Quotient.mk (Pi.single i x' j) = Pi.single i (Quotient.mk x') j
[PROOFSTEP]
rw [Pi.single_eq_of_ne (Ne.symm hij), Pi.single_eq_of_ne (Ne.symm hij), Quotient.mk_zero]


[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
n : N
m₁ m₂ : M
⊢ (fun n m => ↑(↑f m) n) n (m₁ + m₂) = (fun n m => ↑(↑f m) n) n m₁ + (fun n m => ↑(↑f m) n) n m₂
[PROOFSTEP]
simp only [map_add, add_apply]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
c : R
n : N
m : M
⊢ (fun n m => ↑(↑f m) n) n (c • m) = ↑ρ₁₂ c • (fun n m => ↑(↑f m) n) n m
[PROOFSTEP]
simp only [map_smulₛₗ, smul_apply]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f g : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
H : flip f = flip g
m : M
n : N
⊢ ↑(↑(flip f) n) m = ↑(↑(flip g) n) m
[PROOFSTEP]
rw [H]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
m₁ m₂ : M
x✝ : { x // x ∈ q }
⊢ ↑((fun m => domRestrict (↑f m) q) (m₁ + m₂)) x✝ =
    ↑((fun m => domRestrict (↑f m) q) m₁ + (fun m => domRestrict (↑f m) q) m₂) x✝
[PROOFSTEP]
simp only [map_add, domRestrict_apply, add_apply]
[GOAL]
R : Type u_1
inst✝³² : Semiring R
S : Type u_2
inst✝³¹ : Semiring S
R₂ : Type u_3
inst✝³⁰ : Semiring R₂
S₂ : Type u_4
inst✝²⁹ : Semiring S₂
M : Type u_5
N : Type u_6
P : Type u_7
M₂ : Type u_8
N₂ : Type u_9
P₂ : Type u_10
Nₗ : Type u_11
Pₗ : Type u_12
M' : Type u_13
N' : Type u_14
P' : Type u_15
inst✝²⁸ : AddCommMonoid M
inst✝²⁷ : AddCommMonoid N
inst✝²⁶ : AddCommMonoid P
inst✝²⁵ : AddCommMonoid M₂
inst✝²⁴ : AddCommMonoid N₂
inst✝²³ : AddCommMonoid P₂
inst✝²² : AddCommMonoid Nₗ
inst✝²¹ : AddCommMonoid Pₗ
inst✝²⁰ : AddCommGroup M'
inst✝¹⁹ : AddCommGroup N'
inst✝¹⁸ : AddCommGroup P'
inst✝¹⁷ : Module R M
inst✝¹⁶ : Module S N
inst✝¹⁵ : Module R₂ P
inst✝¹⁴ : Module S₂ P
inst✝¹³ : Module R M₂
inst✝¹² : Module S N₂
inst✝¹¹ : Module R P₂
inst✝¹⁰ : Module S₂ P₂
inst✝⁹ : Module R Pₗ
inst✝⁸ : Module S Pₗ
inst✝⁷ : Module R M'
inst✝⁶ : Module S N'
inst✝⁵ : Module R₂ P'
inst✝⁴ : Module S₂ P'
inst✝³ : SMulCommClass S₂ R₂ P
inst✝² : SMulCommClass S R Pₗ
inst✝¹ : SMulCommClass S₂ R₂ P'
inst✝ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P
q : Submodule S N
c : R
m : M
x✝ : { x // x ∈ q }
⊢ ↑(AddHom.toFun
          { toFun := fun m => domRestrict (↑f m) q,
            map_add' :=
              (_ :
                ∀ (m₁ m₂ : M),
                  (fun m => domRestrict (↑f m) q) (m₁ + m₂) =
                    (fun m => domRestrict (↑f m) q) m₁ + (fun m => domRestrict (↑f m) q) m₂) }
          (c • m))
      x✝ =
    ↑(↑ρ₁₂ c •
          AddHom.toFun
            { toFun := fun m => domRestrict (↑f m) q,
              map_add' :=
                (_ :
                  ∀ (m₁ m₂ : M),
                    (fun m => domRestrict (↑f m) q) (m₁ + m₂) =
                      (fun m => domRestrict (↑f m) q) m₁ + (fun m => domRestrict (↑f m) q) m₂) }
            m)
      x✝
[PROOFSTEP]
simp only [f.map_smulₛₗ, domRestrict_apply, smul_apply]
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
⊢ compl₂ f id = f
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
x✝¹ : M
x✝ : N
⊢ ↑(↑(compl₂ f id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
[PROOFSTEP]
rw [compl₂_apply, id_coe, id.def]
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f✝ : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
⊢ compl₁₂ f id id = f
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f✝ : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
x✝¹ : Mₗ
x✝ : Nₗ
⊢ ↑(↑(compl₁₂ f id id) x✝¹) x✝ = ↑(↑f x✝¹) x✝
[PROOFSTEP]
simp_rw [compl₁₂_apply, id_coe, id.def]
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g' ↔ f₁ = f₂
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g' → f₁ = f₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ f₁ = f₂ → compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
⊢ f₁ = f₂
[PROOFSTEP]
ext x y
[GOAL]
case mp.h.h
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
[PROOFSTEP]
cases' hₗ x with x' hx
[GOAL]
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x : Mₗ
y : Nₗ
x' : Qₗ
hx : ↑g x' = x
⊢ ↑(↑f₁ x) y = ↑(↑f₂ x) y
[PROOFSTEP]
subst hx
[GOAL]
case mp.h.h.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
[PROOFSTEP]
cases' hᵣ y with y' hy
[GOAL]
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
y : Nₗ
x' : Qₗ
y' : Qₗ'
hy : ↑g' y' = y
⊢ ↑(↑f₁ (↑g x')) y = ↑(↑f₂ (↑g x')) y
[PROOFSTEP]
subst hy
[GOAL]
case mp.h.h.intro.intro
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
x' : Qₗ
y' : Qₗ'
⊢ ↑(↑f₁ (↑g x')) (↑g' y') = ↑(↑f₂ (↑g x')) (↑g' y')
[PROOFSTEP]
convert LinearMap.congr_fun₂ h x' y' using 0
[GOAL]
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ f₂ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
h : f₁ = f₂
⊢ compl₁₂ f₁ g g' = compl₁₂ f₂ g g'
[PROOFSTEP]
subst h
[GOAL]
case mpr
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
f₁ : Mₗ →ₗ[R] Nₗ →ₗ[R] Pₗ
g : Qₗ →ₗ[R] Mₗ
g' : Qₗ' →ₗ[R] Nₗ
hₗ : Function.Surjective ↑g
hᵣ : Function.Surjective ↑g'
⊢ compl₁₂ f₁ g g' = compl₁₂ f₁ g g'
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝²³ : CommSemiring R
R₂ : Type u_2
inst✝²² : CommSemiring R₂
R₃ : Type u_3
inst✝²¹ : CommSemiring R₃
R₄ : Type u_4
inst✝²⁰ : CommSemiring R₄
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
Mₗ : Type u_9
Nₗ : Type u_10
Pₗ : Type u_11
Qₗ : Type u_12
Qₗ' : Type u_13
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : AddCommMonoid N
inst✝¹⁷ : AddCommMonoid P
inst✝¹⁶ : AddCommMonoid Q
inst✝¹⁵ : AddCommMonoid Mₗ
inst✝¹⁴ : AddCommMonoid Nₗ
inst✝¹³ : AddCommMonoid Pₗ
inst✝¹² : AddCommMonoid Qₗ
inst✝¹¹ : AddCommMonoid Qₗ'
inst✝¹⁰ : Module R M
inst✝⁹ : Module R₂ N
inst✝⁸ : Module R₃ P
inst✝⁷ : Module R₄ Q
inst✝⁶ : Module R Mₗ
inst✝⁵ : Module R Nₗ
inst✝⁴ : Module R Pₗ
inst✝³ : Module R Qₗ
inst✝² : Module R Qₗ'
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₄₂ : R₄ →+* R₂
σ₄₃ : R₄ →+* R₃
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝ : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃
f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P
r s : R
m : M
⊢ (fun x x_1 => x • x_1) s (r • m) = r • (fun x x_1 => x • x_1) s m
[PROOFSTEP]
simp only [smul_smul, smul_eq_mul, mul_comm]