awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)
hqa' : (↑q' : α) < a
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (ha : 0 < a) (hb : 0 ≤ b) (hq : 0 < q) (hqa : (↑(q * q) : β) < inducedMap α β a * inducedMap α β a) (hq' : q < q'),
    q < q'
⊢ LT.lt.{u_2} (α := α) (↑q : α) (↑q' : α)

Tactic:
assumption_mod_cast
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
α : Type u_2
β : Type u_3
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Archimedean α
a : α
ha : 0 < a
b : β
hba : b < inducedMap α β a * inducedMap α β a
hb : 0 ≤ b
q : ℚ
hq : 0 < q
hbq : b < (↑(HPow.hPow (β := ℕ) q 2) : β)
hqa : HMul.hMul (α := β) (↑q : β) (↑q : β) < inducedMap α β a * inducedMap α β a
q' : ℚ
hq' : LT.lt.{u_3} (α := β) (↑q : β) (↑q' : β)
hqa' : (↑q' : α) < a
⊢ HMul.hMul (α := α) (↑q : α) (↑q : α) < a * a

Tactic:
exact mul_self_lt_mul_self (mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)

Premises used: LT.lt.trans', mul_self_lt_mul_self
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
inl :
  ∀ (h : x < 0),
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
inr :
  (inducedAddHom α β : (a : α) → β) (HMul.hMul (α := α) 0 0) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) 0 : β) ((inducedAddHom α β : (a : α) → β) 0 : β)
inr₁ :
  ∀ (h : 0 < x),
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
obtain h | rfl | h := lt_trichotomy x 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
⊢ (inducedAddHom α β : (a : α) → β) (-x * -x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
      ((inducedAddHom α β : (a : α) → β) (-x) : β)

Tactic:
this (-x) (neg_pos.2 h)

Premises used: Iff.mpr, neg_pos, Neg.neg
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)
h₂ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
      ((inducedAddHom α β : (a : α) → β) (-x) : β)
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
convert! this (-x) (neg_pos.2 h) using 1

Premises used: Iff.mpr, neg_pos, Neg.neg
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-(x * -x)) : β)
h₂ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (- -(x * x)) : β)
h₃ h₄ :
  Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
⊢ Eq.{u_3 + 1} (α := β) ((inducedAddHom α β : (a : α) → β) (x * x) : β)
    ((inducedAddHom α β : (a : α) → β) (-x * -x) : β)

Tactic:
rw [neg_mul, mul_neg, neg_neg]

Premises used: neg_neg, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : x < 0
h₁ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) (-(inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
h₂ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    -HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) (-(inducedAddHom α β : (a : α) → β) x : β)
h₃ :
  HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    - -HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
⊢ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) (-x) : β)
      ((inducedAddHom α β : (a : α) → β) (-x) : β)

Tactic:
simp_rw [map_neg, neg_mul, mul_neg, neg_neg]

Premises used: neg_neg, map_neg, neg_mul, mul_neg
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
⊢ (inducedAddHom α β : (a : α) → β) (HMul.hMul (α := α) 0 0) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) 0 : β) ((inducedAddHom α β : (a : α) → β) 0 : β)

Tactic:
simp only [mul_zero, map_zero]

Premises used: map_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : 0 < x
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
this x h
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
this :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
x : α
h : 0 < x
⊢ (inducedAddHom α β : (a : α) → β) (x * x) =
    HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
exact this x h
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
suffices :
  ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
⊢ ∀ (x : α),
    (inducedAddHom α β : (a : α) → β) (x * x) =
      HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
suffices ∀ x, 0 < x → inducedAddHom α β (x * x) = inducedAddHom α β x * inducedAddHom α β x by
        intro x
        obtain h | rfl | h := lt_trichotomy x 0
        · convert! this (-x) (neg_pos.2 h) using 1
          · rw [neg_mul, mul_neg, neg_neg]
          · simp_rw [map_neg, neg_mul, mul_neg, neg_neg]
        · simp only [mul_zero, map_zero]
        · exact this x h
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
⊢ ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_

