mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Ioc a b).Nonempty ↔ a < b

Tactic:
by
  rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
ht : t.Nonempty
hst : ¬(s ∩ t).Nonempty
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)

Tactic:
rcases ht with ⟨m, mt⟩

Goal state after:
case neg
α : Type u_2
r : α → α → Prop
s : Set α
f : (Subrel r fun x ↦ x ∈ s) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s
h : s.WellFoundedOn r
t : Set α
hst : ¬(s ∩ t).Nonempty
m : α
mt : m ∈ t
⊢ ∃ m ∈ t, ∀ x ∈ t, ¬(r x m ∧ x ∈ s ∧ m ∈ s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Icc a b

Tactic:
rw [← coe_subset, coe_Ioc, coe_Icc]

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioc a b ⊆ Set.Icc a b
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a

Tactic:
let _ : Preorder α :=
    { le := r
      le_refl := refl_of r
      le_trans := fun _ _ _ => trans_of r }

Goal state after:
α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s)⁻¹ ≤ closure s⁻¹

Tactic:
inv_le,

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s ≤ (closure s⁻¹)⁻¹
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s ⊆ (↑(closure s⁻¹))⁻¹

Tactic:
← Set.inv_subset

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s⁻¹)
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝³ : Monoid M
inst✝² : AddMonoid A
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α M
S : Submonoid M
⊢ 1 • S = S

Tactic:
by
    change S.map _ = S
    simpa only [map_one] using! S.map_id

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ≠ a ∧ a ≤ a✝ ↔ a ≠ a✝ ∧ a ≤ a✝

Tactic:
ne_comm

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ g • a ∈ orbit G (h • a)

Tactic:
simp only [orbit_smul, mem_orbit]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ico a b ∩ Ico c d) = ↑(Ico (max a c) (min b d))

Tactic:
coe_inter,

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ ↑(Ico a b) ∩ ↑(Ico c d) = ↑(Ico (max a c) (min b d))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

Tactic:
by
  refine ⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩
  simpa [reflTransGen_eq_self] using ReflTransGen.lift f h a b <| le_iff_reflTransGen_covBy.mp hab

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * (a * b) = a * (g * b)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
S : Set M
inst✝ : Semigroup M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
g : M
hg : g ∈ S
⊢ g * a * b = a * (g * b)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) * (s * s ^ n) = ↑(closure s)

Tactic:
← mul_assoc,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) * s * s ^ n = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

pp: case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid

Tactic:
· refine
      closure_induction
        (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
        (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx
    rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd * tl.prod) = hd * (a * tl.prod)

pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute

Tactic:
← mul_assoc,

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * hd * tl.prod = hd * (a * tl.prod)

case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_7
inst✝ : CommMonoid M
s : Finset M
⊢ s.toList.prod = ∏ x ∈ s, x

Tactic:
by
  simpa using! s.prod_map_toList id

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S✝ : Type u_4
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Monoid α
inst✝ : MulDistribMulAction α G
S : Subgroup G
⊢ 1 • S = S

Tactic:
by
    change S.map _ = S
    simpa only [map_one] using! S.map_id

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * (g * n) ∈ H

Tactic:
← mul_assoc,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : ∀ (g : G), MulAut.conj g • H = H
n : G
hn : n ∈ H
g : G
⊢ g⁻¹ * g * n ∈ H
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case mk
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
t : Finset α
f : α → β
val✝ : Multiset α
sl : List α
hsl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) sl)
h : Disjoint { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } t
comm : (↑({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪ t)).Pairwise (Commute on f)
⊢ ({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪ t).noncommProd f comm =
    { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }.noncommProd f ⋯ * t.noncommProd f ⋯

Tactic:
rcases t with ⟨⟨tl⟩, htl⟩

Goal state after:
case mk.mk
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
val✝¹ : Multiset α
sl : List α
hsl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) sl)
val✝ : Multiset α
tl : List α
htl : Multiset.Nodup (Quot.mk (⇑(List.isSetoid α)) tl)
h :
  Disjoint { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }
    { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }
