mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, false) :: tl)).sum =
    mk ((PUnit.unit, false) :: tl)

pp: case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, true) :: tl)).sum =
    mk ((PUnit.unit, true) :: tl)

Tactic:
<;>

Goal state after:
case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, false) :: tl)).sum =
    mk ((PUnit.unit, false) :: tl)

case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, true) :: tl)).sum =
    mk ((PUnit.unit, true) :: tl)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)

pp: case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () * mk tl = mk ((PUnit.unit, true) :: tl)

Tactic:
<;>

Goal state after:
case false
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ (of ())⁻¹ * mk tl = mk ((PUnit.unit, false) :: tl)

case true
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
x✝¹ : FreeGroup Unit
L : List (Unit × Bool)
x✝ : Unit × Bool
tl : List (Unit × Bool)
ih : of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) tl).sum = mk tl
⊢ of () * mk tl = mk ((PUnit.unit, true) :: tl)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
⊢ ∏ x ∈ s, f x = f a * f b

case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∉ s
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case zero
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) 0) = 0

pp: case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) ↑i✝) = ↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (↑i✝ + 1)) = ↑i✝ + 1

pp: case pred
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝)) = -↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝ - 1)) = -↑i✝ - 1

Tactic:
<;>

Goal state after:
case zero
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) 0) = 0

case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) ↑i✝) = ↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (↑i✝ + 1)) = ↑i✝ + 1

case pred
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝)) = -↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝ - 1)) = -↑i✝ - 1
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

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

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

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:
<;>

Goal state after:
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

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

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

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
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

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

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)⁻¹

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:
<;>

Goal state after:
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

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

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)⁻¹

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)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ closure ↑(Finset.univ.biUnion fun i ↦ Finset.image (⇑(MonoidHom.mulSingle M i)) (s i)) = Submonoid.pi Set.univ P

Tactic:
Finset.coe_biUnion,

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ closure (⋃ x ∈ ↑Finset.univ, ↑(Finset.image (⇑(MonoidHom.mulSingle M x)) (s x))) = Submonoid.pi Set.univ P
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 : f i = ⊥
hfij : f i = f j
⊢ g ⊥ = 1

Tactic:
hg_bot

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
⊢ 1 = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
<;>

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f) >>= g = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

pp: case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)

Tactic:
<;>

Goal state after:
case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f (k + 1) / f 0 = f k / f 0 * (f (k + 1) / f k)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x ↦ f x >>= g

Tactic:
<;>

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -(pure x >>= f >>= g) = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

pp: case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))

Tactic:
<;>

Goal state after:
case base
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f 0 / f 0 = 1

case step
G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∀ k < n, f 0 / f (k + 1) = f 0 / f k * (f k / f (k + 1))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:

Tactic:
<;>

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ (∏ x ∈ s₂ \ s₁, f x) * ∏ x ∈ s₁, f x = ∏ x ∈ s₂, f x

Tactic:
prod_sdiff h

Goal state after:
ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂, f x = ∏ x ∈ s₂, f x
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
<;>

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
<;>

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : CommMonoid M
a : M
s : Multiset M
ih : IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a
⊢ IsUnit (a ::ₘ s).prod ↔ ∀ a_1 ∈ a ::ₘ s, IsUnit a_1

Tactic:
simpa using fun _ ↦ ih

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

Goal state before:
pp: case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

pp: case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
<;>

Goal state after:
case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
apply commutator_mono

Goal state after:
case a.left.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁

case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.left.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁

pp: case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂

Tactic:
<;>

Goal state after:
case a.left.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁

case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
apply commutator_mono

Goal state after:
case a.right.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁

case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.right.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁

pp: case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂

Tactic:
<;>

Goal state after:
case a.right.h₁
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁

case h₂
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

pp: case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
<;>

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_1.refine_1
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
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ (w * (s₃ * s₂)) • r = (↑w * (r₃ * ↑u)) • r'

pp: case refine_1.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' 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
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ ↑(w * (s₃ * s₂)) * ↑s = ↑w * (r₃ * ↑u) * ↑s'

Tactic:
<;>

Goal state after:
case refine_1.refine_1
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
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ (w * (s₃ * s₂)) • r = (↑w * (r₃ * ↑u)) • r'

case refine_1.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' 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
this : r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s
w : ↥S
hw : ↑w * (r₃ * v) = ↑w * (↑s₃ * ↑s₂)
⊢ ↑(w * (s₃ * s₂)) * ↑s = ↑w * (r₃ * ↑u) * ↑s'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2.refine_1
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' * u') • r₃ = (r' * v) • r₁

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' * u') * ↑s₃ = r' * v * ↑s₁

Tactic:
<;>

Goal state after:
case refine_2.refine_1
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' * u') • r₃ = (r' * v) • r₁

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' * u') * ↑s₃ = r' * v * ↑s₁
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ 0 ≤ f a

Tactic:
rw [← map_zero f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : 0 ≤ a
⊢ f 0 ≤ f a
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ 0

Tactic:
rw [← map_zero f]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ f 0