Premises used: HMul.hMul, ConditionallyCompleteLinearOrderedField.inducedMap, LinearOrderedField.cutMap_nonempty, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
refine_1 :
  ∀ (x : α) (hx : 0 < x),
    ∀ a ∈ cutMap β (x * x),
      a ≤
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)
refine_2 :
  ∀ (x : α) (hx : 0 < x),
    ∀
      w <
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β),
      ∃ a ∈ cutMap β (x * x), w < a
⊢ ∀ (x : α),
    0 < x →
      (inducedAddHom α β : (a : α) → β) (x * x) =
        HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
refine fun x hx => csSup_eq_of_forall_le_of_forall_lt_exists_gt (cutMap_nonempty β _) ?_ ?_

Premises used: LinearOrderedField.cutMap_nonempty, csSup_eq_of_forall_le_of_forall_lt_exists_gt
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ a ∈ cutMap β (x * x),
    a ≤ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
le_inducedMap_mul_self_of_mem_cutMap hx

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap, ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ a ∈ cutMap β (x * x),
    a ≤ HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β)

Tactic:
exact le_inducedMap_mul_self_of_mem_cutMap hx

Premises used: ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ w < HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β),
    ∃ a ∈ cutMap β (x * x), w < a

Tactic:
exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap, ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
x : α
hx : 0 < x
⊢ ∀ w < HMul.hMul (α := β) (β := β) ((inducedAddHom α β : (a : α) → β) x : β) ((inducedAddHom α β : (a : α) → β) x : β),
    ∃ a ∈ cutMap β (x * x), w < a

Tactic:
exact exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self hx

Premises used: ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
dsimp :
  ∀ {a b : β},
    LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a : γ)
        ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b : γ) ↔
      a ≤ b
⊢ ∀ {a b : β},
    OneHom.toFun (↑(↑(OrderRingHom.toRingHom (inducedOrderRingHom β γ)) : β →* γ) : OneHom β γ) a ≤
        OneHom.toFun (↑(↑(OrderRingHom.toRingHom (inducedOrderRingHom β γ)) : β →* γ) : OneHom β γ) b ↔
      a ≤ b

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
a_1 b_1 : β
⊢ LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
      ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ) ↔
    a_1 ≤ b_1

Tactic:
⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_mono, Iff.intro
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
refine :
  ∀ {a b : β}
    (h :
      LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a : γ)
        ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b : γ)),
    a ≤ b
⊢ ∀ {a b : β},
    LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a : γ)
        ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b : γ) ↔
      a ≤ b

Tactic:
refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ) ≤
    inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)

Tactic:
inducedMap_mono γ β h

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_mono
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
h₁ : a_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
h₂ : b_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
⊢ a_1 ≤ b_1

Tactic:
convert! inducedMap_mono γ β h

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_mono
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
h₁ :
  a_1 =
    inducedMap.{u_4, u_3} γ β
      (({ toFun := inducedMap β γ, map_zero' := ⋯, map_add' := ⋯ : β →+ γ } : (a : β) → γ) a_1 : γ)
⊢ a_1 = inducedMap.{u_4, u_3} γ β ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)

Tactic:
rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]

Premises used: ConditionallyCompleteLinearOrderedField.inducedOrderRingHom, ConditionallyCompleteLinearOrderedField.inducedAddHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
h₁ : a_1 = inducedMap γ β (inducedMap β γ a_1)
⊢ a_1 =
    inducedMap.{u_4, u_3} γ β
      (({ toFun := inducedMap β γ, map_zero' := ⋯, map_add' := ⋯ : β →+ γ } : (a : β) → γ) a_1 : γ)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Order.CompleteField
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Field β
inst_4 : ConditionallyCompleteLinearOrder β
inst_5 : IsStrictOrderedRing β
inst_6 : Field γ
inst_7 : ConditionallyCompleteLinearOrder γ
inst_8 : IsStrictOrderedRing γ
inst_9 : Archimedean α
a : α
b : β
q : ℚ
a_1 b_1 : β
h :
  LE.le.{u_4} (α := γ) ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) a_1 : γ)
    ((OrderRingHom.toRingHom (inducedOrderRingHom β γ) : (a : β) → γ) b_1 : γ)
h₁ h₂ : a_1 = a_1
⊢ a_1 = inducedMap γ β (inducedMap β γ a_1)

Tactic:
rw [inducedMap_inv_self β γ _]

Premises used: ConditionallyCompleteLinearOrderedField.inducedMap_inv_self