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

Goal state before:
pp: α : Type u
x : FreeGroup α
⊢ (map _root_.id) x = x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
⊢ (map g) ((map f) x) = (map (g ∘ f)) x

Tactic:
by

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∀ x ∈ s₁ ∩ s₂, f x = g x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : FreeGroup α →* FreeGroup β
hg : ∀ (x : α), g (FreeGroup.of x) = FreeGroup.of (f x)
⊢ ∀ {x : FreeGroup α}, g x = (map f) x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ map f = lift (of ∘ f)

Tactic:
by

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

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
⊢ ∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ (map f).range = Subgroup.closure (of '' Set.range f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Surjective f
⊢ Function.Surjective ⇑(map f)

Tactic:
by

Goal state after:
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
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ s' ⊆ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Injective f
⊢ Function.Injective ⇑(map f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Bijective f
⊢ Function.Bijective ⇑(map f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Bijective f
⊢ Function.Bijective ⇑(map f)

Tactic:
by
  exact ⟨map_injective hf.injective, map_surjective hf.surjective⟩

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

Goal state before:
pp: α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.38
β : Type ?u.39
e : α ≃ β
x : FreeGroup α
⊢ (map ⇑e.symm) ((map ⇑e) x) = x

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
L L₁ L₂ L₃ L₄ : List (α✝ × Bool)
β✝ : Type v
f : α✝ → β✝
x✝ y : FreeGroup α✝
α : Type ?u.38
β : Type ?u.39
e : α ≃ β
x : FreeGroup β
⊢ (map ⇑e) ((map ⇑e.symm) x) = x

Tactic:
by

Goal state after:
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
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
⊢ ∀ c ∈ s, c ∉ s' → f c = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), (prod.comp (map f)) (of x) = f x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (lift f) x = prod ((map f) x)

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : FreeGroup Unit
⊢ FreeGroup ℤ

Tactic:
by

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

Goal state before:
pp: α : 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
b : Bool
⊢ of () ^ (List.map ((fun x ↦ bif x.2 then x.1 else -x.1) ∘ fun x ↦ (1, x.2)) ((PUnit.unit, b) :: tl)).sum =
    mk ((PUnit.unit, b) :: tl)

Tactic:
by

Goal state after:
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
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ Function.LeftInverse (fun x ↦ of () ^ x) fun x ↦ ((map fun x ↦ 1) x).sum

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) 0) = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) ↑i) = ↑i
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (↑i + 1)) = ↑i + 1

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
i : ℕ
ih : (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (-↑i)) = -↑i
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) (-↑i - 1)) = -↑i - 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x✝ : FreeGroup α
⊢ (⇑equivIntOfUnique.symm ∘ ⇑Multiplicative.toAdd) ((⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x✝ : Multiplicative ℤ
⊢ (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) ((⇑equivIntOfUnique.symm ∘ ⇑Multiplicative.toAdd) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x✝¹ x✝ : FreeGroup α
⊢ (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) (x✝¹ * x✝) =
    (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) x✝¹ * (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) x✝

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x y : FreeAddGroup α
⊢ FreeAddGroup.sum ((FreeAddGroup.map 1) (x + y)) =
    FreeAddGroup.sum ((FreeAddGroup.map 1) x) + FreeAddGroup.sum ((FreeAddGroup.map 1) y)

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ : FreeGroup α✝
x : α✝
ih : id <$> of x = of x
⊢ id <$> (of x)⁻¹ = (of x)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x * y) = x * y

Tactic:
by

Goal state after:
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
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
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
by

Goal state after:
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 : ι → Prop
inst✝ : DecidablePred p
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s with p x, f x

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 : ι → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
s : Finset { x // p x }
f : { x // p x } → M
g : ι → M
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ map (Embedding.subtype fun x ↦ p x) s, g x = ∏ x ∈ s, f x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
F : Fintype (Subtype p)
s : Finset ι
h : ∀ (x : ι), x ∈ s ↔ p x
f : ι → M
⊢ p = fun x ↦ x ∈ s

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
p : ι → Prop
F : Fintype (Subtype p)
s : Finset ι
h : ∀ (x : ι), x ∈ s ↔ p x
f : ι → M
⊢ ∏ a ∈ s, f a = ∏ a, f ↑a

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∀ x ∈ univ, x ∉ s.toFinset → f x = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∀ (x : ι), x ∈ s.toFinset ↔ x ∈ s

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∏ i, f i = ∏ i, g i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ↥s → M
⊢ ∏ x, f x = ∏ x ∈ s, extend Subtype.val f 1 x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
a : ι
ha : a ∈ {x ∈ s | f x ≠ 1}
⊢ f a ≠ 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : g b ≠ 1
H : g b = 1
⊢ False

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
⊢ N = ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : N = ⊤
⊢ ∀ (x x_1 : G), x_1⁻¹ * x ∈ N

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ leftRel N = ⊤ ↔ N = ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
⊢ N = ⊤

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
h : N = ⊤
⊢ ∀ (x x_1 : G), x * x_1⁻¹ ∈ N

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ rightRel N = ⊤ ↔ N = ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ Subsingleton (G ⧸ N) ↔ N = ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ Nontrivial (G ⧸ N) ↔ N ≠ ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : a⁻¹ * b ∈ N
hcd : c⁻¹ * d ∈ N
⊢ c⁻¹ * (a⁻¹ * b) * c⁻¹⁻¹ * (c⁻¹ * d) = (a * c)⁻¹ * (b * d)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
a b c d : G
hab : (leftRel N) a b
hcd : (leftRel N) c d
⊢ (leftRel N) (a * c) (b * d)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P : Submonoid M
x✝ : ∃ S, closure S = P ∧ S.Finite
S : Set M
hS : closure S = P
hf : S.Finite
⊢ closure ↑hf.toFinset = P

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P : Submonoid M
h : P.FG
S : Set M
hS : closure S = P
hf : S.Finite
⊢ AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S) = toAddSubmonoid P

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P : Submonoid M
h : (toAddSubmonoid P).FG
T : Set (Additive M)
hT : AddSubmonoid.closure T = toAddSubmonoid P
hf : T.Finite
⊢ closure (⇑Additive.ofMul ⁻¹' T) = P

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
P : AddSubmonoid M
⊢ P.FG ↔ (toSubmonoid P).FG

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ closure ↑∅ = ⊥

Tactic:
by

Goal state after:
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
h : ∏ x ∈ s, f x ≠ 1
⊢ ∃ a ∈ s, f a ≠ 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ range (n + 1), f x = f n * ∏ x ∈ range n, f x

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ k ∈ range (n + 1 + 1), f k = (∏ k ∈ range (n + 1), f (k + 1)) * f 0

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
n : ℕ
hn : N ≤ n
⊢ ∏ k ∈ range n, u k = ∏ k ∈ range N, u k

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s t : Finset M
⊢ closure ↑(s ∪ t) = closure ↑s ⊔ closure ↑t

Tactic:
by

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

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
f : G →* M
⊢ QuotientGroup.con f.ker = Con.ker f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ x⁻¹ * y ∈ N ↔ ∃ z ∈ N, x * z = y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
ι : Type u_3
s : Finset ι
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
ι : Type u_3
s : Set ι
hs : s.Finite
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ ∀ i ∈ hs.toFinset, (P i).FG

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
ι : Type u_3
s : Set ι
hs : s.Finite
P : ι → Submonoid M
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
ι : Sort u_3
inst✝ : Finite ι
P : ι → Submonoid M
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x : G
⊢ ↑x = 1 ↔ x ∈ N

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
⊢ (mk' N).comp N.subtype = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : MulOneClass I
f : G →* H
inst✝ : f.range.Normal
g : H →* I
h : (mk' f.range).comp g.ker.subtype = 1
x : H
hx : x ∈ g.ker
⊢ ↑x = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n m : ℕ
⊢ ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

Tactic:
by

Goal state after:
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)
inst✝ : DecidableEq ι
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = pi Set.univ P

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 1, f k = f 0

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ ↑x = ↑y ↔ x / y ∈ N

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
⊢ Subgroup.map (mk' N) N = ⊥

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
c : Con G
a✝ b✝ : G
hx : a✝ ∈ {x | c x 1}
hy : b✝ ∈ {x | c x 1}
⊢ a✝ * b✝ ∈ {x | c x 1}

Tactic:
by

Goal state after:
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)
hP : ∀ (i : ι), (P i).FG
⊢ (Submonoid.pi Set.univ P).FG

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
I : Type u_3
M : Type u_4
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
c : Con G
x✝ : G
h : x✝ ∈ {x | c x 1}
⊢ x✝⁻¹ ∈ {x | c x 1}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure ↑Finset.univ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
⊢ FG M

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (⇑e) s) = Submonoid.map e (closure ↑s)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
h : P.FG
e : M →* M'
⊢ (Submonoid.map e P).FG

Tactic:
by

Goal state after: