awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x : MulAction E G := compHom G f
refine : ∀ (x y : G), ∃ (g : E), g • x = y
⊢ IsPretransitive E G

Tactic:
refine ⟨fun x y ↦ ?_⟩
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x_1 : MulAction E G := compHom G f
x y : G
⊢ ∃ (m : F), m • x = y

Tactic:
exists_smul_eq F x y

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x_1 : MulAction E G := compHom G f
x y : G
obtain : ∀ (m : F), ∃ (g : E), g • x = m • x
⊢ ∃ (g : E), g • x = y

Tactic:
obtain ⟨m, rfl⟩ : ∃ m : F, m • x = y := exists_smul_eq F x y

Premises used: MulAction.exists_smul_eq, rfl
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x_1 : MulAction E G := compHom G f
x : G
m : F
⊢ ∃ (e : E), (f : (a : E) → F) e = m

Tactic:
hf m
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x_1 : MulAction E G := compHom G f
x : G
m : F
obtain : ∀ (e : E), ∃ (g : E), g • x = HSMul.hSMul.{u_5, u_6, u_6} (α := F) ((f : (a : E) → F) e : F) x
⊢ ∃ (g : E), g • x = m • x

Tactic:
obtain ⟨e, rfl⟩ : ∃ e, f e = m := hf m

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x_1 : MulAction E G := compHom G f
x : G
e : E
⊢ ∃ (g : E), g • x = HSMul.hSMul.{u_5, u_6, u_6} (α := F) ((f : (a : E) → F) e : F) x

