-- Mathlib/GroupTheory/OreLocalization/Cardinality.lean
theorem cardinalMk_le_max : #(OreLocalization S X) ≤ max (lift.{v} #S) (lift.{u} #X)

Proof state:
case h.e'_4
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = lift.{v, u} #↥S ⊔ lift.{u, v} #X

Tactic:
refine mul_eq_max ?_ ?_ <;> simp

Result:
no goals

Proof state:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Tactic:
exact le_max_of_le_right this

Result:
no goals

Proof state:
case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ 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
h✝ : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Proof state:
case inr.inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ #(OreLocalization S X) ≤ 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)

Result:
case h.e'_4
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ #(X × ↥S) = lift.{v, u} #↥S ⊔ 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
h✝ : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

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

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

Proof state:
case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Tactic:
exact le_max_of_le_right this

Result:
no goals

Proof state:
case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Tactic:
have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_left S X)

Result:
case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Proof state:
case h.e'_4
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ #(X × ↥S) = lift.{v, u} #↥S ⊔ lift.{u, v} #X

Tactic:
rw [mk_prod, mul_comm]

Result:
case h.e'_4
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ lift.{v, u} #↥S * lift.{u, v} #X = lift.{v, u} #↥S ⊔ 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
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Tactic:
rcases finite_or_infinite S with _ | _

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

case inr.inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Infinite ↥S
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ 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
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ 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
h✝ : Finite X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ 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
h✝ : Infinite X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

Proof state:
case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X

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

Result:
case inr.inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
h✝¹ : Infinite X
h✝ : Finite ↥S
this : #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{v, u} #↥S ⊔ lift.{u, v} #X