awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'_1 : a' ∈ s.erase a + t
h' : a' ∈ t
⊢ p a'

Tactic:
h (hr a' h') (hsp a ha)
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'_1 : a' ∈ s.erase a + t
h' : a' ∈ s.erase a
⊢ p a'

Tactic:
exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]

Premises used: Multiset.mem_of_mem_erase
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
rw rw₁ rw₂ :
  (∃ (t : Multiset α) (a : α), (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a
rw₃ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α)
    (h' : a' ∈ s.erase a + t), p a'
inl :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α)
    (h' : a' ∈ s.erase a + t) (h' : a' ∈ s.erase a), p a'
inr :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (ha : a ∈ s) (hsp : ∀ a ∈ s, p a) (a' : α)
    (h' : a' ∈ s.erase a + t) (h' : a' ∈ t), p a'
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Tactic:
classical
  rw [cutExpand_iff]
  rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
  obtain (h' | h') := mem_add.1 h'
  exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]

Premises used: Relation.cutExpand_iff, rfl
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
simp : r a₁ a ∧ r a₂ a
⊢ ∀ (x' : α), Membership.mem (γ := Multiset α) {a₁, a₂} x' → r x' a

Tactic:
simp only [insert_eq_cons, mem_cons, mem_singleton, forall_eq_or_imp, forall_eq]

Premises used: forall_eq, forall_eq_or_imp, Multiset.mem_cons, Multiset.mem_singleton, Multiset.insert_eq_cons
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a a₁ a₂ : α
h₁ : r a₁ a
h₂ : r a₂ a
left : r a₁ a
right : r a₂ a
⊢ r a₁ a ∧ r a₂ a

Tactic:
tauto
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a' a b : α
hr : r a' a
⊢ CutExpand r {a', b} {a, b}

Tactic:
(cutExpand_add_right {b}).2 (cutExpand_singleton_singleton hr)

Premises used: Iff.mpr, Multiset.add, Multiset.cons, Relation.cutExpand_singleton_singleton, List.append, Multiset.ofList, Relation.cutExpand_add_right, Singleton.singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a b' b : α
hr : r b' b
⊢ CutExpand r {a, b'} {a, b}

Tactic:
(cutExpand_add_left {a}).2 (cutExpand_singleton_singleton hr)

Premises used: Iff.mpr, Multiset.add, Relation.cutExpand_add_left, Multiset.cons, Relation.cutExpand_singleton_singleton, List.append, Multiset.ofList, Singleton.singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
a a₁ a₂ b : α
h₁ : r a₁ a
h₂ : r a₂ a
⊢ CutExpand r {a₁, a₂, b} {a, b}

Tactic:
(cutExpand_add_right {b}).2 (cutExpand_double h₁ h₂)

Premises used: Iff.mpr, Multiset.add, Relation.cutExpand_double, Multiset.cons, List.append, Multiset.ofList, Relation.cutExpand_add_right, Singleton.singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0

Tactic:
Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim

Premises used: False.elim, OfNat.ofNat, Relation.not_cutExpand_zero, Acc.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) 0

Tactic:
exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim

Premises used: False.elim, OfNat.ofNat, Relation.not_cutExpand_zero, Acc.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s : Multiset α
ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
cons : Acc (CutExpand r) ({a} + s)
⊢ Acc (CutExpand r) (a ::ₘ s)

Tactic:
rw [← s.singleton_add a]

Premises used: Multiset.singleton_add
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s : Multiset α
ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s
hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}
⊢ Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}

Tactic:
rw [forall_mem_cons] at hs

Premises used: Multiset.forall_mem_cons
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s : Multiset α
ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)

Tactic:
(hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)

Premises used: Relation.cutExpand_fibration, Acc.of_fibration, And.right, And.left, Acc.prod_gameAdd
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
s : Multiset α
ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s
hs : Acc (CutExpand r) {a} ∧ ∀ x ∈ s, Acc (CutExpand r) {x}
⊢ Acc (CutExpand r) ({a} + s)

Tactic:
exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)

