awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
h : Eq.{u_1 + 1} (α := G) |1| 1
⊢ orderOf.{u_1} (G := G) 1 ≤ 2

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
h : Eq.{u_1 + 1} (α := G) |(-1)| 1
⊢ HPow.hPow (α := G) (β := ℕ) (-1) 2 = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Ring G
inst_1 : LinearOrder G
inst_2 : IsStrictOrderedRing G
h : Eq.{u_1 + 1} (α := G) |(-1)| 1
⊢ orderOf.{u_1} (G := G) (-1) ≤ 2

Tactic:
exact orderOf_le_of_pow_eq_one zero_lt_two (by simp)

Premises used: zero_lt_two, orderOf_le_of_pow_eq_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
x : α × β
⊢ orderOf x = (orderOf x.1).lcm (orderOf x.2)

Tactic:
minimalPeriod_prodMap _ _ _

Premises used: Function.minimalPeriod_prodMap, Prod.map, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
x : α × β
⊢ orderOf x.1 ∣ orderOf x

Tactic:
minimalPeriod_fst_dvd

Premises used: Prod.map, orderOf, Function.minimalPeriod_fst_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
x : α × β
⊢ orderOf x.2 ∣ orderOf x

Tactic:
minimalPeriod_snd_dvd

Premises used: Prod.map, orderOf, Function.minimalPeriod_snd_dvd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
x : α × β
hx : IsOfFinOrder x
⊢ IsOfFinOrder x.1

Tactic:
hx.mono orderOf_fst_dvd_orderOf

Premises used: IsOfFinOrder.mono, orderOf_fst_dvd_orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
x : α × β
hx : IsOfFinOrder x
⊢ IsOfFinOrder x.2

Tactic:
hx.mono orderOf_snd_dvd_orderOf

Premises used: IsOfFinOrder.mono, orderOf_snd_dvd_orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
a : α
b : β
⊢ IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Tactic:
simpa only [← orderOf_pos_iff, Prod.orderOf] using Nat.lcm_pos

Premises used: Nat.lcm_pos, orderOf_pos_iff, Prod.orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
x : α × β
⊢ IsOfFinOrder x ↔ IsOfFinOrder x.1 ∧ IsOfFinOrder x.2

Tactic:
⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ .prod_mk h.1 h.2⟩

Premises used: And.right, And.left, And.intro, IsOfFinOrder.prod_mk, Iff.intro, IsOfFinOrder.fst, IsOfFinOrder.snd
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
α : Type u_4
β : Type u_5
inst : Monoid α
inst_1 : Monoid β
a : α
b : β
⊢ orderOf (a, b) = (orderOf a).lcm (orderOf b)

Tactic:
(a, b).orderOf

Premises used: Prod.mk, Prod.orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
⊢ orderOf x = sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), orderOf (x i) ∣ n}

Tactic:
minimalPeriod_piMap

Premises used: Set.Mem, setOf, Function.minimalPeriod_piMap, Pi.map, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
inst_1 : Fintype ι
x : (i : ι) → α i
⊢ orderOf x = Finset.lcm Finset.univ fun (i : ι) ↦ orderOf (x i)

Tactic:
minimalPeriod_piMap_fintype

Premises used: Function.minimalPeriod_piMap_fintype, Pi.map, orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
⊢ ∀ (i : ι), orderOf (x i) ∣ orderOf x

Tactic:
minimalPeriod_single_dvd_minimalPeriod_piMap

