awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a a' : α
b : M
h : a' ≠ a
rw : (if a' = a then b else f.coeff a') = f.coeff a'
⊢ (f.update a b).coeff a' = f.coeff a'
have rw₁ : f.coeff a' = f.coeff a'
Tactic: classical
  rw [f.coeff_update_apply, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ f.update a b =
    HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α) (single a b)
have a₁ : ∀ (x : α),
  (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
⊢ (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x
have pos : ∀ (hx : x = a),
  (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
x : α
pos :
  ∀ (hx : x = a),
    (f.update a b).coeff x =
      (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
            ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
            (single a b)).coeff
        x
⊢ (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x
have neg : ∀ (hx : ¬x = a),
  (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x
Tactic: by_cases hx : x = a
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ f.update a b =
    HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
      ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α) (single a b)
have a₁ : ∀ (x : α),
  (f.update a b).coeff x =
    (HAdd.hAdd (α := SkewMonoidAlgebra M α) (β := SkewMonoidAlgebra M α)
          ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f : SkewMonoidAlgebra M α)
          (single a b)).coeff
      x
Tactic: classical ext x; by_cases hx : x = a <;> aesop (add norm coeff_single_apply)
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
⊢ f.update a 0 = (erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f
have a₁ : ∀ (a_1 : α), (f.update a 0).coeff a_1 = coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Single (goal)
Goal:
M : Type u_4
α : Type u_5
inst : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
⊢ f.update a 0 = (erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f
have a₁ : ∀ (a_1 : α), (f.update a 0).coeff a_1 = coeff ((erase a : (a : SkewMonoidAlgebra M α) → SkewMonoidAlgebra M α) f) a_1
Tactic: classical ext; simp [coeff_update_apply, coeff_erase_apply]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst_1 : DecidableEq G'
inst_2 : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.sum g).support ⊆ f.support.biUnion fun (a : G) ↦ (g a (f.coeff a)).support
have simp_rw : Subset.{u_4} (α := Finset G')
  (Finsupp.support.{u_4, u_3} (M := k') (f.toFinsupp.sum fun (x1 : G) (x2 : k) ↦ (g x1 x2).toFinsupp))
  (f.toFinsupp.support.biUnion fun (a : G) ↦ (g a (f.coeff a)).toFinsupp.support)
Tactic: simp_rw [support, toFinsupp_sum']
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommGroup k
p : SkewMonoidAlgebra k G
⊢ (-p).support = p.support
have rw : (-p).toFinsupp.support = p.support
Tactic: rw [support, toFinsupp_neg, Finsupp.support_neg, support_toFinsupp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommGroup k
p : SkewMonoidAlgebra k G
rw : (-p).toFinsupp.support = p.support
⊢ (-p).support = p.support
have rw₁ : (-p.toFinsupp).support = p.support
Tactic: rw [support, toFinsupp_neg, Finsupp.support_neg, support_toFinsupp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommGroup k
p : SkewMonoidAlgebra k G
rw : (-p).toFinsupp.support = p.support
rw₁ : (-p.toFinsupp).support = p.support
⊢ (-p).support = p.support
have rw₂ : p.toFinsupp.support = p.support
Tactic: rw [support, toFinsupp_neg, Finsupp.support_neg, support_toFinsupp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : AddCommGroup k
p : SkewMonoidAlgebra k G
rw : (-p).toFinsupp.support = p.support
rw₁ : (-p.toFinsupp).support = p.support
rw₂ : p.toFinsupp.support = p.support
⊢ (-p).support = p.support
have rw₃ : p.support = p.support
Tactic: rw [support, toFinsupp_neg, Finsupp.support_neg, support_toFinsupp]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
r : k
a : G
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) {a} f.support) (image (fun (x : G) ↦ a * x) f.support)
have rw : Subset (α := Finset G) (image (fun (b : G) ↦ a * b) f.support) (image (fun (b : G) ↦ a * b) f.support)
Tactic: rw [Finset.image₂_singleton_left]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
r : k
a : G
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) f.support {a}) (image (fun (x : G) ↦ x * a) f.support)
have rw : Subset (α := Finset G) (image (fun (a_1 : G) ↦ a_1 * a) f.support) (image (fun (a_1 : G) ↦ a_1 * a) f.support)
Tactic: rw [Finset.image₂_singleton_right]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = image (fun (x_1 : G) ↦ x * x_1) f.support
have refine : ∀ (y : G) (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y),
  y ∈ (single x r * f).support
Tactic: refine subset_antisymm (support_single_mul_subset f _ _) fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
r : k
x : G
lx : IsLeftRegular x
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) y
⊢ y ∈ (single x r * f).support
have obtain : ∀ (y : G) (yf : y ∈ f.support)
  (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x * x_1) f.support) (x * y)),
  x * y ∈ (single x r * f).support
Tactic: obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
    simpa only [Finset.mem_image, exists_prop] using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = image (fun (x_1 : G) ↦ x_1 * x) f.support
have refine : ∀ (y : G) (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y),
  y ∈ (f * single x r).support
Tactic: refine subset_antisymm (support_mul_single_subset f _ _) fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
r : k
x : G
rx : IsRightRegular x
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
y : G
hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) y
⊢ y ∈ (f * single x r).support
have obtain : ∀ (y : G) (yf : y ∈ f.support)
  (hy : Membership.mem (γ := Finset G) (image (fun (x_1 : G) ↦ x_1 * x) f.support) (y * x)),
  y * x ∈ (f * single x r).support
Tactic: obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by
    simpa only [Finset.mem_image, exists_prop] using hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : IsRightCancelMul G
r : k
x : G
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
have h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : IsRightCancelMul G
r : k
x : G
hrx : ∀ (g : G) (y : k), y * g • r = 0 ↔ y = 0
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support
have h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
Tactic: classical
  ext a
  simp [support_mul_single_eq_image f (IsRightRegular.all x) hrx]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support
have h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
inst_3 : IsLeftCancelMul G
r : k
x : G
hrx : ∀ (y : k), r * x • y = 0 ↔ y = 0
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support
have h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
Tactic: classical
  ext a
  simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
⊢ Membership.mem (γ := Submodule k (SkewMonoidAlgebra k G))
    (Submodule.span k ((⇑(of k G) : (a : G) → SkewMonoidAlgebra k G) '' (↑f.support : Set G))) f
have rw : ∃ (c : (↑(↑f.support : Set G) : Type u_2) → k),
  ∑ i : (↑(↑f.support : Set G) : Type u_2),
      HSMul.hSMul (β := SkewMonoidAlgebra k G) (c i)
        ((of k G : (a : G) → SkewMonoidAlgebra k G) (↑i : G) : SkewMonoidAlgebra k G) =
    f
Tactic: rw [Fintype.mem_span_image_iff_exists_fun k]
-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Support (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f : SkewMonoidAlgebra k G
⊢ ∃ (c : (↑(↑f.support : Set G) : Type u_2) → k),
    ∑ i : (↑(↑f.support : Set G) : Type u_2),
        HSMul.hSMul (β := SkewMonoidAlgebra k G) (c i)
          ((of k G : (a : G) → SkewMonoidAlgebra k G) (↑i : G) : SkewMonoidAlgebra k G) =
      f
have h : ∑ i : (↑(↑f.support : Set G) : Type u_2),
    HSMul.hSMul (β := SkewMonoidAlgebra k G) (f.support.restrict (π := fun (i : G) ↦ k) f.coeff i)
      ((of k G : (a : G) → SkewMonoidAlgebra k G) (↑i : G) : SkewMonoidAlgebra k G) =
  f
Tactic: use Finset.restrict f.support f.coeff
-- Lean 4 proof step from Mathlib.Algebra.SkewPolynomial.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
a : R
⊢ (⇑φ : (a : R) → R)^[n] a =
    HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : Multiplicative ℕ) a
have zero : (⇑φ : (a : R) → R)^[0] a =
  HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 0 : Multiplicative ℕ) a
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
      ← mul_smul, mul_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.SkewPolynomial.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
a : R
zero :
  (⇑φ : (a : R) → R)^[0] a =
    HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 0 : Multiplicative ℕ) a
⊢ (⇑φ : (a : R) → R)^[n] a =
    HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : Multiplicative ℕ) a
