awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s t : Finset β
a : α
ha : a ≠ 0
⊢ a • s ⊆ a • t ↔ s ⊆ t

Tactic:
show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_finset_subset_smul_finset_iff

Premises used: Finset.smul_finset_subset_smul_finset_iff, Set.Mem, setOf
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
simp_rw :
  (Set.PairwiseDisjoint.{u_2, u_1} (α := Set β) s fun (i : α) ↦ i • (↑t : Set β)) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))
⊢ (Set.PairwiseDisjoint.{u_2, u_1} (α := Finset β) s fun (x : α) ↦ x • t) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))

Tactic:
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset]

Premises used: Finset.pairwiseDisjoint_coe, Finset.coe_smul_finset
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (Set.PairwiseDisjoint.{u_2, u_1} (α := Set β) s fun (i : α) ↦ i • (↑t : Set β)) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))

Tactic:
Set.pairwiseDisjoint_image_right_iff (fun a ha => MulAction.injective₀ (hs a ha))

Premises used: MulAction.injective₀, Set.pairwiseDisjoint_image_right_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Set α
t : Finset β
hs : ∀ a ∈ s, a ≠ 0
⊢ (Set.PairwiseDisjoint.{u_2, u_1} (α := Set β) s fun (i : α) ↦ i • (↑t : Set β)) ↔
    Set.InjOn (β := β) (fun (p : α × β) ↦ p.1 • p.2) (s ×ˢ (↑t : Set β))

Tactic:
exact Set.pairwiseDisjoint_image_right_iff (fun a ha => MulAction.injective₀ (hs a ha))

Premises used: MulAction.injective₀, Set.pairwiseDisjoint_image_right_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s t : Finset β
a : α
ha : a ≠ 0
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t

Tactic:
show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_finset_subset_iff

Premises used: Set.Mem, setOf, Finset.smul_finset_subset_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s t : Finset β
a : α
ha : a ≠ 0
⊢ s ⊆ a • t ↔ a⁻¹ • s ⊆ t

Tactic:
show _ ⊆ Units.mk0 a ha • _ ↔ _ from subset_smul_finset_iff

Premises used: Finset.subset_smul_finset_iff, Set.Mem, setOf
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s t : Finset β
a : α
ha : a ≠ 0
⊢ a • (s ∩ t) = a • s ∩ a • t

Tactic:
image_inter _ _ <| MulAction.injective₀ ha

Premises used: Finset.image_inter, MulAction.injective₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s t : Finset β
a : α
ha : a ≠ 0
⊢ a • (s \ t) = a • s \ a • t

Tactic:
image_sdiff _ _ <| MulAction.injective₀ ha

Premises used: MulAction.injective₀, Finset.image_sdiff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s t : Finset β
a : α
ha : a ≠ 0
⊢ a • s ∆ t = (a • s) ∆ (a • t)

Tactic:
image_symmDiff _ _ <| MulAction.injective₀ ha

Premises used: MulAction.injective₀, Finset.image_symmDiff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
a : α
inst_3 : Fintype β
ha : a ≠ 0
push_cast : HSMul.hSMul (β := Set β) a Set.univ = Set.univ
⊢ (↑(HSMul.hSMul (β := Finset β) a univ) : Set β) = (↑univ : Set β)

Tactic:
push_cast
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
a : α
inst_3 : Fintype β
ha : a ≠ 0
⊢ HSMul.hSMul (β := Set β) a Set.univ = Set.univ

Tactic:
Set.smul_set_univ₀ ha

Premises used: Set.smul_set_univ₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
a : α
inst_3 : Fintype β
ha : a ≠ 0
⊢ HSMul.hSMul (β := Set β) a Set.univ = Set.univ

Tactic:
exact Set.smul_set_univ₀ ha

Premises used: Set.smul_set_univ₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
s : Finset β
a : α
inst_3 : Fintype β
ha : a ≠ 0
⊢ a • s = univ ↔ s = univ

