-- Mathlib/GroupTheory/OreLocalization/Cardinality.lean
theorem oreDiv_one_surjective_of_finite_right [Finite X] :
    Surjective (fun x ↦ x /ₒ (1 : ↥S) : X → OreLocalization S X)

Proof state:
case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

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

Result:
no goals

Proof state:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1

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

Result:
case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = ↑(s ^ (j + 1)) • s ^ (i - (j + 1)) • x

case h.refine_2
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ↑(s ^ j) * ↑s = ↑(s ^ (j + 1)) * ↑1

Proof state:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ a, (fun x => x /ₒ 1) a = x /ₒ s

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

Result:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ (fun x => x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s

Proof state:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
⊢ Surjective fun x => x /ₒ 1

Tactic:
refine OreLocalization.ind fun x s ↦ ?_

Result:
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
⊢ ∃ a, (fun x => x /ₒ 1) a = x /ₒ s

Proof state:
case h.refine_2
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ↑(s ^ j) * ↑s = ↑(s ^ (j + 1)) * ↑1

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

Result:
no goals

Proof state:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ (fun x => x /ₒ 1) (s ^ (i - (j + 1)) • x) = x /ₒ s

Tactic:
rw [oreDiv_eq_iff]

Result:
case h
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ u v, u • x = v • s ^ (i - (j + 1)) • x ∧ ↑u * ↑s = v * ↑1

Proof state:
case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = ↑(s ^ (j + 1)) • s ^ (i - (j + 1)) • x

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

Result:
case h.refine_1
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ s ^ j • x = s ^ (j + 1) • s ^ (i - (j + 1)) • x

Proof state:
case intro.intro.intro
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
⊢ ∃ a, (fun x => x /ₒ 1) a = x /ₒ s

Tactic:
wlog hlt : j < i generalizing i j

Result:
case intro.intro.intro.inr
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
this : ∀ (i j : ℕ), i ≠ j → s ^ i • x = s ^ j • x → j < i → ∃ a, (fun x => x /ₒ 1) a = x /ₒ s
hlt : ¬j < i
⊢ ∃ a, (fun x => x /ₒ 1) a = x /ₒ s

R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
hlt : j < i
⊢ ∃ a, (fun x => x /ₒ 1) a = x /ₒ s

Proof state:
case intro.intro.intro.inr
R : Type u
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type v
inst✝¹ : MulAction R X
inst✝ : Finite X
x : X
s : ↥S
i j : ℕ
hne : i ≠ j
heq : s ^ i • x = s ^ j • x
this : ∀ (i j : ℕ), i ≠ j → s ^ i • x = s ^ j • x → j < i → ∃ a, (fun x => x /ₒ 1) a = x /ₒ s
hlt : ¬j < i
⊢ ∃ a, (fun x => x /ₒ 1) a = x /ₒ s

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

Result:
no goals