awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : One G
inst_1 : AddCommMonoidWithOne k
inst_2 : NeZero.{u_1} (R := k) 1
⊢ Eq.{u_2 + 1} (α := Finset G) (support.{u_1, u_2} (k := k) 1) 1

Tactic:
Finsupp.support_single _ one_ne_zero

Premises used: Finsupp.support_single, SkewMonoidAlgebra.support, one_ne_zero
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Semiring k
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G
inst_3 : DecidableEq G
⊢ (f * g).support ⊆ f.support * g.support

Tactic:
support_sum.trans <| biUnion_subset.2 fun _x hx ↦
    support_sum.trans <| biUnion_subset.2 fun _y hy ↦
      support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

Premises used: Iff.mpr, SkewMonoidAlgebra.support_sum, Set.Mem, setOf, Finset.singleton_subset_iff, HasSubset.Subset.trans, Finset.mem_image₂_of_mem, SkewMonoidAlgebra.support_single_subset, Finset.biUnion_subset
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
rw rw₁ : Subset (α := Finset G) (image (fun (b : G) ↦ a * b) f.support) (image (fun (b : G) ↦ a * b) f.support)
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) {a} f.support) (image (fun (x : G) ↦ a * x) f.support)

Tactic:
rw [Finset.image₂_singleton_left]

Premises used: Finset.image₂_singleton_left
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
rw rw₁ : Subset (α := Finset G) (image (fun (a_1 : G) ↦ a_1 * a) f.support) (image (fun (a_1 : G) ↦ a_1 * a) f.support)
⊢ Subset (α := Finset G) (image₂ (fun (x1 x2 : G) ↦ x1 * x2) f.support {a}) (image (fun (x : G) ↦ x * a) f.support)

Tactic:
rw [Finset.image₂_singleton_right]

Premises used: Finset.image₂_singleton_right
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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

Tactic:
subset_antisymm (support_single_mul_subset f _ _) fun y hy ↦ ?_

Premises used: subset_antisymm, SkewMonoidAlgebra.support_single_mul_subset
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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
⊢ (single x r * f).support = image (fun (x_1 : G) ↦ x * x_1) f.support

Tactic:
refine subset_antisymm (support_single_mul_subset f _ _) fun y hy ↦ ?_

Premises used: subset_antisymm, SkewMonoidAlgebra.support_single_mul_subset
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
⊢ ∃ a ∈ f.support, x * a = y

Tactic:
simpa only [Finset.mem_image, exists_prop] using hy

Premises used: Finset.mem_image, exists_prop
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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
⊢ 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

Premises used: SkewMonoidAlgebra.support, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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:
simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, Ne,
    zero_mul, ite_self, sum_zero, lx.eq_iff]

Premises used: ite_self, MulZeroClass.zero_mul, Function.Injective.eq_iff, Ne, SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.mem_support_iff, Iff.mp, SkewMonoidAlgebra.sum_zero, SkewMonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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

Tactic:
subset_antisymm (support_mul_single_subset f _ _) fun y hy ↦ ?_

Premises used: subset_antisymm, SkewMonoidAlgebra.support_mul_single_subset
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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
⊢ (f * single x r).support = image (fun (x_1 : G) ↦ x_1 * x) f.support

Tactic:
refine subset_antisymm (support_mul_single_subset f _ _) fun y hy ↦ ?_

Premises used: subset_antisymm, SkewMonoidAlgebra.support_mul_single_subset
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
⊢ ∃ a ∈ f.support, a * x = y

Tactic:
simpa only [Finset.mem_image, exists_prop] using hy

Premises used: Finset.mem_image, exists_prop
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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
⊢ y ∈ (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

Premises used: SkewMonoidAlgebra.support, rfl
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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:
simp [coeff_mul, mem_support_iff.mp yf, hrx, mem_support_iff, sum_single_index, mul_zero,
    ite_self, rx.eq_iff]

Premises used: ite_self, Function.Injective.eq_iff, SkewMonoidAlgebra.coeff_mul, SkewMonoidAlgebra.mem_support_iff, MulZeroClass.mul_zero, Iff.mp, SkewMonoidAlgebra.sum_single_index
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
ext a
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
a : G
⊢ a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support

Tactic:
simp [support_mul_single_eq_image f (IsRightRegular.all x) hrx]

Premises used: IsRightRegular.all, SkewMonoidAlgebra.support_mul_single_eq_image
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
h : ∀ (a : G), a ∈ (f * single x r).support ↔ a ∈ map (mulRightEmbedding x) f.support
⊢ (f * single x r).support = map (mulRightEmbedding x) f.support

Tactic:
classical
  ext a
  simp [support_mul_single_eq_image f (IsRightRegular.all x) hrx]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
ext a
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
a : G
⊢ a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support

Tactic:
simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]