comm :
  (↑({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl })).Pairwise
    (Commute on f)
⊢ ({ val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl } ∪
          { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }).noncommProd
      f comm =
    { val := Quot.mk (⇑(List.isSetoid α)) sl, nodup := hsl }.noncommProd f ⋯ *
      { val := Quot.mk (⇑(List.isSetoid α)) tl, nodup := htl }.noncommProd f ⋯
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ (insert i (univ.erase i)).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i

Tactic:
noncommProd_insert_of_notMem _ _ _ _ (notMem_erase _ _),

Goal state after:
case convert_8
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ Pi.mulSingle i (x i) i * (univ.erase i).noncommProd (fun j ↦ Pi.mulSingle j (x j) i) ⋯ = x i
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
hf : ∀ (x : M), c (f x * x) 1
x y : M
h : c x y
⊢ c (f x) (f y)

Tactic:
simp only [← Con.eq, coe_one, coe_mul] at *

Goal state after:
M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
x y : M
hf : ∀ (x : M), ↑(f x) * ↑x = 1
h : ↑x = ↑y
⊢ ↑(f x) = ↑(f y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝² : CommMonoid M
f : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = (∏ x ∈ s with p x ∧ ¬q x, f x) * ∏ x ∈ s with q x ∧ ¬p x, f x

Tactic:
by
  classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
  simp only [Xor]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L * mk (List.replicate n L).flatten = mk (List.replicate (n + 1) L).flatten

Tactic:
mul_mk,

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk (L ++ (List.replicate n L).flatten) = mk (List.replicate (n + 1) L).flatten
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), 1 >>= f >>= g = 1 >>= fun x ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_2
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (x : α✝) (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), of x >>= f >>= g = of x >>= fun x ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_3
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (x : α✝),
    (∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), of x >>= f >>= g = of x >>= fun x ↦ f x >>= g) →
      ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), (of x)⁻¹ >>= f >>= g = (of x)⁻¹ >>= fun x ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_4
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ γ✝ : Type u
x : FreeGroup α✝
⊢ ∀ (x y : FreeGroup α✝),
    (∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x >>= f >>= g = x >>= fun x ↦ f x >>= g) →
      (∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), y >>= f >>= g = y >>= fun x ↦ f x >>= g) →
        ∀ (f : α✝ → FreeGroup β✝) (g : β✝ → FreeGroup γ✝), x * y >>= f >>= g = x * y >>= fun x ↦ f x >>= g

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ (do
      let y ← 1
      pure (f y)) =
    f <$> 1

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_2
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ ∀ (x : α✝),
    (do
        let y ← of x
        pure (f y)) =
      f <$> of x

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_3
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ ∀ (x : α✝),
    (do
          let y ← of x
          pure (f y)) =
        f <$> of x →
      (do
          let y ← (of x)⁻¹
          pure (f y)) =
        f <$> (of x)⁻¹

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refine_4
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ β✝ : Type u
f : α✝ → β✝
x : FreeGroup α✝
⊢ ∀ (x y : FreeGroup α✝),
    (do
          let y ← x
          pure (f y)) =
        f <$> x →
      (do
            let y ← y
            pure (f y)) =
          f <$> y →
        (do
            let y ← x * y
            pure (f y)) =
          f <$> (x * y)

Tactic:
simp +instances +contextual [instMonad]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * (f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s) =
    f a ^ count a (a :: s) * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
← mul_assoc,

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a ^ count a (a :: s) * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * (f a * b₂) = (f a * ∏ a ∈ s.erase a, f a) * b₂

Tactic:
← mul_assoc,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s.erase a, f a) * f a * b₂ = (f a * ∏ a ∈ s.erase a, f a) * b₂
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : (_root_.Disjoint on f) i j
hfij : f i = f j
⊢ g (f i) = 1

