-- Mathlib/RingTheory/Valuation/ValuationSubring.lean
theorem unitGroup_le_unitGroup {A B : ValuationSubring K} : A.unitGroup ≤ B.unitGroup ↔ A ≤ B

Proof state:
case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
this : Units.mk0 x h_1 ∈ B.unitGroup
⊢ x ∈ B

Tactic:
exact SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B)

Result:
no goals

Proof state:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
h_2 : 1 + x = 0
⊢ x ∈ B

Tactic:
simp only [← add_eq_zero_iff_neg_eq.1 h_2, neg_mem _ _ (one_mem _)]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup ↔ A ≤ B

Tactic:
constructor

Result:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup → A ≤ B

case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → A.unitGroup ≤ B.unitGroup

Proof state:
case neg.inl
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x < 1
this : Units.mk0 (1 + x) h_2 ∈ B.unitGroup
⊢ x ∈ B

Tactic:
simpa using
  B.add_mem _ _ (show 1 + x ∈ B from SetLike.coe_mem (B.unitGroupMulEquiv ⟨_, this⟩ : B))
    (B.neg_mem _ B.one_mem)

Result:
no goals

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A ≤ B → A.unitGroup ≤ B.unitGroup

Tactic:
rintro h x (hx : A.valuation x = 1)

Result:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : A.valuation ↑x = 1
⊢ x ∈ B.unitGroup

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : A.valuation ↑x = 1
⊢ x ∈ B.unitGroup

Tactic:
apply_fun A.mapOfLE B h at hx

Result:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : (A.mapOfLE B h) (A.valuation ↑x) = (A.mapOfLE B h) 1
⊢ x ∈ B.unitGroup

Proof state:
case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
⊢ x ∈ B

Tactic:
have := h (show Units.mk0 x h_1 ∈ A.unitGroup from hx)

Result:
case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
this : Units.mk0 x h_1 ∈ B.unitGroup
⊢ x ∈ B

Proof state:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
⊢ A.unitGroup ≤ B.unitGroup → A ≤ B

Tactic:
intro h x hx

Result:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : x ∈ A
⊢ x ∈ B

Proof state:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B

Tactic:
by_cases h_2 : 1 + x = 0

Result:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
h_2 : 1 + x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
⊢ x ∈ B

Proof state:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : x ∈ A
⊢ x ∈ B

Tactic:
rw [← A.valuation_le_one_iff x, le_iff_lt_or_eq] at hx

Result:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
⊢ x ∈ B

Proof state:
case neg.inl
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x < 1
⊢ x ∈ B

Tactic:
have := h (show Units.mk0 _ h_2 ∈ A.unitGroup from A.valuation.map_one_add_of_lt hx)

Result:
case neg.inl
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x < 1
this : Units.mk0 (1 + x) h_2 ∈ B.unitGroup
⊢ x ∈ B

Proof state:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : x = 0
⊢ x ∈ B

Tactic:
simp only [h_1, zero_mem]

Result:
no goals

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : (A.mapOfLE B h) (A.valuation ↑x) = (A.mapOfLE B h) 1
⊢ x ∈ B.unitGroup

Tactic:
simpa using hx

Result:
no goals

Proof state:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
⊢ x ∈ B

Tactic:
rcases hx with hx | hx

Result:
case neg.inl
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x < 1
⊢ x ∈ B

case neg.inr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
h_1 : ¬x = 0
h_2 : ¬1 + x = 0
hx : A.valuation x = 1
⊢ x ∈ B

Proof state:
case mp
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
⊢ x ∈ B

Tactic:
by_cases h_1 : x = 0

Result:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A.unitGroup ≤ B.unitGroup
x : K
hx : A.valuation x < 1 ∨ A.valuation x = 1
h_1 : ¬x = 0
⊢ x ∈ B