awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ
hx : 0 ≤ x
rw : (x * y⁻¹).toNNReal = x.toNNReal / y.toNNReal
rw₁ : (x * y⁻¹).toNNReal = x.toNNReal * y.toNNReal⁻¹
rw₂ : (x * y⁻¹).toNNReal = x.toNNReal * y⁻¹.toNNReal
rw₃ rw₄ : (x * y⁻¹).toNNReal = (x * y⁻¹).toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]

Premises used: Real.toNNReal_mul, Real.toNNReal_inv, div_eq_mul_inv
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ
hy : 0 ≤ y
rw : (y⁻¹ * x).toNNReal = x.toNNReal / y.toNNReal
rw₁ : (y⁻¹ * x).toNNReal = y.toNNReal⁻¹ * x.toNNReal
rw₂ : y⁻¹.toNNReal * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
rw₃ rw₄ : y.toNNReal⁻¹ * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
rw [div_eq_inv_mul, div_eq_inv_mul, Real.toNNReal_mul (inv_nonneg.2 hy), Real.toNNReal_inv]

Premises used: Iff.mpr, Real.toNNReal_mul, Real.toNNReal_inv, inv_nonneg, div_eq_inv_mul
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ≥0
hx : x ≠ 0
rw : 1 / x < 1 ↔ 1 < x
rw₁ : 1 < 1 * x ↔ 1 < x
rw₂ rw₃ : 1 < x ↔ 1 < x
⊢ x⁻¹ < 1 ↔ 1 < x

Tactic:
rw [← one_div, div_lt_iff₀ hx.bot_lt, one_mul]

Premises used: div_lt_iff₀, one_div, one_mul, Ne.bot_lt
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ≥0
hx : x ≠ 0
h : x < y
⊢ y⁻¹ < x⁻¹

Tactic:
inv_strictAnti₀ hx.bot_lt h

Premises used: inv_strictAnti₀, Ne.bot_lt
-- Module: Mathlib.Data.NNReal.Defs
Goal:
b : ℝ≥0
hb : 0 < b
⊢ ∃ (n : ℕ), 0 < n ∧ (↑n : ℝ≥0)⁻¹ < b

Tactic:
b.toReal.exists_nat_pos_inv_lt hb

Premises used: Real.exists_nat_pos_inv_lt, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ≥0
⊢ |(↑x : ℝ)| = (↑x : ℝ)

Tactic:
abs_of_nonneg x.property

Premises used: abs_of_nonneg, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ≥0
y : ℝ
h : (↑x : ℝ) ≤ y
⊢ x ≤ y.toNNReal

Tactic:
(le_toNNReal_iff_coe_le <| x.2.trans h).2 h

