awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u
inst : DivInvMonoid G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
n : ℕ
negSucc : Measurable (β := G) fun (x : G) ↦ (x ^ (n + 1))⁻¹
⊢ Measurable (β := G) fun (x : G) ↦ (x, Int.negSucc n).1 ^ (x, Int.negSucc n).2

Tactic:
simp_rw [zpow_negSucc]

Premises used: zpow_negSucc
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u
inst : DivInvMonoid G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
n : ℕ
⊢ Measurable (β := G) fun (x : G) ↦ (x ^ (n + 1))⁻¹

Tactic:
(measurable_id.pow_const (n + 1)).inv

Premises used: measurable_id, Measurable.inv, HAdd.hAdd, OfNat.ofNat, Measurable.pow_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u
inst : DivInvMonoid G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
n : ℕ
⊢ Measurable (β := G) fun (x : G) ↦ (x ^ (n + 1))⁻¹

Tactic:
exact (measurable_id.pow_const (n + 1)).inv

Premises used: measurable_id, Measurable.inv, HAdd.hAdd, OfNat.ofNat, Measurable.pow_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : DivInvMonoid G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
simp : Measurable (β := G) fun (p : G × G) ↦ p.1 * p.2⁻¹
⊢ Measurable (β := G) fun (p : G × G) ↦ p.1 / p.2

Tactic:
simp only [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : DivInvMonoid G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
⊢ Measurable (β := G) fun (p : G × G) ↦ p.1 * p.2⁻¹

Tactic:
measurable_fst.mul measurable_snd.inv

Premises used: Measurable.mul, Measurable.inv, measurable_snd, measurable_fst
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : DivInvMonoid G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
⊢ Measurable (β := G) fun (p : G × G) ↦ p.1 * p.2⁻¹

Tactic:
exact measurable_fst.mul measurable_snd.inv

Premises used: Measurable.mul, Measurable.inv, measurable_snd, measurable_fst
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Group α
inst_2 : MeasurableDiv α
⊢ Measurable.{u_1, u_1} (α := α) Inv.inv

Tactic:
simpa using measurable_const_div (1 : α)

Premises used: MeasurableDiv.measurable_const_div, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Mul M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
⊢ MeasurableSMul₂ M M

Tactic:
⟨measurable_mul⟩

Premises used: MeasurableMul₂.measurable_mul, MeasurableSMul₂.mk
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α : Type u_3
inst : MeasurableSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : MeasurableConstSMul M α
s : Submonoid M
c : ↥s
⊢ Measurable (β := α) fun (x : α) ↦ c • x

Tactic:
simpa only using measurable_const_smul (c : M)

Premises used: MeasurableConstSMul.measurable_const_smul, Subtype.val
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
inst : MeasurableSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableConstSMul G α
s : Subgroup G
⊢ MeasurableConstSMul.{u_2, u_3} (↥s) α

Tactic:
s.toSubmonoid.instMeasurableConstSMul

Premises used: Set.Mem, Submonoid.instMeasurableConstSMul, Subgroup.toSubmonoid
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : MeasurableSpace α
inst_2 : Group G
inst_3 : MulAction G α
inst_4 : MeasurableSMul G α
s : Subgroup G
⊢ MeasurableSMul.{u_2, u_3} (↥s) α

Tactic:
s.toSubmonoid.instMeasurableSMul

Premises used: Submonoid.instMeasurableSMul, Set.Mem, Subgroup.toSubmonoid
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
g : α → X
inst_2 : MeasurableConstSMul M X
hg : Measurable g
c : M
⊢ Measurable (c • g)

Tactic:
(measurable_const_smul c).comp hg

Premises used: Measurable.comp, MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
μ : Measure α
g : α → X
inst_2 : MeasurableConstSMul M X
hg : AEMeasurable g μ
c : M
⊢ AEMeasurable (c • g) μ

Tactic:
(measurable_const_smul c).comp_aemeasurable hg

Premises used: MeasurableConstSMul.measurable_const_smul, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M
g : α → X
inst_2 : MeasurableConstSMul M X
inst_3 : SMul M α
inst_4 : SMul.{u_2, u_4} Mᵐᵒᵖ α
inst_5 : IsCentralScalar M α
inst_6 : MeasurableConstSMul M α
⊢ ∀ (c : Mᵐᵒᵖ), Measurable (β := α) fun (x : α) ↦ c • x

Tactic:
simpa using measurable_const_smul

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
f : α → M
g : α → X
inst_2 : MeasurableSpace M
inst_3 : MeasurableSMul₂ M X
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_4, u_3} (β := X) fun (x : α) ↦ f x • g x