Premises used: SkewMonoidAlgebra.support_single_mul_eq_image, IsLeftRegular.all
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
h : ∀ (a : G), a ∈ (single x r * f).support ↔ a ∈ map (mulLeftEmbedding x) f.support
⊢ (single x r * f).support = map (mulLeftEmbedding x) f.support

Tactic:
classical
  ext a
  simp [support_single_mul_eq_image f (IsLeftRegular.all x) hrx]
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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
⊢ Membership.mem (γ := Submodule k (SkewMonoidAlgebra k G))
    (Submodule.span k ((⇑(of k G) : (a : G) → SkewMonoidAlgebra k G) '' (↑f.support : Set G))) f

Tactic:
rw [Fintype.mem_span_image_iff_exists_fun k]

Premises used: Fintype.mem_span_image_iff_exists_fun
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
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
⊢ ∃ (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:
use Finset.restrict f.support f.coeff

Premises used: Finset.restrict, SkewMonoidAlgebra.support, SkewMonoidAlgebra.coeff
-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Support
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
⊢ ∑ 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:
simp [smul_single, ← sum_def', sum_single]

Premises used: SkewMonoidAlgebra.sum_def', SkewMonoidAlgebra.sum_single, SkewMonoidAlgebra.smul_single
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
⊢ support.{u_1} (R := R) 0 = ∅

Tactic:
rfl

Premises used: Multiset.map, List.map, Finset.map, Multiset.zero, Finset.empty, Multiset.ofList, SkewPolynomial.support, rfl
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
p : SkewPolynomial R
⊢ p.support = ∅ ↔ p = 0

Tactic:
simp [support]

Premises used: SkewPolynomial.support
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
p : SkewPolynomial R
⊢ p.support.card = 0 ↔ p = 0

Tactic:
simp
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
p q : SkewPolynomial R
⊢ (p + q).support ⊆ p.support ∪ q.support

Tactic:
simpa [support, ← Finset.map_union, Finset.map_subset_map] using SkewMonoidAlgebra.support_add

Premises used: SkewMonoidAlgebra.support_add, Finset.map_subset_map, SkewPolynomial.support, Finset.map_union
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
⊢ Eq (α := R →+* R) φ
    (MulSemiringAction.toRingHom (Multiplicative ℕ) R ((ofAdd : (a : ℕ) → Multiplicative ℕ) 1 : Multiplicative ℕ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
a : R
⊢ (⇑φ : (a : R) → R)^[0] a =
    HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) 0 : Multiplicative ℕ) a

Tactic:
simp
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
a : R
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:
simp_all [MulSemiringAction.toRingHom_apply, Function.iterate_succ', -Function.iterate_succ,
      ← mul_smul, mul_comm]

Premises used: MulSemiringAction.toRingHom_apply, Function.iterate_succ, Function.iterate_succ', mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
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
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
⊢ (⇑φ : (a : R) → R)^[n] a =
    HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : 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]

Premises used: MulSemiringAction.toRingHom_apply, Function.iterate_succ, Function.iterate_succ', mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := SkewPolynomial R) ((monomial n : (a : R) → SkewPolynomial R) 0) 0

Tactic:
single_zero _

Premises used: SkewMonoidAlgebra.single_zero, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
⊢ Eq.{u_1 + 1} (α := SkewPolynomial R) ((monomial 0 : (a : R) → SkewPolynomial R) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
⊢ Eq (α := SkewPolynomial R) ((monomial n : (a : R) → SkewPolynomial R) a : SkewPolynomial R)
    (single ((ofAdd : (a : ℕ) → Multiplicative ℕ) n) a : SkewMonoidAlgebra R (Multiplicative ℕ))

Tactic:
rfl

Premises used: SkewMonoidAlgebra.single, rfl
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r s : R
⊢ (monomial n : (a : R) → SkewPolynomial R) (r + s) =
    HAdd.hAdd (α := SkewPolynomial R) (β := SkewPolynomial R)
      ((monomial n : (a : R) → SkewPolynomial R) r : SkewPolynomial R)
      ((monomial n : (a : R) → SkewPolynomial R) s : SkewPolynomial R)

Tactic:
single_add ..

Premises used: SkewMonoidAlgebra.single_add, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_5
inst_1 : Semiring S
inst_2 : Module S R
a : S
n : ℕ
b : R
⊢ HSMul.hSMul (β := SkewPolynomial R) a ((monomial n : (a : R) → SkewPolynomial R) b : SkewPolynomial R) =
    (monomial n : (a : R) → SkewPolynomial R) (a • b)

Tactic:
smul_single ..

Premises used: SkewMonoidAlgebra.smul_single, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
Goal:
R : Type u_1
inst : Semiring R
inst_1 : MulSemiringAction (Multiplicative ℕ) R
n m : ℕ
r s : R
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)
⊢ 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)

