awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f g : α → M
μ : Measure α
inst_2 : MeasurableMul₂ M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (f * g) μ

Tactic:
measurable_mul.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableMul₂.measurable_mul, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
f g : α → M
μ : Measure α
inst_2 : MeasurableMul₂ M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_3, u_2} (β := M) (fun (a : α) ↦ f a * g a) μ

Tactic:
measurable_mul.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableMul₂.measurable_mul, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α_2 : Type u_3
β : Type u_4
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α_2
mβ : MeasurableSpace β
f g : α_2 → M
μ : Measure α_2
ι : Type u_5
α : ι → Type u_6
inst_2 : (i : ι) → Mul (α i)
inst_3 : (i : ι) → MeasurableSpace (α i)
inst_4 : ∀ (i : ι), MeasurableMul.{u_6} (α i)
⊢ MeasurableMul ((i : ι) → α i)

Tactic:
⟨fun _ => measurable_pi_iff.mpr fun i => (measurable_pi_apply i).const_mul _, fun _ =>
    measurable_pi_iff.mpr fun i => (measurable_pi_apply i).mul_const _⟩

Premises used: Iff.mpr, measurable_pi_iff, measurable_pi_apply, MeasurableMul.mk, Measurable.const_mul, Measurable.mul_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
M : Type u_2
α_2 : Type u_3
β : Type u_4
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α_2
mβ : MeasurableSpace β
f g : α_2 → M
μ : Measure α_2
ι : Type u_5
α : ι → Type u_6
inst_2 : (i : ι) → Mul (α i)
inst_3 : (i : ι) → MeasurableSpace (α i)
inst_4 : ∀ (i : ι), MeasurableMul₂.{u_6} (α i)
⊢ MeasurableMul₂ ((i : ι) → α i)

Tactic:
⟨measurable_pi_iff.mpr fun _ => measurable_fst.eval.mul measurable_snd.eval⟩

Premises used: Iff.mpr, Measurable.mul, measurable_pi_iff, measurable_snd, Measurable.eval, MeasurableMul₂.mk, measurable_fst
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
simp_rw : Measurable (β := G) fun (h : G) ↦ h * g⁻¹
⊢ Measurable (β := G) fun (h : G) ↦ h / g

Tactic:
simp_rw [div_eq_mul_inv, measurable_mul_const]

Premises used: div_eq_mul_inv, MeasurableMul.measurable_mul_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
⊢ Measurable (β := M) fun (x : M) ↦ HPow.hPow (β := ℕ) (x, 0).1 (x, 0).2

Tactic:
simp only [pow_zero, ← Pi.one_def, measurable_one]

Premises used: pow_zero, measurable_one, Pi.one_def
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
n : ℕ
ih : Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2
succ : Measurable (β := M) fun (x : M) ↦ x ^ n * x
⊢ Measurable (β := M) fun (x : M) ↦ (x, n + 1).1 ^ (x, n + 1).2

Tactic:
simp only [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
n : ℕ
ih : Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2
⊢ Measurable (β := M) fun (x : M) ↦ x ^ n * x

Tactic:
ih.mul measurable_id

Premises used: Measurable.mul, measurable_id
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
n : ℕ
ih : Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2
⊢ Measurable (β := M) fun (x : M) ↦ x ^ n * x

Tactic:
exact ih.mul measurable_id

Premises used: Measurable.mul, measurable_id
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
n : ℕ
zero : Measurable (β := M) fun (x : M) ↦ HPow.hPow (β := ℕ) (x, 0).1 (x, 0).2
succ :
  ∀ (n : ℕ) (ih : Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2),
    Measurable (β := M) fun (x : M) ↦ (x, n + 1).1 ^ (x, n + 1).2
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2

Tactic:
induction n with
      | zero => simp only [pow_zero, ← Pi.one_def, measurable_one]
      | succ n ih =>
        simp only [pow_succ]
        exact ih.mul measurable_id

Premises used: pow_succ, pow_zero, measurable_one, Pi.one_def
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_2
γ : Type u_3
α : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Pow β γ
inst_3 : MeasurablePow β γ
m : MeasurableSpace α
f : α → β
g : α → γ
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_4, u_2} (β := β) fun (x : α) ↦ f x ^ g x

Tactic:
measurable_pow.comp (hf.prodMk hg)