Tactic:
measurable_smul.comp (hf.prodMk hg)

Premises used: Measurable.comp, Measurable.prodMk, MeasurableSMul₂.measurable_smul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableSpace M
inst_3 : MeasurableSMul₂ M X
f : α → β → M
g : α → β → X
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
dsimp : Measurable.{u_4, u_3} (β := X) fun (a : α) ↦ f a (h a) • g a (h a)
⊢ Measurable.{u_4, u_3} (β := X) fun (a : α) ↦ (f a • g a) (h a)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableSpace M
inst_3 : MeasurableSMul₂ M X
f : α → β → M
g : α → β → X
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable.{u_4, u_3} (β := X) fun (a : α) ↦ f a (h a) • g a (h a)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
f : α → M
g : α → X
inst_2 : MeasurableSpace M
inst_3 : MeasurableSMul₂ M X
μ : Measure α
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_4, u_3} (β := X) (fun (x : α) ↦ f x • g x) μ

Tactic:
MeasurableSMul₂.measurable_smul.comp_aemeasurable (hf.prodMk hg)

Premises used: AEMeasurable.prodMk, MeasurableSMul₂.measurable_smul, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
f : α → M
inst_2 : MeasurableSpace M
inst_3 : MeasurableSMul M X
hf : Measurable f
y : X
⊢ Measurable.{u_4, u_3} (β := X) fun (x : α) ↦ f x • y

Tactic:
(MeasurableSMul.measurable_smul_const y).comp hf

Premises used: Measurable.comp, MeasurableSMul.measurable_smul_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
X : Type u_3
α : Type u_4
inst : MeasurableSpace X
inst_1 : SMul M X
m : MeasurableSpace α
μ : Measure α
f : α → M
inst_2 : MeasurableSpace M
inst_3 : MeasurableSMul M X
hf : AEMeasurable f μ
y : X
⊢ AEMeasurable.{u_4, u_3} (β := X) (fun (x : α) ↦ f x • y) μ

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
this : Measurable (β := M) fun (p : M × ℕ) ↦ p.2 • p.1
⊢ Measurable.{u_6, u_6} (α := ℕ × M) (β := M) (Function.uncurry fun (x1 : ℕ) (x2 : M) ↦ x1 • x2)

Tactic:
apply this.comp measurable_swap

Premises used: Measurable.comp, measurable_swap
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
suffices : Measurable (β := M) fun (p : M × ℕ) ↦ p.2 • p.1
⊢ Measurable.{u_6, u_6} (α := ℕ × M) (β := M) (Function.uncurry fun (x1 : ℕ) (x2 : M) ↦ x1 • x2)

Tactic:
suffices Measurable fun p : M × ℕ => p.2 • p.1 by apply this.comp measurable_swap
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
⊢ Measurable (β := M) fun (p : M × ℕ) ↦ p.2 • p.1

Tactic:
measurable_from_prod_countable_left fun n => ?_

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
refine : ∀ (n : ℕ), Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
⊢ Measurable (β := M) fun (p : M × ℕ) ↦ p.2 • p.1

Tactic:
refine measurable_from_prod_countable_left fun n => ?_

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
⊢ Measurable (β := M) fun (x : M) ↦ HSMul.hSMul (α := ℕ) (x, 0).2 (x, 0).1

Tactic:
simp only [zero_smul, ← Pi.zero_def, measurable_zero]

Premises used: Pi.zero_def, zero_smul, measurable_zero
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
n : ℕ
ih : Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
succ : Measurable (β := M) fun (x : M) ↦ n • x + x
⊢ Measurable (β := M) fun (x : M) ↦ (x, n + 1).2 • (x, n + 1).1

Tactic:
simp only [succ_nsmul]

Premises used: succ_nsmul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
n : ℕ
ih : Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
⊢ Measurable (β := M) fun (x : M) ↦ n • x + x

Tactic:
ih.add measurable_id

Premises used: measurable_id, Measurable.add
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
n : ℕ
ih : Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
⊢ Measurable (β := M) fun (x : M) ↦ n • x + x