Premises used: Pi.map, orderOf, Function.minimalPeriod_single_dvd_minimalPeriod_piMap
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst_1 : Finite ι
have : ∀ (this : Fintype ι), (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst_1 : Finite ι
this : Fintype ι
simp : (∀ (i : ι), orderOf (x i) ≠ 0) → Ne (α := ℕ) (Finset.lcm Finset.univ fun (i : ι) ↦ orderOf (x i)) 0
⊢ (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

Tactic:
simp only [← orderOf_ne_zero_iff, Pi.orderOf]

Premises used: orderOf_ne_zero_iff, Pi.orderOf
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
α : ι → Type u_7
inst : (i : ι) → Monoid (α i)
x : (i : ι) → α i
inst_1 : Finite ι
this : Fintype ι
⊢ (∀ (i : ι), orderOf (x i) ≠ 0) → Ne (α := ℕ) (Finset.lcm Finset.univ fun (i : ι) ↦ orderOf (x i)) 0

Tactic:
simp [Finset.lcm_eq_zero_iff]

Premises used: Finset.lcm_eq_zero_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : AddGroupWithOne R
inst_1 : Fintype R
rw : HSMul.hSMul (β := R) (card R) 1 = 0
rw₁ rw₂ : Eq.{u_6 + 1} (α := R) 0 0
⊢ Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0

Tactic:
rw [← nsmul_one, card_nsmul_eq_zero]

Premises used: card_nsmul_eq_zero, nsmul_one
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
n : ℕ
rw : HSMul.hSMul (β := R) n 1 = 0 ↔ addOrderOf.{u_6} (G := R) 1 ∣ n
rw₁ rw₂ : HSMul.hSMul (β := R) n 1 = 0 ↔ HSMul.hSMul (β := R) n 1 = 0
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ addOrderOf.{u_6} (G := R) 1 ∣ n

Tactic:
rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]

Premises used: addOrderOf_dvd_iff_nsmul_eq_zero, Nat.smul_one_eq_cast
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
rw : Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
rw₁ rw₂ : Eq.{u_6 + 1} (α := R) 0 0
⊢ Eq.{u_6 + 1} (α := R) (↑p : R) 0

Tactic:
rw [← hn, Nat.cast_card_eq_zero]

Premises used: Nat.cast_card_eq_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
⊢ Eq.{u_6 + 1} (α := R) (↑p : R) 0

Tactic:
have H : (p : R) = 0 := by rw [← hn, Nat.cast_card_eq_zero]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
mp : Eq.{u_6 + 1} (α := R) (↑n : R) 0 → p ∣ n
mpr : p ∣ n → Eq.{u_6 + 1} (α := R) (↑n : R) 0
⊢ Eq.{u_6 + 1} (α := R) (↑n : R) 0 ↔ p ∣ n

Tactic:
constructor
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑n : R) 0
⊢ Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0

Tactic:
rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h

Premises used: MulZeroClass.zero_mul, Nat.cast_add, Nat.mod_add_div, Nat.cast_mul, add_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
mp : n % p = 0
⊢ p ∣ n

Tactic:
rw [Nat.dvd_iff_mod_eq_zero]

Premises used: Nat.dvd_iff_mod_eq_zero
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
apply : 0 < p
⊢ n % p = 0

Tactic:
apply hR _ (Nat.mod_lt _ _) h

Premises used: Nat.mod_lt
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
rw : Nonempty R
⊢ 0 < p

Tactic:
rw [← hn, Fintype.card_pos_iff]

Premises used: Fintype.card_pos_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
⊢ Nonempty R

Tactic:
⟨0⟩

Premises used: Nonempty.intro, OfNat.ofNat
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
n : ℕ
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
h : Eq.{u_6 + 1} (α := R) (↑(n % p) : R) 0
⊢ Nonempty R

Tactic:
exact ⟨0⟩
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : NonAssocRing R
p : ℕ
inst_1 : Fintype R
hn : card R = p
hR : ∀ i < p, Eq.{u_6 + 1} (α := R) (↑i : R) 0 → i = 0
H : Eq.{u_6 + 1} (α := R) (↑p : R) 0
n : ℕ
mpr : HMul.hMul (α := R) (↑p : R) (↑n : R) = 0
mpr₁ : HMul.hMul (α := R) 0 (↑n : R) = 0
mpr₂ mpr₃ : Eq.{u_6 + 1} (α := R) 0 0
⊢ Eq.{u_6 + 1} (α := R) (↑(p * n) : R) 0

Tactic:
rw [Nat.cast_mul, H, zero_mul]

Premises used: MulZeroClass.zero_mul, Nat.cast_mul
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
obtain : ∀ (c : ℕ) (hc : CharP R c), CharP R (p ^ n)
⊢ CharP R (p ^ n)

Tactic:
obtain ⟨c, hc⟩ := CharP.exists R

Premises used: CharP.exists
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
c : ℕ
hc : CharP R c
rw : Eq.{u_6 + 1} (α := R) (↑(p ^ n) : R) 0
rw₁ : Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
rw₂ rw₃ : Eq.{u_6 + 1} (α := R) 0 0
⊢ c ∣ p ^ n

Tactic:
rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]

Premises used: Nat.cast_card_eq_zero, CharP.cast_eq_zero_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
c : ℕ
hc : CharP R c
⊢ c ∣ p ^ n

