[GOAL]
R : Type u
inst✝ : Semiring R
⊢ StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
[PROOFSTEP]
refine' ⟨fun h n => fun f hf => _, fun h => ⟨@fun n m f hf => _⟩⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
⊢ False
[PROOFSTEP]
letI : StrongRankCondition R := h
[GOAL]
case refine'_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ↑f
this : StrongRankCondition R := h
⊢ False
[PROOFSTEP]
exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)
[GOAL]
case refine'_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ↑f
⊢ n ≤ m
[PROOFSTEP]
by_contra H
[GOAL]
case refine'_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ↑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ↑f
H : ¬n ≤ m
⊢ False
[PROOFSTEP]
exact
  h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
    (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ↑f
⊢ Fintype.card α ≤ Fintype.card β
[PROOFSTEP]
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ↑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card α ≤ Fintype.card β
[PROOFSTEP]
let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ↑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card α ≤ Fintype.card β
[PROOFSTEP]
exact
  le_of_fin_injective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
    (((LinearEquiv.symm Q).injective.comp i).comp (LinearEquiv.injective P))
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ↑f
⊢ Fintype.card α ≤ Fintype.card β
[PROOFSTEP]
let P := Finsupp.linearEquivFunOnFinite R R β
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ↑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card α ≤ Fintype.card β
[PROOFSTEP]
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ↑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)
⊢ Fintype.card α ≤ Fintype.card β
[PROOFSTEP]
exact card_le_of_injective R ((P.toLinearMap.comp f).comp Q.toLinearMap) ((P.injective.comp i).comp Q.injective)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ↑f
⊢ Fintype.card β ≤ Fintype.card α
[PROOFSTEP]
let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ↑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
⊢ Fintype.card β ≤ Fintype.card α
[PROOFSTEP]
let Q := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Surjective ↑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card β ≤ Fintype.card α
[PROOFSTEP]
exact
  le_of_fin_surjective R ((Q.symm.toLinearMap.comp f).comp P.toLinearMap)
    (((LinearEquiv.symm Q).surjective.comp i).comp (LinearEquiv.surjective P))
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ↑f
⊢ Fintype.card β ≤ Fintype.card α
[PROOFSTEP]
let P := Finsupp.linearEquivFunOnFinite R R β
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ↑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
⊢ Fintype.card β ≤ Fintype.card α
[PROOFSTEP]
let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
[GOAL]
R : Type u
inst✝³ : Semiring R
inst✝² : RankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Surjective ↑f
P : (β →₀ R) ≃ₗ[R] β → R := Finsupp.linearEquivFunOnFinite R R β
Q : (α → R) ≃ₗ[R] α →₀ R := LinearEquiv.symm (Finsupp.linearEquivFunOnFinite R R α)
⊢ Fintype.card β ≤ Fintype.card α
[PROOFSTEP]
exact card_le_of_surjective R ((P.toLinearMap.comp f).comp Q.toLinearMap) ((P.surjective.comp i).comp Q.surjective)
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
⊢ Nontrivial R
[PROOFSTEP]
by_contra h
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ False
[PROOFSTEP]
refine' zero_ne_one (eq_of_fin_equiv R _)
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
[PROOFSTEP]
haveI := not_nontrivial_iff_subsingleton.1 h
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this : Subsingleton R
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
[PROOFSTEP]
haveI : Subsingleton (Fin 1 → R) := Subsingleton.intro <| fun a b => funext fun x => Subsingleton.elim _ _
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ (Fin 0 → R) ≃ₗ[R] Fin 1 → R
[PROOFSTEP]
exact
  { toFun := 0
    invFun := 0
    map_add' := by aesop
    map_smul' := by aesop
    left_inv := fun _ => by simp
    right_inv := fun _ => by simp }
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = OfNat.ofNat 0 x + OfNat.ofNat 0 y
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
⊢ ∀ (r : R) (x : Fin 0 → R),
    AddHom.toFun { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) } (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) } x