Tactic:
exact ih.add measurable_id

Premises used: measurable_id, Measurable.add
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : AddMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
n : ℕ
zero : Measurable (β := M) fun (x : M) ↦ HSMul.hSMul (α := ℕ) (x, 0).2 (x, 0).1
succ :
  ∀ (n : ℕ) (ih : Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1),
    Measurable (β := M) fun (x : M) ↦ (x, n + 1).2 • (x, n + 1).1
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1

Tactic:
induction n with
    | zero => simp only [zero_smul, ← Pi.zero_def, measurable_zero]
    | succ n ih =>
      simp only [succ_nsmul]
      exact ih.add measurable_id

Premises used: Pi.zero_def, zero_smul, measurable_zero, succ_nsmul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
this : Measurable (β := M) fun (p : M × ℤ) ↦ p.2 • p.1
⊢ Measurable.{u_6, u_6} (α := ℤ × M) (β := M) (Function.uncurry fun (x1 : ℤ) (x2 : M) ↦ x1 • x2)

Tactic:
apply this.comp measurable_swap

Premises used: Measurable.comp, measurable_swap
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
suffices : Measurable (β := M) fun (p : M × ℤ) ↦ p.2 • p.1
⊢ Measurable.{u_6, u_6} (α := ℤ × M) (β := M) (Function.uncurry fun (x1 : ℤ) (x2 : M) ↦ x1 • x2)

Tactic:
suffices Measurable fun p : M × ℤ => p.2 • p.1 by apply this.comp measurable_swap
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
⊢ Measurable (β := M) fun (p : M × ℤ) ↦ p.2 • p.1

Tactic:
measurable_from_prod_countable_left fun n => ?_

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
refine : ∀ (n : ℤ), Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
⊢ Measurable (β := M) fun (p : M × ℤ) ↦ p.2 • p.1

Tactic:
refine measurable_from_prod_countable_left fun n => ?_

Premises used: measurable_from_prod_countable_left
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℕ
ofNat : Measurable (β := M) fun (x : M) ↦ n • x
⊢ Measurable (β := M) fun (x : M) ↦ (x, Int.ofNat n).2 • (x, Int.ofNat n).1

Tactic:
simp only [Int.ofNat_eq_natCast, natCast_zsmul]

Premises used: Int.ofNat_eq_natCast, natCast_zsmul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℕ
⊢ Measurable (β := M) fun (x : M) ↦ n • x

Tactic:
measurable_const_smul _

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℕ
⊢ Measurable (β := M) fun (x : M) ↦ n • x

Tactic:
exact measurable_const_smul _

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℕ
negSucc : Measurable (β := M) fun (x : M) ↦ -((n + 1) • x)
⊢ Measurable (β := M) fun (x : M) ↦ (x, Int.negSucc n).2 • (x, Int.negSucc n).1

Tactic:
simp only [negSucc_zsmul]

Premises used: negSucc_zsmul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℕ
⊢ Measurable (β := M) fun (x : M) ↦ -((n + 1) • x)

Tactic:
(measurable_const_smul _).neg

Premises used: MeasurableConstSMul.measurable_const_smul, Measurable.neg
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℕ
⊢ Measurable (β := M) fun (x : M) ↦ -((n + 1) • x)

Tactic:
exact (measurable_const_smul _).neg

Premises used: MeasurableConstSMul.measurable_const_smul, Measurable.neg
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M_1 : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
inst : MeasurableSpace X
inst_1 : SMul M_1 X
m : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → M_1
g : α → X
inst_2 : MeasurableSpace M_1
inst_3 : MeasurableSMul M_1 X
M : Type u_6
inst_4 : SubNegMonoid M
inst_5 : MeasurableSpace M
inst_6 : MeasurableAdd₂ M
inst_7 : MeasurableNeg M
n : ℤ
ofNat : ∀ (n : ℕ), Measurable (β := M) fun (x : M) ↦ (x, Int.ofNat n).2 • (x, Int.ofNat n).1
negSucc : ∀ (n : ℕ), Measurable (β := M) fun (x : M) ↦ (x, Int.negSucc n).2 • (x, Int.negSucc n).1
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1

