awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
h : max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R
⊢ #(OreLocalization S R) ≤ #R

Tactic:
convert! ← cardinalMk_le_max S R

Premises used: OreLocalization.cardinalMk_le_max
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
Goal:
R : Type u
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
h : max #↥S #R = #R
h₁ : #↥S ≤ #R
⊢ max (lift.{u, u} #↥S) (lift.{u, u} #R) = #R

Tactic:
simp_rw [lift_id, max_eq_right_iff, mk_subtype_le]

Premises used: Cardinal.mk_subtype_le, max_eq_right_iff, Cardinal.lift_id
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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'
inl : Finite X → #(OreLocalization S X) ≤ lift.{u, v} #X
inr : Infinite X → #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
rcases finite_or_infinite X with _ | _

Premises used: finite_or_infinite
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : Finite X
⊢ lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X

Tactic:
have := lift_mk_le_lift_mk_of_surjective (oreDiv_one_surjective_of_finite_right S X)
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
inl : ∀ (this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{u, v} #X), #(OreLocalization S X) ≤ lift.{u, v} #X
inl₁ inl₂ inl₃ inl₄ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #X), #(OreLocalization S X) ≤ lift.{u, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

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

Premises used: Cardinal.lift_id'
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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'
rw : ∃ (u : ↥S) (v : R), u • x = v • x ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)
⊢ Eq (α := OreLocalization S X) (x /ₒ s) (x /ₒ s')

Tactic:
rw [oreDiv_eq_iff]

Premises used: OreLocalization.oreDiv_eq_iff
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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)

Tactic:
⟨s, s'.1, h, ?_⟩

Premises used: And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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'
refine : (↑s : R) * (↑s' : R) = (↑s' : R) * (↑s : R)
⊢ ∃ (u : ↥S) (v : R), u • x = v • x ∧ (↑u : R) * (↑s' : R) = v * (↑s : R)

Tactic:
refine ⟨s, s'.1, h, ?_⟩
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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'
⊢ (↑s : R) * (↑s' : R) = (↑s' : R) * (↑s : R)

Tactic:
exact_mod_cast hc
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ Surjective i

Tactic:
have hsurj : Surjective i := Quotient.mk''_surjective
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ RightInverse (surjInv hsurj) i

Tactic:
have hi := rightInverse_surjInv hsurj
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
⊢ 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
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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 : #(OreLocalization S X) ≤ lift.{u, v} #X * lift.{u, v} #X
⊢ ℵ₀ ≤ lift.{u, v} #X

Tactic:
simp
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
rwa₅ rwa₆ rwa₇ rwa₈ : ∀ (this : #(OreLocalization S X) ≤ lift.{u, v} #X), #(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

Premises used: Cardinal.lift_id', Cardinal.mul_eq_self, Cardinal.lift_mul, Cardinal.lift_id, Cardinal.mk_prod
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
inr : Injective j
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

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
-- Module: Mathlib.GroupTheory.OreLocalization.Cardinality
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
a₁ : OreLocalization S X
⊢ ∀ ⦃a₂ : OreLocalization S X⦄, j a₁ = j a₂ → a₁ = a₂

Tactic:
grind
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r₁ r₂ : R
s : ↥S
h : r₁ * (↑s : R) = r₂ * (↑s : R)
⊢ ∃ (s' : ↥S), (↑s' : R) * r₁ = (↑s' : R) * r₂

Tactic:
OreSet.ore_right_cancel r₁ r₂ s h

Premises used: OreLocalization.OreSet.ore_right_cancel
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
r : R
s : ↥S
⊢ (↑(oreDenom r s) : R) * r = oreNum r s * (↑s : R)

Tactic:
OreSet.ore_eq r s

Premises used: OreLocalization.OreSet.ore_eq, OreLocalization.oreNum
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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)
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
⊢ (↑s : R) * x = (↑s : R) * x_1

Tactic:
rcases s with ⟨s, hs⟩
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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)
⊢ s = 1

Tactic:
rw [Submonoid.mem_bot] at hs

Premises used: Submonoid.mem_bot
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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)
hs₁ : s = 1
⊢ 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)

Tactic:
rw [Submonoid.mem_bot] at hs

Premises used: Submonoid.mem_bot
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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)
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
⊢ (↑(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

Tactic:
subst hs
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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)
⊢ x = x_1

Tactic:
rw [mul_one, mul_one] at h

Premises used: mul_one
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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
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
⊢ (↑(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 h
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x : R
hs : Membership.mem (γ := Submonoid R) ⊥ 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

Tactic:
rfl
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x : R
s : ↥⊥
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)
⊢ (↑s : R) * x = x * (↑s : R)

Tactic:
rcases s with ⟨s, hs⟩
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x s : R
hs : Membership.mem (γ := Submonoid R) ⊥ s
⊢ s = 1

Tactic:
rw [Submonoid.mem_bot] at hs

Premises used: Submonoid.mem_bot
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_1
inst : Monoid R
S : Submonoid R
inst_1 : OreSet S
x s : R
hs_1 : Membership.mem (γ := Submonoid R) ⊥ s
hs : s = 1
⊢ (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs_1) : R) * x =
    x * (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) ⊥ x) s hs_1) : R)

Tactic:
simp [hs]
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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)
rw₂ rw₃ : n * (↑s : R) = n * (↑s : R)
⊢ (↑s : R) * m = (↑s : R) * n

Tactic:
rw [mul_comm (s : R) n, mul_comm (s : R) m, h]

Premises used: mul_comm, Subtype.val
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
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
rw rw₁ : r * (↑s : R) = r * (↑s : R)
⊢ (↑s : R) * r = r * (↑s : R)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_2
inst : CommMonoid R
S : Submonoid R
r : R
s : ↥S
⊢ oreNum r s = r