Tactic:
⟨e, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
E : Type u_4
F : Type u_5
G : Type u_6
inst : Monoid E
inst_1 : Monoid F
inst_2 : MulAction F G
inst_3 : IsPretransitive F G
f : E →* F
hf : Surjective.{u_4 + 1, u_5 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x_1 : MulAction E G := compHom G f
x : G
e : E
⊢ ∃ (g : E), g • x = HSMul.hSMul.{u_5, u_6, u_6} (α := F) ((f : (a : E) → F) e : F) x

Tactic:
exact ⟨e, rfl⟩
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
M : Type u_4
N : Type u_5
α : Type u_6
inst : Monoid M
inst_1 : Monoid N
inst_2 : MulAction N α
f : M →* N
h : IsPretransitive M α
⊢ IsPretransitive N α

Tactic:
letI := compHom α f; h.of_smul_eq f rfl

Premises used: MulAction.IsPretransitive.of_smul_eq, DFunLike.coe, rfl
-- Module: Mathlib.Algebra.Group.Action.Hom
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
M : Type u_4
N : Type u_5
inst : Monoid M
inst_1 : MulOneClass N
inst_2 : MulAction M N
inst_3 : IsScalarTower M N N
x y : M
rw : HSMul.hSMul (β := N) (x * y) 1 = x • HSMul.hSMul (β := N) y 1
rw₁ rw₂ : HSMul.hSMul (β := N) (x * y) 1 = HSMul.hSMul (β := N) (x * y) 1
⊢ HSMul.hSMul (β := N) (x * y) 1 = HSMul.hSMul (β := N) x 1 * HSMul.hSMul (β := N) y 1

Tactic:
rw [smul_one_mul, smul_smul]

Premises used: smul_smul, smul_one_mul
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
inst_1 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
r : M
a : α
⊢ op (r • a) = op r • op a

Tactic:
(op_smul_eq_smul r (op a)).symm

Premises used: MulOpposite.unop, Eq.symm, IsCentralScalar.op_smul_eq_smul, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
inst_1 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_2 : IsCentralScalar M α
r : Mᵐᵒᵖ
a : αᵐᵒᵖ
⊢ unop (r • a) = unop r • unop a

Tactic:
(unop_smul_eq_smul r (unop a)).symm

Premises used: IsCentralScalar.unop_smul_eq_smul, MulOpposite.unop, Eq.symm
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a •> b = a •> b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ b <• a = b <• a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a +ᵥ> b = a +ᵥ> b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ b <+ᵥ a = b <+ᵥ a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a₁ •> a₂ •> b = a₁ •> a₂ •> b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ b <• a₂ <• a₁ = b <• a₂ <• a₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a₁ +ᵥ> a₂ +ᵥ> b = a₁ +ᵥ> a₂ +ᵥ> b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ b <+ᵥ a₂ <+ᵥ a₁ = b <+ᵥ a₂ <+ᵥ a₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a₁ •> b <• a₂ = a₁ •> b <• a₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a₁ •> a₂ •> b <• a₃ <• a₄ = a₁ •> a₂ •> b <• a₃ <• a₄

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a₁ +ᵥ> b <+ᵥ a₂ = a₁ +ᵥ> b <+ᵥ a₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : SMul α β
inst_1 : SMul.{u_3, u_4} αᵐᵒᵖ β
inst_2 : VAdd α β
inst_3 : VAdd.{u_3, u_4} αᵃᵒᵖ β
a a₁ a₂ a₃ a₄ : α
b : β
⊢ a₁ +ᵥ> a₂ +ᵥ> b <+ᵥ a₃ <+ᵥ a₄ = a₁ +ᵥ> a₂ +ᵥ> b <+ᵥ a₃ <+ᵥ a₄

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
α : Type u_3
β : Type u_4
inst : Monoid α
inst_1 : MulAction.{u_3, u_4} αᵐᵒᵖ β
b : β
a₁ a₂ : α
⊢ b <• a₁ <• a₂ = b <• (a₁ * a₂)

Tactic:
smul_smul _ _ _

Premises used: smul_smul, MulOpposite.unop
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
α : Type u_3
β : Type u_4
inst : Monoid α
inst_1 : MulAction.{u_3, u_4} αᵐᵒᵖ β
b : β
a₁ a₂ : α
⊢ b <• (a₁ * a₂) = b <• a₁ <• a₂

Tactic:
mul_smul _ _ _

Premises used: MulOpposite.unop, SemigroupAction.mul_smul, MulOpposite.op
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Semigroup α
⊢ SMulCommClass α αᵐᵒᵖ α

Tactic:
SMulCommClass.symm _ _ _

Premises used: SMulCommClass.symm
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst : Mul N
inst_1 : SMul M N
inst_2 : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
h : ∀ (X : N), x • op X • z = op X • x • z
⊢ x • y • z = y • x • z

Tactic:
induction y using MulOpposite.rec'
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M_1 : Type u_1
N_1 : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst : Mul N
inst_1 : SMul M N
inst_2 : IsScalarTower M N N
x : M
z X : N
⊢ x • op X • z = op X • x • z

Tactic:
simp only [smul_mul_assoc, MulOpposite.smul_eq_mul_unop]

Premises used: smul_mul_assoc, MulOpposite.smul_eq_mul_unop
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid α
⊢ Eq.{u_3 + 1} (α := MulAction αᵐᵒᵖ αᵐᵒᵖ) (Monoid.toMulAction αᵐᵒᵖ) instMulAction

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Opposite
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst : Monoid α
⊢ Eq.{u_3 + 1} (α := MulAction αᵐᵒᵖ αᵐᵒᵖ) (Monoid.toMulAction αᵐᵒᵖ) instMulAction

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
a : M
x : Option α
⊢ a • x = Option.map (fun (x : α) ↦ a • x) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
a : M
⊢ HSMul.hSMul (β := Option α) a none = none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
α : Type u_3
inst : SMul M α
a : M
b : α
⊢ a • some b = some (a • b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b_1 : α
x_1 : Option α
inst_2 : SMul M N
inst_3 : IsScalarTower M N α
a : M
b : N
x : Option α
none : HSMul.hSMul (β := Option α) (a • b) Option.none = a • HSMul.hSMul (β := Option α) b Option.none
some : ∀ (val : α), (a • b) • Option.some val = a • b • Option.some val
⊢ (a • b) • x = a • b • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b_1 : α
x : Option α
inst_2 : SMul M N
inst_3 : IsScalarTower M N α
a : M
b : N
⊢ HSMul.hSMul (β := Option α) (a • b) none = a • HSMul.hSMul (β := Option α) b none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b_1 : α
x : Option α
inst_2 : SMul M N
inst_3 : IsScalarTower M N α
a : M
b : N
val : α
⊢ (a • b) • some val = a • b • some val

Tactic:
congr_arg some (smul_assoc _ _ _)

Premises used: smul_assoc, Option.some, congr_arg
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b_1 : α
x : Option α
inst_2 : SMul M N
inst_3 : IsScalarTower M N α
a : M
b : N
⊢ HSMul.hSMul (β := Option α) (a • b) none = a • HSMul.hSMul (β := Option α) b none

Tactic:
exacts [rfl, congr_arg some (smul_assoc _ _ _)]

Premises used: smul_assoc, Option.some, congr_arg, rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a : M
b : α
x : Option α
inst_2 : SMulCommClass M N α
⊢ SMulCommClass.{u_1, u_2, u_3} M N (Option α)

Tactic:
⟨fun _ _ => Function.Commute.option_map <| smul_comm _ _⟩

Premises used: Function.Commute.option_map, SMulCommClass.smul_comm, SMulCommClass.mk
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b : α
x_1 : Option α
inst_2 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_3 : IsCentralScalar M α
a : M
x : Option α
none : HSMul.hSMul (β := Option α) (MulOpposite.op a) Option.none = HSMul.hSMul (β := Option α) a Option.none
some : ∀ (val : α), MulOpposite.op a • Option.some val = a • Option.some val
⊢ MulOpposite.op a • x = a • x

Tactic:
cases x
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b : α
x : Option α
inst_2 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_3 : IsCentralScalar M α
a : M
⊢ HSMul.hSMul (β := Option α) (MulOpposite.op a) none = HSMul.hSMul (β := Option α) a none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b : α
x : Option α
inst_2 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_3 : IsCentralScalar M α
a : M
val : α
⊢ MulOpposite.op a • some val = a • some val

Tactic:
congr_arg some (op_smul_eq_smul _ _)

Premises used: Option.some, congr_arg, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a_1 : M
b : α
x : Option α
inst_2 : SMul.{u_1, u_3} Mᵐᵒᵖ α
inst_3 : IsCentralScalar M α
a : M
⊢ HSMul.hSMul (β := Option α) (MulOpposite.op a) none = HSMul.hSMul (β := Option α) a none

Tactic:
exacts [rfl, congr_arg some (op_smul_eq_smul _ _)]

Premises used: Option.some, congr_arg, IsCentralScalar.op_smul_eq_smul, rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : SMul M α
inst_1 : SMul N α
a : M
b_1 : α
x : Option α
inst_2 : FaithfulSMul M α
m₁ m₂ : M
h : ∀ (a : Option α), m₁ • a = m₂ • a
b : α
⊢ m₁ • b = m₂ • b

Tactic:
injection h (some b)

Premises used: Option.some
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
b : Option α
none : HSMul.hSMul (β := Option α) (a₁ * a₂) Option.none = a₁ • HSMul.hSMul (β := Option α) a₂ Option.none
some : ∀ (val : α), (a₁ * a₂) • Option.some val = a₁ • a₂ • Option.some val
⊢ (a₁ * a₂) • b = a₁ • a₂ • b

Tactic:
cases b
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
⊢ HSMul.hSMul (β := Option α) (a₁ * a₂) none = a₁ • HSMul.hSMul (β := Option α) a₂ none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
val : α
⊢ (a₁ * a₂) • some val = a₁ • a₂ • some val

Tactic:
congr_arg some (mul_smul _ _ _)

Premises used: Option.some, congr_arg, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
a₁ a₂ : M
⊢ HSMul.hSMul (β := Option α) (a₁ * a₂) none = a₁ • HSMul.hSMul (β := Option α) a₂ none

Tactic:
exacts [rfl, congr_arg some (mul_smul _ _ _)]

Premises used: Option.some, congr_arg, SemigroupAction.mul_smul, rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
b : Option α
none : HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Option α) 1 Option.none = Option.none
some : ∀ (val : α), HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (Option.some val) = Option.some val
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 b = b

Tactic:
cases b
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Option α) 1 none = none

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
val : α
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) 1 (some val) = some val