Tactic:
have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
rwa rwa₁ rwa₂ rwa₃ : ∀ (hcpn : ∃ k ≤ n, c = p ^ k), ∃ i ≤ n, c = p ^ i
⊢ ∃ i ≤ n, c = p ^ i

Tactic:
rwa [Nat.dvd_prime_pow hp.1] at hcpn

Premises used: Fact.out, Nat.dvd_prime_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
c : ℕ
hc : CharP R c
hcpn : c ∣ p ^ n
obtain : ∀ (i : ℕ) (hi : i ≤ n) (hc : CharP R (p ^ i)) (hcpn : p ^ i ∣ p ^ n), CharP R (p ^ n)
⊢ CharP R (p ^ n)

Tactic:
obtain ⟨i, hi, rfl⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn

Premises used: rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
rw : Eq.{u_6 + 1} (α := R) (↑(p ^ i) : R) 0
rw₁ rw₂ : Eq.{u_6 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) (↑p : R) i = 0

Tactic:
rw [← Nat.cast_pow, CharP.cast_eq_zero]

Premises used: CharP.cast_eq_zero, Nat.cast_pow
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p n : ℕ
hp : Fact (Nat.Prime p)
hn : card R = p ^ n
hR : ∀ i ≤ n, HPow.hPow (α := R) (↑p : R) i = 0 → i = n
i : ℕ
hi : i ≤ n
hc : CharP R (p ^ i)
hcpn : p ^ i ∣ p ^ n
obtain :
  ∀ (hn : card R = p ^ i) (hR : ∀ i_1 ≤ i, HPow.hPow (α := R) (↑p : R) i_1 = 0 → i_1 = i) (hi : i ≤ i)
    (hcpn : p ^ i ∣ p ^ i), CharP R (p ^ i)
⊢ CharP R (p ^ n)

Tactic:
obtain rfl : i = n := hR i hi <| by rw [← Nat.cast_pow, CharP.cast_eq_zero]

Premises used: rfl
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
R : Type u_6
inst : Ring R
inst_1 : Fintype R
p : ℕ
hp : Fact (Nat.Prime p)
i : ℕ
hc : CharP R (p ^ i)
hn : card R = p ^ i
hR : ∀ i_1 ≤ i, HPow.hPow (α := R) (↑p : R) i_1 = 0 → i_1 = i
hi : i ≤ i
hcpn : p ^ i ∣ p ^ i
⊢ CharP R (p ^ i)

Tactic:
assumption
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
rw : ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
⊢ orderOf x = orderOf y

Tactic:
rw [orderOf_eq_orderOf_iff]

Premises used: orderOf_eq_orderOf_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ x ^ n = 1 ↔ y ^ n = 1

Tactic:
(h.pow_right n).eq_one_iff

Premises used: SemiconjBy.pow_right, SemiconjBy.eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ x ^ n = 1 ↔ y ^ n = 1

Tactic:
exact (h.pow_right n).eq_one_iff

Premises used: SemiconjBy.pow_right, SemiconjBy.eq_one_iff
-- Module: Mathlib.GroupTheory.OrderOfElement
Goal:
ι : Type u_6
inst : DecidableEq ι
M : ι → Type u_7
inst_1 : (i : ι) → Monoid (M i)
i : ι
g : M i
⊢ orderOf (Pi.mulSingle (M := M) i g) = orderOf g

Tactic:
orderOf_injective (MonoidHom.mulSingle M i) (Pi.mulSingle_injective i) g

Premises used: Function.update, MonoidHom.mulSingle, dite, Pi.mulSingle_injective, Pi.mulSingle, orderOf_injective
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
x : Prod.{u_2, u_1} X ↥S
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := ↥S) 1 x.fst = HSMul.hSMul.{u_1, u_2, u_2} (α := R) 1 x.fst ∧
    (↑1 : R) * (↑x.snd : R) = 1 * (↑x.snd : R)

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
refine_1 :
  ∀ {x y : Prod.{u_2, u_1} X ↥S},
    (∃ (u : ↥S), ∃ (v : R), u • y.fst = v • x.fst ∧ (↑u : R) * (↑y.snd : R) = v * (↑x.snd : R)) →
      ∃ (u : ↥S), ∃ (v : R), u • x.fst = v • y.fst ∧ (↑u : R) * (↑x.snd : R) = v * (↑y.snd : R)