[PROOFSTEP]
aesop
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
x✝ : Fin 0 → R
⊢ OfNat.ofNat 0
      (AddHom.toFun
        { toAddHom := { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) },
            map_smul' := (_ : ∀ (r : R) (x : Fin 0 → R), OfNat.ofNat 0 (r • x) = r • 0) }.toAddHom
        x✝) =
    x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : Semiring R
inst✝ : InvariantBasisNumber R
h : ¬Nontrivial R
this✝ : Subsingleton R
this : Subsingleton (Fin 1 → R)
x✝ : Fin 1 → R
⊢ AddHom.toFun
      { toAddHom := { toFun := 0, map_add' := (_ : ∀ (x y : Fin 0 → R), OfNat.ofNat 0 (x + y) = 0 + 0) },
          map_smul' := (_ : ∀ (r : R) (x : Fin 0 → R), OfNat.ofNat 0 (r • x) = r • 0) }.toAddHom
      (OfNat.ofNat 0 x✝) =
    x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
⊢ StrongRankCondition R
[PROOFSTEP]
constructor
[GOAL]
case le_of_fin_injective
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
⊢ ∀ {n m : ℕ} (f : (Fin n → R) →ₗ[R] Fin m → R), Injective ↑f → n ≤ m
[PROOFSTEP]
intro m n f i
[GOAL]
case le_of_fin_injective
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
m n : ℕ
f : (Fin m → R) →ₗ[R] Fin n → R
i : Injective ↑f
⊢ m ≤ n
[PROOFSTEP]
by_contra h
[GOAL]
case le_of_fin_injective
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
m n : ℕ
f : (Fin m → R) →ₗ[R] Fin n → R
i : Injective ↑f
h : ¬m ≤ n
⊢ False
[PROOFSTEP]
rw [not_le, ← Nat.add_one_le_iff, le_iff_exists_add] at h
[GOAL]
case le_of_fin_injective
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
m n : ℕ
f : (Fin m → R) →ₗ[R] Fin n → R
i : Injective ↑f
h : ∃ c, m = n + 1 + c
⊢ False
[PROOFSTEP]
obtain ⟨m, rfl⟩ := h
[GOAL]
case le_of_fin_injective.intro
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
n m : ℕ
f : (Fin (n + 1 + m) → R) →ₗ[R] Fin n → R
i : Injective ↑f
⊢ False
[PROOFSTEP]
let e : Fin (n + 1 + m) ≃ Sum (Fin n) (Fin (1 + m)) := (finCongr (add_assoc _ _ _)).trans finSumFinEquiv.symm
[GOAL]
case le_of_fin_injective.intro
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
n m : ℕ
f : (Fin (n + 1 + m) → R) →ₗ[R] Fin n → R
i : Injective ↑f
e : Fin (n + 1 + m) ≃ Fin n ⊕ Fin (1 + m) := (finCongr (_ : n + 1 + m = n + (1 + m))).trans finSumFinEquiv.symm
⊢ False
[PROOFSTEP]
let f' := f.comp ((LinearEquiv.sumArrowLequivProdArrow _ _ R R).symm.trans (LinearEquiv.funCongrLeft R R e)).toLinearMap
[GOAL]
case le_of_fin_injective.intro
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
n m : ℕ
f : (Fin (n + 1 + m) → R) →ₗ[R] Fin n → R
i : Injective ↑f
e : Fin (n + 1 + m) ≃ Fin n ⊕ Fin (1 + m) := (finCongr (_ : n + 1 + m = n + (1 + m))).trans finSumFinEquiv.symm
f' : (Fin n → R) × (Fin (1 + m) → R) →ₗ[R] Fin n → R :=
  LinearMap.comp f
    ↑(LinearEquiv.trans (LinearEquiv.symm (LinearEquiv.sumArrowLequivProdArrow (Fin n) (Fin (1 + m)) R R))
        (LinearEquiv.funCongrLeft R R e))
⊢ False
[PROOFSTEP]
have i' : Injective f' := i.comp (LinearEquiv.injective _)
[GOAL]
case le_of_fin_injective.intro
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
n m : ℕ
f : (Fin (n + 1 + m) → R) →ₗ[R] Fin n → R
i : Injective ↑f
e : Fin (n + 1 + m) ≃ Fin n ⊕ Fin (1 + m) := (finCongr (_ : n + 1 + m = n + (1 + m))).trans finSumFinEquiv.symm
f' : (Fin n → R) × (Fin (1 + m) → R) →ₗ[R] Fin n → R :=
  LinearMap.comp f
    ↑(LinearEquiv.trans (LinearEquiv.symm (LinearEquiv.sumArrowLequivProdArrow (Fin n) (Fin (1 + m)) R R))
        (LinearEquiv.funCongrLeft R R e))
i' : Injective ↑f'
⊢ False
[PROOFSTEP]
apply @zero_ne_one (Fin (1 + m) → R) _ _
[GOAL]
case le_of_fin_injective.intro.a
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
n m : ℕ
f : (Fin (n + 1 + m) → R) →ₗ[R] Fin n → R
i : Injective ↑f
e : Fin (n + 1 + m) ≃ Fin n ⊕ Fin (1 + m) := (finCongr (_ : n + 1 + m = n + (1 + m))).trans finSumFinEquiv.symm
f' : (Fin n → R) × (Fin (1 + m) → R) →ₗ[R] Fin n → R :=
  LinearMap.comp f
    ↑(LinearEquiv.trans (LinearEquiv.symm (LinearEquiv.sumArrowLequivProdArrow (Fin n) (Fin (1 + m)) R R))
        (LinearEquiv.funCongrLeft R R e))
i' : Injective ↑f'
⊢ 0 = 1
[PROOFSTEP]
apply (IsNoetherian.equivPUnitOfProdInjective f' i').injective
[GOAL]
case le_of_fin_injective.intro.a.a
R : Type u
inst✝² : Ring R
inst✝¹ : Nontrivial R
inst✝ : IsNoetherianRing R
n m : ℕ
f : (Fin (n + 1 + m) → R) →ₗ[R] Fin n → R
i : Injective ↑f
e : Fin (n + 1 + m) ≃ Fin n ⊕ Fin (1 + m) := (finCongr (_ : n + 1 + m = n + (1 + m))).trans finSumFinEquiv.symm
f' : (Fin n → R) × (Fin (1 + m) → R) →ₗ[R] Fin n → R :=
  LinearMap.comp f
    ↑(LinearEquiv.trans (LinearEquiv.symm (LinearEquiv.sumArrowLequivProdArrow (Fin n) (Fin (1 + m)) R R))
        (LinearEquiv.funCongrLeft R R e))
i' : Injective ↑f'
⊢ ↑(IsNoetherian.equivPUnitOfProdInjective f' i') 0 = ↑(IsNoetherian.equivPUnitOfProdInjective f' i') 1
[PROOFSTEP]
ext
[GOAL]
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi I ι
⊢ ∀ (a b : ι → R),
    Setoid.r a b →
      (fun y => ↑(Ideal.Quotient.mk (Ideal.pi I ι')) (↑e y)) a =
        (fun y => ↑(Ideal.Quotient.mk (Ideal.pi I ι')) (↑e y)) b
[PROOFSTEP]
refine' fun a b hab => Ideal.Quotient.eq.2 fun h => _
[GOAL]
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi I ι
a b : ι → R
hab : Setoid.r a b
h : ι'
⊢ (↑e a - ↑e b) h ∈ I
[PROOFSTEP]
rw [Submodule.quotientRel_r_def] at hab
[GOAL]
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi I ι
a b : ι → R
hab : a - b ∈ Ideal.pi I ι
h : ι'
⊢ (↑e a - ↑e b) h ∈ I
[PROOFSTEP]
rw [← LinearMap.map_sub]
[GOAL]
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi I ι
a b : ι → R
hab : a - b ∈ Ideal.pi I ι
h : ι'
⊢ ↑e (a - b) h ∈ I
[PROOFSTEP]
exact Ideal.map_pi _ _ hab e h
[GOAL]
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ((ι → R) ⧸ Ideal.pi I ι) ≃ₗ[R ⧸ I] (ι' → R) ⧸ Ideal.pi I ι'
[PROOFSTEP]
refine'
  { toFun := induced_map I e
    invFun := induced_map I e.symm .. }
[GOAL]
case refine'_1
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ∀ (x y : (ι → R) ⧸ Ideal.pi I ι), induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y
case refine'_2
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
    AddHom.toFun { toFun := induced_map I ↑e, map_add' := ?refine'_1 } (r • x) =
      ↑(RingHom.id (R ⧸ I)) r • AddHom.toFun { toFun := induced_map I ↑e, map_add' := ?refine'_1 } x
case refine'_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ LeftInverse (induced_map I ↑(LinearEquiv.symm e))
    { toAddHom := { toFun := induced_map I ↑e, map_add' := ?refine'_1 }, map_smul' := ?refine'_2 }.toAddHom.toFun
case refine'_4
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ Function.RightInverse (induced_map I ↑(LinearEquiv.symm e))
    { toAddHom := { toFun := induced_map I ↑e, map_add' := ?refine'_1 }, map_smul' := ?refine'_2 }.toAddHom.toFun
[PROOFSTEP]
all_goals
  first
  | rintro ⟨a⟩ ⟨b⟩
  |
    rintro
      ⟨a⟩
          -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
            -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_1
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ∀ (x y : (ι → R) ⧸ Ideal.pi I ι), induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y
[PROOFSTEP]
first
| rintro ⟨a⟩ ⟨b⟩
|
  rintro
    ⟨a⟩
        -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
          -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_1
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ∀ (x y : (ι → R) ⧸ Ideal.pi I ι), induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case refine'_2
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
    AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (r • x) =
      ↑(RingHom.id (R ⧸ I)) r •
        AddHom.toFun
          { toFun := induced_map I ↑e,
            map_add' :=
              (_ :
                ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                  induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
          x
[PROOFSTEP]
first
| rintro ⟨a⟩ ⟨b⟩
|
  rintro
    ⟨a⟩
        -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
          -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_2
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
    AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (r • x) =
      ↑(RingHom.id (R ⧸ I)) r •
        AddHom.toFun
          { toFun := induced_map I ↑e,
            map_add' :=
              (_ :
                ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                  induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
          x
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case refine'_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ LeftInverse (induced_map I ↑(LinearEquiv.symm e))
    {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
first
| rintro ⟨a⟩ ⟨b⟩
|
  rintro
    ⟨a⟩
        -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
          -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ LeftInverse (induced_map I ↑(LinearEquiv.symm e))
    {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case refine'_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ LeftInverse (induced_map I ↑(LinearEquiv.symm e))
    {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
rintro
  ⟨a⟩
      -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
        -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_4
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ Function.RightInverse (induced_map I ↑(LinearEquiv.symm e))
    {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
first
| rintro ⟨a⟩ ⟨b⟩
|
  rintro
    ⟨a⟩
        -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
          -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_4
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ Function.RightInverse (induced_map I ↑(LinearEquiv.symm e))
    {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
rintro ⟨a⟩ ⟨b⟩
[GOAL]
case refine'_4
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
⊢ Function.RightInverse (induced_map I ↑(LinearEquiv.symm e))
    {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom.toFun
[PROOFSTEP]
rintro
  ⟨a⟩
      -- porting note: the next 4 lines were necessary because Lean couldn't correctly infer `(I.pi ι)`
        -- and `(I.pi ι')` on its own.
[GOAL]
case refine'_1.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ induced_map I (↑e) (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    induced_map I (↑e) (Quot.mk Setoid.r a) + induced_map I (↑e) (Quot.mk Setoid.r b)
case refine'_2.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ AddHom.toFun
      { toFun := induced_map I ↑e,
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
      (Quot.mk Setoid.r a • Quot.mk Setoid.r b) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a) •
      AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (Quot.mk Setoid.r b)
case refine'_3.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
⊢ induced_map I (↑(LinearEquiv.symm e))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := induced_map I ↑e,
                map_add' :=
                  (_ :
                    ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                      induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
            map_smul' :=
              (_ :
                ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                  AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      (r • x) =
                    ↑(RingHom.id (R ⧸ I)) r •
                      AddHom.toFun
                        { toFun := induced_map I ↑e,
                          map_add' :=
                            (_ :
                              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                        x) }.toAddHom
        (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
case refine'_4.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom
      (induced_map I (↑(LinearEquiv.symm e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
pick_goal 3
[GOAL]
case refine'_3.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
⊢ induced_map I (↑(LinearEquiv.symm e))
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := induced_map I ↑e,
                map_add' :=
                  (_ :
                    ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                      induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
            map_smul' :=
              (_ :
                ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                  AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      (r • x) =
                    ↑(RingHom.id (R ⧸ I)) r •
                      AddHom.toFun
                        { toFun := induced_map I ↑e,
                          map_add' :=
                            (_ :
                              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                        x) }.toAddHom
        (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
case refine'_1.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ induced_map I (↑e) (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    induced_map I (↑e) (Quot.mk Setoid.r a) + induced_map I (↑e) (Quot.mk Setoid.r b)
case refine'_2.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ AddHom.toFun
      { toFun := induced_map I ↑e,
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
      (Quot.mk Setoid.r a • Quot.mk Setoid.r b) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a) •
      AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (Quot.mk Setoid.r b)
case refine'_4.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom
      (induced_map I (↑(LinearEquiv.symm e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι) _ = Ideal.Quotient.mk (I.pi ι) _
[GOAL]
case refine'_3.mk.convert_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
⊢ ↑(Ideal.Quotient.mk (Ideal.pi I ι)) (↑↑(LinearEquiv.symm e) (↑↑e a)) = ↑(Ideal.Quotient.mk (Ideal.pi I ι)) a
case refine'_1.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ induced_map I (↑e) (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    induced_map I (↑e) (Quot.mk Setoid.r a) + induced_map I (↑e) (Quot.mk Setoid.r b)
case refine'_2.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ AddHom.toFun
      { toFun := induced_map I ↑e,
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
      (Quot.mk Setoid.r a • Quot.mk Setoid.r b) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a) •
      AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (Quot.mk Setoid.r b)
case refine'_4.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom
      (induced_map I (↑(LinearEquiv.symm e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
congr
[GOAL]
case refine'_3.mk.convert_3.h.e_6.h
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
⊢ ↑↑(LinearEquiv.symm e) (↑↑e a) = a
case refine'_1.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ induced_map I (↑e) (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    induced_map I (↑e) (Quot.mk Setoid.r a) + induced_map I (↑e) (Quot.mk Setoid.r b)
case refine'_2.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ AddHom.toFun
      { toFun := induced_map I ↑e,
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
      (Quot.mk Setoid.r a • Quot.mk Setoid.r b) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a) •
      AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (Quot.mk Setoid.r b)
case refine'_4.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom
      (induced_map I (↑(LinearEquiv.symm e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
simp only [LinearEquiv.coe_coe, LinearEquiv.symm_apply_apply]
[GOAL]
case refine'_1.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ induced_map I (↑e) (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    induced_map I (↑e) (Quot.mk Setoid.r a) + induced_map I (↑e) (Quot.mk Setoid.r b)
case refine'_2.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ AddHom.toFun
      { toFun := induced_map I ↑e,
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
      (Quot.mk Setoid.r a • Quot.mk Setoid.r b) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a) •
      AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (Quot.mk Setoid.r b)
case refine'_4.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom
      (induced_map I (↑(LinearEquiv.symm e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
all_goals
  convert_to Ideal.Quotient.mk (I.pi ι') _ = Ideal.Quotient.mk (I.pi ι') _
  congr
  simp only [map_add, LinearEquiv.coe_coe, LinearEquiv.map_smulₛₗ, RingHom.id_apply, LinearEquiv.apply_symm_apply]
[GOAL]
case refine'_1.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ induced_map I (↑e) (Quot.mk Setoid.r a + Quot.mk Setoid.r b) =
    induced_map I (↑e) (Quot.mk Setoid.r a) + induced_map I (↑e) (Quot.mk Setoid.r b)
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι') _ = Ideal.Quotient.mk (I.pi ι') _
[GOAL]
case refine'_1.mk.mk.convert_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ ↑(Ideal.Quotient.mk (Ideal.pi I ι')) (↑↑e ((fun x x_1 => x + x_1) a b)) =
    ↑(Ideal.Quotient.mk (Ideal.pi I ι')) ((fun x x_1 => x + x_1) (↑↑e a) (↑↑e b))
[PROOFSTEP]
congr
[GOAL]
case refine'_1.mk.mk.convert_3.h.e_6.h
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi I ι
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ ↑↑e ((fun x x_1 => x + x_1) a b) = (fun x x_1 => x + x_1) (↑↑e a) (↑↑e b)
[PROOFSTEP]
simp only [map_add, LinearEquiv.coe_coe, LinearEquiv.map_smulₛₗ, RingHom.id_apply, LinearEquiv.apply_symm_apply]
[GOAL]
case refine'_2.mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ AddHom.toFun
      { toFun := induced_map I ↑e,
        map_add' :=
          (_ :
            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
      (Quot.mk Setoid.r a • Quot.mk Setoid.r b) =
    ↑(RingHom.id (R ⧸ I)) (Quot.mk Setoid.r a) •
      AddHom.toFun
        { toFun := induced_map I ↑e,
          map_add' :=
            (_ :
              ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
        (Quot.mk Setoid.r b)
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι') _ = Ideal.Quotient.mk (I.pi ι') _
[GOAL]
case refine'_2.mk.mk.convert_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ ↑(Ideal.Quotient.mk (Ideal.pi I ι')) (↑↑e (a • b)) = ↑(Ideal.Quotient.mk (Ideal.pi I ι')) (a • ↑↑e b)
[PROOFSTEP]
congr
[GOAL]
case refine'_2.mk.mk.convert_3.h.e_6.h
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
r✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi I ι
b : ι → R
⊢ ↑↑e (a • b) = a • ↑↑e b
[PROOFSTEP]
simp only [map_add, LinearEquiv.coe_coe, LinearEquiv.map_smulₛₗ, RingHom.id_apply, LinearEquiv.apply_symm_apply]
[GOAL]
case refine'_4.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := induced_map I ↑e,
              map_add' :=
                (_ :
                  ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                    induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) },
          map_smul' :=
            (_ :
              ∀ (r : R ⧸ I) (x : (ι → R) ⧸ Ideal.pi I ι),
                AddHom.toFun
                    { toFun := induced_map I ↑e,
                      map_add' :=
                        (_ :
                          ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                            induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                    (r • x) =
                  ↑(RingHom.id (R ⧸ I)) r •
                    AddHom.toFun
                      { toFun := induced_map I ↑e,
                        map_add' :=
                          (_ :
                            ∀ (x y : (ι → R) ⧸ Ideal.pi I ι),
                              induced_map I (↑e) (x + y) = induced_map I (↑e) x + induced_map I (↑e) y) }
                      x) }.toAddHom
      (induced_map I (↑(LinearEquiv.symm e)) (Quot.mk Setoid.r a)) =
    Quot.mk Setoid.r a
[PROOFSTEP]
convert_to Ideal.Quotient.mk (I.pi ι') _ = Ideal.Quotient.mk (I.pi ι') _
[GOAL]
case refine'_4.mk.convert_3
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ ↑(Ideal.Quotient.mk (Ideal.pi I ι')) (↑↑e (↑↑(LinearEquiv.symm e) a)) = ↑(Ideal.Quotient.mk (Ideal.pi I ι')) a
[PROOFSTEP]
congr
[GOAL]
case refine'_4.mk.convert_3.h.e_6.h
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi I ι'
a : ι' → R
⊢ ↑↑e (↑↑(LinearEquiv.symm e) a) = a
[PROOFSTEP]
simp only [map_add, LinearEquiv.coe_coe, LinearEquiv.map_smulₛₗ, RingHom.id_apply, LinearEquiv.apply_symm_apply]