Premises used: Relation.cutExpand_fibration, Acc.of_fibration, And.right, And.left, Acc.prod_gameAdd
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
s : Multiset α
hs : ∀ a ∈ s, Acc (CutExpand r) {a}
empty : ∀ (hs : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → Acc (CutExpand r) {a}), Acc (CutExpand r) 0
cons :
  ∀ (a : α) (s : Multiset α) (ihs : ∀ (hs : ∀ a ∈ s, Acc (CutExpand r) {a}), Acc (CutExpand r) s)
    (hs : ∀ a_1 ∈ a ::ₘ s, Acc (CutExpand r) {a_1}), Acc (CutExpand r) (a ::ₘ s)
⊢ Acc (CutExpand r) s

Tactic:
induction s using Multiset.induction with
  | empty => exact Acc.intro 0 fun s h ↦ (not_cutExpand_zero s h).elim
  | cons a s ihs =>
    rw [← s.singleton_add a]
    rw [forall_mem_cons] at hs
    exact (hs.1.prod_gameAdd <| ihs fun a ha ↦ hs.2 a ha).of_fibration _ (cutExpand_fibration r)

Premises used: False.elim, Multiset.cons, OfNat.ofNat, Relation.not_cutExpand_zero, Multiset.forall_mem_cons, Acc.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a : α
hacc : Acc r a
intro :
  ∀ (a : α) (h : ∀ (y : α), r y a → Acc r y) (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), Acc (CutExpand r) {a}
⊢ Acc (CutExpand r) {a}

Tactic:
induction hacc with | _ a h ih
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) {a}

Tactic:
Acc.intro _ fun s ↦ ?_

Premises used: Acc.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
intro : ∀ (s : Multiset α), CutExpand r s {a} → Acc (CutExpand r) s
⊢ Acc (CutExpand r) {a}

Tactic:
refine Acc.intro _ fun s ↦ ?_

Premises used: Acc.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
⊢ CutExpand r s {a} → Acc (CutExpand r) s

Tactic:
simp only [cutExpand_iff, mem_singleton]

Premises used: Multiset.mem_singleton, Relation.cutExpand_iff
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
⊢ Acc (CutExpand r) (erase {a} a + t)

Tactic:
acc_of_singleton fun a' ↦ ?_

Premises used: Relation.acc_of_singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
intro : ∀ a' ∈ erase {a} a + t, Acc (CutExpand r) {a'}
⊢ Acc (CutExpand r) (erase {a} a + t)

Tactic:
refine acc_of_singleton fun a' ↦ ?_

Premises used: Relation.acc_of_singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
intro : a' ∈ t → Acc (CutExpand r) {a'}
⊢ a' ∈ erase {a} a + t → Acc (CutExpand r) {a'}

Tactic:
rw [erase_singleton, zero_add]

Premises used: zero_add, Multiset.erase_singleton
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ t → Acc (CutExpand r) {a'}

Tactic:
ih a' ∘ hr a'

Premises used: Function.comp
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 : α
t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
a' : α
⊢ a' ∈ t → Acc (CutExpand r) {a'}

Tactic:
exact ih a' ∘ hr a'
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Irrefl r
a_1 a : α
h : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}
s : Multiset α
intro : (∃ (t : Multiset α) (a_2 : α), (∀ a' ∈ t, r a' a_2) ∧ a_2 = a ∧ s = erase {a} a_2 + t) → Acc (CutExpand r) s
intro₁ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
    (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), Acc (CutExpand r) (erase {a} a + t)
intro₂ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
    (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), ∀ a' ∈ erase {a} a + t, Acc (CutExpand r) {a'}
intro₃ :
  ∀ (t : Multiset α) (a : α) (hr : ∀ a' ∈ t, r a' a) (h : ∀ (y : α), r y a → Acc r y)
    (ih : ∀ (y : α), r y a → Acc (CutExpand r) {y}), ∀ a' ∈ t, Acc (CutExpand r) {a'}
⊢ CutExpand r s {a} → Acc (CutExpand r) s

