-- 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
heq : j y = j y'
⊢ i (surjInv hsurj y) = i (surjInv hsurj y')

Tactic:
simp_rw [j, comp_apply, Prod.ext_iff] at heq

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
⊢ i (surjInv hsurj y) = i (surjInv hsurj y')

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'
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
let i (x : X × S) := x.1 /ₒ x.2

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
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Proof state:
case inr.intro
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'
h1 : x.1 = x'.1
h2 : x.2 • x.1 = x'.2 • x'.1
⊢ x.1 /ₒ x.2 = x'.1 /ₒ x'.2

Tactic:
rw [← h1] at h2 ⊢

Result:
case inr.intro
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'
h1 : x.1 = x'.1
h2 : 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
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
have hi := rightInverse_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
⊢ #(OreLocalization S X) ≤ lift.{u, v} #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
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

Tactic:
obtain ⟨h1, h2⟩ := heq

Result:
case inr.intro
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'
h1 : x.1 = x'.1
h2 : x.2 • x.1 = x'.2 • x'.1
⊢ x.1 /ₒ x.2 = x'.1 /ₒ x'.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'
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

Tactic:
refine ⟨s, s'.1, h, ?_⟩

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'
⊢ ↑s * ↑s' = ↑s' * ↑s