-- Mathlib/GroupTheory/OreLocalization/Cardinality.lean
theorem cardinalMk_le_lift_cardinalMk_of_commute (hc : ∀ s s' : S, Commute s s') :
    #(OreLocalization S X) ≤ lift.{u} #X

Proof state:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
y y' : OreLocalization S X
x : X × ↥S := surjInv hsurj y
heq : x.1 = (surjInv hsurj y').1 ∧ x.2 • x.1 = (surjInv hsurj y').2 • (surjInv hsurj y').1
⊢ x.1 /ₒ x.2 = (surjInv hsurj y').1 /ₒ (surjInv hsurj y').2

Tactic:
set x' := surjInv hsurj y'

Result:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
y y' : OreLocalization S X
x : X × ↥S := surjInv hsurj y
x' : X × ↥S := surjInv hsurj y'
heq : x.1 = x'.1 ∧ x.2 • x.1 = x'.2 • x'.1
⊢ x.1 /ₒ x.2 = x'.1 /ₒ x'.2

Proof state:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
let j := (fun x : X × S ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj

Result:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Proof state:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : 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

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

Result:
no goals

Proof state:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
y y' : OreLocalization S X
heq :
  (surjInv hsurj y).1 = (surjInv hsurj y').1 ∧
    (surjInv hsurj y).2 • (surjInv hsurj y).1 = (surjInv hsurj y').2 • (surjInv hsurj y').1
⊢ i (surjInv hsurj y) = i (surjInv hsurj y')

Tactic:
simp_rw [i]

Result:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
y y' : OreLocalization S X
heq :
  (surjInv hsurj y).1 = (surjInv hsurj y').1 ∧
    (surjInv hsurj y).2 • (surjInv hsurj y).1 = (surjInv hsurj y').2 • (surjInv hsurj y').1
⊢ (surjInv hsurj y).1 /ₒ (surjInv hsurj y).2 = (surjInv hsurj y').1 /ₒ (surjInv hsurj y').2

Proof state:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
rcases finite_or_infinite X with _ | _

Result:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Proof state:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
this : Injective j
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
have := lift_mk_le_lift_mk_of_injective this

Result:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
this✝ : Injective j
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Proof state:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x => x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun x => (x.1, x.2 • x.1)) ∘ surjInv hsurj
this✝ : Injective j
this : #(OreLocalization S X) ≤ lift.{u, v} #X * lift.{u, v} #X
⊢ ℵ₀ ≤ lift.{u, v} #X

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc✝ : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ x /ₒ s = x /ₒ s'

Tactic:
rw [oreDiv_eq_iff]

Result:
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc✝ : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ ∃ u v, u • x = v • x ∧ ↑u * ↑s' = v * ↑s