have succ : ∀ (n : ℕ)
  (hn :
    (⇑φ : (a : R) → R)^[n] a =
      HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : Multiplicative ℕ) a),
  (⇑φ : (a : R) → R)^[n + 1] a =
    HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) (n + 1) : Multiplicative ℕ) a
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
      ← mul_smul, mul_comm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.SkewPolynomial.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
n m : ℕ
r s : R
⊢ HMul.hMul (α := SkewPolynomial R) (β := SkewPolynomial R)
      ((monomial n : (a : R) → SkewPolynomial R) r : SkewPolynomial R)
      ((monomial m : (a : R) → SkewPolynomial R) s : SkewPolynomial R) =
    (monomial (n + m) : (a : R) → SkewPolynomial R) (r * (⇑φ : (a : R) → R)^[n] s)
have rw : HMul.hMul (α := SkewPolynomial R) (β := SkewPolynomial R)
    ((monomial n : (a : R) → SkewPolynomial R) r : SkewPolynomial R)
    ((monomial m : (a : R) → SkewPolynomial R) s : SkewPolynomial R) =
  (monomial (n + m) : (a : R) → SkewPolynomial R)
    (r * HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : Multiplicative ℕ) s)
Tactic: rw [φ_iterate_apply]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ ¬Squarefree.{u_1} (R := R) 0
have rw : ∃ (x : R), ¬(x * x ∣ 0 → IsUnit x)
Tactic: rw [Squarefree, not_forall]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * y * z
⊢ IsUnit y
have hz₁ : x = y * (y * z)
Tactic: rw [mul_assoc] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
⊢ IsUnit y
have inl : ∀ (hu : IsUnit y), IsUnit y
Tactic: rcases h.isUnit_or_isUnit hz with (hu | hu)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
inl : ∀ (hu : IsUnit y), IsUnit y
⊢ IsUnit y
have inr : ∀ (hu : IsUnit (y * z)), IsUnit y
Tactic: rcases h.isUnit_or_isUnit hz with (hu | hu)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : ¬IsUnit x
⊢ n = 0 ∨ n = 1
have contrapose! : ∀ (h' : n ≠ 0 ∧ n ≠ 1), IsUnit x
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : n ≠ 0 ∧ n ≠ 1
⊢ IsUnit x
have h'₁ : 2 ≤ n
Tactic: replace h' : 2 ≤ n := by lia
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ x * x ∣ x ^ n
have rw : HPow.hPow (β := ℕ) x 2 ∣ x ^ n
Tactic: rw [← sq]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : Monoid R
x : R
n : ℕ
h : Squarefree (x ^ n)
h' : 2 ≤ n
⊢ IsUnit x
have this : x * x ∣ x ^ n
Tactic: have : x * x ∣ x ^ n := by rw [← sq]; exact pow_dvd_pow x h'
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
⊢ x ^ n ∣ x
have pos : ∀ (hu : IsUnit x), x ^ n ∣ x
Tactic: by_cases hu : IsUnit x
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
pos : ∀ (hu : IsUnit x), x ^ n ∣ x
⊢ x ^ n ∣ x
have neg : ∀ (hu : ¬IsUnit x), x ^ n ∣ x
Tactic: by_cases hu : IsUnit x
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : ¬IsUnit x
⊢ x ^ n ∣ x
have neg : ∀ (h : HPow.hPow (β := ℕ) x 0 ∣ y), HPow.hPow (β := ℕ) x 0 ∣ x
Tactic: rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : Monoid R
x y : R
n : ℕ
hx : Squarefree y
h : x ^ n ∣ y
hu : ¬IsUnit x
neg : ∀ (h : HPow.hPow (β := ℕ) x 0 ∣ y), HPow.hPow (β := ℕ) x 0 ∣ x
⊢ x ^ n ∣ x
have neg₁ : ∀ (h : HPow.hPow (β := ℕ) x 1 ∣ y), HPow.hPow (β := ℕ) x 1 ∣ x
Tactic: rcases (hx.squarefree_of_dvd h).eq_zero_or_one_of_pow_of_not_isUnit hu with rfl | rfl
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
r : R
⊢ Squarefree r ↔ ∀ (x : R), emultiplicity x r ≤ 1 ∨ IsUnit x
have refine : ∀ (a : R), a * a ∣ r → IsUnit a ↔ emultiplicity a r ≤ 1 ∨ IsUnit a
Tactic: refine forall_congr' fun a => ?_
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
r a : R
⊢ a * a ∣ r → IsUnit a ↔ emultiplicity a r ≤ 1 ∨ IsUnit a
have rw : (↑2 : ℕ∞) ≤ emultiplicity a r ↔ 1 < emultiplicity a r
Tactic: rw [← sq, pow_dvd_iff_le_emultiplicity, or_iff_not_imp_left, not_le, imp_congr _ Iff.rfl]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
⊢ Squarefree x ↔ ∀ (p : R), Irreducible p → ¬p * p ∣ x
have refine : ∀ (h : ∀ (p : R), Irreducible p → ¬p * p ∣ x) (d : R) (hd : d * d ∣ x) (hdu : ¬IsUnit d), False
Tactic: refine ⟨fun h p hp hp' ↦ hp.not_isUnit (h p hp'), fun h d hd ↦ by_contra fun hdu ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
⊢ False
have hd₀ : d ≠ 0
Tactic: have hd₀ : d ≠ 0 := ne_zero_of_dvd_ne_zero (ne_zero_of_dvd_ne_zero hx₀ hd) (dvd_mul_left d d)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
x : R
hx₀ : x ≠ 0
h : ∀ (p : R), Irreducible p → ¬p * p ∣ x
d : R
hd : d * d ∣ x
hdu : ¬IsUnit d
hd₀ : d ≠ 0
⊢ False
have obtain : ∀ (p : R) (irr : Irreducible p) (dvd : p ∣ d), False
Tactic: obtain ⟨p, irr, dvd⟩ := WfDvdMonoid.exists_irreducible_factor hdu hd₀
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
have refine_1 : ∀ (h : ∀ (x : R), Irreducible x → ¬x * x ∣ r), (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
refine_1 : ∀ (h : ∀ (x : R), Irreducible x → ¬x * x ∣ r), (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
⊢ (∀ (x : R), Irreducible x → ¬x * x ∣ r) ↔ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
have refine_2 : (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r → ∀ (x : R), Irreducible x → ¬x * x ∣ r
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
have refine_1 : ∀ (h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0),
  (Eq.{u_1 + 1} (α := R) 0 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree.{u_1} (R := R) 0
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
h : ∀ (x : R), Irreducible x → ¬x * x ∣ r
refine_1 :
  ∀ (h : ∀ (x : R), Irreducible x → ¬x * x ∣ 0),
    (Eq.{u_1 + 1} (α := R) 0 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree.{u_1} (R := R) 0
⊢ (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
have refine_1₁ : ∀ (hr : r ≠ 0), (r = 0 ∧ ∀ (x : R), ¬Irreducible x) ∨ Squarefree r
Tactic: rcases eq_or_ne r 0 with (rfl | hr)
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : WfDvdMonoid R
r : R
hr : ∃ (x : R), Irreducible x
⊢ Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r
have rw : Squarefree r ↔ (r = 0 ∧ ¬∃ (x : R), Irreducible x) ∨ Squarefree r
Tactic: rw [irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree, ← not_exists]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : DecompositionMonoid R
x : R
hx : Squarefree x
y : R
hy : x ∣ HPow.hPow (β := ℕ) y 2
⊢ x ∣ y
have obtain : ∀ (a b : R) (ha : a ∣ y) (hb : b ∣ y) (hx : Squarefree (a * b)) (hy : a * b ∣ HPow.hPow (β := ℕ) y 2), a * b ∣ y
Tactic: obtain ⟨a, b, ha, hb, rfl⟩ := exists_dvd_and_dvd_of_dvd_mul (sq y ▸ hy)
Cleared hypotheses: x, hx, hy
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
⊢ HPow.hPow (β := ℕ) (z * w) 2 = z * z * w * w
have simp_rw : z * w * (z * w) = z * z * w * w
Tactic: simp_rw [pow_two, mul_left_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Squarefree.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
z w : R
h0 : z * z * w ≠ 0
h : IsRadical (z * z * w)
simp_rw : z * w * (z * w) = z * z * w * w
⊢ HPow.hPow (β := ℕ) (z * w) 2 = z * z * w * w
have simp_rw₁ : z * (z * w * w) = z * z * w * w
Tactic: simp_rw [pow_two, mul_left_comm, ← mul_assoc]