Tactic:
congr_arg some (one_smul _ _)

Premises used: Option.some, one_smul, congr_arg
-- Module: Mathlib.Algebra.Group.Action.Option
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MulAction M α
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Option α) 1 none = none

Tactic:
exacts [rfl, congr_arg some (one_smul _ _)]

Premises used: Option.some, one_smul, congr_arg, rfl
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
inst : (i : ι) → SMul.{u_4, u_5} (α i) (β i)
s : (i : ι) → α i
x : (i : ι) → β i
⊢ s • x = fun (i : ι) ↦ s i • x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
α : ι → Type u_4
β : ι → Type u_5
i : ι
inst : (i : ι) → SMul.{u_4, u_5} (α i) (β i)
s : (i : ι) → α i
x : (i : ι) → β i
⊢ (s • x) i = s i • x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
β : ι → Type u_5
γ : ι → Type u_6
i : ι
inst : (i : ι) → SMul.{u_2, u_5} M (β i)
inst_1 : (i : ι) → SMul.{u_4, u_5} (α i) (β i)
inst_2 : ∀ (i : ι), SMulCommClass.{u_2, u_4, u_5} M (α i) (β i)
⊢ SMulCommClass M ((i : ι) → α i) ((i : ι) → β i)

Tactic:
⟨fun x y z => funext fun i ↦ smul_comm x (y i) (z i)⟩