Premises used: Iff.mpr, Real.le_toNNReal_iff_coe_le, LE.le.trans, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ≥0
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
grind [csSup_of_not_bddAbove, csSup_empty, bot_eq_zero']

Premises used: csSup_empty, csSup_of_not_bddAbove, bot_eq_zero'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_1
f : ι → ℝ≥0
hf : ¬BddAbove (range f)
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0

Tactic:
sSup_of_not_bddAbove hf

Premises used: iSup, NNReal.sSup_of_not_bddAbove
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ≥0
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0

Tactic:
ciSup_of_empty f

Premises used: ciSup_of_empty
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_1
inst : IsEmpty ι
f : ι → ℝ≥0
rw : Eq (α := ℝ≥0) (sInf ∅) 0
rw₁ rw₂ : Eq (α := ℝ≥0) 0 0
⊢ Eq (α := ℝ≥0) (⨅ (i : ι), f i) 0

Tactic:
rw [_root_.iInf_of_isEmpty, sInf_empty]

Premises used: iInf_of_isEmpty, NNReal.sInf_empty
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
inl : IsEmpty ι → (Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0)
inr : Nonempty ι → (Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0)
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h : IsEmpty ι
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
ι : Sort u_1
f : ι → ℝ≥0
hf : BddAbove (range f)
h : Nonempty ι
⊢ Eq (α := ℝ≥0) (⨆ (i : ι), f i) 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp [← bot_eq_zero', ← le_bot_iff, ciSup_le_iff hf]

Premises used: le_bot_iff, ciSup_le_iff, bot_eq_zero'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
α : Sort u_2
rw : ⨅ (i : α), (↑0 : ℝ) = (↑0 : ℝ)
⊢ Eq (α := ℝ≥0) (⨅ (x : α), 0) 0

Tactic:
rw [← coe_inj, coe_iInf]

Premises used: NNReal.coe_iInf, NNReal.coe_inj
-- Module: Mathlib.Data.NNReal.Defs
Goal:
α : Sort u_2
⊢ ⨅ (i : α), (↑0 : ℝ) = (↑0 : ℝ)

Tactic:
Real.iInf_const_zero

Premises used: Real.iInf_const_zero, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
α : Sort u_2
⊢ ⨅ (i : α), (↑0 : ℝ) = (↑0 : ℝ)

Tactic:
exact Real.iInf_const_zero

Premises used: Real.iInf_const_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
⊢ (toReal ⁻¹' s).OrdConnected

Tactic:
h.preimage_mono NNReal.coe_mono

Premises used: NNReal.coe_mono, Set.OrdConnected.preimage_mono
-- Module: Mathlib.Data.NNReal.Defs
Goal:
t : Set ℝ≥0
h : t.OrdConnected
⊢ (toReal '' t).OrdConnected

Tactic:
⟨forall_mem_image.2 fun x hx =>
      forall_mem_image.2 fun _y hy z hz => ⟨⟨z, x.2.trans hz.1⟩, h.out hx hy hz, rfl⟩⟩

Premises used: Iff.mpr, Set.OrdConnected.out, Subtype.mk, Set.OrdConnected.mk, And.left, And.intro, Exists.intro, LE.le.trans, Set.forall_mem_image, rfl, Subtype.property
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
⊢ (toNNReal '' s).OrdConnected

Tactic:
⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩

Premises used: Iff.mpr, Set.OrdConnected.mk, Set.forall_mem_image
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
refine : ∀ (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s) (z : ℝ≥0) (hz : z ∈ Icc x.toNNReal y.toNNReal), z ∈ toNNReal '' s
⊢ (toNNReal '' s).OrdConnected

Tactic:
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
inl : ∀ (hy₀ : y ≤ 0), z ∈ toNNReal '' s
inr : ∀ (hy₀ : 0 ≤ y), z ∈ toNNReal '' s
⊢ z ∈ toNNReal '' s

Tactic:
rcases le_total y 0 with hy₀ | hy₀

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
⊢ x.toNNReal ≤ z ∧ z = 0

Tactic:
rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz

Premises used: Real.toNNReal_of_nonpos, Set.mem_Icc, nonpos_iff_eq_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : y ≤ 0
hz₁ : x.toNNReal ≤ z ∧ z = 0
⊢ y ≤ 0

Tactic:
rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz

Premises used: Real.toNNReal_of_nonpos, Set.mem_Icc, nonpos_iff_eq_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Tactic:
⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩

Premises used: Set.Mem, setOf, Real.toNNReal_of_nonpos, And.right, And.intro, Exists.intro, Set.image, Eq.symm, Eq.trans
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Tactic:
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : 0 ≤ y
⊢ 0 ≤ y

Tactic:
hy₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : z ∈ Icc x.toNNReal y.toNNReal
hy₀ : 0 ≤ y
inr : ∀ (y : ℝ≥0) (hy : (↑y : ℝ) ∈ s) (hz : z ∈ Icc x.toNNReal (↑y : ℝ).toNNReal), z ∈ toNNReal '' s
⊢ z ∈ toNNReal '' s

Tactic:
lift y to ℝ≥0 using hy₀
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : (↑y : ℝ) ∈ s
hz : z ∈ Icc x.toNNReal (↑y : ℝ).toNNReal
⊢ z ∈ Icc x.toNNReal y

Tactic:
rw [toNNReal_coe] at hz

Premises used: Real.toNNReal_coe
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : (↑y : ℝ) ∈ s
hz : z ∈ Icc x.toNNReal y
⊢ z ∈ toNNReal '' s

Tactic:
⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩

Premises used: Set.Mem, setOf, Set.OrdConnected.out, And.right, And.left, And.intro, Exists.intro, Iff.mp, Real.toNNReal_coe, Set.image, Real.toNNReal_le_iff_le_coe, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
z y : ℝ≥0
hy : (↑y : ℝ) ∈ s
hz : z ∈ Icc x.toNNReal y
⊢ z ∈ toNNReal '' s

Tactic:
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩
-- Module: Mathlib.Data.NNReal.Defs
Goal:
t : Set ℝ≥0
h : t.OrdConnected
⊢ (toNNReal ⁻¹' t).OrdConnected

Tactic:
h.preimage_mono Real.toNNReal_monotone

Premises used: Real.toNNReal_monotone, Set.OrdConnected.preimage_mono
-- Module: Mathlib.Data.NNReal.Defs
Goal:
simp : Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 0 ⋯) 0
⊢ Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |0| ⋯) 0

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 0 ⋯) 0

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
simp : Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 1 ⋯) 1
⊢ Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |1| ⋯) 1

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
⊢ Eq (α := ℝ≥0) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) 1 ⋯) 1

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ
simp :
  Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (|x| * |y|) ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x| ⋯ * Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |y| ⋯
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x * y| ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x| ⋯ * Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |y| ⋯

