awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
inst_3 : Nontrivial M
⊢ Nonempty.{u_1 + 1} (FiniteMulArchimedeanClass M)
have obtain : ∀ (x : M) (hx : x ≠ 1), Nonempty.{u_1 + 1} (FiniteMulArchimedeanClass M)
Tactic: obtain ⟨x, hx⟩ := exists_ne (1 : M)
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
⊢ α
have refine_1 : ∀ (a b : M) (h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)),
  Eq.{u_2 + 1} (α := WithTop α)
    ((fun (b : M) ↦
        (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α) : WithTop α))
      a)
    ((fun (b : M) ↦
        (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α) : WithTop α))
      b)
Tactic: refine (MulArchimedeanClass.lift
    (fun b ↦ if h : b = 1 then ⊤ else WithTop.some (f ⟨b, h⟩)) (fun a b h' ↦ ?_) A).untop ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
refine_1 :
  ∀ (a b : M) (h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)),
    Eq.{u_2 + 1} (α := WithTop α)
      ((fun (b : M) ↦
          (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α) : WithTop α))
        a)
      ((fun (b : M) ↦
          (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α) : WithTop α))
        b)
⊢ α
have refine_2 : Ne.{u_2 + 1} (α := WithTop α)
  (MulArchimedeanClass.lift
    (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) sorry A)
  ⊤
Tactic: refine (MulArchimedeanClass.lift
    (fun b ↦ if h : b = 1 then ⊤ else WithTop.some (f ⟨b, h⟩)) (fun a b h' ↦ ?_) A).untop ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
⊢ Eq.{u_2 + 1} (α := WithTop α)
    (if h : a = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a h)) : WithTop α))
    (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α))
have pos : ∀ (ha : a = 1) (hb : b = 1), Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
pos : ∀ (ha : a = 1) (hb : b = 1), Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
⊢ Eq.{u_2 + 1} (α := WithTop α)
    (if h : a = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a h)) : WithTop α))
    (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α))
have neg : ∀ (ha : a = 1) (hb : ¬b = 1), ⊤ = (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
pos : ∀ (ha : a = 1) (hb : b = 1), Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
neg : ∀ (ha : a = 1) (hb : ¬b = 1), ⊤ = (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
⊢ Eq.{u_2 + 1} (α := WithTop α)
    (if h : a = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a h)) : WithTop α))
    (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α))
have pos₁ : ∀ (ha : ¬a = 1) (hb : b = 1), (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) = ⊤
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
pos : ∀ (ha : a = 1) (hb : b = 1), Eq.{u_2 + 1} (α := WithTop α) ⊤ ⊤
neg : ∀ (ha : a = 1) (hb : ¬b = 1), ⊤ = (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
pos₁ : ∀ (ha : ¬a = 1) (hb : b = 1), (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) = ⊤
⊢ Eq.{u_2 + 1} (α := WithTop α)
    (if h : a = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a h)) : WithTop α))
    (if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α))
have neg₁ : ∀ (ha : ¬a = 1) (hb : ¬b = 1),
  (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) =
    (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
Tactic: split_ifs with ha hb hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b_1 : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
a b : M
h' : Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b)
ha : ¬a = 1
hb : ¬b = 1
⊢ (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) a ha)) : WithTop α) =
    (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
have neg : (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α) =
  (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b hb)) : WithTop α)