Tactic:
cases n with
    | ofNat n =>
      simp only [Int.ofNat_eq_natCast, natCast_zsmul]
      exact measurable_const_smul _
    | negSucc n =>
      simp only [negSucc_zsmul]
      exact (measurable_const_smul _).neg

Premises used: Int.ofNat_eq_natCast, MeasurableConstSMul.measurable_const_smul, Measurable.neg, negSucc_zsmul, natCast_zsmul
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_2
x : MeasurableSpace α
f : α → α
⊢ MeasurableSMul (IterateMulAct f) α ↔ Measurable f

Tactic:
⟨fun _ ↦ measurable_const_smul (IterateMulAct.mk (f := f) 1), fun h ↦
    have := h.measurableSMul₂_iterateMulAct; inferInstance⟩

Premises used: inferInstance, IterateMulAct.mk, MeasurableConstSMul.measurable_const_smul, Iff.intro, OfNat.ofNat, Measurable.measurableSMul₂_iterateMulAct
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_2
x : MeasurableSpace α
f : α → α
⊢ MeasurableSMul₂ (IterateMulAct f) α ↔ Measurable f

Tactic:
⟨fun _ ↦ measurableSMul_iterateMulAct.mp inferInstance,
    Measurable.measurableSMul₂_iterateMulAct⟩

Premises used: inferInstance, measurableSMul_iterateMulAct, Iff.intro, Iff.mp, Measurable.measurableSMul₂_iterateMulAct
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_5
α : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace α
f : α → β
G : Type u_7
inst_2 : Group G
inst_3 : MulAction G β
inst_4 : MeasurableConstSMul G β
c : G
h : Measurable.{u_6, u_5} (β := β) fun (x : α) ↦ c • f x
⊢ Measurable f

Tactic:
simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹

Premises used: inv_smul_smul, Measurable.const_smul, Inv.inv, Pi.smul_def
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_5
α : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace α
f : α → β
μ : Measure α
G : Type u_7
inst_2 : Group G
inst_3 : MulAction G β
inst_4 : MeasurableConstSMul G β
c : G
h : AEMeasurable.{u_6, u_5} (β := β) (fun (x : α) ↦ c • f x) μ
⊢ AEMeasurable f μ

Tactic:
simpa [inv_smul_smul, Pi.smul_def] using h.const_smul c⁻¹

Premises used: AEMeasurable.const_smul, inv_smul_smul, Inv.inv, Pi.smul_def
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_4
β : Type u_5
α : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace α
f : α → β
inst_2 : Monoid M
inst_3 : MulAction M β
inst_4 : MeasurableConstSMul M β
c : M
hc : IsUnit c
⊢ (Measurable.{u_6, u_5} (β := β) fun (x : α) ↦ c • f x) ↔ Measurable f

Tactic:
let ⟨u, hu⟩ := hc
  hu ▸ measurable_const_smul_iff u

Premises used: Measurable, Eq.rec, Iff, HSMul.hSMul, _private.0.IsUnit.measurable_const_smul_iff.match_1, measurable_const_smul_iff
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_4
β : Type u_5
α : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace α
f : α → β
μ : Measure α
inst_2 : Monoid M
inst_3 : MulAction M β
inst_4 : MeasurableConstSMul M β
c : M
hc : IsUnit c
⊢ AEMeasurable.{u_6, u_5} (β := β) (fun (x : α) ↦ c • f x) μ ↔ AEMeasurable f μ

Tactic:
let ⟨u, hu⟩ := hc
  hu ▸ aemeasurable_const_smul_iff u

Premises used: AEMeasurable, Eq.rec, Iff, aemeasurable_const_smul_iff, HSMul.hSMul, _private.0.IsUnit.measurable_const_smul_iff.match_1
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G₀ : Type u_3
β : Type u_5
α : Type u_6
inst : MeasurableSpace β
inst_1 : MeasurableSpace α
f : α → β
inst_2 : GroupWithZero G₀
inst_3 : MulAction G₀ β
inst_4 : MeasurableConstSMul G₀ β
c : G₀
hc : c ≠ 0
⊢ (Measurable.{u_6, u_5} (β := β) fun (x : α) ↦ c • f x) ↔ Measurable f

Tactic:
(IsUnit.mk0 c hc).measurable_const_smul_iff

Premises used: IsUnit.mk0, IsUnit.measurable_const_smul_iff