Tactic:
simp [abs_mul]

Premises used: abs_mul
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x y : ℝ
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (|x| * |y|) ⋯ =
    Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |x| ⋯ * Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |y| ⋯

Tactic:
rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
⊢ (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = |x|

Tactic:
rfl

Premises used: abs, NNReal.toReal, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
h : 0 ≤ x
a : (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = (↑x.toNNReal : ℝ)
⊢ (nnabs : (a : ℝ) → ℝ≥0) x = x.toNNReal

Tactic:
ext
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
h : 0 ≤ x
a : (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = x
a₁ : |x| = x
a₂ a₃ : x = x
⊢ (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ) = (↑x.toNNReal : ℝ)

Tactic:
rw [coe_toNNReal x h, coe_nnabs, abs_of_nonneg h]

Premises used: Real.coe_nnabs, Real.coe_toNNReal, abs_of_nonneg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ≥0
⊢ (nnabs : (a : ℝ) → ℝ≥0) (↑x : ℝ) = x

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
⊢ (↑x.toNNReal : ℝ) ≤ |x|

Tactic:
max_le (le_abs_self _) (abs_nonneg _)

Premises used: le_abs_self, max_le, abs_nonneg, NNReal.toReal
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
⊢ (↑|x|.toNNReal : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) x) : ℝ)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
⊢ Eq (α := ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) (↑n : ℝ≥0)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ Eq (α := ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
simp
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℤ
a : (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
⊢ Eq (α := ℝ≥0) (↑n.natAbs : ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ))

Tactic:
ext
-- Module: Mathlib.Data.NNReal.Defs
Goal:
n : ℤ
a : (↑n.natAbs : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
a₁ : (↑|n| : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)
a₂ : Eq (α := ℝ) (↑|n| : ℝ) |(↑n : ℝ)|
a₃ a₄ : Eq (α := ℝ) |(↑n : ℝ)| |(↑n : ℝ)|
⊢ (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑((nnabs : (a : ℝ) → ℝ≥0) (↑n : ℝ)) : ℝ)

Tactic:
rw [NNReal.coe_natCast, Nat.cast_natAbs, Real.coe_nnabs, Int.cast_abs]

Premises used: Int.cast_abs, Nat.cast_natAbs, Real.coe_nnabs, NNReal.coe_natCast
-- Module: Mathlib.Data.NNReal.Defs
Goal:
x : ℝ
⊢ LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) x : ℝ≥0) ↔ x ≠ 0

Tactic:
simp [← NNReal.coe_pos]

Premises used: NNReal.coe_pos
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
⊢ 0 ≤ r ∨ 0 ≤ -r

Tactic:
simpa using le_total ..

Premises used: le_total
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
inl : ∀ (hr : 0 ≤ r), ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
inr : ∀ (hr : 0 ≤ -r), ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)