refine_2 :
  ∀ {x y z : Prod.{u_2, u_1} X ↥S},
    (∃ (u : ↥S), ∃ (v : R), u • y.fst = v • x.fst ∧ (↑u : R) * (↑y.snd : R) = v * (↑x.snd : R)) →
      (∃ (u : ↥S), ∃ (v : R), u • z.fst = v • y.fst ∧ (↑u : R) * (↑z.snd : R) = v * (↑y.snd : R)) →
        ∃ (u : ↥S), ∃ (v : R), u • z.fst = v • x.fst ∧ (↑u : R) * (↑z.snd : R) = v * (↑x.snd : R)
⊢ Equivalence fun (rs rs' : Prod.{u_2, u_1} X ↥S) ↦
    ∃ (u : ↥S), ∃ (v : R), u • rs'.fst = v • rs.fst ∧ (↑u : R) * (↑rs'.snd : R) = v * (↑rs.snd : R)

Tactic:
refine ⟨fun _ => ⟨1, 1, by simp⟩, ?_, ?_⟩
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • (r', s').fst = v • (r, s).fst
hsu : (↑u : R) * (↑(r', s').snd : R) = v * (↑(r, s).snd : R)
refine_1 : ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • (r, s).fst = v • (r', s').fst ∧ (↑u : R) * (↑(r, s).snd : R) = v * (↑(r', s').snd : R)

Tactic:
dsimp only at *
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
refine_1 :
  ∀ (r₂ : R) (s₂ : ↥S) (h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)),
    ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)

Tactic:
rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩

Premises used: OreLocalization.oreCondition, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
refine_1 :
  ∀ (r₃ : R) (s₃ : ↥S) (h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)),
    ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)

Tactic:
rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩

Premises used: OreLocalization.oreCondition
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
rw : r₃ * v * (↑s : R) = (↑s₃ : R) * ((↑s₂ : R) * (↑s : R))
rw₁ : r₃ * v * (↑s : R) = (↑s₃ : R) * (r₂ * (↑s' : R))
rw₂ : r₃ * v * (↑s : R) = (↑s₃ : R) * r₂ * (↑s' : R)
rw₃ : r₃ * v * (↑s : R) = r₃ * (↑u : R) * (↑s' : R)
rw₄ : r₃ * (v * (↑s : R)) = r₃ * (↑u : R) * (↑s' : R)
rw₅ : r₃ * ((↑u : R) * (↑s' : R)) = r₃ * (↑u : R) * (↑s' : R)
rw₆ rw₇ : r₃ * (↑u : R) * (↑s' : R) = r₃ * (↑u : R) * (↑s' : R)
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)

Tactic:
rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]

Premises used: mul_assoc, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)

Tactic:
have : r₃ * v * s = s₃ * s₂ * s := by
        -- Porting note: the proof used `assoc_rw`
        rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
refine_1 :
  ∀ (w : ↥S) (hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))),
    ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)

Tactic:
rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩

Premises used: HMul.hMul, OreLocalization.ore_right_cancel, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
w : ↥S
hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)

Tactic:
⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
w : ↥S
hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))
refine_1 : (w * (s₃ * s₂)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'
refine_1₁ : (↑(w * (s₃ * s₂)) : R) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)

Tactic:
refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
w : ↥S
hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))
refine_1 : ((↑w : R) * (r₃ * v)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'
⊢ (w * (s₃ * s₂)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'

Tactic:
simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]

Premises used: Submonoid.smul_def, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
w : ↥S
hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))
refine_1 : (↑w : R) * (r₃ * v) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)
⊢ (↑(w * (s₃ * s₂)) : R) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)

Tactic:
simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]

Premises used: Submonoid.smul_def, Submonoid.coe_mul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
w : ↥S
hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))
⊢ ((↑w : R) * (r₃ * v)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'

Tactic:
simp only [mul_smul, hru, ← Submonoid.smul_def]

Premises used: Submonoid.smul_def, SemigroupAction.mul_smul
-- Module: Mathlib.GroupTheory.OreLocalization.Basic
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : (↑u : R) * (↑s' : R) = v * (↑s : R)
r₂ : R
s₂ : ↥S
h₁ : (↑s₂ : R) * (↑s : R) = r₂ * (↑s' : R)
r₃ : R
s₃ : ↥S
h₂ : (↑s₃ : R) * r₂ = r₃ * (↑u : R)
this : r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
w : ↥S
hw : (↑w : R) * (r₃ * v) = (↑w : R) * ((↑s₃ : R) * (↑s₂ : R))
⊢ (↑w : R) * (r₃ * v) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)

Tactic:
simp only [mul_assoc, hsu]

Premises used: mul_assoc