Tactic:
rfl

Premises used: OreLocalization.oreNum, rfl
-- Module: Mathlib.GroupTheory.OreLocalization.OreSet
Goal:
R : Type u_2
inst : CommMonoid R
S : Submonoid R
r : R
s : ↥S
⊢ oreDenom r s = s

Tactic:
rfl

Premises used: rfl, OreLocalization.oreDenom
-- Module: Mathlib.GroupTheory.PGroup
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ g ^ p ^ k = 1

Tactic:
rw [← hk, pow_orderOf_eq_one]

Premises used: pow_orderOf_eq_one
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
n : ℕ
hG : Nat.card G = p ^ n
g : G
rw : g ^ Nat.card G = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := G) 1 1
⊢ g ^ p ^ n = 1

Tactic:
rw [← hG, pow_card_eq_one']

Premises used: pow_card_eq_one'
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
rw : 1 = HPow.hPow (β := ℕ) p 0
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ Nat.card.{u_1} ↥⊥ = HPow.hPow (β := ℕ) p 0

Tactic:
rw [Subgroup.card_bot, pow_zero]

Premises used: Subgroup.card_bot, pow_zero
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
⊢ Nat.card G ≠ 0

Tactic:
have hG : Nat.card G ≠ 0 := Nat.card_pos.ne'
-- Module: Mathlib.GroupTheory.PGroup
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

Tactic:
⟨fun h => ?_, fun ⟨n, hn⟩ => of_card hn⟩

Premises used: _private.0.IsPGroup.iff_card.match_1, IsPGroup, Iff.intro, IsPGroup.of_card
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
inst_1 : Fact (Nat.Prime p)
inst_2 : Finite G
hG : Nat.card G ≠ 0
refine : ∀ (h : IsPGroup p G), ∃ (n : ℕ), Nat.card G = p ^ n
⊢ IsPGroup p G ↔ ∃ (n : ℕ), Nat.card G = p ^ n

Tactic:
refine ⟨fun h => ?_, fun ⟨n, hn⟩ => of_card hn⟩
-- Module: Mathlib.GroupTheory.PGroup
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 = p ^ (Nat.card G).primeFactorsList.length
⊢ ∃ (n : ℕ), Nat.card G = p ^ n

Tactic:
use (Nat.card G).primeFactorsList.length

Premises used: Nat.card, List.length, Nat.primeFactorsList
-- Module: Mathlib.GroupTheory.PGroup
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
h₃ h₄ : Nat.card G = Nat.card G
⊢ Nat.card G = p ^ (Nat.card G).primeFactorsList.length

Tactic:
rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_primeFactorsList hG]

Premises used: List.eq_replicate_of_mem, List.prod_replicate, Nat.prod_primeFactorsList
-- Module: Mathlib.GroupTheory.PGroup
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
suffices : ∀ q ∈ (Nat.card G).primeFactorsList, q = p
⊢ ∃ (n : ℕ), Nat.card G = p ^ n

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]
-- Module: Mathlib.GroupTheory.PGroup
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
⊢ Nat.Prime q

Tactic:
obtain ⟨hq1, hq2⟩ := (Nat.mem_primeFactorsList hG).mp hq

Premises used: Nat.mem_primeFactorsList, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
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 ∣ Nat.card G

Tactic:
obtain ⟨hq1, hq2⟩ := (Nat.mem_primeFactorsList hG).mp hq

Premises used: Nat.mem_primeFactorsList, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
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
⊢ Fact (Nat.Prime q)

Tactic:
haveI : Fact q.Prime := ⟨hq1⟩
-- Module: Mathlib.GroupTheory.PGroup
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)
obtain : ∀ (g : G) (hg : orderOf g = q), q = p
⊢ q = p

Tactic:
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card' q hq2

Premises used: exists_prime_orderOf_dvd_card'
-- Module: Mathlib.GroupTheory.PGroup
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
obtain : ∀ (k : ℕ) (hk : orderOf g = p ^ k), q = p
⊢ q = p

Tactic:
obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g

Premises used: Iff.mp, IsPGroup.iff_orderOf
-- Module: Mathlib.GroupTheory.PGroup
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
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p

Tactic:
(hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm

Premises used: And.left, Iff.mp, Eq.symm, Eq.trans, Nat.Prime.pow_eq_iff
-- Module: Mathlib.GroupTheory.PGroup
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
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p

Tactic:
exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm

Premises used: And.left, Iff.mp, Eq.symm, Eq.trans, Nat.Prime.pow_eq_iff
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : H →* G
hϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑ϕ : (a : H) → G)
simp_rw : ∀ (g : H), ∃ (k : ℕ), HPow.hPow (α := G) ((ϕ : (a : H) → G) g : G) (p ^ k) = 1
⊢ IsPGroup p H

Tactic:
simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]

Premises used: IsPGroup, Function.Injective.eq_iff, MonoidHom.map_one, MonoidHom.map_pow
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : H →* G
hϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑ϕ : (a : H) → G)
⊢ ∀ (g : H), ∃ (k : ℕ), HPow.hPow (α := G) ((ϕ : (a : H) → G) g : G) (p ^ k) = 1

Tactic:
fun h => hG (ϕ h)

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : H →* G
hϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑ϕ : (a : H) → G)
⊢ ∀ (g : H), ∃ (k : ℕ), HPow.hPow (α := G) ((ϕ : (a : H) → G) g : G) (p ^ k) = 1

Tactic:
exact fun h => hG (ϕ h)

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Subgroup G
⊢ IsPGroup.{u_1} p ↥H

Tactic:
hG.of_injective H.subtype Subtype.coe_injective

Premises used: Subgroup.subtype, Subtype.coe_injective, IsPGroup.of_injective