internlm/Lean-Github huggingface dataset:
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
Tactic:
use v
Proof state after:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∀ (r : R), r ≠ 0 → r • v ∉ N
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
⊢ ∀ (r : R), r ≠ 0 → r • v ∉ N
Tactic:
intro r hr
Proof state after:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
⊢ r • v ∉ N
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
⊢ r • v ∉ N
Tactic:
have := linearIndependent_iff.mp hs' (Finsupp.single ⟨_, hv⟩ r)
Proof state after:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this :
  (Finsupp.total { x // x ∈ s } (M ⧸ N) R Subtype.val) (Finsupp.single ⟨N.mkQ v, hv⟩ r) = 0 →
    Finsupp.single ⟨N.mkQ v, hv⟩ r = 0
⊢ r • v ∉ N
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this :
  (Finsupp.total { x // x ∈ s } (M ⧸ N) R Subtype.val) (Finsupp.single ⟨N.mkQ v, hv⟩ r) = 0 →
    Finsupp.single ⟨N.mkQ v, hv⟩ r = 0
⊢ r • v ∉ N
Tactic:
rw [Finsupp.total_single, Finsupp.single_eq_zero, ← LinearMap.map_smul,
  Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at this
Proof state after:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this : r • v ∈ N → r = 0
⊢ r • v ∉ N
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
case h
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
v : M
hv : N.mkQ v ∈ s
r : R
hr : r ≠ 0
this : r • v ∈ N → r = 0
⊢ r • v ∉ N
Tactic:
exact mt this hr
Proof state after:
no goals
Theorem: FiniteDimensional.exists_of_finrank_lt
Proof state before:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : Nontrivial R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
N✝ : Submodule R M
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ s.Nonempty
Tactic:
rwa [Finset.nonempty_iff_ne_empty, ne_eq, ← Finset.card_eq_zero, hs,
  FiniteDimensional.finrank_quotient, tsub_eq_zero_iff_le, not_le]
Proof state after:
no goals
Theorem: Ideal.ramificationIdx_comap_eq
Proof 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₂
⊢ ramificationIdx (algebraMap R S₁) p (comap e P) = ramificationIdx (algebraMap R S₂) p P
Tactic:
show sSup _ = sSup _
Proof 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₂
⊢ sSup {n | map (algebraMap R S₁) p ≤ comap e P ^ n} = sSup {n | map (algebraMap R S₂) p ≤ P ^ n}
Theorem: Ideal.ramificationIdx_comap_eq
Proof 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₂
⊢ sSup {n | map (algebraMap R S₁) p ≤ comap e P ^ n} = sSup {n | map (algebraMap R S₂) p ≤ P ^ n}
Tactic:
congr
Proof state after:
case e_a
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₂
⊢ {n | map (algebraMap R S₁) p ≤ comap e P ^ n} = {n | map (algebraMap R S₂) p ≤ P ^ n}
Theorem: Ideal.ramificationIdx_comap_eq
Proof state before:
case e_a
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₂
⊢ {n | map (algebraMap R S₁) p ≤ comap e P ^ n} = {n | map (algebraMap R S₂) p ≤ P ^ n}
Tactic:
ext n
Proof state after:
case e_a.h
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₂
n : ℕ
⊢ n ∈ {n | map (algebraMap R S₁) p ≤ comap e P ^ n} ↔ n ∈ {n | map (algebraMap R S₂) p ≤ P ^ n}
Theorem: Ideal.ramificationIdx_comap_eq
Proof state before:
case e_a.h
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₂
n : ℕ
⊢ n ∈ {n | map (algebraMap R S₁) p ≤ comap e P ^ n} ↔ n ∈ {n | map (algebraMap R S₂) p ≤ P ^ n}
Tactic:
simp only [Set.mem_setOf_eq, Ideal.map_le_iff_le_comap]
Proof state after:
case e_a.h
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₂
n : ℕ
⊢ p ≤ comap (algebraMap R S₁) (comap e P ^ n) ↔ p ≤ comap (algebraMap R S₂) (P ^ n)
Theorem: Ideal.ramificationIdx_comap_eq
Proof state before:
case e_a.h
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₂
n : ℕ
⊢ p ≤ comap (algebraMap R S₁) (comap e P ^ n) ↔ p ≤ comap (algebraMap R S₂) (P ^ n)
Tactic:
rw [← Ideal.comap_coe e, ← e.toRingEquiv_toRingHom, Ideal.comap_coe,
  ← RingEquiv.symm_symm (e : S₁ ≃+* S₂), ← Ideal.map_comap_of_equiv, ← Ideal.map_pow,
  Ideal.map_comap_of_equiv, ← Ideal.comap_coe (RingEquiv.symm _), Ideal.comap_comap,
  RingEquiv.symm_symm, e.toRingEquiv_toRingHom, ← e.toAlgHom_toRingHom, AlgHom.comp_algebraMap]
Proof state after:
no goals
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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]
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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 ‹_›)]
Proof 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)
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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
Proof state after:
no goals
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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]
Proof state after:
no goals
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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]
Proof 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
Theorem: Ideal.inertiaDeg_comap_eq
Proof 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]
Proof state after:
no goals