Tactic: rw [h ⟨a, ha⟩ ⟨b, hb⟩ (by simpa [mk] using h')]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
α : Type u_2
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), Eq (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a = f b
x : FiniteMulArchimedeanClass M
A : MulArchimedeanClass M
hA : A ≠ ⊤
⊢ Ne.{u_2 + 1} (α := WithTop α)
    (MulArchimedeanClass.lift
      (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) ⋯ A)
    ⊤
have refine_2 : ∀ (a : M) (hA : Ne (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤),
  Ne.{u_2 + 1} (α := WithTop α)
    (MulArchimedeanClass.lift
      (fun (b : M) ↦ if h : b = 1 then ⊤ else (↑(f (Subtype.mk (p := fun (a : M) ↦ a ≠ 1) b h)) : WithTop α)) sorry
      (MulArchimedeanClass.mk a))
    ⊤
Tactic: induction A using MulArchimedeanClass.ind with | mk a
Cleared hypotheses: A, hA
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a b : M
α : Type u_2
inst_3 : PartialOrder α
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), LE.le (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a ≤ f b
A B : FiniteMulArchimedeanClass M
hAB : A ≤ B
⊢ lift f ⋯ A ≤ lift f ⋯ B
have mk : ∀ (a : M) (ha : a ≠ 1) (hAB : mk a ha ≤ B), lift f sorry (mk a ha) ≤ lift f sorry B
Tactic: induction A using ind with | mk a ha
Cleared hypotheses: A, hAB
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
a_1 b : M
α : Type u_2
inst_3 : PartialOrder α
f : { a : M // a ≠ 1 } → α
h : ∀ (a b : { a : M // a ≠ 1 }), LE.le (α := FiniteMulArchimedeanClass M) (mk (↑a : M) ⋯) (mk (↑b : M) ⋯) → f a ≤ f b
B : FiniteMulArchimedeanClass M
a : M
ha : a ≠ 1
hAB : mk a ha ≤ B
⊢ lift f ⋯ (mk a ha) ≤ lift f ⋯ B
have mk : ∀ (b : M) (hb : b ≠ 1) (hAB : LE.le (α := FiniteMulArchimedeanClass M) (mk a ha) (mk b hb)),
  lift f sorry (mk a ha) ≤ lift f sorry (mk b hb)
Tactic: induction B using ind with | mk b hb
Cleared hypotheses: B, hAB
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (hypothesis)
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
⊢ LT.lt.{u_1} (α := UpperSet (MulArchimedeanClass M))
    ((fun (s : UpperSet (FiniteMulArchimedeanClass M)) ↦
        ({
            carrier :=
              {a : MulArchimedeanClass M |
                ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ s},
            upper' := ⋯ } :
          UpperSet (MulArchimedeanClass M)))
      s)
    ((fun (s : UpperSet (FiniteMulArchimedeanClass M)) ↦
        ({
            carrier :=
              {a : MulArchimedeanClass M |
                ∀ (h : a ≠ ⊤), Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ A ≠ ⊤) a h ∈ s},
            upper' := ⋯ } :
          UpperSet (MulArchimedeanClass M)))
      t)
have lt₁ : s ≤ t ∧ ¬t ≤ s
Tactic: simp_rw [lt_iff_le_not_ge] at lt ⊢
Cleared hypotheses: lt
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
Goal:
M : Type u_1
inst : CommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
⊢ Eq.{u_1 + 1} (α := Subgroup M) (subgroup ⊤) ⊥
have h : ∀ (x : M), Membership.mem (γ := Subgroup M) (subgroup ⊤) x ↔ Membership.mem (γ := Subgroup M) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Class (goal)
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 : a ≠ 1), mk a h ∈ s
have simp_rw : a ∈ subgroup s ↔
  ∀ (h : ¬Eq (α := MulArchimedeanClass M) (MulArchimedeanClass.mk a) ⊤),
    Subtype.mk (p := fun (A : MulArchimedeanClass M) ↦ ¬A = ⊤) (MulArchimedeanClass.mk a) sorry ∈ s
Tactic: simp_rw [mk, Ne, ← MulArchimedeanClass.mk_eq_top_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Defs (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
inst_3 : Archimedean R
x : R
⊢ ∃ (n : ℕ), x ≤ (↑n : R)
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Defs (goal)
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
have rw : -(↑n : R) < x
Tactic: rw [Int.cast_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (goal)
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 β
⊢ f = g
have h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (goal)
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 : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
have h : ∀ (h' : Ne.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)), False
Tactic: by_contra h' : f x ≠ g x
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (goal)
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 : β)
⊢ False
have 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
Tactic: wlog h : f x < g x with h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (goal)
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
⊢ False
have 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
Tactic: wlog h : f x < g x with h₂
Cleared hypotheses: inst_4, inst_5, f, g, x, h'
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (goal)
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 : β)
⊢ False
have obtain : ∀ (q : ℚ) (hf : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((↑q : β) : β))
  (hg : LT.lt.{u_2} (α := β) ((↑q : β) : β) ((g : (a : α) → β) x : β)), False
Tactic: obtain ⟨q, hf, hg⟩ := exists_rat_btwn h
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (hypothesis)
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 : β)
⊢ False
have hf₁ : LT.lt.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) (↑q : α) : β)
Tactic: rw [← map_ratCast f] at hf
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (hypothesis)
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 : β)
⊢ False
have hg₁ : LT.lt.{u_2} (α := β) ((g : (a : α) → β) (↑q : α) : β) ((g : (a : α) → β) x : β)
Tactic: rw [← map_ratCast g] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.Hom (goal)
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : Archimedean α
f : α →+*o α
x : α
⊢ (f : (a : α) → α) x = x
have rw : (OrderRingHom.id α : (a : α) → α) x = x
Tactic: rw [f.eq_id]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
x : ℕ
hx : x ∈ hs.toFinset (s := s)
⊢ s.indicator (fun (x : ℕ) ↦ a) x = a
have rw : a = a
Tactic: rw [indicator_of_mem (hs.mem_toFinset.1 hx) (fun _ ↦ a)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (hypothesis)
Goal:
α : Type u_1
inst : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ a) k = Nat.card (↑s : Type) • a
have key : ∀ 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)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
⊢ ∀ᶠ (n : ℕ) in atTop, ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ a) k = Nat.card (↑s : Type) • a
have 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)
Tactic: rw [Nat.card_eq_card_finite_toFinset hs, ← sum_eq_card_nsmul key, eventually_atTop]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
⊢ ∃ (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)
have obtain : ∀ (m : ℕ) (hm : m ∈ upperBounds s),
  ∃ (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)
Tactic: obtain ⟨m, hm⟩ := hs.bddAbove
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
m : ℕ
hm : m ∈ upperBounds s
⊢ ∃ (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)
have refine_1 : ∀ (n : ℕ) (n_m : n ≥ m + 1), hs.toFinset (s := s) ⊆ Finset.range n
Tactic: refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
m : ℕ
hm : m ∈ upperBounds s
refine_1 : ∀ (n : ℕ) (n_m : n ≥ m + 1), hs.toFinset (s := s) ⊆ Finset.range n
⊢ ∃ (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)
have refine_2 : ∀ (n : ℕ) (n_m : n ≥ m + 1),
  ∀ x ∈ Finset.range n, x ∉ hs.toFinset (s := s) → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0
Tactic: refine ⟨m + 1, fun n n_m ↦ (sum_subset ?_ ?_).symm⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ hs.toFinset (s := s) → x ∈ Finset.range n
have refine_1 : x ∈ s → x ∈ Finset.range n
Tactic: rw [hs.mem_toFinset]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ Finset.range n → x ∉ hs.toFinset (s := s) → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0
have refine_2 : x ∈ Finset.range n → x ∉ s → Eq.{u_1 + 1} (α := α) (s.indicator (fun (x : ℕ) ↦ a) x) 0
Tactic: rw [hs.mem_toFinset]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
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
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : n ≥ m + 1
x : ℕ
⊢ x ∈ s → x ∈ Finset.range n
have refine_1 : x ∈ s → x < n
Tactic: rw [Finset.mem_range]
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ s.Infinite ↔
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
have mp : s.Infinite → Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
mp :
  s.Infinite →
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
⊢ s.Infinite ↔
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop
have mpr : Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k) atTop atTop → s.Infinite
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Archimedean.IndicatorCard (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
inst_1 : PartialOrder R
inst_2 : IsOrderedAddMonoid R
inst_3 : AddLeftStrictMono R
inst_4 : Archimedean R
r : R
h : 0 < r
s : Set ℕ
⊢ Monotone.{0, u_1} (β := R) fun (n : ℕ) ↦ ∑ k ∈ Finset.range n, s.indicator (fun (x : ℕ) ↦ r) k
have refine : ∀ (x : ℕ), LE.le.{u_1} (α := R) 0 (s.indicator (fun (x : ℕ) ↦ r) x)
Tactic: refine (sum_mono_set_of_nonneg ?_).comp range_mono