apply (config := {allowSynthFailures := true }) LinearEquiv.mk
case isTrue.f
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ (S₁ ⧸ comap e P) ≃ₗ[R ⧸ p] S₂ ⧸ P
case isTrue.f.left_inv
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ Function.LeftInverse ?isTrue.f.invFun ?isTrue.f.toLinearMap.toFun

case isTrue.f.right_inv
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ Function.RightInverse ?isTrue.f.invFun ?isTrue.f.toLinearMap.toFun

case isTrue.f.toLinearMap
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ S₁ ⧸ comap e P →ₗ[R ⧸ p] S₂ ⧸ P

case isTrue.f.invFun
R : Type u_1
S₁ : Type u_2
S₂ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S₁
inst✝³ : CommRing S₂
inst✝² : Algebra R S₁
inst✝¹ : Algebra R S₂
e : S₁ ≃ₐ[R] S₂
p : Ideal R
P : Ideal S₂
inst✝ : p.IsMaximal
this : comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
h✝ : comap (algebraMap R S₁) (comap e P) = p
E : (S₁ ⧸ comap e P) ≃ₐ[R] S₂ ⧸ P
⊢ S₂ ⧸ P → S₁ ⧸ comap e P