-- 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.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:
exact key x.1 x.2 x'.2 h2 (hc _ _)

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
⊢ Injective j

Tactic:
intro y y' 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 : j y = j y'
⊢ y = 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'
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'
⊢ y = y'

Tactic:
rw [← hi y, ← hi 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
heq : j y = j y'
⊢ i (surjInv hsurj y) = i (surjInv hsurj y')

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

Tactic:
rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] 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
⊢ (surjInv hsurj y).1 /ₒ (surjInv hsurj y).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
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

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

Tactic:
suffices Injective j by
  have := lift_mk_le_lift_mk_of_injective this
  rwa [lift_umax.{v, u}, lift_id', mk_prod, lift_id, lift_mul, mul_eq_self (by simp)] at this

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
⊢ Injective j

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

Tactic:
have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)

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
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #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
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ ↑s * ↑s' = ↑s' * ↑s

Tactic:
exact_mod_cast hc

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

Tactic:
have hsurj : Surjective i := Quotient.mk''_surjective

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