diff --git a/OrderedSemigroups/OrderedGroup/Basic.lean b/OrderedSemigroups/OrderedGroup/Basic.lean index 958973f..d6810ca 100644 --- a/OrderedSemigroups/OrderedGroup/Basic.lean +++ b/OrderedSemigroups/OrderedGroup/Basic.lean @@ -88,7 +88,7 @@ theorem pos_arch {x y : α} (pos_x : 1 < x) (pos_y : 1 < y) : we have a least z such that x^z > y. -/ theorem pos_min_arch {x y : α} (arch : archimedean_group α) (pos_x : 1 < x) (pos_y : 1 < y) : - ∃z : ℤ, x^z > y ∧ z > 0 ∧ (∀t : ℤ, x^t > y → z ≤ t) := by + ∃z : ℤ, x^z > y ∧ (∀t : ℤ, x^t > y → z ≤ t) := by -- Define predicate for numbers satisfying x^n > y let P : ℕ → Prop := fun n => x^(n : ℤ) > y @@ -117,8 +117,6 @@ theorem pos_min_arch {x y : α} (arch : archimedean_group α) (pos_x : 1 < x) (p have hz₀ := Nat.find_spec exists_P -- x^z₀ > y constructor · exact hz₀ -- x^z₀ > y - constructor - · exact_mod_cast pos_arch pos_x pos_y z₀ hz₀ -- z₀ > 0 · -- For all t, if x^t > y, then z₀ ≤ t -- t < z₀, but x^t > y, so t ∈ S and t < z₀, contradicting minimality of z₀ intro t ht @@ -152,7 +150,7 @@ theorem neg_case_left_arch_false {g h : α} (arch : is_archimedean (α := α)) ( (conj_lt_one : h * g * h⁻¹ < 1) : False := by simp [←arch_group_semigroup] at arch have pos_hinv : 1 < h⁻¹ := one_lt_inv_of_inv neg_h - obtain ⟨z, gz_gt_hinv, _, z_maximum⟩ := pos_min_arch arch pos_g pos_hinv + obtain ⟨z, gz_gt_hinv, z_maximum⟩ := pos_min_arch arch pos_g pos_hinv have hinv_lt : h⁻¹ < g⁻¹ * h⁻¹ := by have : h⁻¹ * (h * g * h⁻¹) < h⁻¹ * 1 := mul_lt_mul_left' conj_lt_one (h⁻¹) simp [mul_assoc] at this @@ -200,7 +198,7 @@ theorem left_arch_ordered (arch : is_archimedean (α := α)) : rcases pos_h.eq_or_lt with h_eq_one | neg_h -- The case where `h = 1` · simp [h_eq_one] at * - exact (lt_self_iff_false 1).mp (lt_imp_lt_of_le_imp_le (fun a ↦ not_pos_conj) pos_g) + exact (lt_self_iff_false 1).mp (lt_imp_lt_of_le_imp_le (fun _ ↦ not_pos_conj) pos_g) -- The case where `h` is in the negative cone · exact False.elim (neg_case_left_arch_false arch pos_g neg_h conj_lt_one) case pos =>