Tactic:
rw [φ_iterate_apply]

Premises used: SkewPolynomial.φ_iterate_apply
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
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 * HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : Multiplicative ℕ) s)

Tactic:
SkewMonoidAlgebra.single_mul_single

Premises used: SkewMonoidAlgebra.single_mul_single, SkewMonoidAlgebra.single
-- Module: Mathlib.Algebra.SkewPolynomial.Basic
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 * HSMul.hSMul (α := Multiplicative ℕ) ((ofAdd : (a : ℕ) → Multiplicative ℕ) n : Multiplicative ℕ) s)

Tactic:
exact SkewMonoidAlgebra.single_mul_single

Premises used: SkewMonoidAlgebra.single_mul_single
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
m n : R
h : Squarefree (m * n)
⊢ IsRelPrime m n

Tactic:
fun c hca hcb ↦ h c (mul_dvd_mul hca hcb)

Premises used: IsRelPrime, mul_dvd_mul
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : IsUnit x
⊢ Squarefree x

Tactic:
fun _ hdvd =>
  isUnit_of_mul_isUnit_left (isUnit_of_dvd_unit hdvd h)

Premises used: isUnit_of_dvd_unit, isUnit_of_mul_isUnit_left, Squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
⊢ Squarefree.{u_1} (R := R) 1

Tactic:
isUnit_one.squarefree

Premises used: IsUnit.squarefree, isUnit_one
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
rw : ∃ (x : R), ¬(x * x ∣ 0 → IsUnit x)
⊢ ¬Squarefree.{u_1} (R := R) 0

Tactic:
rw [Squarefree, not_forall]

Premises used: Squarefree, Classical.not_forall
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ ¬(HMul.hMul (α := R) 0 0 ∣ 0 → IsUnit.{u_1} (M := R) 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
⊢ ∃ (x : R), ¬(x * x ∣ 0 → IsUnit x)

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
hm : Squarefree.{u_1} (R := R) 0
⊢ False

Tactic:
not_squarefree_zero hm

Premises used: not_squarefree_zero
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : MonoidWithZero R
inst_1 : Nontrivial R
hm : Squarefree.{u_1} (R := R) 0
⊢ False

Tactic:
exact not_squarefree_zero hm

Premises used: not_squarefree_zero
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * y * z
⊢ x = y * (y * z)

Tactic:
rw [mul_assoc] at hz

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Squarefree.Basic
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
inr : ∀ (hu : IsUnit (y * z)), IsUnit y
⊢ IsUnit y

Tactic:
rcases h.isUnit_or_isUnit hz with (hu | hu)

Premises used: Irreducible.isUnit_or_isUnit
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

Tactic:
hu
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit y
⊢ IsUnit y

Tactic:
exact hu
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
x : R
h : Irreducible x
y z : R
hz : x = y * (y * z)
hu : IsUnit (y * z)
⊢ IsUnit y

Tactic:
apply isUnit_of_mul_isUnit_left hu

Premises used: isUnit_of_mul_isUnit_left
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : IsCancelMulZero R
x : R
h : Prime x
⊢ Squarefree x

Tactic:
h.irreducible.squarefree

Premises used: Prime.irreducible, Irreducible.squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
m n : R
hmn : Squarefree (m * n)
⊢ Squarefree m

Tactic:
fun p hp => hmn p (dvd_mul_of_dvd_left hp n)

Premises used: dvd_mul_of_dvd_left, Squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoid R
m n : R
hmn : Squarefree (m * n)
⊢ Squarefree n

Tactic:
fun p hp => hmn p (dvd_mul_of_dvd_right hp m)

Premises used: dvd_mul_of_dvd_right, Squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : Monoid R
x y : R
hdvd : x ∣ y
hsq : Squarefree y
⊢ Squarefree x

Tactic:
fun _ h => hsq _ (h.trans hdvd)

Premises used: Squarefree, Dvd.dvd.trans