awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf u) : ℝ))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
hsG : ∀ (g : ↥G), g +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
have rw : HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
    (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
Tactic: rw [(isAddFundamentalDomain_of_ae_ball I u x hu hI).measure_eq_card_smul_of_vadd_ae_eq_self s hsG,
    ← Nat.card_zmultiples u]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hI : I =ᶠ[ae (F := Measure (AddCircle T)) volume] ball x (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf u) : ℝ))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
hsG : ∀ (g : ↥G), g +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
rw :
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
      (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
⊢ (volume : (a : Set (AddCircle T)) → ℝ≥0∞) s =
    HSMul.hSMul (β := ℝ≥0∞) (addOrderOf u) ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
have rw₁ : HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
    (((volume : Measure (AddCircle T)) : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞) =
  HSMul.hSMul (β := ℝ≥0∞) (Nat.card ↥(AddSubgroup.zmultiples u))
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I) : ℝ≥0∞)
Tactic: rw [(isAddFundamentalDomain_of_ae_ball I u x hu hI).measure_eq_card_smul_of_vadd_ae_eq_self s hsG,
    ← Nat.card_zmultiples u]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
β : Type u_4
inst : MeasurableSpace M
inst_1 : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst_2 : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable.{u_3, u_2} (β := M) fun (a : α) ↦ (f a * g a) (h a)
have dsimp : Measurable.{u_3, u_2} (β := M) fun (a : α) ↦ f a (h a) * g a (h a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
G : Type u_2
inst : DivInvMonoid G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ Measurable (β := G) fun (h : G) ↦ h / g
have simp_rw : Measurable (β := G) fun (h : G) ↦ h * g⁻¹
Tactic: simp_rw [div_eq_mul_inv, measurable_mul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 + 1).1 ^ (x, n + 1).2
have succ : Measurable (β := M) fun (x : M) ↦ x ^ n * x
Tactic: simp only [pow_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
n : ℕ
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2
have zero : Measurable (β := M) fun (x : M) ↦ HPow.hPow (β := ℕ) (x, 0).1 (x, 0).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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).1 ^ (x, n).2
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 / g a) (h a)
have dsimp : Measurable.{u_3, u_2} (β := G) fun (a : α) ↦ f a (h a) / g a (h a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ MeasurableEq E
have measurableSet_diagonal : MeasurableSet (Set.diagonal E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 (Set.diagonal E)
have measurableSet_diagonal : MeasurableSet.{u_5} (α := E × E) {p : E × E | p.1 - p.2 = 0}
Tactic: simp_rw +singlePass [Set.diagonal, ← sub_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 β
⊢ MeasurableEq β
have measurableSet_diagonal : MeasurableSet (Set.diagonal β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 (Set.diagonal β)
have measurableSet_diagonal : MeasurableSet.{u_5} (α := β × β) {p : β × β | p.1 - p.2 = 0 ∧ p.2 - p.1 = 0}
Tactic: simp_rw [Set.diagonal, le_antisymm_iff, ← tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
have h : Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ c / x) fun (x : G) ↦ c * x⁻¹
Tactic: convert! measurable_inv.const_mul c using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ c / x) fun (x : G) ↦ c * x⁻¹
have h : ∀ (x : G), c / x = c * x⁻¹
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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) ↦ x / c
have h : Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ x / c) fun (x : G) ↦ id x * c⁻¹
Tactic: convert! measurable_id.mul_const c⁻¹ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ Eq.{u_2 + 1} (α := G → G) (fun (x : G) ↦ x / c) fun (x : G) ↦ id x * c⁻¹
have h : ∀ (x : G), x / c = id x * c⁻¹
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 ^ (x, n).2
have ofNat : ∀ (n : ℕ), Measurable (β := G) fun (x : G) ↦ (x, Int.ofNat n).1 ^ (x, Int.ofNat n).2
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ Measurable (β := G) fun (x : G) ↦ (x, n).1 ^ (x, n).2
have negSucc : ∀ (n : ℕ), Measurable (β := G) fun (x : G) ↦ (x, Int.negSucc n).1 ^ (x, Int.negSucc n).2
Tactic: rcases n with n | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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, Int.ofNat n).1 ^ (x, Int.ofNat n).2
have ofNat : Measurable (β := G) fun (x : G) ↦ x ^ n
Tactic: simp_rw [Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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, Int.negSucc n).1 ^ (x, Int.negSucc n).2
have negSucc : Measurable (β := G) fun (x : G) ↦ (x ^ (n + 1))⁻¹
Tactic: simp_rw [zpow_negSucc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
have simp : Measurable (β := G) fun (p : G × G) ↦ p.1 * p.2⁻¹
Tactic: simp only [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 • g a) (h a)
have dsimp : Measurable.{u_4, u_3} (β := X) fun (a : α) ↦ f a (h a) • g a (h a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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.{u_6, u_6} (α := ℕ × M) (β := M) (Function.uncurry fun (x1 : ℕ) (x2 : M) ↦ x1 • x2)
have suffices : Measurable (β := M) fun (p : M × ℕ) ↦ p.2 • p.1
Tactic: suffices Measurable fun p : M × ℕ => p.2 • p.1 by apply this.comp measurable_swap
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
have refine : ∀ (n : ℕ), Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
Tactic: refine measurable_from_prod_countable_left fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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) ↦ (x, n + 1).2 • (x, n + 1).1
have succ : Measurable (β := M) fun (x : M) ↦ n • x + x
Tactic: simp only [succ_nsmul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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 : ℕ
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
have zero : Measurable (β := M) fun (x : M) ↦ HSMul.hSMul (α := ℕ) (x, 0).2 (x, 0).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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
have 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
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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.{u_6, u_6} (α := ℤ × M) (β := M) (Function.uncurry fun (x1 : ℤ) (x2 : M) ↦ x1 • x2)
have suffices : Measurable (β := M) fun (p : M × ℤ) ↦ p.2 • p.1
Tactic: suffices Measurable fun p : M × ℤ => p.2 • p.1 by apply this.comp measurable_swap
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
have refine : ∀ (n : ℤ), Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
Tactic: refine measurable_from_prod_countable_left fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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) ↦ (x, Int.ofNat n).2 • (x, Int.ofNat n).1
have ofNat : Measurable (β := M) fun (x : M) ↦ n • x
Tactic: simp only [Int.ofNat_eq_natCast, natCast_zsmul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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) ↦ (x, Int.negSucc n).2 • (x, Int.negSucc n).1
have negSucc : Measurable (β := M) fun (x : M) ↦ -((n + 1) • x)
Tactic: simp only [negSucc_zsmul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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) ↦ (x, n).2 • (x, n).1
have ofNat : ∀ (n : ℕ), Measurable (β := M) fun (x : M) ↦ (x, Int.ofNat n).2 • (x, Int.ofNat 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
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
⊢ Measurable (β := M) fun (x : M) ↦ (x, n).2 • (x, n).1
have negSucc : ∀ (n : ℕ), Measurable (β := M) fun (x : M) ↦ (x, Int.negSucc n).2 • (x, Int.negSucc 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
α_1 : Type u_1
M : Type u_2
α : Type u_3
inst : MeasurableSpace M
inst_1 : MeasurableSpace α
inst_2 : SMul M α
inst_3 : SMul.{u_2, u_3} Mᵐᵒᵖ α
inst_4 : IsCentralScalar M α
inst_5 : MeasurableSMul₂ M α
⊢ Measurable (β := α) fun (x : Prod.{u_2, u_3} Mᵐᵒᵖ α) ↦ MulOpposite.op (unop x.1) • x.2
have simp_rw : Measurable (β := α) fun (x : Prod.{u_2, u_3} Mᵐᵒᵖ α) ↦ unop x.1 • x.2
Tactic: simp_rw [op_smul_eq_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (hypothesis)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod
hl : ∀ f_1 ∈ f :: l, Measurable f_1
⊢ Measurable (f :: l).prod
have hl₁ : Measurable f ∧ ∀ x ∈ l, Measurable x
Tactic: rw [List.forall_mem_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod
hl : Measurable f ∧ ∀ x ∈ l, Measurable x
⊢ Measurable (f :: l).prod
have cons : Measurable (f * l.prod)
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
⊢ Measurable l.prod
have nil : ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → Measurable f),
  Measurable.{u_3, u_2} (α := α) (β := M) (prod [])
Tactic: induction l with
  | nil => exact measurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
l : List (α → M)
hl : ∀ f ∈ l, Measurable f
nil :
  ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → Measurable f),
    Measurable.{u_3, u_2} (α := α) (β := M) (prod [])
⊢ Measurable l.prod
have cons : ∀ (f : α → M) (l : List (α → M)) (ihl : ∀ (hl : ∀ f ∈ l, Measurable f), Measurable l.prod)
  (hl : ∀ f_1 ∈ f :: l, Measurable f_1), Measurable (f :: l).prod
Tactic: induction l with
  | nil => exact measurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (hypothesis)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ
hl : ∀ f_1 ∈ f :: l, AEMeasurable f_1 μ
⊢ AEMeasurable (f :: l).prod μ
have hl₁ : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
Tactic: rw [List.forall_mem_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
f : α → M
l : List (α → M)
ihl : ∀ (hl : ∀ f ∈ l, AEMeasurable f μ), AEMeasurable l.prod μ
hl : AEMeasurable f μ ∧ ∀ x ∈ l, AEMeasurable x μ
⊢ AEMeasurable (f :: l).prod μ
have cons : AEMeasurable (f * l.prod) μ
Tactic: rw [List.prod_cons]
-- Lean 4 proof step from Mathlib.MeasureTheory.Group.Arithmetic (goal)
Goal:
M : Type u_2
α : Type u_3
inst : Monoid M
inst_1 : MeasurableSpace M
inst_2 : MeasurableMul₂ M
m : MeasurableSpace α
μ : Measure α
l : List (α → M)
hl : ∀ f ∈ l, AEMeasurable f μ
⊢ AEMeasurable l.prod μ
have nil : ∀ (hl : ∀ (f : α → M), Membership.mem (γ := List (α → M)) [] f → AEMeasurable f μ),
  AEMeasurable.{u_3, u_2} (β := M) (prod []) μ
Tactic: induction l with
  | nil => exact aemeasurable_one
  | cons f l ihl =>
    rw [List.forall_mem_cons] at hl
    rw [List.prod_cons]
    exact hl.1.mul (ihl hl.2)
Cleared hypotheses: l, hl