awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc_1 : ∀ (s s' : ↥S), Commute s s'
h_1 : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
have rw : ∃ (u : ↥S) (v : R), u • x = v • x ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)
Tactic: rw [oreDiv_eq_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc_1 : ∀ (s s' : ↥S), Commute s s'
h_1 : Infinite X
x : X
s s' : ↥S
h : s • x = s' • x
hc : Commute s s'
⊢ ∃ (u : ↥S) (v : R), u • x = v • x ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)
have refine : (↑s : R) * (↑s' : R) = (↑s' : R) * (↑s : R)
Tactic: refine ⟨s, s'.1, h, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
Tactic: have key (x : X) (s s' : S) (h : s • x = s' • x) (hc : Commute s s') : x /ₒ s = x /ₒ s' := by
    rw [oreDiv_eq_iff]
    refine ⟨s, s'.1, h, ?_⟩
    · exact_mod_cast hc
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have hsurj : Surjective i
Tactic: have hsurj : Surjective i := Quotient.mk''_surjective
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have hi : RightInverse (surjInv hsurj) i
Tactic: have hi := rightInverse_surjInv hsurj
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (hypothesis)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this : Injective j
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have this₁ : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
Tactic: have := lift_mk_le_lift_mk_of_injective this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this_1 : 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
have rwa : ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this_1 : Injective j
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
rwa :
  ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have rwa₁ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this_1 : Injective j
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
rwa :
  ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₁ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have rwa₂ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} (lift.{v, v} #X * lift.{v, v} #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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this_1 : Injective j
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
rwa :
  ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₁ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₂ :
  ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} (lift.{v, v} #X * lift.{v, v} #X)),
    #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have rwa₃ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this_1 : Injective j
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
rwa :
  ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₁ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₂ :
  ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} (lift.{v, v} #X * lift.{v, v} #X)),
    #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₃ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} (#X * #X)), #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have rwa₄ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #X * lift.{u, v} #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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
this_1 : Injective j
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #(X × X)
rwa :
  ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₁ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #(X × X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₂ :
  ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} (lift.{v, v} #X * lift.{v, v} #X)),
    #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₃ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} (#X * #X)), #(OreLocalization S X) ≤ lift.{u, v} #X
rwa₄ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #X * lift.{u, v} #X), #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have rwa₅ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.Cardinality (goal)
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
X : Type v
inst_2 : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h : Infinite X
key : ∀ (x : X) (s s' : ↥S) (h : s • x = s' • x) (hc : Commute s s'), Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')
i : (x : Prod.{v, u} X ↥S) → OreLocalization S X := fun (x : Prod.{v, u} X ↥S) ↦ x.1 /ₒ x.2
hsurj : Surjective i
hi : RightInverse (surjInv hsurj) i
j : OreLocalization S X → X × X := (fun (x : Prod.{v, u} X ↥S) ↦ (x.1, x.2 • x.1)) ∘ surjInv hsurj
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
have inr : Injective j
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
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x x_1 : R
s : ↥⊥
h : x * (↑s : R) = x_1 * (↑s : R)
⊢ (↑s : R) * x = (↑s : R) * x_1
have rcases : ∀ (s : R) (hs : Membership.mem (γ := Submonoid R) ⊥ s)
  (h :
    x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) =
      x_1 * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R)),
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) * x_1
Tactic: rcases s with ⟨s, hs⟩
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x x_1 s : R
hs : Membership.mem (γ := Submonoid R) ⊥ s
h :
  x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) =
    x_1 * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) * x_1
have hs₁ : s = 1
Tactic: rw [Submonoid.mem_bot] at hs
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x x_1 s : R
hs_1 : Membership.mem (γ := Submonoid R) ⊥ s
hs : s = 1
h :
  x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs_1) : R) =
    x_1 * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs_1) : R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs_1) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs_1) : R) * x_1
have subst : ∀ (hs : Membership.mem (γ := Submonoid R) ⊥ 1)
  (h :
    x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) =
      x_1 * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R)),
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x_1
Tactic: subst hs
Cleared hypotheses: s, hs_1, hs, h
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x x_1 : R
hs : Membership.mem (γ := Submonoid R) ⊥ 1
h :
  x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) =
    x_1 * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R)
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x_1
have h₁ : x = x_1
Tactic: rw [mul_one, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x x_1 : R
hs : Membership.mem (γ := Submonoid R) ⊥ 1
h : x = x_1
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x =
    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x_1
have subst : (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x =
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) 1 hs) : R) * x
Tactic: subst h
Cleared hypotheses: x_1, h
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x : R
s : ↥⊥
⊢ (↑s : R) * x = x * (↑s : R)
have rcases : ∀ (s : R) (hs : Membership.mem (γ := Submonoid R) ⊥ s),
  (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) * x =
    x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R)
Tactic: rcases s with ⟨s, hs⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x s : R
hs : Membership.mem (γ := Submonoid R) ⊥ s
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R) * x =
    x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs) : R)