Premises used: Measurable.comp, MeasurablePow.measurable_pow, Measurable.prodMk
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_2
γ : Type u_3
α : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Pow β γ
inst_3 : MeasurablePow β γ
m : MeasurableSpace α
μ : Measure α
f : α → β
g : α → γ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_4, u_2} (β := β) (fun (x : α) ↦ f x ^ g x) μ

Tactic:
measurable_pow.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurablePow.measurable_pow, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_2
γ : Type u_3
α : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Pow β γ
inst_3 : MeasurablePow β γ
m : MeasurableSpace α
f : α → β
hf : Measurable f
c : γ
⊢ Measurable.{u_4, u_2} (β := β) fun (x : α) ↦ f x ^ c

Tactic:
hf.pow measurable_const

Premises used: measurable_const, Measurable.pow
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_2
γ : Type u_3
α : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Pow β γ
inst_3 : MeasurablePow β γ
m : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEMeasurable f μ
c : γ
⊢ AEMeasurable.{u_4, u_2} (β := β) (fun (x : α) ↦ f x ^ c) μ

Tactic:
hf.pow aemeasurable_const

Premises used: AEMeasurable.pow, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_2
γ : Type u_3
α : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Pow β γ
inst_3 : MeasurablePow β γ
m : MeasurableSpace α
g : α → γ
hg : Measurable g
c : β
⊢ Measurable.{u_4, u_2} (β := β) fun (x : α) ↦ c ^ g x

Tactic:
measurable_const.pow hg

Premises used: measurable_const, Measurable.pow
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
β : Type u_2
γ : Type u_3
α : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace γ
inst_2 : Pow β γ
inst_3 : MeasurablePow β γ
m : MeasurableSpace α
μ : Measure α
g : α → γ
hg : AEMeasurable g μ
c : β
⊢ AEMeasurable.{u_4, u_2} (β := β) (fun (x : α) ↦ c ^ g x) μ

Tactic:
aemeasurable_const.pow hg

Premises used: AEMeasurable.pow, aemeasurable_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f : α → G
inst_2 : MeasurableDiv G
hf : Measurable f
c : G
⊢ Measurable.{u_3, u_2} (β := G) fun (x : α) ↦ c / f x

Tactic:
(MeasurableDiv.measurable_const_div c).comp hf

Premises used: Measurable.comp, MeasurableDiv.measurable_const_div
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f : α → G
μ : Measure α
inst_2 : MeasurableDiv G
hf : AEMeasurable f μ
c : G
⊢ AEMeasurable.{u_3, u_2} (β := G) (fun (x : α) ↦ c / f x) μ

Tactic:
(MeasurableDiv.measurable_const_div c).comp_aemeasurable hf

Premises used: MeasurableDiv.measurable_const_div, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f : α → G
inst_2 : MeasurableDiv G
hf : Measurable f
c : G
⊢ Measurable.{u_3, u_2} (β := G) fun (x : α) ↦ f x / c

Tactic:
(MeasurableDiv.measurable_div_const c).comp hf

Premises used: MeasurableDiv.measurable_div_const, Measurable.comp
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f : α → G
μ : Measure α
inst_2 : MeasurableDiv G
hf : AEMeasurable f μ
c : G
⊢ AEMeasurable.{u_3, u_2} (β := G) (fun (x : α) ↦ f x / c) μ

Tactic:
(MeasurableDiv.measurable_div_const c).comp_aemeasurable hf

Premises used: MeasurableDiv.measurable_div_const, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f g : α → G
inst_2 : MeasurableDiv₂ G
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_3, u_2} (β := G) fun (a : α) ↦ f a / g a

Tactic:
measurable_div.comp (hf.prodMk hg)

Premises used: Measurable.comp, MeasurableDiv₂.measurable_div, Measurable.prodMk
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
dsimp : Measurable.{u_3, u_2} (β := G) fun (a : α) ↦ f a (h a) / g a (h a)
⊢ Measurable.{u_3, u_2} (β := G) fun (a : α) ↦ (f a / g a) (h a)

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableDiv₂ G
f g : α → β → G
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable.{u_3, u_2} (β := G) fun (a : α) ↦ f a (h a) / g a (h a)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f g : α → G
μ : Measure α
inst_2 : MeasurableDiv₂ G
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (f / g) μ

