awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
e : OrderIso.{u_1, u_2} (MulArchimedeanClass M) (MulArchimedeanClass N)
⊢ (congrOrderIso e).symm = congrOrderIso e.symm

Tactic:
rfl

Premises used: Equiv.subtypeEquiv, RelIso.symm, OrderIso.symm, Equiv.symm, FiniteMulArchimedeanClass.congrOrderIso, rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s < t
⊢ s ≤ t ∧ ¬t ≤ s

Tactic:
simp_rw [lt_iff_le_not_ge] at lt ⊢

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s ≤ t ∧ ¬t ≤ s
⊢ LE.le.{u_1} (α := UpperSet (MulArchimedeanClass M))
      {
        carrier :=
          {a : MulArchimedeanClass M |
            ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ s},
        upper' := ⋯ }
      {
        carrier :=
          {a : MulArchimedeanClass M |
            ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ t},
        upper' := ⋯ } ∧
    ¬LE.le.{u_1} (α := UpperSet (MulArchimedeanClass M))
        {
          carrier :=
            {a : MulArchimedeanClass M |
              ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ t},
          upper' := ⋯ }
        {
          carrier :=
            {a : MulArchimedeanClass M |
              ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ s},
          upper' := ⋯ }

Tactic:
⟨fun _ mem ne ↦ lt.1 (mem _), fun hst ↦ lt.2 fun x mem ↦ hst (fun _ ↦ mem) x.2⟩

Premises used: And.right, And.left, And.intro, Subtype.property
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
s t : UpperSet (FiniteMulArchimedeanClass M)
lt : s ≤ t ∧ ¬t ≤ s
⊢ LE.le.{u_1} (α := UpperSet (MulArchimedeanClass M))
      {
        carrier :=
          {a : MulArchimedeanClass M |
            ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ s},
        upper' := ⋯ }
      {
        carrier :=
          {a : MulArchimedeanClass M |
            ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ t},
        upper' := ⋯ } ∧
    ¬LE.le.{u_1} (α := UpperSet (MulArchimedeanClass M))
        {
          carrier :=
            {a : MulArchimedeanClass M |
              ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ t},
          upper' := ⋯ }
        {
          carrier :=
            {a : MulArchimedeanClass M |
              ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ s},
          upper' := ⋯ }

Tactic:
exact ⟨fun _ mem ne ↦ lt.1 (mem _), fun hst ↦ lt.2 fun x mem ↦ hst (fun _ ↦ mem) x.2⟩
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
N : Type u_2
inst_3 : CommGroup N
inst_4 : LinearOrder N
inst_5 : IsOrderedMonoid N
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ ∀ {x : M},
    Membership.mem (γ := Set M)
        (Subsemigroup.carrier
          (MulArchimedeanClass.subsemigroup
            ((toUpperSetMulArchimedeanClass :
                (a : UpperSet (FiniteMulArchimedeanClass M)) → UpperSet (MulArchimedeanClass M))
              s)))
        x →
      Membership.mem (γ := Set M)
        (Subsemigroup.carrier
          (MulArchimedeanClass.subsemigroup
            ((toUpperSetMulArchimedeanClass :
                (a : UpperSet (FiniteMulArchimedeanClass M)) → UpperSet (MulArchimedeanClass M))
              s)))
        x⁻¹

Tactic:
simp [MulArchimedeanClass.subsemigroup]

Premises used: MulArchimedeanClass.subsemigroup
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ (↑(MulArchimedeanClass.subsemigroup
          ((toUpperSetMulArchimedeanClass :
              (a : UpperSet (FiniteMulArchimedeanClass M)) → UpperSet (MulArchimedeanClass M))
            s)) :
      Set M) =
    (↑(subgroup s) : Set M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
h : ∀ (x : M), Membership.mem (γ := Subgroup M) (subgroup ⊤) x ↔ Membership.mem (γ := Subgroup M) ⊥ x
⊢ Eq.{u_1 + 1} (α := Subgroup M) (subgroup ⊤) ⊥

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
x : M
⊢ Membership.mem (γ := Subgroup M) (subgroup ⊤) x ↔ Membership.mem (γ := Subgroup M) ⊥ x

Tactic:
simp [subgroup, MulArchimedeanClass.subsemigroup, toUpperSetMulArchimedeanClass]

Premises used: MulArchimedeanClass.subsemigroup, FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass, FiniteMulArchimedeanClass.subgroup
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
simp_rw :
  a ∈ subgroup s ↔
    ∀ (h : ¬Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤),
      Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ ¬A = ⊤) (MulArchimedeanClass.mk a) ⋯ ∈ s
⊢ a ∈ subgroup s ↔ ∀ (h : a ≠ 1), mk a h ∈ s

Tactic:
simp_rw [mk, Ne, ← MulArchimedeanClass.mk_eq_top_iff]

Premises used: Ne, MulArchimedeanClass.mk_eq_top_iff, FiniteMulArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
s : UpperSet (FiniteMulArchimedeanClass M)
⊢ a ∈ subgroup s ↔
    ∀ (h : ¬Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤),
      Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ ¬A = ⊤) (MulArchimedeanClass.mk a) ⋯ ∈ s

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ StrictAnti.{u_1, u_1} (α := UpperSet (FiniteMulArchimedeanClass M)) subgroup

Tactic:
fun _ _ h ↦
  MulArchimedeanClass.subsemigroup_strictAnti (toUpperSetMulArchimedeanClass.strictMono h)

Premises used: MulArchimedeanClass.subsemigroup_strictAnti, OrderEmbedding.strictMono, FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass, StrictAnti
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
c : FiniteMulArchimedeanClass M
⊢ a ∈ c.ballSubgroup ↔ ∀ (h : a ≠ 1), c < mk a h

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a : M
c : FiniteMulArchimedeanClass M
⊢ a ∈ c.closedBallSubgroup ↔ ∀ (h : a ≠ 1), c ≤ mk a h

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Class
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ StrictAnti.{u_1, u_1} (α := FiniteMulArchimedeanClass M) ballSubgroup

Tactic:
fun _ _ h ↦ subgroup_strictAnti <| UpperSet.Ioi_strictMono _ h

Premises used: StrictAnti, UpperSet.Ioi_strictMono, FiniteMulArchimedeanClass.subgroup_strictAnti, FiniteMulArchimedeanClass
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : PartialOrder R
inst_2 : MulLeftStrictMono R
inst_3 : MulArchimedean R
a : R
ha : 1 < a
b : R
⊢ ∃ (n : ℕ), b < a ^ n

Tactic:
let ⟨k, hk⟩ := MulArchimedean.arch b ha
  ⟨k + 1, hk.trans_lt <| pow_lt_pow_right' ha k.lt_succ_self⟩

Premises used: pow_lt_pow_right', Exists, Nat.lt_succ_self, HPow.hPow, HAdd.hAdd, LT.lt, Exists.intro, _private.0.exists_lt_pow.match_1, OfNat.ofNat, LE.le.trans_lt, MulArchimedean.arch
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : CommGroup R
inst_1 : LinearOrder R
inst_2 : IsOrderedMonoid R
inst_3 : MulArchimedean R
a : R
ha : a < 1
b : R
⊢ ∀ (a_1 : ℕ), b⁻¹ < a⁻¹ ^ a_1 → a ^ a_1 < b

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
x : R
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
x : R
h_1 : Nontrivial R
n : ℕ
h : x ≤ HSMul.hSMul (β := R) n 1
rwa rwa₁ rwa₂ rwa₃ : x ≤ HSMul.hSMul (β := R) n 1
⊢ x ≤ (↑n : R)

Tactic:
rwa [← nsmul_one]

Premises used: nsmul_one
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
x : R
h : Nontrivial R
⊢ ∃ (n : ℕ), x ≤ (↑n : R)

Tactic:
exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]

Premises used: Exists.imp, Archimedean.arch, one_pos
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℕ
hn : x < HSMul.hSMul (β := R) n 1
rwa rwa₁ rwa₂ rwa₃ : x < HSMul.hSMul (β := R) n 1
⊢ x < (↑n : R)

Tactic:
rwa [← nsmul_one]

Premises used: nsmul_one
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
x : R
⊢ ∃ (n : ℤ), x ≤ (↑n : R)

Tactic:
let ⟨n, h⟩ := exists_nat_ge x; ⟨n, mod_cast h⟩

Premises used: Int.cast, Int.cast_natCast, congrArg, cast, Exists, exists_nat_ge, LE.le, Nat.cast, Exists.intro, _private.0.exists_int_ge.match_1, Eq.symm
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
h : -x ≤ (↑n : R)
⊢ (↑(-n) : R) ≤ x

Tactic:
simpa [neg_le] using h

Premises used: neg_le
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℕ
h : x < (↑n : R)
rwa rwa₁ rwa₂ rwa₃ : x < (↑n : R)
⊢ x < (↑(↑n : ℤ) : R)

Tactic:
rwa [Int.cast_natCast]

Premises used: Int.cast_natCast
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
h : -x < (↑n : R)
rw : -(↑n : R) < x
⊢ (↑(-n) : R) < x

Tactic:
rw [Int.cast_neg]

Premises used: Int.cast_neg
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
h : -x < (↑n : R)
⊢ -(↑n : R) < x

Tactic:
neg_lt.1 h

Premises used: Iff.mp, neg_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Defs
Goal:
R : Type u_1
inst : Ring R
inst_1 : PartialOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : Archimedean R
x : R
n : ℤ
h : -x < (↑n : R)
⊢ -(↑n : R) < x

Tactic:
exact neg_lt.1 h

Premises used: Iff.mp, neg_lt
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing β
inst_5 : Archimedean β
f g : α →+*o β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing β
inst_5 : Archimedean β
f g : α →+*o β
x : α
h : ∀ (h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
by_contra h' : f x ≠ g x

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing β
inst_5 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h :
  ∀
    (h₂ :
      ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_6 : LinearOrder α] [inst_7 : Field β]
        [inst_8 : LinearOrder β] [IsStrictOrderedRing β] [Archimedean β] (f g : α →+*o β) (x : α)
        (h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
        (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False)
    (h : ¬LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False
wlog :
  ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_6 : LinearOrder α] [inst_7 : Field β] [inst_8 : LinearOrder β]
    [IsStrictOrderedRing β] [Archimedean β] (f g : α →+*o β) (x : α)
    (h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False
⊢ False

Tactic:
wlog h : f x < g x with h₂

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing β
inst_5 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h₂ :
  ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_6 : LinearOrder α] [inst_7 : Field β] [inst_8 : LinearOrder β]
    [IsStrictOrderedRing β] [Archimedean β] (f g : α →+*o β) (x : α)
    (h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False
h : ¬LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ False

Tactic:
h₂ g f x (Ne.symm h') (h'.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing β
inst_5 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h₂ :
  ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_6 : LinearOrder α] [inst_7 : Field β] [inst_8 : LinearOrder β]
    [IsStrictOrderedRing β] [Archimedean β] (f g : α →+*o β) (x : α)
    (h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β))
    (h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False
h : ¬LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ False

Tactic:
exact h₂ g f x (Ne.symm h') (h'.lt_or_gt.resolve_left h)

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Field α_1
inst_1 : LinearOrder α_1
inst_2 : Field β_1
inst_3 : LinearOrder β_1
α : Type u_1
β : Type u_2
inst_4 : Field α
inst_5 : LinearOrder α
inst_6 : Field β
inst_7 : LinearOrder β
inst_8 : IsStrictOrderedRing β
inst_9 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
obtain :
  ∀ (q : ℚ) (hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((↑q : β) : β))
    (hg : LT.lt.{u_2} (α := β) ((↑q : β) : β) ((g : (a : α) → β) x : β)), False
⊢ False

Tactic:
obtain ⟨q, hf, hg⟩ := exists_rat_btwn h

Premises used: exists_rat_btwn
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Field α_1
inst_1 : LinearOrder α_1
inst_2 : Field β_1
inst_3 : LinearOrder β_1
α : Type u_1
β : Type u_2
inst_4 : Field α
inst_5 : LinearOrder α
inst_6 : Field β
inst_7 : LinearOrder β
inst_8 : IsStrictOrderedRing β
inst_9 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
q : ℚ
hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((↑q : β) : β)
hg : LT.lt.{u_2} (α := β) ((↑q : β) : β) ((g : (a : α) → β) x : β)
⊢ LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (↑q : α) : β)

Tactic:
rw [← map_ratCast f] at hf

Premises used: map_ratCast
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Field α_1
inst_1 : LinearOrder α_1
inst_2 : Field β_1
inst_3 : LinearOrder β_1
α : Type u_1
β : Type u_2
inst_4 : Field α
inst_5 : LinearOrder α
inst_6 : Field β
inst_7 : LinearOrder β
inst_8 : IsStrictOrderedRing β
inst_9 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
q : ℚ
hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((↑q : β) : β)
hg : LT.lt.{u_2} (α := β) ((↑q : β) : β) ((g : (a : α) → β) x : β)
hf₁ : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (↑q : α) : β)
⊢ LT.lt.{u_2} (α := β) ((↑q : β) : β) ((g : (a : α) → β) x : β)

Tactic:
rw [← map_ratCast f] at hf

Premises used: map_ratCast
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Field α_1
inst_1 : LinearOrder α_1
inst_2 : Field β_1
inst_3 : LinearOrder β_1
α : Type u_1
β : Type u_2
inst_4 : Field α
inst_5 : LinearOrder α
inst_6 : Field β
inst_7 : LinearOrder β
inst_8 : IsStrictOrderedRing β
inst_9 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
q : ℚ
hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (↑q : α) : β)
hg : LT.lt.{u_2} (α := β) ((↑q : β) : β) ((g : (a : α) → β) x : β)
⊢ LT.lt.{u_2} (α := β) ((g : (a : α) → β) (↑q : α) : β) ((g : (a : α) → β) x : β)

Tactic:
rw [← map_ratCast g] at hg

Premises used: map_ratCast
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Field α_1
inst_1 : LinearOrder α_1
inst_2 : Field β_1
inst_3 : LinearOrder β_1
α : Type u_1
β : Type u_2
inst_4 : Field α
inst_5 : LinearOrder α
inst_6 : Field β
inst_7 : LinearOrder β
inst_8 : IsStrictOrderedRing β
inst_9 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
q : ℚ
hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (↑q : α) : β)
hg : LT.lt.{u_2} (α := β) ((g : (a : α) → β) (↑q : α) : β) ((g : (a : α) → β) x : β)
⊢ False

Tactic:
(lt_asymm ((OrderHomClass.mono g).reflect_lt hg) <|
          (OrderHomClass.mono f).reflect_lt hf).elim

Premises used: False.elim, lt_asymm, Monotone.reflect_lt, OrderHomClass.mono
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α_1 : Type u_1
β_1 : Type u_2
inst : Field α_1
inst_1 : LinearOrder α_1
inst_2 : Field β_1
inst_3 : LinearOrder β_1
α : Type u_1
β : Type u_2
inst_4 : Field α
inst_5 : LinearOrder α
inst_6 : Field β
inst_7 : LinearOrder β
inst_8 : IsStrictOrderedRing β
inst_9 : Archimedean β
f g : α →+*o β
x : α
h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
h : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
q : ℚ
hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (↑q : α) : β)
hg : LT.lt.{u_2} (α := β) ((g : (a : α) → β) (↑q : α) : β) ((g : (a : α) → β) x : β)
⊢ False

Tactic:
exact
      (lt_asymm ((OrderHomClass.mono g).reflect_lt hg) <|
          (OrderHomClass.mono f).reflect_lt hf).elim

Premises used: False.elim, lt_asymm, Monotone.reflect_lt, OrderHomClass.mono
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing β
inst_5 : Archimedean β
⊢ Subsingleton (α ≃+*o β)

Tactic:
OrderRingIso.toOrderRingHom_injective.subsingleton

Premises used: Function.Injective.subsingleton, OrderRingIso.toOrderRingHom_injective
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
β : Type u_2
inst : Field α
inst_1 : LinearOrder α
inst_2 : Field β
inst_3 : LinearOrder β
inst_4 : IsStrictOrderedRing α
inst_5 : Archimedean α
⊢ Subsingleton (α ≃+*o β)

Tactic:
OrderRingIso.symm_bijective.injective.subsingleton

Premises used: OrderRingIso.symm_bijective, Function.Injective.subsingleton, Function.Bijective.injective
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : α →+*o α
⊢ f = OrderRingHom.id α

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : α ≃+*o α
⊢ f = OrderRingIso.refl α

Tactic:
Subsingleton.elim ..

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : α →+*o α
x : α
rw : (OrderRingHom.id α : (a : α) → α) x = x
⊢ (f : (a : α) → α) x = x

Tactic:
rw [f.eq_id]

Premises used: OrderRingHom.eq_id
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : α →+*o α
x : α
⊢ (OrderRingHom.id α : (a : α) → α) x = x

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Archimedean.Hom
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : α ≃+*o α
x : α
⊢ (f : (a : α) → α) x = x

Tactic:
f.toOrderRingHom.apply_eq_self x

Premises used: OrderRingHom.apply_eq_self, OrderRingIso.toOrderRingHom
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
hx : x ∈ hs.toFinset (s := s)
rw rw₁ : a = a
⊢ s.indicator (fun (x : ℕ) ↦ a) x = a

Tactic:
rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]

Premises used: Set.Finite.mem_toFinset, Set.indicator_of_mem, Iff.mp
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
⊢ ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a

Tactic:
have key : ∀ x ∈ hs.toFinset, s.indicator (fun _ ↦ a) x = a := by
    intro x hx
    rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]
-- Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) x = a
rw :
  ∃ (a_1 : ℕ),
    ∀ b ≥ a_1,
      Eq.{u_1 + 1} (α := α) (∑ k ∈ Finset.range b, s.indicator (fun (x : ℕ) ↦ a) k)
        (∑ a_3 ∈ hs.toFinset (s := s), s.indicator (fun (x : ℕ) ↦ a) a_3)
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ a) k = Nat.card (↑s : Type) • a

Tactic:
rw [Nat.card_eq_card_finite_toFinset hs, ← sum_eq_card_nsmul key, eventually_atTop]

Premises used: Finset.sum_eq_card_nsmul, Filter.eventually_atTop, Nat.card_eq_card_finite_toFinset