-- Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
theorem RingEquivClass.isDiscreteValuationRing {A B E : Type*} [CommRing A] [IsDomain A]
    [CommRing B] [IsDomain B] [IsDiscreteValuationRing A] [EquivLike E A B] [RingEquivClass E A B]
    (e : E) : IsDiscreteValuationRing B where
  principal := (isPrincipalIdealRing_iff _).1 <|
    IsPrincipalIdealRing.of_surjective _ (e : A ≃+* B).surjective
  __ : IsLocalRing B := (e : A ≃+* B).isLocalRing
  not_a_field'

Proof state:
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ e ↑a ≠ 0

Tactic:
simp only [ne_eq, EmbeddingLike.map_eq_zero_iff, ZeroMemClass.coe_eq_zero,
ha, not_false_eq_true]

Result:
no goals

Proof state:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ↑a ∈ maximalIdeal A

Tactic:
exact a.2

Result:
no goals

Proof state:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ maximalIdeal B ≠ ⊥

Tactic:
rw [Submodule.ne_bot_iff]

Result:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ∃ x ∈ maximalIdeal B, x ≠ 0

Proof state:
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
⊢ maximalIdeal B ≠ ⊥

Tactic:
obtain ⟨a, ha⟩ := Submodule.nonzero_mem_of_bot_lt (bot_lt_iff_ne_bot.mpr
  <| IsDiscreteValuationRing.not_a_field A)

Result:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ maximalIdeal B ≠ ⊥

Proof state:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ∃ x ∈ maximalIdeal B, x ≠ 0

Tactic:
refine ⟨e a, ⟨?_, by simp only [ne_eq, EmbeddingLike.map_eq_zero_iff, ZeroMemClass.coe_eq_zero,
  ha, not_false_eq_true]⟩⟩

Result:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ e ↑a ∈ maximalIdeal B

Proof state:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ e ↑a ∈ maximalIdeal B

Tactic:
rw [IsLocalRing.mem_maximalIdeal, map_mem_nonunits_iff e, ← IsLocalRing.mem_maximalIdeal]

Result:
case intro
A : Type u_2
B : Type u_3
E : Type u_4
inst✝⁶ : CommRing A
inst✝⁵ : IsDomain A
inst✝⁴ : CommRing B
inst✝³ : IsDomain B
inst✝² : IsDiscreteValuationRing A
inst✝¹ : EquivLike E A B
inst✝ : RingEquivClass E A B
e : E
a : ↥(maximalIdeal A)
ha : a ≠ 0
⊢ ↑a ∈ maximalIdeal A