awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
rw : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₂ * s₁)) (r₁ * r₂ /ₒ (s₁ * s₂))
rw₁ rw₂ : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₁ * s₂)) (r₁ * r₂ /ₒ (s₁ * s₂))
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) = r₁ * r₂ /ₒ (s₁ * s₂)

Tactic:
rw [oreDiv_mul_char r₁ r₂ s₁ s₂ r₁ s₂ (by simp [mul_comm]), mul_comm s₂]

Premises used: OreLocalization.oreDiv_mul_char, mul_comm
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
x y : OreLocalization S R
c : ∀ (r₁ : R) (s₁ : ↥S), r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)
⊢ x * y = y * x

Tactic:
cases x with | _ r₁ s₁
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
y : OreLocalization S R
r₁ : R
s₁ : ↥S
c :
  ∀ (r₂ : R) (s₂ : ↥S),
    HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
      HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
⊢ r₁ /ₒ s₁ * y = y * (r₁ /ₒ s₁)

Tactic:
cases y with | _ r₂ s₂
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : CommMonoid R
S : Submonoid R
inst_1 : OreSet S
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
c : r₁ * r₂ /ₒ (s₁ * s₂) = HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)
c₁ : Eq (α := OreLocalization S R) (r₁ * r₂ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
c₂ : Eq (α := OreLocalization S R) (r₂ * r₁ /ₒ (s₁ * s₂)) (r₂ * r₁ /ₒ (s₂ * s₁))
c₃ c₄ : Eq (α := OreLocalization S R) (r₂ * r₁ /ₒ (s₂ * s₁)) (r₂ * r₁ /ₒ (s₂ * s₁))
⊢ HMul.hMul (α := OreLocalization S R) (r₁ /ₒ s₁) (r₂ /ₒ s₂) =
    HMul.hMul (α := OreLocalization S R) (r₂ /ₒ s₂) (r₁ /ₒ s₁)

Tactic:
rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]

Premises used: mul_comm, OreLocalization.oreDiv_mul_oreDiv_comm
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : Zero X
inst_3 : MulAction R X
⊢ Eq (α := OreLocalization S X) 0 (0 /ₒ 1)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : Zero X
inst_3 : MulAction R X
⊢ Eq (α := OreLocalization S X) 0 (0 /ₒ 1)

Tactic:
with_unfolding_all rfl
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ Surjective (β := OreLocalization S X) fun (x : X) ↦ x /ₒ 1

Tactic:
OreLocalization.ind fun x s ↦ ?_

Premises used: OreLocalization.ind, Function.Surjective
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
refine :
  ∀ (x : X) (s : ↥S),
    ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
⊢ Surjective (β := OreLocalization S X) fun (x : X) ↦ x /ₒ 1

Tactic:
refine OreLocalization.ind fun x s ↦ ?_
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
obtain :
  ∀ (i j : ℕ) (hne : i ≠ j) (heq : s ^ i = s ^ 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)

Tactic:
obtain ⟨i, j, hne, heq⟩ := Finite.exists_ne_map_eq_of_infinite (α := ℕ) (s ^ ·)

Premises used: Finite.exists_ne_map_eq_of_infinite, HPow.hPow
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)
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)
⊢ ∃ (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
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
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)

Tactic:
this j i hne.symm heq.symm (hne.lt_of_le hlt)

Premises used: Ne.symm, Eq.symm, Ne.lt_of_le
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
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)

Tactic:
exact this j i hne.symm heq.symm (hne.lt_of_le hlt)

Premises used: Ne.symm, Eq.symm, Ne.lt_of_le
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)

Tactic:
use s ^ (i - (j + 1)) • x

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
⊢ Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)

Tactic:
rw [oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)

Tactic:
⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩

Premises used: HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₁ : (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
⊢ ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)

Tactic:
refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)) : R) • s ^ (i - (j + 1)) • x

Tactic:
change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₃ h₄ : s ^ j • x = s ^ j • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Tactic:
rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]

Premises used: pow_add, Nat.add_sub_cancel', SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₂ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1)
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)

Tactic:
simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

Premises used: OneMemClass.coe_one, pow_succ, SubmonoidClass.coe_pow, mul_one
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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

Tactic:
OreLocalization.ind fun x s ↦ ?_

Premises used: OreLocalization.ind, Function.Surjective
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
refine :
  ∀ (x : X) (s : ↥S),
    ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)
⊢ Surjective (β := OreLocalization S X) fun (x : X) ↦ x /ₒ 1

Tactic:
refine OreLocalization.ind fun x s ↦ ?_
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
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)
⊢ ∃ (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)