Tactic:
exact_mod_cast smul_finset_eq_univ (α := Units α) (a := Units.mk0 a ha)

Premises used: Finset.smul_finset_eq_univ
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ ¬(↑s : Set α) ⊆ (↑0 : Set α)

Tactic:
rw [← coe_subset] at hs

Premises used: Finset.coe_subset
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : ¬(↑s : Set α) ⊆ (↑0 : Set α)
push_cast : ∀ (hs : ¬(↑s : Set α) ⊆ 0), HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)

Tactic:
push_cast at hs ⊢
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : ¬(↑s : Set α) ⊆ 0
⊢ HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ

Tactic:
Set.smul_univ₀ hs

Premises used: Set.smul_univ₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : ¬(↑s : Set α) ⊆ 0
⊢ HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ

Tactic:
exact Set.smul_univ₀ hs

Premises used: Set.smul_univ₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nontrivial
push_cast : HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ
⊢ (↑(HSMul.hSMul (β := Finset β) s univ) : Set β) = (↑univ : Set β)

Tactic:
push_cast
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ

Tactic:
Set.smul_univ₀' hs

Premises used: Set.smul_univ₀'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
inst_3 : Fintype β
s : Finset α
hs : s.Nontrivial
⊢ HSMul.hSMul (β := Set β) (↑s : Set α) Set.univ = Set.univ

Tactic:
exact Set.smul_univ₀' hs

Premises used: Set.smul_univ₀'
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
a : α
ha : a ≠ 0
s : Finset β
⊢ #(a • s) = #s

Tactic:
card_image_of_injective _ (MulAction.injective₀ ha)

Premises used: Finset.card_image_of_injective, MulAction.injective₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : GroupWithZero α
inst_2 : MulAction α β
t : Finset β
s : Finset α
hs : ∀ a ∈ s, a ≠ 0
⊢ Set.PairwiseDisjoint.{u_2, u_2} (α := Finset β) ((fun (x : α) ↦ x • t) '' (↑s : Set α)) id → #t ∣ #(s • t)

Tactic:
card_dvd_card_image₂_right fun a ha => MulAction.injective₀ (hs a ha)