Tactic:
rw [Function.onFun, ← hfij, disjoint_self] at hdisj

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝³ : CommMonoid M
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
i j : κ
hdisj : f i = ⊥
hfij : f i = f j
⊢ g (f i) = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
⊢ (lift (g ∘ f)) 0 = (lift g) ((map f) 0)

Tactic:
simp only [map_zero]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}

Tactic:
have h₂ :
    (∑ x ∈ s.toFinset, k • (count x s / k) • ({x} : Multiset ι)) =
      ∑ x ∈ s.toFinset, count x s • {x} := by
    apply Finset.sum_congr rfl
    intro x hx
    rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]

Goal state after:
case h
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
h₂ : ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}
⊢ s = k • ∑ a ∈ s.toFinset, (count a s / k) • {a}
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ (lift fun x₂ ↦ of (1 * x₂)) (x1 + x2) = x1 + x2

Tactic:
map_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ (lift fun x₂ ↦ of (1 * x₂)) x1 + (lift fun x₂ ↦ of (1 * x₂)) x2 = x1 + x2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₁ ↦ of (x₁ * 1)) x1 = x1
ih2 : (lift fun x₁ ↦ of (x₁ * 1)) x2 = x2
⊢ (lift fun x₁ ↦ of (x₁ * 1)) (x1 + x2) = x1 + x2

Tactic:
map_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₁ ↦ of (x₁ * 1)) x1 = x1
ih2 : (lift fun x₁ ↦ of (x₁ * 1)) x2 = x2
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x1 + (lift fun x₁ ↦ of (x₁ * 1)) x2 = x1 + x2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1 + x * y2) = (lift ⇑f) x * (lift ⇑f) (y1 + y2)

Tactic:
map_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1) + (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) (y1 + y2)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1) + (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) (y1 + y2)

Tactic:
map_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1) + (lift ⇑f) (x * y2) = (lift ⇑f) x * ((lift ⇑f) y1 + (lift ⇑f) y2)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = ↑s₃ * (r₂ * ↑s')

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = ↑s₃ * r₂ * ↑s'
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: case H
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ (monoidOf ⊤).mk' ↑y✝.2 ⟨y✝.1, ⋯⟩ * (monoidOf ⊤).mk' y✝.1 y✝.2 = 1

Tactic:
← Submonoid.LocalizationMap.mk'_mul

Goal state after:
case H
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ (monoidOf ⊤).mk' (↑y✝.2 * y✝.1) (⟨y✝.1, ⋯⟩ * y✝.2) = 1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * (v' * ↑s₂) = r' * (v * ↑s₁)

Tactic:
← mul_assoc,

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : ↑u • r₂ = v • r₁
hs₁u : ↑u * ↑s₂ = v * ↑s₁
u' : ↥S
v' : R
hur₂ : ↑u' • r₃ = v' • r₂
hs₂u : ↑u' * ↑s₃ = v' * ↑s₂
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ↑s' * v' * ↑s₂ = r' * (v * ↑s₁)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 =
    g ↑(f.sec (x * y)).2 *
      (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹ *
        (g (f.sec y).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec y).2)⁻¹))

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 =
    g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹) *
      (g (f.sec y).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec y).2)⁻¹)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 =
    g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹) *
      (g (f.sec y).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec y).2)⁻¹)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 =
    g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹) * g (f.sec y).1 *
      ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec y).2)⁻¹
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 =
    g (f.sec y).1 * g ↑(f.sec (x * y)).2 * (g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹)

Tactic:
← mul_assoc,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x y : N
⊢ g (f.sec (x * y)).1 * g ↑(f.sec y).2 =
    g (f.sec y).1 * g ↑(f.sec (x * y)).2 * g (f.sec x).1 * ↑((IsUnit.liftRight (g.domRestrict S) hg) (f.sec x).2)⁻¹