Premises used: Finite.exists_ne_map_eq_of_infinite, HPow.hPow, HSMul.hSMul
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)
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)
⊢ ∃ (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
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
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:
this j i hne.symm heq.symm (hne.lt_of_le hlt)

Premises used: Ne.symm, Eq.symm, Ne.lt_of_le
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
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:
exact this j i hne.symm heq.symm (hne.lt_of_le hlt)

Premises used: Ne.symm, Eq.symm, Ne.lt_of_le
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)
⊢ ∃ (a : X), Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) a) (x /ₒ s)

Tactic:
use s ^ (i - (j + 1)) • x

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)
⊢ Eq (α := OreLocalization S X) ((fun (x : X) ↦ (x /ₒ 1 : OreLocalization S X)) (s ^ (i - (j + 1)) • x)) (x /ₒ s)

Tactic:
rw [oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)

Tactic:
⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩

Premises used: HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₁ : (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)
⊢ ∃ (u : ↥S) (v : R), u • x = v • s ^ (i - (j + 1)) • x ∧ (↑u : R) * (↑s : R) = v * (↑1 : R)

Tactic:
refine ⟨s ^ j, (s ^ (j + 1)).1, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)) : R) • s ^ (i - (j + 1)) • x

Tactic:
change s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₃ h₄ : s ^ j • x = s ^ j • x
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Tactic:
rw [← mul_smul, ← pow_add, Nat.add_sub_cancel' hlt, heq]

Premises used: pow_add, Nat.add_sub_cancel', SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₂ : (↑s : R) ^ j * (↑s : R) = (↑s : R) ^ (j + 1)
⊢ (↑(s ^ j) : R) * (↑s : R) = (↑(s ^ (j + 1)) : R) * (↑1 : R)

Tactic:
simp_rw [SubmonoidClass.coe_pow, OneMemClass.coe_one, mul_one, pow_succ]

Premises used: OneMemClass.coe_one, pow_succ, SubmonoidClass.coe_pow, mul_one
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
inst_2 : Finite.{u + 1} ↥S
⊢ Surjective.{u + 1, u + 1} (α := R) (β := OreLocalization S R) (⇑numeratorHom : (a : R) → OreLocalization S R)

Tactic:
oreDiv_one_surjective_of_finite_left S R

Premises used: Quotient.mk', OreLocalization.oreDiv_one_surjective_of_finite_left, OreLocalization.oreDiv
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)
inr : Infinite 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)

Tactic:
rcases finite_or_infinite X with _ | _

Premises used: finite_or_infinite
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ 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)
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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) ≤ lift.{u, v} #X

Tactic:
rw [lift_umax.{v, u}, lift_id'] at this

Premises used: Cardinal.lift_id'
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
le_max_of_le_right this

Premises used: le_max_of_le_right
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
exact le_max_of_le_right this

Premises used: le_max_of_le_right
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)
inr₁ : Infinite.{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)

Tactic:
rcases finite_or_infinite S with _ | _

Premises used: finite_or_infinite, Membership.mem, Subtype
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ 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)
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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) ≤ lift.{u, v} #X

Tactic:
rw [lift_umax.{v, u}, lift_id'] at this

Premises used: Cardinal.lift_id'
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
le_max_of_le_right this

Premises used: le_max_of_le_right
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
exact le_max_of_le_right this

Premises used: le_max_of_le_right
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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) ≤ #(Prod.{v, u} X ↥S)

Tactic:
mk_le_of_surjective (show Surjective fun x : X × S ↦ x.1 /ₒ x.2 from Quotient.mk''_surjective)

Premises used: Cardinal.mk_le_of_surjective, Quotient.mk''_surjective
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : #(Prod.{v, u} X ↥S) = max (lift.{v, u} #↥S) (lift.{u, v} #X)
⊢ #(OreLocalization S X) ≤ 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)

Premises used: Cardinal.mk_le_of_surjective, Quotient.mk''_surjective
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)
⊢ #(Prod.{v, u} X ↥S) = max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
rw [mk_prod, mul_comm]

Premises used: mul_comm, Cardinal.mk_prod
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)

Tactic:
mul_eq_max ?_ ?_

Premises used: Cardinal.mul_eq_max
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
h₁ : ℵ₀ ≤ lift.{u, v} #X
⊢ lift.{v, u} #↥S * lift.{u, v} #X = max (lift.{v, u} #↥S) (lift.{u, v} #X)

Tactic:
refine mul_eq_max ?_ ?_

Premises used: Cardinal.mul_eq_max
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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.{u, v} #X

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
⊢ #(OreLocalization S R) ≤ max (lift.{u, u} #↥S) (lift.{u, u} #R)

Tactic:
cardinalMk_le_max S R

Premises used: OreLocalization.cardinalMk_le_max