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

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

Tactic:
by_cases h_1 : x = 0

Result:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : x = 0
⊢ x ∈ B

case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
⊢ x ∈ B

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

Tactic:
intro h x hx

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

Proof state:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False

Tactic:
exact not_lt.2 (monotone_mapOfLE _ _ h (not_lt.1 h_1)) hx

Result:
no goals

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

Tactic:
rw [add_eq_zero_iff_eq_neg, inv_eq_iff_eq_inv, inv_neg, inv_one] at h_2

Result:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x = -1
⊢ x ∈ B

Proof state:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx✝¹ : ¬A.valuation x⁻¹ < 1
hx✝ : ¬A.valuation (x⁻¹ + 1 - 1) < 1
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
hx : Units.mk0 (x⁻¹ + 1) h_2 ∉ A.principalUnitGroup
⊢ Units.mk0 (x⁻¹ + 1) h_2 ∉ B.principalUnitGroup

Tactic:
simpa only [hx] using @h (Units.mk0 (x⁻¹ + 1) h_2)

Result:
no goals

Proof state:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
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
⊢ A ≤ B → B.principalUnitGroup ≤ A.principalUnitGroup

Tactic:
intro h x hx

Result:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
⊢ x ∈ A.principalUnitGroup

Proof state:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x = -1
⊢ x ∈ B

Tactic:
simpa only [h_2] using B.neg_mem _ B.one_mem

Result:
no goals

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

Tactic:
by_contra h_1

Result:
case mpr
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : A ≤ B
x : Kˣ
hx : x ∈ B.principalUnitGroup
h_1 : x ∉ A.principalUnitGroup
⊢ False

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

Tactic:
constructor

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

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

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

Tactic:
rw [← valuation_le_one_iff, ← not_lt, Valuation.one_lt_val_iff _ h_1,
  ← add_sub_cancel_right x⁻¹, ← Units.val_mk0 h_2, ← mem_principalUnitGroup_iff] at hx ⊢

Result:
case neg
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx✝¹ : ¬A.valuation x⁻¹ < 1
hx✝ : ¬A.valuation (x⁻¹ + 1 - 1) < 1
h_1 : ¬x = 0
h_2 : ¬x⁻¹ + 1 = 0
hx : Units.mk0 (x⁻¹ + 1) h_2 ∉ A.principalUnitGroup
⊢ Units.mk0 (x⁻¹ + 1) h_2 ∉ B.principalUnitGroup

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

Tactic:
by_cases h_2 : x⁻¹ + 1 = 0

Result:
case pos
K : Type u
inst✝ : Field K
A B : ValuationSubring K
h : B.principalUnitGroup ≤ A.principalUnitGroup
x : K
hx : x ∈ A
h_1 : ¬x = 0
h_2 : x⁻¹ + 1 = 0
⊢ x ∈ B

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