Tactic:
classical
  simp only [cutExpand_iff, mem_singleton]
  rintro ⟨t, a, hr, rfl, rfl⟩
  refine acc_of_singleton fun a' ↦ ?_
  rw [erase_singleton, zero_add]
  exact ih a' ∘ hr a'

Premises used: Relation.acc_of_singleton, zero_add, Multiset.erase_singleton, Multiset.mem_singleton, Relation.cutExpand_iff, rfl
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
hr : WellFounded r
⊢ WellFounded (CutExpand r)

Tactic:
⟨have := hr.irrefl; fun _ ↦ acc_of_singleton fun a _ ↦ (hr.apply a).cutExpand⟩

Premises used: WellFounded.apply, WellFounded.irrefl, Acc.cutExpand, Relation.acc_of_singleton, WellFounded.intro
-- Module: Mathlib.Logic.Hydra
Goal:
α : Type u_1
r : α → α → Prop
h : IsWellFounded α r
⊢ IsWellFounded (Multiset α) (CutExpand r)

Tactic:
⟨h.wf.cutExpand⟩

Premises used: WellFounded.cutExpand, IsWellFounded.mk, IsWellFounded.wf
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
α : Type u_3
inst : MeasurableSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableConstSMul G α
c : G
⊢ MeasurableEmbedding (β := α) fun (x : α) ↦ c • x

Tactic:
(smul c).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
α : Type u_3
inst : MeasurableSpace α
inst_1 : Group G
inst_2 : MulAction G α
inst_3 : MeasurableConstSMul G α
c : G
⊢ Eq.{u_3 + 1} (α := α ≃ᵐ α) (symm (smul c)) (smul c⁻¹)

Tactic:
ext rfl

Premises used: MeasurableEquiv.ext, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
α : Type u_3
inst : MeasurableSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : MeasurableConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ Eq.{u_3 + 1} (α := (a : α) → α) (⇑(smul₀ c hc) : (a : α) → α) fun (x : α) ↦ c • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
α : Type u_3
inst : MeasurableSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : MeasurableConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ Eq.{u_3 + 1} (α := α ≃ᵐ α) (symm (smul₀ c hc)) (smul₀ c⁻¹ ⋯)

Tactic:
ext rfl

Premises used: MeasurableEquiv.ext, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
α : Type u_3
inst : MeasurableSpace α
inst_1 : GroupWithZero G₀
inst_2 : MulAction G₀ α
inst_3 : MeasurableConstSMul G₀ α
c : G₀
hc : c ≠ 0
⊢ MeasurableEmbedding (β := α) fun (x : α) ↦ c • x

Tactic:
(smul₀ c hc).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.smul₀
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ Eq (α := (a : G) → G) (⇑(mulLeft g) : (a : G) → G) fun (x : G) ↦ g * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ Eq (α := G ≃ᵐ G) (symm (mulLeft g)) (mulLeft g⁻¹)

Tactic:
ext rfl

Premises used: MeasurableEquiv.ext, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ toEquiv (mulLeft g) = Equiv.mulLeft g

Tactic:
rfl

Premises used: MulAction.toPerm, Equiv.mulLeft, Units.mulLeft, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ g * x

Tactic:
(mulLeft g).measurableEmbedding

Premises used: MeasurableEquiv.mulLeft, MeasurableEquiv.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ x * g

Tactic:
(mulRight g).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.mulRight
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ Eq (α := (a : G) → G) (⇑(mulRight g) : (a : G) → G) fun (x : G) ↦ x * g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ Eq (α := G ≃ᵐ G) (symm (mulRight g)) (mulRight g⁻¹)

Tactic:
ext rfl

Premises used: MeasurableEquiv.ext, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ toEquiv (mulRight g) = Equiv.mulRight g

Tactic:
rfl

Premises used: Units.mulRight, Equiv.mulRight, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ MeasurableEmbedding (β := G₀) fun (x : G₀) ↦ g * x

Tactic:
(mulLeft₀ g hg).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.mulLeft₀
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ Eq (α := (a : G₀) → G₀) (⇑(mulLeft₀ g hg) : (a : G₀) → G₀) fun (x : G₀) ↦ g * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ Eq (α := G₀ ≃ᵐ G₀) (symm (mulLeft₀ g hg)) (mulLeft₀ g⁻¹ ⋯)

