awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Eq.{u_6 + 1} (α := R) (↑(p * n) : R) 0
have mpr₁ : HMul.hMul (α := R) 0 (↑n : R) = 0
Tactic: rw [Nat.cast_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ Eq.{u_6 + 1} (α := R) (↑(p * n) : R) 0
have mpr₂ : Eq.{u_6 + 1} (α := R) 0 0
Tactic: rw [Nat.cast_mul, H, zero_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ CharP R (p ^ n)
have obtain : ∀ (c : ℕ) (hc : CharP R c), CharP R (p ^ n)
Tactic: obtain ⟨c, hc⟩ := CharP.exists R
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
have rw : Eq.{u_6 + 1} (α := R) (↑(p ^ n) : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ c ∣ p ^ n
have rw₁ : Eq.{u_6 + 1} (α := R) (↑(card R) : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ c ∣ p ^ n
have rw₂ : Eq.{u_6 + 1} (α := R) 0 0
Tactic: rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (hypothesis)
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
⊢ CharP R (p ^ n)
have hcpn : c ∣ p ^ n
Tactic: have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ ∃ i ≤ n, c = p ^ i
have rwa : ∀ (hcpn : ∃ k ≤ n, c = p ^ k), ∃ i ≤ n, c = p ^ i
Tactic: rwa [Nat.dvd_prime_pow hp.1] at hcpn
Cleared hypotheses: hcpn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ CharP R (p ^ n)
have obtain : ∀ (i : ℕ) (hi : i ≤ n) (hc : CharP R (p ^ i)) (hcpn : p ^ i ∣ 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
Cleared hypotheses: c, hc, hcpn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ HPow.hPow (α := R) (↑p : R) i = 0
have rw : Eq.{u_6 + 1} (α := R) (↑(p ^ i) : R) 0
Tactic: rw [← Nat.cast_pow, CharP.cast_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ HPow.hPow (α := R) (↑p : R) i = 0
have rw₁ : Eq.{u_6 + 1} (α := R) 0 0
Tactic: rw [← Nat.cast_pow, CharP.cast_eq_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
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
⊢ CharP R (p ^ n)
have 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)
Tactic: obtain rfl : i = n := hR i hi <| by rw [← Nat.cast_pow, CharP.cast_eq_zero]
Cleared hypotheses: n, hn, hR, hi, hcpn
-- Lean 4 proof step from Mathlib.GroupTheory.OrderOfElement (goal)
Goal:
G : Type u_1
inst : Group G
a x y : G
h : SemiconjBy a x y
⊢ orderOf x = orderOf y
have rw : ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
Tactic: rw [orderOf_eq_orderOf_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type u_2
inst_2 : MulAction R X
⊢ 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)
have 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)
Tactic: refine ⟨fun _ => ⟨1, 1, by simp⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: refine ⟨fun _ => ⟨1, 1, by simp⟩, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ ∃ (u : ↥S), ∃ (v : R), u • (r, s).fst = v • (r', s').fst ∧ (↑u : R) * (↑(r, s).snd : R) = v * (↑(r', s').snd : R)
have refine_1 : ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
Tactic: dsimp only at *
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
have 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)
Tactic: rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
have 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)
Tactic: rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
have rw : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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))
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
have rw₁ : r₃ * v * (↑s : R) = (↑s₃ : R) * (r₂ * (↑s' : R))
Tactic: rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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))
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
have rw₂ : r₃ * v * (↑s : R) = (↑s₃ : R) * r₂ * (↑s' : R)
Tactic: rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
have rw₃ : r₃ * v * (↑s : R) = r₃ * (↑u : R) * (↑s' : R)
Tactic: rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
have rw₄ : r₃ * (v * (↑s : R)) = r₃ * (↑u : R) * (↑s' : R)
Tactic: rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
have rw₅ : r₃ * ((↑u : R) * (↑s' : R)) = r₃ * (↑u : R) * (↑s' : R)
Tactic: rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ r₃ * v * (↑s : R) = (↑s₃ : R) * (↑s₂ : R) * (↑s : R)
have rw₆ : r₃ * (↑u : R) * (↑s' : R) = r₃ * (↑u : R) * (↑s' : R)
Tactic: rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (hypothesis)
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)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
have this : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
have 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)
Tactic: rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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)
have refine_1 : (w * (s₃ * s₂)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'
Tactic: refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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'
⊢ ∃ (u : ↥S), ∃ (v : R), u • r = v • r' ∧ (↑u : R) * (↑s : R) = v * (↑s' : R)
have refine_1₁ : (↑(w * (s₃ * s₂)) : R) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)
Tactic: refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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 * (s₃ * s₂)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'
have refine_1 : ((↑w : R) * (r₃ * v)) • r = ((↑w : R) * (r₃ * (↑u : R))) • r'
Tactic: simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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 * (s₃ * s₂)) : R) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)
have refine_1 : (↑w : R) * (r₃ * v) * (↑s : R) = (↑w : R) * (r₃ * (↑u : R)) * (↑s' : R)
Tactic: simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : (↑u : R) * (↑(r₂, s₂).snd : R) = v * (↑(r₁, s₁).snd : R)
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : (↑u' : R) * (↑(r₃, s₃).snd : R) = v' * (↑(r₂, s₂).snd : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ (↑u : R) * (↑(r₃, s₃).snd : R) = v * (↑(r₁, s₁).snd : R)
have refine_2 : ∀ (r' : R) (s' : ↥S) (h : (↑s' : R) * v' = r' * (↑u : 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: rcases oreCondition v' u with ⟨r', s', h⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : (↑u : R) * (↑(r₂, s₂).snd : R) = v * (↑(r₁, s₁).snd : R)
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : (↑u' : R) * (↑(r₃, s₃).snd : R) = v' * (↑(r₂, s₂).snd : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ (↑u : R) * (↑(r₃, s₃).snd : R) = v * (↑(r₁, s₁).snd : R)
have refine_2 : ∃ (u : ↥S), ∃ (v : R), u • r₃ = v • r₁ ∧ (↑u : R) * (↑s₃ : R) = v * (↑s₁ : R)
Tactic: dsimp only at *
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ ∃ (u : ↥S), ∃ (v : R), u • r₃ = v • r₁ ∧ (↑u : R) * (↑s₃ : R) = v * (↑s₁ : R)
have refine_2 : (s' * u') • r₃ = (r' * v) • r₁
Tactic: refine ⟨s' * u', r' * v, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (s' * u') • r₃ = (r' * v) • r₁
⊢ ∃ (u : ↥S), ∃ (v : R), u • r₃ = v • r₁ ∧ (↑u : R) * (↑s₃ : R) = v * (↑s₁ : R)
have refine_2₁ : (↑(s' * u') : R) * (↑s₃ : R) = r' * v * (↑s₁ : R)
Tactic: refine ⟨s' * u', r' * v, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ (s' * u') • r₃ = (r' * v) • r₁
have refine_2 : (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
Tactic: simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : u' • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ (↑(s' * u') : R) * (↑s₃ : R) = r' * v * (↑s₁ : R)
have refine_2 : (↑s' : R) * ((↑u' : R) * (↑s₃ : R)) = r' * (v * (↑s₁ : R))
Tactic: simp only [Submonoid.smul_def, Submonoid.coe_mul, mul_smul, mul_assoc] at *
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
⊢ (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
have refine_2 : (↑s' : R) • v' • r₂ = r' • v • r₁
Tactic: rw [hur₂, smul_smul, h, mul_smul, hur₁]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Basic (goal)
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₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : (↑u : R) • r₂ = v • r₁
hs₁u : (↑u : R) * (↑s₂ : R) = v * (↑s₁ : R)
u' : ↥S
v' : R
hur₂ : (↑u' : R) • r₃ = v' • r₂
hs₂u : (↑u' : R) * (↑s₃ : R) = v' * (↑s₂ : R)
r' : R
s' : ↥S
h : (↑s' : R) * v' = r' * (↑u : R)
refine_2 : (↑s' : R) • v' • r₂ = r' • v • r₁
⊢ (↑s' : R) • (↑u' : R) • r₃ = r' • v • r₁
have refine_2₁ : ((↑s' : R) * v') • r₂ = r' • v • r₁
Tactic: rw [hur₂, smul_smul, h, mul_smul, hur₁]