awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
ι : Type u_2
s : Finset ι
f : ι → M₀
h : ∀ i ∈ s, Membership.mem (γ := Submonoid M₀) M₀⁰ (f i)
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰ (∏ i ∈ s, f i)

Tactic:
s.prod_induction _ _ (fun _ _ ↦ and_imp.mp mul_mem_nonZeroDivisors.mpr) (one_mem _) h

Premises used: Iff.mpr, and_imp, Finset.prod_induction, Iff.mp, OneMemClass.one_mem, mul_mem_nonZeroDivisors
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
x : G₀
u : G₀ˣ
⊢ (fun (u : ↥G₀⁰) ↦ Units.mk0 (↑u : G₀) ⋯)
      ((fun (u : G₀ˣ) ↦ Subtype.mk (p := fun (x : G₀) ↦ Membership.mem (γ := Submonoid G₀) G₀⁰ x) (↑u : G₀) ⋯) u) =
    u

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
x : G₀
u v : ↥G₀⁰
⊢ Units.mk0 (↑(u * v) : G₀) ⋯ = Units.mk0 (↑u : G₀) ⋯ * Units.mk0 (↑v : G₀) ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
x : G₀
hx : Membership.mem (γ := Submonoid G₀) G₀⁰ x
⊢ IsUnit x

Tactic:
(nonZeroDivisorsEquivUnits ⟨x, hx⟩).isUnit

Premises used: Subtype.mk, Units.isUnit, nonZeroDivisorsEquivUnits, DFunLike.coe
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
M : Type u_2
inst : MonoidWithZero M₀
inst_1 : Zero M
inst_2 : MulAction M₀ M
x : M₀
⊢ Membership.mem (γ := Submonoid M₀) M₀⁰[M] x ↔ ∀ (m : M), x • m = 0 → m = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) (↑u : M₀) ⋯ *
      Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) (↑u⁻¹ : M₀) ⋯ =
    1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : ↥M₀⁰
u : M₀ˣ
⊢ Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) (↑u⁻¹ : M₀) ⋯ *
      Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) (↑u : M₀) ⋯ =
    1

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : ↥M₀⁰
simp : (∃ (b_1 : (↥M₀⁰)ˣ), (↑a : M₀) * (↑(↑b_1 : ↥M₀⁰) : M₀) = (↑b : M₀)) ↔ ∃ (u : (↥M₀⁰)ˣ), a * (↑u : ↥M₀⁰) = b
⊢ (∃ (b_1 : (↥M₀⁰)ˣ),
      (↑a : M₀) *
          (↑((Equiv.symm (MulEquiv.toEquiv (MulEquiv.symm unitsNonZeroDivisorsEquiv)) : (a : (↥M₀⁰)ˣ) → M₀ˣ) b_1) :
            M₀) =
        (↑b : M₀)) ↔
    Associated a b

Tactic:
simp [Associated]

Premises used: Associated
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : MonoidWithZero M₀
a b : ↥M₀⁰
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (∃ (b_1 : (↥M₀⁰)ˣ), a * (↑b_1 : ↥M₀⁰) = b) ↔ ∃ (u : (↥M₀⁰)ˣ), a * (↑u : ↥M₀⁰) = b
⊢ (∃ (b_1 : (↥M₀⁰)ˣ), (↑a : M₀) * (↑(↑b_1 : ↥M₀⁰) : M₀) = (↑b : M₀)) ↔ ∃ (u : (↥M₀⁰)ˣ), a * (↑u : ↥M₀⁰) = b