Tactic:
measurable_div.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableDiv₂.measurable_div, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
f g : α → G
μ : Measure α
inst_2 : MeasurableDiv₂ G
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_3, u_2} (β := G) (fun (a : α) ↦ f a / g a) μ

Tactic:
measurable_div.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableDiv₂.measurable_div, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → G
μ : Measure α
inst_2 : MeasurableDiv₂ G
⊢ MeasurableDiv G

Tactic:
⟨fun _ => measurable_const.div measurable_id, fun _ => measurable_id.div measurable_const⟩

Premises used: measurable_id, Measurable.div, MeasurableDiv.mk, measurable_const
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α_2 : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α_2
mβ : MeasurableSpace β
f g : α_2 → G
μ : Measure α_2
ι : Type u_5
α : ι → Type u_6
inst_2 : (i : ι) → Div (α i)
inst_3 : (i : ι) → MeasurableSpace (α i)
inst_4 : ∀ (i : ι), MeasurableDiv.{u_6} (α i)
⊢ MeasurableDiv ((i : ι) → α i)

Tactic:
⟨fun _ => measurable_pi_iff.mpr fun i => (measurable_pi_apply i).const_div _, fun _ =>
    measurable_pi_iff.mpr fun i => (measurable_pi_apply i).div_const _⟩

Premises used: Iff.mpr, measurable_pi_iff, measurable_pi_apply, Measurable.div_const, MeasurableDiv.mk, Measurable.const_div
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α_2 : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α_2
mβ : MeasurableSpace β
f g : α_2 → G
μ : Measure α_2
ι : Type u_5
α : ι → Type u_6
inst_2 : (i : ι) → Div (α i)
inst_3 : (i : ι) → MeasurableSpace (α i)
inst_4 : ∀ (i : ι), MeasurableDiv₂.{u_6} (α i)
⊢ MeasurableDiv₂ ((i : ι) → α i)

Tactic:
⟨measurable_pi_iff.mpr fun _ => measurable_fst.eval.div measurable_snd.eval⟩

Premises used: Iff.mpr, measurable_pi_iff, MeasurableDiv₂.mk, Measurable.div, measurable_snd, Measurable.eval, measurable_fst
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → G
μ : Measure α
E : Type u_5
inst_2 : MeasurableSpace E
inst_3 : AddGroup E
inst_4 : MeasurableSingletonClass E
inst_5 : MeasurableSub₂ E
measurableSet_diagonal : MeasurableSet (Set.diagonal E)
⊢ MeasurableEq E

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → G
μ : Measure α
E : Type u_5
inst_2 : MeasurableSpace E
inst_3 : AddGroup E
inst_4 : MeasurableSingletonClass E
inst_5 : MeasurableSub₂ E
measurableSet_diagonal : MeasurableSet.{u_5} (α := E × E) {p : E × E | p.1 - p.2 = 0}
⊢ MeasurableSet (Set.diagonal E)

Tactic:
simp_rw +singlePass [Set.diagonal, ← sub_eq_zero]

Premises used: sub_eq_zero, Set.diagonal
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β
f g : α → G
μ : Measure α
E : Type u_5
inst_2 : MeasurableSpace E
inst_3 : AddGroup E
inst_4 : MeasurableSingletonClass E
inst_5 : MeasurableSub₂ E
⊢ MeasurableSet.{u_5} (α := E × E) {p : E × E | p.1 - p.2 = 0}

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β_1 : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β_1
f g : α → G
μ : Measure α
β : Type u_5
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : CanonicallyOrderedAdd β
inst_5 : Sub β
inst_6 : OrderedSub β
x : MeasurableSpace β
inst_7 : MeasurableSub₂ β
inst_8 : MeasurableSingletonClass β
measurableSet_diagonal : MeasurableSet (Set.diagonal β)
⊢ MeasurableEq β

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β_1 : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β_1
f g : α → G
μ : Measure α
β : Type u_5
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : CanonicallyOrderedAdd β
inst_5 : Sub β
inst_6 : OrderedSub β
x : MeasurableSpace β
inst_7 : MeasurableSub₂ β
inst_8 : MeasurableSingletonClass β
measurableSet_diagonal : MeasurableSet.{u_5} (α := β × β) {p : β × β | p.1 - p.2 = 0 ∧ p.2 - p.1 = 0}
⊢ MeasurableSet (Set.diagonal β)