Premises used: funext, SMulCommClass.smul_comm, SMulCommClass.mk
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : ∀ (i : ι), Nonempty.{u_4 + 1} (α i)
i : ι
inst_2 : FaithfulSMul.{u_2, u_4} M (α i)
m₁ m₂ : M
h : ∀ (a : (i : ι) → α i), m₁ • a = m₂ • a
a : α i
⊢ m₁ • a = m₂ • a

Tactic:
simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i

Premises used: Function.update, Classical.choice, congr_fun
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : ∀ (i : ι), Nonempty.{u_4 + 1} (α i)
i : ι
inst_2 : FaithfulSMul.{u_2, u_4} M (α i)
m₁ m₂ : M
h : ∀ (a : (i : ι) → α i), m₁ • a = m₂ • a
a : α i
⊢ m₁ • a = m₂ • a

Tactic:
classical
    simpa using
      congr_fun (h <| Function.update (fun j => Classical.choice (‹∀ i, Nonempty (α i)› j)) i a) i
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α : ι → Type u_4
β : ι → Type u_5
γ : ι → Type u_6
i : ι
inst : Nonempty ι
inst_1 : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_2 : ∀ (i : ι), Nonempty.{u_4 + 1} (α i)
inst_3 : ∀ (i : ι), FaithfulSMul.{u_2, u_4} M (α i)
⊢ FaithfulSMul M ((i : ι) → α i)

Tactic:
let ⟨i⟩ := ‹Nonempty ι›
  faithfulSMul_at i

Premises used: Pi.faithfulSMul_at, FaithfulSMul, _private.0.Pi.faithfulSMul.match_1
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
N : Type u_3
α_1 : ι → Type u_4
β : ι → Type u_5
γ : ι → Type u_6
i : ι
α : Type u_7
inst : SMul M α
inst_1 : SMul N α
inst_2 : SMulCommClass M N α
⊢ SMulCommClass M N (ι → α)

