Theorem: Ideal.inertiaDeg_comap_eq (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
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
⊢ inertiaDeg (algebraMap R S₁) p (comap e P) = inertiaDeg (algebraMap R S₂) p P
Tactic:
delta Ideal.inertiaDeg
State after:
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
⊢ (if hPp : comap (algebraMap R S₁) (comap e P) = p then FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) else 0) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

State before:
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
⊢ (if hPp : comap (algebraMap R S₁) (comap e P) = p then FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) else 0) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0
Tactic:
have : (P.comap e).comap (algebraMap R S₁) = p ↔ P.comap (algebraMap R S₂) = p := by
  rw [← Ideal.comap_coe e, Ideal.comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
State after:
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
⊢ (if hPp : comap (algebraMap R S₁) (comap e P) = p then FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) else 0) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

State before:
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
⊢ (if hPp : comap (algebraMap R S₁) (comap e P) = p then FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) else 0) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0
Tactic:
split
State after:
case isTrue
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
⊢ FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

case isFalse
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
⊢ 0 = if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

State before:
case isTrue
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
⊢ FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

case isFalse
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
⊢ 0 = if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0
Tactic:
swap
State after:
case isFalse
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
⊢ 0 = if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

case isTrue
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
⊢ FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0

State before:
case isTrue
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
⊢ FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) =
    if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0
Tactic:
rw [dif_pos (this.mp ‹_›)]
State after:
case isTrue
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
⊢ FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) = FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P)

State before:
case isTrue
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
⊢ FiniteDimensional.finrank (R ⧸ p) (S₁ ⧸ comap e P) = FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P)
Tactic:
apply (config := { allowSynthFailures := true }) LinearEquiv.finrank_eq
State after:
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
⊢ (S₁ ⧸ comap e P) ≃ₗ[R ⧸ p] S₂ ⧸ P

State before:
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
⊢ (S₁ ⧸ comap e P) ≃ₗ[R ⧸ p] S₂ ⧸ P
Tactic:
have E := quotientEquivAlg (R₁ := R) (P.comap e) P e
  (Ideal.map_comap_of_surjective _ e.surjective P).symm
State after:
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

State before:
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
Tactic:
apply (config := {allowSynthFailures := true }) LinearEquiv.mk
State after:
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

State before:
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 { toAddHom := E.toLinearMap.toAddHom, map_smul' := ⋯ }.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 { toAddHom := E.toLinearMap.toAddHom, map_smul' := ⋯ }.toFun

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
Tactic:
exact E.left_inv
State after:
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 E.invFun { toAddHom := E.toLinearMap.toAddHom, map_smul' := ⋯ }.toFun

State before:
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 E.invFun { toAddHom := E.toLinearMap.toAddHom, map_smul' := ⋯ }.toFun
Tactic:
exact E.right_inv
State after:
no goals

State before:
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
⊢ comap (algebraMap R S₁) (comap e P) = p ↔ comap (algebraMap R S₂) P = p
Tactic:
rw [← Ideal.comap_coe e, Ideal.comap_comap, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
State after:
no goals

State before:
case isFalse
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
⊢ 0 = if hPp : comap (algebraMap R S₂) P = p then FiniteDimensional.finrank (R ⧸ p) (S₂ ⧸ P) else 0
Tactic:
rw [dif_neg]
State after:
case isFalse.hnc
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
⊢ ¬comap (algebraMap R S₂) P = p

State before:
case isFalse.hnc
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
⊢ ¬comap (algebraMap R S₂) P = p
Tactic:
rwa [← this]
State after:
no goals

State before:
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
Tactic:
apply (config := {allowSynthFailures := true }) LinearMap.mk
State after:
case map_smul'
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
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), ?toAddHom.toFun (m • x) = (RingHom.id (R ⧸ p)) m • ?toAddHom.toFun x

case toAddHom
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
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)

State before:
case map_smul'
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
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), ?toAddHom.toFun (m • x) = (RingHom.id (R ⧸ p)) m • ?toAddHom.toFun x

case toAddHom
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
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)
Tactic:
swap
State after:
case toAddHom
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
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)

case map_smul'
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
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), ?toAddHom.toFun (m • x) = (RingHom.id (R ⧸ p)) m • ?toAddHom.toFun x

State before:
case toAddHom
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
⊢ AddHom (S₁ ⧸ comap e P) (S₂ ⧸ P)
Tactic:
exact E.toLinearMap.toAddHom
State after:
no goals

State before:
case map_smul'
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
⊢ ∀ (m : R ⧸ p) (x : S₁ ⧸ comap e P), E.toLinearMap.toFun (m • x) = (RingHom.id (R ⧸ p)) m • E.toLinearMap.toFun x
Tactic:
intro r x
State after:
case map_smul'
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
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E.toLinearMap.toFun (r • x) = (RingHom.id (R ⧸ p)) r • E.toLinearMap.toFun x

State before:
case map_smul'
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
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E.toLinearMap.toFun (r • x) = (RingHom.id (R ⧸ p)) r • E.toLinearMap.toFun x
Tactic:
show E (_ * _) = _ * (E x)
State after:
case map_smul'
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
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) r * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) r) * E x

State before:
case map_smul'
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
r : R ⧸ p
x : S₁ ⧸ comap e P
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) r * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) r) * E x
Tactic:
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
State after:
case map_smul'.intro
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
x : S₁ ⧸ comap e P
r : R
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) ((Quotient.mk p) r) * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) ((Quotient.mk p) r)) * E x

State before:
case map_smul'.intro
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
x : S₁ ⧸ comap e P
r : R
⊢ E ((Quotient.lift p ((Quotient.mk (comap e P)).comp (algebraMap R S₁)) ⋯) ((Quotient.mk p) r) * x) =
    (Quotient.lift p ((Quotient.mk P).comp (algebraMap R S₂)) ⋯) ((RingHom.id (R ⧸ p)) ((Quotient.mk p) r)) * E x
Tactic:
simp only [Quotient.mk_comp_algebraMap, Quotient.lift_mk, _root_.map_mul, AlgEquiv.commutes,
  RingHomCompTriple.comp_apply]
State after:
no goals