have hs₁ : s = 1
Tactic: rw [Submonoid.mem_bot] at hs
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R_1 : Type u_1
inst : Monoid R_1
S_1 : Submonoid R_1
inst_1 : OreSet S_1
R : Type u_2
inst_2 : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * (↑s : R) = n * (↑s : R)
⊢ (↑s : R) * m = (↑s : R) * n
have rw : (↑s : R) * m = n * (↑s : R)
Tactic: rw [mul_comm (s : R) n, mul_comm (s : R) m, h]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R_1 : Type u_1
inst : Monoid R_1
S_1 : Submonoid R_1
inst_1 : OreSet S_1
R : Type u_2
inst_2 : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * (↑s : R) = n * (↑s : R)
rw : (↑s : R) * m = n * (↑s : R)
rw₁ : m * (↑s : R) = n * (↑s : R)
⊢ (↑s : R) * m = (↑s : R) * n
have rw₂ : n * (↑s : R) = n * (↑s : R)
Tactic: rw [mul_comm (s : R) n, mul_comm (s : R) m, h]
-- Lean 4 proof step from Mathlib.GroupTheory.OreLocalization.OreSet (goal)
Goal:
R_1 : Type u_1
inst : Monoid R_1
S_1 : Submonoid R_1
inst_1 : OreSet S_1
R : Type u_2
inst_2 : CommMonoid R
S : Submonoid R
r : R
s : ↥S
⊢ (↑s : R) * r = r * (↑s : R)
have rw : r * (↑s : R) = r * (↑s : R)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
g : G
k : ℕ
hk : orderOf g = p ^ k
⊢ g ^ p ^ k = 1
have rw : g ^ orderOf g = 1
Tactic: rw [← hk, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hp : Fact (Nat.Prime p)
g : G
k : ℕ
hk : orderOf g = p ^ k
rw : g ^ orderOf g = 1
⊢ g ^ p ^ k = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← hk, pow_orderOf_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
n : ℕ
hG : Nat.card G = p ^ n
g : G
⊢ g ^ p ^ n = 1
have rw : g ^ Nat.card G = 1
Tactic: rw [← hG, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
n : ℕ
hG : Nat.card G = p ^ n
g : G
rw : g ^ Nat.card G = 1
⊢ g ^ p ^ n = 1
have rw₁ : Eq.{u_1 + 1} (α := G) 1 1
Tactic: rw [← hG, pow_card_eq_one']
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
⊢ Nat.card.{u_1} ↥⊥ = HPow.hPow (β := ℕ) p 0
have rw : 1 = HPow.hPow (β := ℕ) p 0
Tactic: rw [Subgroup.card_bot, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
rw : 1 = HPow.hPow (β := ℕ) p 0
⊢ Nat.card.{u_1} ↥⊥ = HPow.hPow (β := ℕ) p 0
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [Subgroup.card_bot, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
⊢ IsPGroup p G ↔ ∃ (n : ℕ), Nat.card G = p ^ n
have hG : Nat.card G ≠ 0
Tactic: have hG : Nat.card G ≠ 0 := Nat.card_pos.ne'
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
⊢ IsPGroup p G ↔ ∃ (n : ℕ), Nat.card G = p ^ n
have refine : ∀ (h : IsPGroup p G), ∃ (n : ℕ), Nat.card G = p ^ n
Tactic: refine ⟨fun h => ?_, fun ⟨n, hn⟩ => of_card hn⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
⊢ ∃ (n : ℕ), Nat.card G = p ^ n
have h₁ : Nat.card G = p ^ (Nat.card G).primeFactorsList.length
Tactic: use (Nat.card G).primeFactorsList.length
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
⊢ Nat.card G = p ^ (Nat.card G).primeFactorsList.length
have h₁ : Nat.card G = (List.replicate (Nat.card G).primeFactorsList.length p).prod
Tactic: rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
h₁ : Nat.card G = (List.replicate (Nat.card G).primeFactorsList.length p).prod
⊢ Nat.card G = p ^ (Nat.card G).primeFactorsList.length
have h₂ : Nat.card G = (Nat.card G).primeFactorsList.prod
Tactic: rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
this : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
h₁ : Nat.card G = (List.replicate (Nat.card G).primeFactorsList.length p).prod
h₂ : Nat.card G = (Nat.card G).primeFactorsList.prod
⊢ Nat.card G = p ^ (Nat.card G).primeFactorsList.length
have h₃ : Nat.card G = Nat.card G
Tactic: rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
⊢ ∃ (n : ℕ), Nat.card G = p ^ n
have suffices : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
Tactic: suffices ∀ q ∈ (Nat.card G).primeFactorsList, q = p by
    use (Nat.card G).primeFactorsList.length
    rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
⊢ q = p
have hq1 : Nat.Prime q
Tactic: obtain ⟨hq1, hq2⟩ := (Nat.mem_primeFactorsList hG).mp hq
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
⊢ q = p
have hq2 : q ∣ Nat.card G
Tactic: obtain ⟨hq1, hq2⟩ := (Nat.mem_primeFactorsList hG).mp hq
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
⊢ q = p
have this : Fact (Nat.Prime q)
Tactic: haveI : Fact q.Prime := ⟨hq1⟩
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
⊢ q = p
have obtain : ∀ (g : G) (hg : orderOf g = q), q = p
Tactic: obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card' q hq2
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ (Nat.card G).primeFactorsList
hq1 : Nat.Prime q
hq2 : q ∣ Nat.card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p
have obtain : ∀ (k : ℕ) (hk : orderOf g = p ^ k), q = p
Tactic: obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g