Tactic:
norm_cast
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
rw : (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0
⊢ Membership.mem (γ := Submonoid (Associates M₀)) (Associates M₀)⁰ (Associates.mk a) ↔
    Membership.mem (γ := Submonoid M₀) M₀⁰ a

Tactic:
rw [mem_nonZeroDivisors_iff_right, mem_nonZeroDivisors_iff_right]

Premises used: mem_nonZeroDivisors_iff_right
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
contrapose! : (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
⊢ (∀ (x : Associates M₀), x * Associates.mk a = 0 → x = 0) ↔ ∀ (x : M₀), x * a = 0 → x = 0

Tactic:
contrapose!
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
mp : (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) → ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
mpr : (∃ (x : M₀), x * a = 0 ∧ x ≠ 0) → ∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0
⊢ (∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0) ↔ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
⊢ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0

Tactic:
⟨x, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
mp : x * a = 0
mp₁ : x ≠ 0
⊢ ∃ (x : M₀), x * a = 0 ∧ x ≠ 0

Tactic:
refine ⟨x, ?_, ?_⟩
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
mp : Eq (α := Associates M₀) (Associates.mk (x * a)) 0
mp₁ : HMul.hMul (α := Associates M₀) (Associates.mk x) (Associates.mk a) = 0
mp₂ mp₃ mp₄ mp₅ :
  HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
⊢ x * a = 0

Tactic:
rwa [← Associates.mk_eq_zero, ← Associates.mk_mul_mk, ← Associates.quot_mk_eq_mk]

Premises used: Associates.mk_mul_mk, Associates.quot_mk_eq_mk, Associates.mk_eq_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
w : Associates M₀
x : M₀
hx₁ : HMul.hMul (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) (Associates.mk a) = 0
hx₂ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
mp : Ne (α := Associates M₀) (Associates.mk x) 0
mp₁ mp₂ mp₃ mp₄ : Ne (α := Associates M₀) (Quot.mk (⇑(Associated.setoid M₀) : M₀ → M₀ → Prop) x) 0
⊢ x ≠ 0

Tactic:
rwa [← Associates.mk_ne_zero, ← Associates.quot_mk_eq_mk]

Premises used: Associates.quot_mk_eq_mk, Associates.mk_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
h : ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ rwa rwa₁ rwa₂ rwa₃ : b ≠ 0
⊢ Ne (α := Associates M₀) (Associates.mk b) 0

Tactic:
rwa [Associates.mk_ne_zero]

Premises used: Associates.mk_ne_zero
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
mpr :
  (∃ (x : M₀), x * a = 0 ∧ x ≠ 0) →
    ∀ (b : M₀) (hb₁ : b * a = 0) (hb₂ : b ≠ 0), HMul.hMul (α := Associates M₀) (Associates.mk b) (Associates.mk a) = 0
⊢ (∃ (x : M₀), x * a = 0 ∧ x ≠ 0) → ∃ (x : Associates M₀), x * Associates.mk a = 0 ∧ x ≠ 0

Tactic:
refine fun ⟨b, hb₁, hb₂⟩ ↦ ⟨Associates.mk b, ?_, by rwa [Associates.mk_ne_zero]⟩
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
h : ∃ (x : M₀), x * a = 0 ∧ x ≠ 0
b : M₀
hb₁ : b * a = 0
hb₂ : b ≠ 0
mpr : Eq (α := Associates M₀) (Associates.mk (b * a)) 0
mpr₁ : Eq.{u_1 + 1} (α := Associates M₀) (Associates.mk 0) 0
mpr₂ mpr₃ : Eq.{u_1 + 1} (α := Associates M₀) 0 0
⊢ HMul.hMul (α := Associates M₀) (Associates.mk b) (Associates.mk a) = 0

Tactic:
rw [Associates.mk_mul_mk, hb₁, Associates.mk_zero]

Premises used: Associates.mk_zero, Associates.mk_mul_mk
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀_1 : ?m.1
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (a : M₀),
    Membership.mem (γ := Submonoid M₀) M₀⁰ a ↔
      (fun (x : Quotient (Associated.setoid M₀)) ↦
          Membership.mem (γ := Submonoid (Quotient (Associated.setoid M₀))) (Quotient (Associated.setoid M₀))⁰ x)
        ⟦a⟧

Tactic:
simp [mem_nonZeroDivisors_iff, Quotient.forall, Associates.mk_mul_mk]

Premises used: Quotient.forall, mem_nonZeroDivisors_iff, Associates.mk_mul_mk
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀_1 : ?m.1
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (x y : ↥M₀⁰),
    (Associated.setoid ↥M₀⁰ : ↥M₀⁰ → ↥M₀⁰ → Prop) x y ↔ (Associated.setoid M₀ : M₀ → M₀ → Prop) (↑x : M₀) (↑y : M₀)

Tactic:
simp +instances [Associated.setoid]

Premises used: Associated.setoid
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀_1 : ?m.1
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (x y : ↥(Associates M₀)⁰),
    Equiv.toFun
        (Equiv.subtypeQuotientEquivQuotientSubtype (fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x)
          (fun (x : Quotient (Associated.setoid M₀)) ↦
            Membership.mem (γ := Submonoid (Quotient (Associated.setoid M₀))) (Quotient (Associated.setoid M₀))⁰ x)
          ⋯ ⋯)
        (x * y) =
      Equiv.toFun
          (Equiv.subtypeQuotientEquivQuotientSubtype (fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x)
            (fun (x : Quotient (Associated.setoid M₀)) ↦
              Membership.mem (γ := Submonoid (Quotient (Associated.setoid M₀))) (Quotient (Associated.setoid M₀))⁰ x)
            ⋯ ⋯)
          x *
        Equiv.toFun
          (Equiv.subtypeQuotientEquivQuotientSubtype (fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x)
            (fun (x : Quotient (Associated.setoid M₀)) ↦
              Membership.mem (γ := Submonoid (Quotient (Associated.setoid M₀))) (Quotient (Associated.setoid M₀))⁰ x)
            ⋯ ⋯)
          y

Tactic:
simp [Quotient.forall, Associates.mk_mul_mk]

Premises used: Quotient.forall, Associates.mk_mul_mk
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
ha : Membership.mem (γ := Submonoid (Associates M₀)) (Associates M₀)⁰ ⟦a⟧
⊢ Eq (α := Associates ↥M₀⁰)
    ((associatesNonZeroDivisorsEquiv : (a : ↥(Associates M₀)⁰) → Associates ↥M₀⁰)
        (Subtype.mk (p := fun (x : Associates M₀) ↦ Membership.mem (γ := Submonoid (Associates M₀)) (Associates M₀)⁰ x)
          ⟦a⟧ ha) :
      Associates ↥M₀⁰)
    (⟦Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) a ⋯⟧ :
      Quotient (α := ↥M₀⁰) (Associated.setoid ↥M₀⁰))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Goal:
M₀ : Type u_1
inst : CommMonoidWithZero M₀
a : M₀
ha : Membership.mem (γ := Submonoid M₀) M₀⁰ a
⊢ (MulEquiv.symm associatesNonZeroDivisorsEquiv : (a : Associates ↥M₀⁰) → ↥(Associates M₀)⁰)
      ⟦Subtype.mk (p := fun (x : M₀) ↦ Membership.mem (γ := Submonoid M₀) M₀⁰ x) a ha⟧ =
    Subtype.mk (p := fun (x : Associates M₀) ↦ Membership.mem (γ := Submonoid (Associates M₀)) (Associates M₀)⁰ x) ⟦a⟧ ⋯

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
h : ∀ (x : ι), HMul.hMul (α := (i : ι) → α i) 0 a x = 0 x
⊢ 0 * a = 0

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
x : ι
⊢ HMul.hMul (α := (i : ι) → α i) 0 a x = 0 x

Tactic:
zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
x : ι
⊢ HMul.hMul (α := (i : ι) → α i) 0 a x = 0 x

Tactic:
exact zero_mul _

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
h : ∀ (x : ι), HMul.hMul (β := (i : ι) → α i) a 0 x = 0 x
⊢ a * 0 = 0

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
x : ι
⊢ HMul.hMul (β := (i : ι) → α i) a 0 x = 0 x

Tactic:
mul_zero _

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f a : (i : ι) → α i
x : ι
⊢ HMul.hMul (β := (i : ι) → α i) a 0 x = 0 x

Tactic:
exact mul_zero _

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
x y : α i
⊢ single (M := α) i (x * y) = single (M := α) i x * single (M := α) i y

Tactic:
(MulHom.single _).map_mul _ _

Premises used: Function.update, Pi.single, dite, MulHom.map_mul, MulHom.single
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i j : ι
a : α i
f : (i : ι) → α i
⊢ single (M := α) i (a * f i) j = single (M := α) i a j * f j

Tactic:
(apply_single (fun i ↦ (· * f i)) (fun _ ↦ zero_mul _) _ _ _).symm

Premises used: HMul.hMul, MulZeroClass.zero_mul, Pi.apply_single, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i j : ι
f : (i : ι) → α i
a : α i
⊢ single (M := α) i (f i * a) j = f j * single (M := α) i a j

Tactic:
(apply_single (f · * ·) (fun _ ↦ mul_zero _) _ _ _).symm

Premises used: HMul.hMul, Pi.apply_single, MulZeroClass.mul_zero, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f : (i : ι) → α i
a : α i
⊢ single (M := α) i (a * f i) = single (M := α) i a * f

Tactic:
funext fun _ ↦ single_mul_left_apply _ _ _ _

Premises used: Pi.single_mul_left_apply, funext
-- Module: Mathlib.Algebra.GroupWithZero.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → MulZeroClass (α i)
inst_1 : DecidableEq ι
i : ι
f : (i : ι) → α i
a : α i
⊢ single (M := α) i (f i * a) = f * single (M := α) i a

Tactic:
funext fun _ ↦ single_mul_right_apply _ _ _ _

Premises used: funext, Pi.single_mul_right_apply
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s t : Finset α
a : α
inst_3 : IsLeftCancelMulZero α
has : a ∈ s
ha : a ≠ 0
⊢ #t ≤ #(s * t)

Tactic:
card_le_card_mul_left_of_injective has (mul_right_injective₀ ha)

Premises used: mul_right_injective₀, Finset.card_le_card_mul_left_of_injective
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s t : Finset α
a : α
inst_3 : IsRightCancelMulZero α
hat : a ∈ t
ha : a ≠ 0
⊢ #s ≤ #(s * t)

Tactic:
card_le_card_mul_right_of_injective hat (mul_left_injective₀ ha)

Premises used: mul_left_injective₀, Finset.card_le_card_mul_right_of_injective
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
inl : ∀ (hs : s.erase 0 = ∅), #s ≤ #(s * s)
inr : ∀ (hs : (s.erase 0).Nonempty), #s ≤ #(s * s)
⊢ #s ≤ #(s * s)

Tactic:
obtain hs | hs := (s.erase 0).eq_empty_or_nonempty

Premises used: OfNat.ofNat, Finset.erase, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : s.erase 0 = ∅
⊢ s = ∅ ∨ s = {0}

Tactic:
rw [erase_eq_empty_iff] at hs

Premises used: Finset.erase_eq_empty_iff
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : s = ∅ ∨ s = {0}
inl : card.{u_1} (α := α) ∅ ≤ #(HMul.hMul (α := Finset α) ∅ ∅)
inl₁ : card (α := α) {0} ≤ #(HMul.hMul (α := Finset α) {0} {0})
⊢ #s ≤ #(s * s)

Tactic:
obtain rfl | rfl := hs

Premises used: rfl
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
inst_3 : IsLeftCancelMulZero α
⊢ card.{u_1} (α := α) ∅ ≤ #(HMul.hMul (α := Finset α) ∅ ∅)

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
inst_3 : IsLeftCancelMulZero α
⊢ card (α := α) {0} ≤ #(HMul.hMul (α := Finset α) {0} {0})

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
hs : (s.erase 0).Nonempty
inr : ∀ (a : α) (ha : a ∈ s.erase 0), #s ≤ #(s * s)
⊢ #s ≤ #(s * s)

Tactic:
obtain ⟨a, ha⟩ := hs
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
a : α
ha : a ∈ s.erase 0
⊢ ¬a = 0 ∧ a ∈ s

Tactic:
simp only [mem_erase, ne_eq] at ha

Premises used: ne_eq, Finset.mem_erase
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
a : α
ha : ¬a = 0 ∧ a ∈ s
⊢ #s ≤ #(s * s)

Tactic:
card_le_card_mul_left₀ ha.2 ha.1

Premises used: And.right, And.left, Finset.card_le_card_mul_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : Mul α
inst_1 : Zero α
inst_2 : DecidableEq α
s : Finset α
inst_3 : IsLeftCancelMulZero α
a : α
ha : ¬a = 0 ∧ a ∈ s
⊢ #s ≤ #(s * s)

Tactic:
exact card_le_card_mul_left₀ ha.2 ha.1

Premises used: And.right, And.left, Finset.card_le_card_mul_left₀
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
s : Finset α
⊢ s * 0 ⊆ 0

Tactic:
simp [subset_iff, mem_mul]

Premises used: Finset.subset_iff, Finset.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
s : Finset α
⊢ 0 * s ⊆ 0

Tactic:
simp [subset_iff, mem_mul]

Premises used: Finset.subset_iff, Finset.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
simpa [mem_mul] using hs

Premises used: Finset.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
simpa [mem_mul] using hs

Premises used: Finset.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
⊢ s / 0 ⊆ 0

Tactic:
simp [subset_iff, mem_div]

Premises used: Finset.mem_div, Finset.subset_iff
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
⊢ 0 / s ⊆ 0

Tactic:
simp [subset_iff, mem_div]

Premises used: Finset.mem_div, Finset.subset_iff
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
simpa [mem_div] using hs

Premises used: Finset.mem_div
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
simpa [mem_div] using hs

Premises used: Finset.mem_div
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
h : ∀ (a : α), Membership.mem (γ := Finset α) 0⁻¹ a ↔ Membership.mem (γ := Finset α) 0 a
⊢ Eq.{u_1 + 1} (α := Finset α) 0⁻¹ 0

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
⊢ Membership.mem (γ := Finset α) 0⁻¹ a ↔ Membership.mem (γ := Finset α) 0 a

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
s : Set α
⊢ s * 0 ⊆ 0

Tactic:
simp [subset_def, mem_mul]

Premises used: Set.subset_def, Set.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
s : Set α
⊢ 0 * s ⊆ 0

Tactic:
simp [subset_def, mem_mul]

Premises used: Set.subset_def, Set.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s * 0

Tactic:
simpa [mem_mul] using hs

Premises used: Set.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : MulZeroClass α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 * s

Tactic:
simpa [mem_mul] using hs

Premises used: Set.mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
⊢ s / 0 ⊆ 0

Tactic:
simp [subset_def, mem_div]

Premises used: Set.subset_def, Set.mem_div
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
⊢ 0 / s ⊆ 0

Tactic:
simp [subset_def, mem_div]

Premises used: Set.subset_def, Set.mem_div
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
simpa [mem_div] using hs

Premises used: Set.mem_div
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
simpa [mem_div] using hs

Premises used: Set.mem_div
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
h : ∀ (x : α), Membership.mem (γ := Set α) 0⁻¹ x ↔ Membership.mem (γ := Set α) 0 x
⊢ Eq.{u_1 + 1} (α := Set α) 0⁻¹ 0

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Goal:
α : Type u_1
inst : GroupWithZero α
x : α
⊢ Membership.mem (γ := Set α) 0⁻¹ x ↔ Membership.mem (γ := Set α) 0 x

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero M₀
inst_2 : MulActionWithZero G₀ M₀
a : G₀
ha : a ≠ 0
s : Set M₀
⊢ #(↑(a • s) : Type u_2) = #(↑s : Type u_2)

Tactic:
Cardinal.mk_image_eq_of_injOn _ _ (MulAction.injective₀ ha).injOn

Premises used: Function.Injective.injOn, MulAction.injective₀, Cardinal.mk_image_eq_of_injOn
-- Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
Goal:
G₀ : Type u_1
M₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : Zero M₀
inst_2 : MulActionWithZero G₀ M₀
a : G₀
ha : a ≠ 0
s : Set M₀
⊢ Nat.card.{u_2} (↑(a • s) : Type u_2) = Nat.card.{u_2} (↑s : Type u_2)

Tactic:
Nat.card_image_of_injective (MulAction.injective₀ ha) _

Premises used: Nat.card_image_of_injective, MulAction.injective₀
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MulZeroClass M₀
inst_1 : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp [Prod.mul_def]

Premises used: Prod.mul_def
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MulZeroClass M₀
inst_1 : MulZeroClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp [Prod.mul_def]

Premises used: Prod.mul_def
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : SemigroupWithZero M₀
inst_1 : SemigroupWithZero N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : SemigroupWithZero M₀
inst_1 : SemigroupWithZero N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MulZeroOneClass M₀
inst_1 : MulZeroOneClass N₀
⊢ ∀ (a : M₀ × N₀), 0 * a = 0

Tactic:
simp
-- Module: Mathlib.Algebra.GroupWithZero.Prod
Goal:
M₀ : Type u_1
N₀ : Type u_2
inst : MulZeroOneClass M₀
inst_1 : MulZeroOneClass N₀
⊢ ∀ (a : M₀ × N₀), a * 0 = 0

Tactic:
simp