Tactic:
simp_rw [Set.diagonal, le_antisymm_iff, ← tsub_eq_zero_iff_le]

Premises used: tsub_eq_zero_iff_le, Set.diagonal, le_antisymm_iff
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α : Type u_3
β_1 : Type u_4
inst : MeasurableSpace G
inst_1 : Div G
m : MeasurableSpace α
mβ : MeasurableSpace β_1
f g : α → G
μ : Measure α
β : Type u_5
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : CanonicallyOrderedAdd β
inst_5 : Sub β
inst_6 : OrderedSub β
x : MeasurableSpace β
inst_7 : MeasurableSub₂ β
inst_8 : MeasurableSingletonClass β
⊢ MeasurableSet.{u_5} (α := β × β) {p : β × β | p.1 - p.2 = 0 ∧ p.2 - p.1 = 0}

Tactic:
measurability
-- 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
c : G
⊢ Measurable (β := G) fun (x : G) ↦ c * x⁻¹

Tactic:
measurable_inv.const_mul c

Premises used: MeasurableInv.measurable_inv, Measurable.const_mul
-- 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
c : G
h : Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ c / x) fun (x : G) ↦ c * x⁻¹
⊢ Measurable (β := G) fun (x : G) ↦ c / x

Tactic:
convert! measurable_inv.const_mul c using 1

Premises used: MeasurableInv.measurable_inv, Measurable.const_mul
-- 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
c : G
h : ∀ (x : G), c / x = c * x⁻¹
⊢ Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ c / x) fun (x : G) ↦ c * x⁻¹

Tactic:
ext1
-- 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
c x : G
⊢ c / x = c * x⁻¹

Tactic:
apply 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
c : G
⊢ Measurable (β := G) fun (x : G) ↦ id x * c⁻¹

Tactic:
measurable_id.mul_const c⁻¹

Premises used: measurable_id, Inv.inv, Measurable.mul_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
c : G
h : Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ x / c) fun (x : G) ↦ id x * c⁻¹
⊢ Measurable (β := G) fun (x : G) ↦ x / c

Tactic:
convert! measurable_id.mul_const c⁻¹ using 1

Premises used: measurable_id, Inv.inv, Measurable.mul_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
c : G
h : ∀ (x : G), x / c = id x * c⁻¹
⊢ Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ x / c) fun (x : G) ↦ id x * c⁻¹

Tactic:
ext1
-- 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
c x : G
⊢ x / c = id x * c⁻¹

Tactic:
apply div_eq_mul_inv

Premises used: div_eq_mul_inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : Inv G
inst_1 : MeasurableSpace G
inst_2 : MeasurableInv G
m : MeasurableSpace α
f : α → G
hf : Measurable f
⊢ Measurable.{u_3, u_2} (β := G) fun (x : α) ↦ (f x)⁻¹

Tactic:
measurable_inv.comp hf

Premises used: Measurable.comp, MeasurableInv.measurable_inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
α : Type u_3
inst : Inv G
inst_1 : MeasurableSpace G
inst_2 : MeasurableInv G
m : MeasurableSpace α
f : α → G
μ : Measure α
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_3, u_2} (β := G) (fun (x : α) ↦ (f x)⁻¹) μ

Tactic:
measurable_inv.comp_aemeasurable hf

Premises used: MeasurableInv.measurable_inv, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_3
m : MeasurableSpace α
G : Type u_4
inst : InvolutiveInv G
inst_1 : MeasurableSpace G
inst_2 : MeasurableInv G
f : α → G
h : Measurable.{u_3, u_4} (β := G) fun (x : α) ↦ (f x)⁻¹
⊢ Measurable f

Tactic:
simpa only [inv_inv] using h.inv

Premises used: Measurable.inv, inv_inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_3
m : MeasurableSpace α
μ : Measure α
G : Type u_4
inst : InvolutiveInv G
inst_1 : MeasurableSpace G
inst_2 : MeasurableInv G
f : α → G
h : AEMeasurable.{u_3, u_4} (β := G) (fun (x : α) ↦ (f x)⁻¹) μ
⊢ AEMeasurable f μ

Tactic:
simpa only [inv_inv] using h.inv