Tactic:
ext rfl

Premises used: MeasurableEquiv.ext, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ toEquiv (mulLeft₀ g hg) = Equiv.mulLeft₀ g hg

Tactic:
rfl

Premises used: Equiv.mulLeft₀, MulAction.toPerm, Units.mulLeft, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ MeasurableEmbedding (β := G₀) fun (x : G₀) ↦ x * g

Tactic:
(mulRight₀ g hg).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.mulRight₀
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ Eq (α := (a : G₀) → G₀) (⇑(mulRight₀ g hg) : (a : G₀) → G₀) fun (x : G₀) ↦ x * g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ Eq (α := G₀ ≃ᵐ G₀) (symm (mulRight₀ g hg)) (mulRight₀ g⁻¹ ⋯)

Tactic:
ext rfl

Premises used: MeasurableEquiv.ext, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G₀ : Type u_2
inst : GroupWithZero G₀
inst_1 : MeasurableSpace G₀
inst_2 : MeasurableMul G₀
g : G₀
hg : g ≠ 0
⊢ toEquiv (mulRight₀ g hg) = Equiv.mulRight₀ g hg

Tactic:
rfl

Premises used: Units.mulRight, Equiv.mulRight₀, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_4
inst : MeasurableSpace G
inst_1 : InvolutiveInv G
inst_2 : MeasurableInv G
⊢ Eq (α := G ≃ᵐ G) (symm (inv G)) (inv G)

Tactic:
rfl

Premises used: MeasurableEquiv.inv, Equiv.inv, MeasurableEquiv.symm, Function.Involutive.toPerm, Equiv.symm, rfl
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
g : G
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ x / g

Tactic:
(divRight g).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.divRight
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul G
inst_3 : MeasurableInv G
g : G
⊢ MeasurableEmbedding (β := G) fun (x : G) ↦ g / x

Tactic:
(divLeft g).measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEquiv.divLeft
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
rw :
  Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map
      ((fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ∘ fun (x : A) ↦
        HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x)
      μ)
hg : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x
hf : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x
⊢ Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x) μ))

Tactic:
rw [map_map]

Premises used: MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Eq (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) (g * g')⁻¹ : G) x) μ)
    (map
      ((fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ∘ fun (x : A) ↦
        HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x)
      μ)

Tactic:
simp [Function.comp_def, mul_smul]

Premises used: Function.comp_def, SemigroupAction.mul_smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x

Tactic:
measurable_const_smul ..

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x

Tactic:
exact measurable_const_smul ..

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x

Tactic:
measurable_const_smul ..

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g_1 : G
g g' : Gᵈᵐᵃ
μ : Measure A
⊢ Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g'⁻¹ : G) x

Tactic:
exact measurable_const_smul ..

Premises used: MeasurableConstSMul.measurable_const_smul
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν : Measure A
g : G
μ : Measure A
⊢ map (fun (x : A) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) 1⁻¹ : G) x) μ = μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ ν : Measure A
g_1 : G
g : Gᵈᵐᵃ
⊢ Eq.{u_2 + 1} (α := Measure A)
    (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν_1 : Measure A
g_1 : G
g : Gᵈᵐᵃ
μ ν : Measure A
hf : Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x
⊢ map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) (μ + ν) =
    HAdd.hAdd (α := Measure A)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) μ)
      (map (fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x) ν)

Tactic:
rw [Measure.map_add]

Premises used: MeasureTheory.Measure.map_add
-- Module: Mathlib.MeasureTheory.Group.MeasurableEquiv
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : MulAction G A
inst_2 : MeasurableSpace A
inst_3 : MeasurableConstSMul G A
μ_1 ν_1 : Measure A
g_1 : G
g : Gᵈᵐᵃ
μ ν : Measure A
⊢ Measurable (β := A) fun (x : A) ↦ HSMul.hSMul (α := G) ((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g⁻¹ : G) x

Tactic:
measurable_const_smul ..

Premises used: MeasurableConstSMul.measurable_const_smul