Tactic:
Pi.smulCommClass

Premises used: Pi.smulCommClass
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
inst_1 : DecidableEq ι
c : M
f₁ : (i : ι) → α i
i : ι
x₁ : α i
⊢ update (β := α) (c • f₁) i (c • x₁) = c • update (β := α) f₁ i x₁

Tactic:
funext fun j => (apply_update (β := α) (fun _ ↦ (c • ·)) f₁ i x₁ j).symm

Premises used: Function.apply_update, funext, HSMul.hSMul, Eq.symm
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
h : ∀ (x : α), extend f (r • g) (r • e) x = (r • extend f g e) x
⊢ extend f (r • g) (r • e) = r • extend f g e

Tactic:
funext x
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h :
  (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) else r • e x) =
    HSMul.hSMul (β := β) r
      (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Tactic:
simp only [extend_def, Pi.smul_apply]

Premises used: Function.extend_def, Pi.smul_apply
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
pos :
  ∀ (h : ∃ (a : ι), f a = x),
    r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) =
      r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h)
neg : (¬∃ (a : ι), f a = x) → r • e x = r • e x
⊢ (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) else r • e x) =
    HSMul.hSMul (β := β) r
      (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h : ∃ (a : ι), f a = x
⊢ r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) =
    r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h)

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h : ¬∃ (a : ι), f a = x
⊢ r • e x = r • e x

Tactic:
rfl
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_7
α : Type u_8
β : Type u_9
inst : SMul M β
r : M
f : ι → α
g : ι → β
e : α → β
x : α
h :
  (if h : ∃ (a : ι), f a = x then r • g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) ⋯) else r • e x) =
    HSMul.hSMul (β := β) r
      (if h : ∃ (a : ι), f a = x then g (Classical.choose (p := fun (x_1 : ι) ↦ f x_1 = x) h) else e x)
⊢ extend f (r • g) (r • e) x = (r • extend f g e) x

Tactic:
classical
  simp only [extend_def, Pi.smul_apply]
  split_ifs <;> rfl

Premises used: Function.extend_def, Pi.smul_apply
-- Module: Mathlib.Algebra.Group.Action.Pi
Goal:
ι : Type u_1
M : Type u_2
α : ι → Type u_4
inst : (i : ι) → SMul.{u_2, u_4} M (α i)
s : Set ι
inst_1 : (i : ι) → Decidable (i ∈ s)
c : M
f₁ g₁ : (i : ι) → α i
⊢ s.piecewise (β := α) (c • f₁) (c • g₁) = c • s.piecewise (β := α) f₁ g₁

Tactic:
s.piecewise_op (δ' := α) f₁ _ fun _ ↦ (c • ·)

Premises used: HSMul.hSMul, Set.piecewise_op
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} α β (Finset γ)

Tactic:
⟨fun _ _ => Commute.finset_image <| smul_comm _ _⟩

Premises used: Function.Commute.finset_image, SMulCommClass.smul_comm, SMulCommClass.mk
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : SMulCommClass α β γ
a : α
s : Finset β
t : Finset γ
⊢ (↑(a • s • t) : Set γ) = (↑(s • a • t) : Set γ)

Tactic:
simp only [coe_smul_finset, coe_smul, smul_comm]

Premises used: Finset.coe_smul_finset, SMulCommClass.smul_comm, Finset.coe_smul
-- Module: Mathlib.Algebra.Group.Action.Pointwise.Finset
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : DecidableEq γ
inst_1 : SMul α γ
inst_2 : SMul β γ
inst_3 : SMulCommClass α β γ
⊢ SMulCommClass.{u_2, u_3, u_4} (Finset α) β (Finset γ)

Tactic:
haveI := SMulCommClass.symm α β γ
  SMulCommClass.symm _ _ _

Premises used: Finset, SMulCommClass.symm