awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
inr :
  ∀
    (this :
      ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i = s ^ j) (hlt : j < i),
        ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s))
    (hlt : i ≤ j), ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have wlog! : ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i = s ^ j) (hlt : j < i),
  ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: wlog! hlt : j < i generalizing i j
Cleared hypotheses: i, j, hne, heq
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have h : Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)
Tactic: use s ^ (i - (j + 1)) • x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)
have h : ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
Tactic: rw [oreDiv_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
have h : s ^ j • x = (↑(s ^ (j + 1)) : R) • s ^ (i - (j + 1)) • x
Tactic: refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
h : s ^ j • x = (↑(s ^ (j + 1)) : R) • s ^ (i - (j + 1)) • x
⊢ ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
have h₁ : (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
Tactic: refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ s ^ j • x = (↑(s ^ (j + 1)) : R) • s ^ (i - (j + 1)) • x
have h : s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
Tactic: change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h₁ : s ^ j • x = s ^ (j + 1 + (i - (j + 1))) • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
h₁ : s ^ j • x = s ^ (j + 1 + (i - (j + 1))) • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h₂ : s ^ j • x = s ^ i • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
h₁ : s ^ j • x = s ^ (j + 1 + (i - (j + 1))) • x
h₂ : s ^ j • x = s ^ i • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h₃ : s ^ j • x = s ^ j • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
have h : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * (↑1 : R)
Tactic: simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
h : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * (↑1 : R)
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
have h₁ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * 1
Tactic: simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite.{u + 1} ↥S
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i = s ^ j
hlt : j < i
h : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * (↑1 : R)
h₁ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * 1
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
have h₂ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1)
Tactic: simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
⊢ Surjective (β := OreLocalization S X) fun (x : X) ↦ x /ₒ 1
have refine : ∀ (x : X) (s : ↥S), ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: refine OreLocalization.ind fun x s ↦ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have obtain : ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i • x = s ^ j • x),
  ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ · • x)
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have inr : ∀
  (this :
    ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i • x = s ^ j • x) (hlt : j < i),
      ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s))
  (hlt : i ≤ j), ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: wlog! hlt : j < i generalizing i j
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
inr :
  ∀
    (this :
      ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i • x = s ^ j • x) (hlt : j < i),
        ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s))
    (hlt : i ≤ j), ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have wlog! : ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i • x = s ^ j • x) (hlt : j < i),
  ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
Tactic: wlog! hlt : j < i generalizing i j
Cleared hypotheses: i, j, hne, heq
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
have h : Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)
Tactic: use s ^ (i - (j + 1)) • x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)
have h : ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
Tactic: rw [oreDiv_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
have h : s ^ j • x = (↑(s ^ (j + 1)) : R) • s ^ (i - (j + 1)) • x
Tactic: refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
h : s ^ j • x = (↑(s ^ (j + 1)) : R) • s ^ (i - (j + 1)) • x
⊢ ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
have h₁ : (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
Tactic: refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = (↑(s ^ (j + 1)) : R) • s ^ (i - (j + 1)) • x
have h : s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
Tactic: change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h₁ : s ^ j • x = s ^ (j + 1 + (i - (j + 1))) • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
h₁ : s ^ j • x = s ^ (j + 1 + (i - (j + 1))) • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h₂ : s ^ j • x = s ^ i • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
h : s ^ j • x = (s ^ (j + 1) * s ^ (i - (j + 1))) • x
h₁ : s ^ j • x = s ^ (j + 1 + (i - (j + 1))) • x
h₂ : s ^ j • x = s ^ i • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x
have h₃ : s ^ j • x = s ^ j • x
Tactic: rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
have h : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * (↑1 : R)
Tactic: simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
h : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * (↑1 : R)
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
have h₁ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * 1
Tactic: simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inst_3 : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
h : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * (↑1 : R)
h₁ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1) * 1
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
have h₂ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1)
Tactic: simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have inl : Finite X → #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
Tactic: rcases finite_or_infinite X with _ | _
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
inl : Finite X → #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have inr : Infinite X → #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
Tactic: rcases finite_or_infinite X with _ | _
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Finite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
Tactic: have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have this₁ : #(OreLocalization S X) ≤ lift.{u, v} #X
Tactic: rw [lift_umax.{v, u}, lift_id'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have inr : Finite.{u + 1} ↥S → #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
Tactic: rcases finite_or_infinite S with _ | _
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
inr : Finite.{u + 1} ↥S → #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have inr₁ : Infinite.{u + 1} ↥S → #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
Tactic: rcases finite_or_infinite S with _ | _
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
h_1 : Finite.{u + 1} ↥S
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
Tactic: have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_left S X)
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
h_1 : Finite.{u + 1} ↥S
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have this₁ : #(OreLocalization S X) ≤ lift.{u, v} #X
Tactic: rw [lift_umax.{v, u}, lift_id'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
h_1 : Infinite.{u + 1} ↥S
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)
have h : #(Prod.{v, u} X ↥S) = max (lift.{v, u} #↥S) (lift.{u, v} #X)
Tactic: convert! ←
    mk_le_of_surjective (show Surjective fun x : X × S ↦ x.1 /ₒ x.2 from Quotient.mk''_surjective)
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
h_1 : Infinite.{u + 1} ↥S
⊢ #(Prod.{v, u} X ↥S) = max (lift.{v, u} #↥S) (lift.{u, v} #X)
have h : lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)
Tactic: rw [mk_prod, mul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h : Infinite X
h_1 : Infinite.{u + 1} ↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)
have h : ℵ₀ ≤ lift.{v, u} #↥S
Tactic: refine mul_eq_max ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
h_1 : Infinite X
h_2 : Infinite.{u + 1} ↥S
h : ℵ₀ ≤ lift.{v, u} #↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)
have h₁ : ℵ₀ ≤ lift.{u, v} #X
Tactic: refine mul_eq_max ?_ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
⊢ #(OreLocalization S R) ≤ #R
have h : max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R
Tactic: convert! ← cardinalMk_le_max S R
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R
have h : max #↥S #R = #R
Tactic: simp_rw [lift_id, max_eq_right_iff, mk_subtype_le]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
h : max #↥S #R = #R
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R
have h₁ : #↥S ≤ #R
Tactic: simp_rw [lift_id, max_eq_right_iff, mk_subtype_le]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have inl : Finite X → #(OreLocalization S X) ≤ lift.{u, v} #X
Tactic: rcases finite_or_infinite X with _ | _
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
inl : Finite X → #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have inr : Infinite X → #(OreLocalization S X) ≤ lift.{u, v} #X
Tactic: rcases finite_or_infinite X with _ | _
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Finite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
Tactic: have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have inl : ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #X), #(OreLocalization S X) ≤ lift.{u, v} #X
Tactic: rwa [lift_umax.{v, u}, lift_id'] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
inl : ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #X), #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have inl₁ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #X), #(OreLocalization S X) ≤ lift.{u, v} #X
Tactic: rwa [lift_umax.{v, u}, lift_id'] at this
Cleared hypotheses: this