Tactic:
obtain (hr | hr) : 0 ≤ r ∨ 0 ≤ -r := by simpa using le_total ..
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ r
inl : ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)

Tactic:
rw [← neg_neg r]

Premises used: neg_neg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ r
inl : ∀ (r : ℝ≥0), ∃ (x : ℝ≥0), - -(↑r : ℝ) = (↑x : ℝ) ∨ - -(↑r : ℝ) = -(↑x : ℝ)
⊢ ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)

Tactic:
lift (_ : ℝ) to ℝ≥0 using hr with r
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r_1 : ℝ
r : ℝ≥0
⊢ ∃ (x : ℝ≥0), - -(↑r : ℝ) = (↑x : ℝ) ∨ - -(↑r : ℝ) = -(↑x : ℝ)

Tactic:
aesop
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ -r
inr : ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)
⊢ ∃ (x : ℝ≥0), r = (↑x : ℝ) ∨ r = -(↑x : ℝ)

Tactic:
rw [← neg_neg r]

Premises used: neg_neg
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ -r
⊢ 0 ≤ -r

Tactic:
hr
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
hr : 0 ≤ -r
inr : ∀ (r : ℝ≥0), ∃ (x : ℝ≥0), -(↑r : ℝ) = (↑x : ℝ) ∨ -(↑r : ℝ) = -(↑x : ℝ)
⊢ ∃ (x : ℝ≥0), - -r = (↑x : ℝ) ∨ - -r = -(↑x : ℝ)

Tactic:
lift (_ : ℝ) to ℝ≥0 using hr with r
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r_1 : ℝ
r : ℝ≥0
⊢ ∃ (x : ℝ≥0), -(↑r : ℝ) = (↑x : ℝ) ∨ -(↑r : ℝ) = -(↑x : ℝ)

Tactic:
aesop
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
obtain : ∀ (x : ℝ≥0) (hx : r = (↑x : ℝ) ∨ r = -(↑x : ℝ)), r = 0 ∨ ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))
⊢ r = 0 ∨ ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))

Tactic:
obtain ⟨x, hx⟩ := nnreal_dichotomy r

Premises used: Real.nnreal_dichotomy
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
x : ℝ≥0
hx : r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
rw : ¬r = 0 → ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))
⊢ r = 0 ∨ ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Data.NNReal.Defs
Goal:
r : ℝ
x : ℝ≥0
hx : r = (↑x : ℝ) ∨ r = -(↑x : ℝ)
⊢ ¬r = 0 → ∃ (x : ℝ≥0), 0 < x ∧ (r = (↑x : ℝ) ∨ r = -(↑x : ℝ))

Tactic:
aesop (add simp pos_iff_ne_zero)

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive (↑x : ℝ)
nonpos : ∀ (x : ℝ≥0), motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ
inl : ∀ (r : ℝ≥0), motive (↑r : ℝ)
inr : ∀ (r : ℝ≥0), motive (-(↑r : ℝ))
⊢ motive r

Tactic:
obtain ⟨r, (rfl | rfl)⟩ := r.nnreal_dichotomy

Premises used: Real.nnreal_dichotomy, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive (↑x : ℝ)
nonpos : ∀ (x : ℝ≥0), motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ≥0
⊢ motive (↑r : ℝ)

Tactic:
simp_all
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
nonneg : ∀ (x : ℝ≥0), motive (↑x : ℝ)
nonpos : ∀ (x : ℝ≥0), motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ≥0
⊢ motive (-(↑r : ℝ))

Tactic:
simp_all
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ)
neg : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ
inl : motive 0
inr : ∀ (r : ℝ≥0) (hr : 0 < r), motive (↑r : ℝ)
inr₁ : ∀ (r : ℝ≥0) (hr : 0 < r), motive (-(↑r : ℝ))
⊢ motive r