Premises used: inv_inv, AEMeasurable.inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α_1 : Type u_1
G : Type u_2
α_2 : Type u_3
inst : Inv G
inst_1 : MeasurableSpace G
inst_2 : MeasurableInv G
m : MeasurableSpace α_2
f : α_2 → G
μ : Measure α_2
ι : Type u_4
α : ι → Type u_5
inst_3 : (i : ι) → Inv (α i)
inst_4 : (i : ι) → MeasurableSpace (α i)
inst_5 : ∀ (i : ι), MeasurableInv.{u_5} (α i)
⊢ MeasurableInv ((i : ι) → α i)

Tactic:
⟨measurable_pi_iff.mpr fun i => (measurable_pi_apply i).inv⟩

Premises used: Iff.mpr, measurable_pi_iff, measurable_pi_apply, MeasurableInv.mk, Measurable.inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
G : Type u_2
inst : Inv G
inst_1 : MeasurableSpace G
inst_2 : MeasurableInv G
s : Set G
hs : MeasurableSet s
⊢ MeasurableSet s⁻¹

Tactic:
measurable_inv hs

Premises used: MeasurableInv.measurable_inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_3
m : MeasurableSpace α
inst : InvolutiveInv α
inst_1 : MeasurableInv α
⊢ MeasurableEmbedding.{u_3, u_3} (α := α) Inv.inv

Tactic:
⟨inv_injective, measurable_inv, fun s hs ↦ s.image_inv_eq_inv ▸ hs.inv⟩

Premises used: MeasurableEmbedding.mk, Eq.rec, MeasurableInv.measurable_inv, MeasurableSet.inv, inv_injective, Eq.symm, Set.image_inv_eq_inv
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace α
inst_2 : CommGroup G
inst_3 : MeasurableMul₂ G
inst_4 : MeasurableInv G
f g : α → G
hf : Measurable f
h : Measurable (f * g)
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Premises used: mul_inv_cancel_comm
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace α
inst_2 : CommGroup G
inst_3 : MeasurableMul₂ G
inst_4 : MeasurableInv G
μ : Measure α
f g : α → G
hf : AEMeasurable f μ
h : AEMeasurable (f * g) μ
⊢ g = f * g * f⁻¹

Tactic:
simp only [mul_inv_cancel_comm]

Premises used: mul_inv_cancel_comm
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace α
inst_2 : CommGroup G
inst_3 : MeasurableMul₂ G
inst_4 : MeasurableInv G
f g : α → G
hf : Measurable f
⊢ Measurable (g * f) ↔ Measurable g

Tactic:
mul_comm g f ▸ Measurable.mul_iff_right hf

Premises used: Measurable.mul_iff_right, Eq.rec, mul_comm, Eq.symm
-- Module: Mathlib.MeasureTheory.Group.Arithmetic
Goal:
α : Type u_1
G : Type u_2
inst : MeasurableSpace G
inst_1 : MeasurableSpace α
inst_2 : CommGroup G
inst_3 : MeasurableMul₂ G
inst_4 : MeasurableInv G
μ : Measure α
f g : α → G
hf : AEMeasurable f μ
⊢ AEMeasurable (g * f) μ ↔ AEMeasurable g μ

Tactic:
mul_comm g f ▸ AEMeasurable.mul_iff_right hf

Premises used: Eq.rec, AEMeasurable.mul_iff_right, mul_comm, Eq.symm
-- 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 : ℤ
ofNat : ∀ (n : ℕ), Measurable (β := G) fun (x : G) ↦ (x, Int.ofNat n).1 ^ (x, Int.ofNat n).2
negSucc : ∀ (n : ℕ), Measurable (β := G) fun (x : G) ↦ (x, Int.negSucc n).1 ^ (x, Int.negSucc n).2
⊢ Measurable (β := G) fun (x : G) ↦ (x, n).1 ^ (x, n).2

Tactic:
rcases n with n | n
-- 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 : ℕ
ofNat : Measurable (β := G) fun (x : G) ↦ x ^ n
⊢ Measurable (β := G) fun (x : G) ↦ (x, Int.ofNat n).1 ^ (x, Int.ofNat n).2

Tactic:
simp_rw [Int.ofNat_eq_natCast, zpow_natCast]

Premises used: zpow_natCast, Int.ofNat_eq_natCast
-- 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

Tactic:
measurable_id.pow_const _

Premises used: measurable_id, 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

Tactic:
exact measurable_id.pow_const _

Premises used: measurable_id, Measurable.pow_const