Premises used: Finset.card_dvd_card_image₂_right, MulAction.injective₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
inl : (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
inr : ∀ (ha : a ≠ 0), (a •> s)⁻¹ = s⁻¹ <• a⁻¹
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
inl : (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹
inl₁ : ∀ (hs : s.Nonempty), (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
inr : ∀ (a_1 : α), a_1 ∈ (a •> s)⁻¹ ↔ a_1 ∈ s⁻¹ <• a⁻¹
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a_1 : α
⊢ a_1 ∈ (a •> s)⁻¹ ↔ a_1 ∈ s⁻¹ <• a⁻¹

Tactic:
simp only [mem_inv', ne_eq, not_false_eq_true, ← inv_smul_mem_iff₀, smul_eq_mul,
      MulOpposite.op_inv, inv_eq_zero, MulOpposite.op_eq_zero_iff, inv_inv,
      MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]

Premises used: inv_eq_zero, MulOpposite.op_eq_zero_iff, ne_eq, Finset.mem_inv', inv_inv, MulOpposite.unop_op, Finset.inv_smul_mem_iff₀, mul_inv_rev, smul_eq_mul, MulOpposite.smul_eq_mul_unop, not_false_eq_true, MulOpposite.op_inv
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
inl : (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
inr : ∀ (ha : a ≠ 0), (s <• a)⁻¹ = a⁻¹ •> s⁻¹
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
inl : (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹
inl₁ : ∀ (hs : s.Nonempty), (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
simp [*]
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
inr : ∀ (a_1 : α), a_1 ∈ (s <• a)⁻¹ ↔ a_1 ∈ a⁻¹ •> s⁻¹
⊢ (s <• a)⁻¹ = a⁻¹ •> s⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
a_1 : α
⊢ a_1 ∈ (s <• a)⁻¹ ↔ a_1 ∈ a⁻¹ •> s⁻¹

Tactic:
simp only [mem_inv', ne_eq, MulOpposite.op_eq_zero_iff, not_false_eq_true, ←
      inv_smul_mem_iff₀, MulOpposite.smul_eq_mul_unop, MulOpposite.unop_inv, MulOpposite.unop_op,
      inv_eq_zero, inv_inv, smul_eq_mul, mul_inv_rev, ha]

Premises used: inv_eq_zero, MulOpposite.op_eq_zero_iff, ne_eq, Finset.mem_inv', inv_inv, MulOpposite.unop_op, Finset.inv_smul_mem_iff₀, MulOpposite.unop_inv, mul_inv_rev, smul_eq_mul, MulOpposite.smul_eq_mul_unop, not_false_eq_true
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Monoid α
inst_2 : AddGroup β
inst_3 : DistribMulAction α β
a : α
t : Finset β
⊢ a • -t = -(a • t)

Tactic:
simp only [← image_smul, ← image_neg_eq_neg, Function.comp_def, image_image, smul_neg]

Premises used: smul_neg, Finset.image_smul, Function.comp_def, Finset.image_neg_eq_neg, Finset.image_image
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Monoid α
inst_2 : AddGroup β
inst_3 : DistribMulAction α β
s : Finset α
t : Finset β
⊢ HSMul.hSMul (β := Finset β) s (image (fun (x : β) ↦ -x) t) = image (fun (x : β) ↦ -x) (s • t)

Tactic:
image_image₂_right_comm smul_neg

Premises used: smul_neg, Finset.image_image₂_right_comm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Goal:
α : Type u_1
β : Type u_2
inst : DecidableEq β
inst_1 : Monoid α
inst_2 : AddGroup β
inst_3 : DistribMulAction α β
s : Finset α
t : Finset β
⊢ HSMul.hSMul (β := Finset β) s (image (fun (x : β) ↦ -x) t) = image (fun (x : β) ↦ -x) (s • t)

Tactic:
exact image_image₂_right_comm smul_neg

Premises used: smul_neg, Finset.image_image₂_right_comm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
M : Type u_3
ι : Type u_4
α : ι → Type u_5
inst : GroupWithZero M
inst_1 : (i : ι) → MulAction.{u_3, u_5} M (α i)
c : M
hc : c ≠ 0
I : Set ι
s : (i : ι) → Set (α i)
⊢ c • I.pi (α := α) s = I.pi (α := α) (c • s)

Tactic:
smul_set_pi_of_isUnit (.mk0 _ hc) I s

Premises used: Set.smul_set_pi_of_isUnit, IsUnit.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
M : Type u_3
ι : Type u_4
α : ι → Type u_5
inst : GroupWithZero M
inst_1 : (i : ι) → MulAction.{u_3, u_5} M (α i)
c : M
I : Set ι
h : c ≠ 0 ∨ I = univ
s : (i : ι) → Set (α i)
⊢ c • I.pi (α := α) s = I.pi (α := α) (c • s)

Tactic:
h.elim (fun hc ↦ smul_set_pi_of_isUnit (.mk0 _ hc) I s) (fun hI ↦ hI ▸ smul_set_univ_pi ..)

Premises used: Eq.rec, Set.smul_set_pi_of_isUnit, IsUnit.mk0, Set.smul_set_univ_pi, Or.elim, Eq.symm
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : SMulZeroClass α β
s : Set α
t : Set β
a x : α
rw : Eq (α := Set β) {0} 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set β) 0 0
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 0} 0

Tactic:
rw [smul_zero, singleton_zero]

Premises used: smul_zero, Set.singleton_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : SMulZeroClass α β
s : Set α
⊢ HSMul.hSMul (β := Set β) s 0 ⊆ 0

Tactic:
simp [subset_def, mem_smul]

Premises used: Set.mem_smul, Set.subset_def
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : SMulZeroClass α β
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ HSMul.hSMul (β := Set β) s 0

Tactic:
simpa [mem_smul] using hs

Premises used: Set.mem_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero β
inst_1 : SMulZeroClass α β
t : Set β
a : α
h : 0 ∈ t
⊢ 0 ∈ a • t

Tactic:
⟨0, h, smul_zero _⟩

Premises used: Set.Mem, setOf, smul_zero, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
t : Set β
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := Set α) 0 t ⊆ 0

Tactic:
simp [subset_def, mem_smul]

Premises used: Set.mem_smul, Set.subset_def
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
t : Set β
ht : t.Nonempty
⊢ 0 ⊆ HSMul.hSMul.{u_1, u_2, u_2} (α := Set α) 0 t

Tactic:
simpa [mem_smul] using ht

Premises used: Set.mem_smul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
s : Set β
h : s.Nonempty
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 s = 0

Tactic:
simp only [← image_smul, zero_smul, h.image_const, singleton_zero]

Premises used: Set.image_smul, Set.Nonempty.image_const, zero_smul, Set.singleton_zero
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
s : Set β
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 s ⊆ 0

Tactic:
image_subset_iff.2 fun x _ ↦ zero_smul α x

Premises used: Iff.mpr, zero_smul, Set.image_subset_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Zero β
inst_2 : SMulWithZero α β
s : Set β
⊢ (HSMul.hSMul.{u_1, u_2, u_2} (α := α) 0 s).Subsingleton

Tactic:
subsingleton_singleton.anti <| zero_smul_set_subset s

Premises used: Set.subsingleton_singleton, Set.Subsingleton.anti, Set.zero_smul_set_subset
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Monoid α
inst_1 : Monoid β
inst_2 : MulDistribMulAction α β
x : α
rw : Eq (α := Set β) {1} 1
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set β) 1 1
⊢ Eq (α := Set β) {HSMul.hSMul (β := β) x 1} 1

Tactic:
rw [smul_one, singleton_one]

Premises used: MulDistribMulAction.smul_one, Set.singleton_one
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
by_contra! : ∀ (H : s ≠ 0 ∧ t ≠ 0), False
⊢ s = 0 ∨ t = 0

Tactic:
by_contra! H
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
⊢ (s * t).Nonempty

Tactic:
have hst : (s * t).Nonempty := h.symm.subst zero_nonempty
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
hst : (s * t).Nonempty
⊢ ¬s ⊆ 0 ∧ ¬t ⊆ 0

Tactic:
rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H

Premises used: Ne, Set.Nonempty.subset_zero_iff, Set.Nonempty.of_smul_left, Set.Nonempty.of_smul_right
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : s ≠ 0 ∧ t ≠ 0
hst : (s * t).Nonempty
H₁ : ¬s ⊆ 0 ∧ ¬t ⊆ 0
⊢ (s * t).Nonempty

Tactic:
rw [Ne, ← hst.of_smul_left.subset_zero_iff, Ne, ← hst.of_smul_right.subset_zero_iff] at H

Premises used: Ne, Set.Nonempty.subset_zero_iff, Set.Nonempty.of_smul_left, Set.Nonempty.of_smul_right
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
H : ¬s ⊆ 0 ∧ ¬t ⊆ 0
hst : (s * t).Nonempty
⊢ (∃ a ∈ s, ¬a = 0) ∧ ∃ a ∈ t, ¬a = 0

Tactic:
simp only [not_subset, mem_zero] at H

Premises used: Set.mem_zero, Set.not_subset
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
H : (∃ a ∈ s, ¬a = 0) ∧ ∃ a ∈ t, ¬a = 0
obtain : ∀ (a : α) (hs : a ∈ s) (ha : ¬a = 0) (b : α) (ht : b ∈ t) (hb : ¬b = 0), False
⊢ False

Tactic:
obtain ⟨⟨a, hs, ha⟩, b, ht, hb⟩ := H
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
a : α
hs : a ∈ s
ha : ¬a = 0
b : α
ht : b ∈ t
hb : ¬b = 0
⊢ False

Tactic:
(eq_zero_or_eq_zero_of_mul_eq_zero <| h.subset <| mul_mem_mul hs ht).elim ha hb

Premises used: Eq.subset, Or.elim, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero, Set.mul_mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : Zero α
inst_1 : Mul α
inst_2 : NoZeroDivisors α
s t : Set α
h : s * t = 0
hst : (s * t).Nonempty
a : α
hs : a ∈ s
ha : ¬a = 0
b : α
ht : b ∈ t
hb : ¬b = 0
⊢ False

Tactic:
exact (eq_zero_or_eq_zero_of_mul_eq_zero <| h.subset <| mul_mem_mul hs ht).elim ha hb

Premises used: Eq.subset, Or.elim, NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero, Set.mul_mem_mul
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
A : Set β
x : β
⊢ a • x ∈ a • A ↔ x ∈ A

Tactic:
show Units.mk0 a ha • _ ∈ _ ↔ _ from smul_mem_smul_set_iff

Premises used: Set.Mem, Set.smul_mem_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
A : Set β
x : β
⊢ x ∈ a • A ↔ a⁻¹ • x ∈ A

Tactic:
show _ ∈ Units.mk0 a ha • _ ↔ _ from mem_smul_set_iff_inv_smul_mem

Premises used: Set.Mem, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
A : Set β
x : β
⊢ x ∈ a⁻¹ • A ↔ a • x ∈ A

Tactic:
show _ ∈ (Units.mk0 a ha)⁻¹ • _ ↔ _ from mem_inv_smul_set_iff

Premises used: Set.Mem, Set.mem_inv_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
t : Set β
⊢ (fun (x : β) ↦ a • x) ⁻¹' t = a⁻¹ • t

Tactic:
preimage_smul (Units.mk0 a ha) t

Premises used: Set.preimage_smul, Units.mk0
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
t : Set β
⊢ (fun (x : β) ↦ a⁻¹ • x) ⁻¹' t = a • t

Tactic:
preimage_smul (Units.mk0 a ha)⁻¹ t

Premises used: Set.preimage_smul, Units.mk0, Inv.inv
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
A B : Set β
⊢ a • A ⊆ a • B ↔ A ⊆ B

Tactic:
show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_set_subset_smul_set_iff

Premises used: Set.smul_set_subset_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
A B : Set β
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Tactic:
show Units.mk0 a ha • _ ⊆ _ ↔ _ from smul_set_subset_iff_subset_inv_smul_set

Premises used: Set.smul_set_subset_iff_subset_inv_smul_set
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
a : α
ha : a ≠ 0
A B : Set β
⊢ A ⊆ a • B ↔ a⁻¹ • A ⊆ B

Tactic:
show _ ⊆ Units.mk0 a ha • _ ↔ _ from subset_smul_set_iff

Premises used: Set.subset_smul_set_iff
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
s t : Set β
a : α
ha : a ≠ 0
⊢ a • (s ∩ t) = a • s ∩ a • t

Tactic:
show Units.mk0 a ha • _ = _ from smul_set_inter

Premises used: Set.smul_set_inter
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
s t : Set β
a : α
ha : a ≠ 0
⊢ a • (s \ t) = a • s \ a • t

Tactic:
image_diff (MulAction.injective₀ ha) _ _

Premises used: Set.image_diff, MulAction.injective₀
-- Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Goal:
α : Type u_1
β : Type u_2
inst : GroupWithZero α
inst_1 : MulAction α β
s t : Set β
a : α
ha : a ≠ 0
⊢ a • s ∆ t = (a • s) ∆ (a • t)

Tactic:
image_symmDiff (MulAction.injective₀ ha) _ _

Premises used: Set.image_symmDiff, MulAction.injective₀