Tactic:
obtain rfl | ⟨r, hr, (rfl | rfl)⟩ := r.nnreal_trichotomy

Premises used: Real.nnreal_trichotomy, rfl
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ)
neg : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ) → motive (-(↑x : ℝ))
⊢ motive 0

Tactic:
simp_all
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ)
neg : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ≥0
hr : 0 < r
⊢ motive (↑r : ℝ)

Tactic:
simp_all
-- Module: Mathlib.Data.NNReal.Defs
Goal:
motive : ℝ → Prop
zero : motive 0
pos : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ)
neg : ∀ (x : ℝ≥0), 0 < x → motive (↑x : ℝ) → motive (-(↑x : ℝ))
r : ℝ≥0
hr : 0 < r
⊢ motive (-(↑r : ℝ))

Tactic:
simp_all
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
obtain : ∀ (g : Γ₀ˣ) (hg1 : g ≠ 1), ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r

Tactic:
obtain ⟨g, hg1⟩ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mp h

Premises used: nontrivial_iff_exists_ne, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
⊢ let u := if g < 1 then g else g⁻¹;
  u = if g < 1 then g else g⁻¹

Tactic:
set u : Γ₀ˣ := if g < 1 then g else g⁻¹ with hu
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
rw : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑(if g < 1 then g else g⁻¹) : Γ₀) : ℝ≥0) (1 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)

Tactic:
rw [hu]
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
pos : ∀ (hu1 : g < 1), LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (1 : ℝ≥0)
neg : ∀ (hu1 : ¬g < 1), LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g⁻¹ : Γ₀) : ℝ≥0) (1 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑(if g < 1 then g else g⁻¹) : Γ₀) : ℝ≥0) (1 : ℝ≥0)

Tactic:
split_ifs with hu1
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
pos : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (1 : ℝ≥0)

Tactic:
rw [← map_one f]

Premises used: map_one
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0)

Tactic:
hf hu1
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0)

Tactic:
exact hf hu1
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
⊢ Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)

Tactic:
have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
⊢ 1 < g

Tactic:
have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
hg1' : 1 < g
neg : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g⁻¹ : Γ₀) : ℝ≥0) (1 : ℝ≥0)

Tactic:
rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]

Premises used: Units.val_inv_eq_inv_val, map_inv₀, map_one, NNReal.inv_lt_one_iff
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
hg1' : 1 < g
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0)

Tactic:
hf hg1'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : Ne (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0) (0 : ℝ≥0)
hg1' : 1 < g
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) 1 : ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑g : Γ₀) : ℝ≥0)

Tactic:
exact hf hg1'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
⊢ LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)

Tactic:
have hfu : f u < 1 := by
    rw [hu]
    split_ifs with hu1
    · rw [← map_one f]; exact hf hu1
    · have hfg0 : f g ≠ 0 :=
        fun h0 ↦ (Units.ne_zero g) ((map_eq_zero f).mp h0)
      have hg1' : 1 < g := lt_of_le_of_ne (not_lt.mp hu1) hg1.symm
      rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]
      exact hf hg1'
-- Module: Mathlib.Data.NNReal.Defs
Goal:
Γ₀ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial.{u_1} Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono (α := Γ₀) (β := ℝ≥0) (⇑f : (a : Γ₀) → ℝ≥0)
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hfu : LT.lt (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) (1 : ℝ≥0)
obtain :
  ∀ (n : ℕ) (hn : HPow.hPow (α := ℝ≥0) ((f : (a : Γ₀) → ℝ≥0) (↑u : Γ₀) : ℝ≥0) n < r),
    ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r
⊢ ∃ (d : Γ₀ˣ), (f : (a : Γ₀) → ℝ≥0) (↑d : Γ₀) < r

Tactic:
obtain ⟨n, hn⟩ := exists_pow_lt_of_lt_one hr hfu

Premises used: NNReal.exists_pow_lt_of_lt_one