mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : ι → κ
he : Set.InjOn e ↑s
hest : Set.MapsTo e ↑s ↑t
h' : ∀ i ∈ t, i ∉ e '' ↑s → g i = 1
h : ∀ i ∈ s, f i = g (e i)
⊢ ∏ i ∈ s, f i = ∏ j ∈ t, g j

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
w✝ x✝ y✝ z✝ : M
h1 : (Setoid.ker ⇑f) w✝ x✝
h2 : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ * y✝) (x✝ * z✝)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
w✝ x✝ y✝ z✝ : N
h₁ : (c.mapOfSurjective (⇑f) h hf) w✝ x✝
h₂ : (c.mapOfSurjective (⇑f) h hf) y✝ z✝
⊢ (c.mapOfSurjective (⇑f) h hf) (w✝ * y✝) (x✝ * z✝)

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
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s with g i ∈ t, f i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = mapOfSurjective f h hf

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : { d // c ≤ d }
⊢ ker c.mkMulHom ≤ ↑d

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
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
j : κ
x✝ : j ∈ t
i : ι
hi : i ∈ {i ∈ s | g i = j}
⊢ f j = f (g i)

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
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s with g i ∈ t, f (g i)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : c.Quotient
⊢ ((fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯) ((fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩) d)) x y ↔ d x y

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
s t : { d // c ≤ d }
⊢ { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        s ≤
      { toFun := fun d ↦ mapOfSurjective c.mkMulHom ⋯ ⋯, invFun := fun d ↦ ⟨comap toQuotient ⋯ d, ⋯⟩, left_inv := ⋯,
          right_inv := ⋯ }
        t ↔
    s ≤ t

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x y : M
f : M →* P
H : c ≤ ker f
⊢ Con.liftOn 1 ⇑f ⋯ = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ Con.liftOn (↑m * ↑n) ⇑f ⋯ = Con.liftOn ↑m ⇑f ⋯ * Con.liftOn ↑n ⇑f ⋯

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 κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
⊢ (c.lift f H).comp c.mk' = f

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 κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
x✝ : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
⊢ f y = f (g x)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
⊢ c.lift (f.comp c.mk') ⋯ = f

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹

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 κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
⊢ ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (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
inst✝ : CommMonoid M
s : Finset ι
f : ι × ι → M
⊢ ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (leftRel s) a b = (a⁻¹ * b ∈ s)

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((leftRel s) 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
s : Finset ι
inst✝ : CommMonoid M
f g : ι → M
⊢ ∏ x ∈ s, f x * g x = fold (fun x1 x2 ↦ x1 * x2) (1 * 1) (fun x ↦ f x * g x) s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f g : c.Quotient →* P
h : f.comp c.mk' = g.comp c.mk'
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
H : Step L₁ L₂
⊢ L₂ <+ L₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), (rightRel s) a b = (b * a⁻¹ ∈ s)

Tactic:
by

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

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((rightRel s) 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
s : Finset ι
inst✝ : CommMonoid M
f g h i : ι → M
⊢ (∏ a ∈ s, f a * g a) * ∏ a ∈ s, h a * i a = (∏ a ∈ s, f a * h a) * ∏ a ∈ s, g a * i a

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, L₁.length = L₂.length + 2 * n

Tactic:
by

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

Goal state before:
pp: α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflGen Red.Step b b

Tactic:
by

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

Goal state before:
pp: α : Type u
x✝ b✝ c b : List (α × Bool)
hab hac : Red.Step x✝ b
⊢ ReflTransGen Red.Step b b

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red.Step L₁ L₂
⊢ Join Red L₁ L₂

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : b * a⁻¹ ∈ s
⊢ (b * a⁻¹)⁻¹ = a⁻¹⁻¹ * b⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : IsReduced L₁
step : Red.Step L₁ L₂
⊢ False

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
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
h₁ : x ∈ s
h₂ : ¬f x = 1
⊢ p x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (rightRel s) a b → (leftRel s) a⁻¹ 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
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → x ∉ {x ∈ s | p x} → 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
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ f a = if p a then f a else 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : a⁻¹ * b ∈ s
⊢ (a⁻¹ * b)⁻¹ = b⁻¹ * a⁻¹⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ IsReduced ((a₁, b₁) :: (a₂, b₂) :: L₁)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b → (rightRel s) a⁻¹ b⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ : List (α × Bool)
⊢ (invRev L₁).length = L₁.length

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ : List (α × Bool)
⊢ invRev (invRev L₁) = L₁

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
⊢ invRev (L₁ ++ L₂) = invRev L₂ ++ invRev L₁

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ (rightRel s) ((fun g ↦ g⁻¹) ((fun g ↦ g⁻¹) g)) g

Tactic:
by

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
a : α × Bool
⊢ invRev (a :: L) = invRev L ++ invRev [a]

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ (leftRel s) ((fun g ↦ g⁻¹) ((fun g ↦ g⁻¹) g)) 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
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ ¬p x

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
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
⊢ (∏ a ∈ s with p a, if p a then f a else 1) = ∏ a ∈ s, if p a then f a else 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ (leftRel s) a b ↔ a⁻¹ * b ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ ⦃a b : List (α × Bool)⦄, Red.Step a b → Red.Step (invRev a) (invRev b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out ↑g = g * ↑⟨g⁻¹ * Quotient.out ↑g, ⋯⟩

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Step L₁ L₂
⊢ Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
b a : α
hb : b ∈ s
⊢ ↑(a * b) = ↑a

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂)
⊢ Step L₁ L₂

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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = ∏ x ∈ {a}, 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
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = f a

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red (invRev L₁) (invRev L₂)
⊢ Red L₁ L₂

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 : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h₁ : a ∉ s → f a = 1
this✝ : DecidableEq ι
this : a ∉ s
b : ι
hb : b ∈ s
⊢ b ≠ a

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a b c : FreeGroup α), a * b * c = a * (b * c)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1 ∈ s, x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * 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)
⊢ ∀ (a : FreeGroup α), 1 * a = a

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a * 1 = a

Tactic:
by

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

Goal state before:
pp: α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (Quot.mk Red.Step tl)⁻¹ * Quot.mk Red.Step tl = 1
x : α
b : Bool
⊢ Red.Step (invRev ((x, b) :: tl) ++ (x, b) :: tl) (invRev tl ++ tl)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1 ∈ N, x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N

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 : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
by

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
⊢ ∀ (a : FreeGroup α), a⁻¹ * a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' mk '' s = ⋃ x, (fun x_1 ↦ x_1 * ↑x) ⁻¹' s

Tactic:
by

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

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

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✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∉ s
⊢ ∀ b ∈ s, f b = 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✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' mk '' s = ⋃ x, (fun x_1 ↦ x_1 * ↑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
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
⊢ ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a

Tactic:
by

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = g (of x)⁻¹

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' mk '' s = s * ↑N

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₁ \ s₂, a ∉ s₁ ∩ s₂ → f a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
⊢ mk ⁻¹' {↑1} = ↑N

Tactic:
by

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
⊢ f = g

Tactic:
by

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

Goal state before:
pp: α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
H : Step L₁ L₂
⊢ Lift.aux f L₁ = Lift.aux f L₂

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
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ ∀ (a b : FreeGroup α), Quot.lift (Lift.aux f) ⋯ (a * b) = Quot.lift (Lift.aux f) ⋯ a * Quot.lift (Lift.aux 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)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) = f

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
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
⊢ (fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g) = g

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : α
⊢ (lift 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 : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ (lift f) (Quot.mk Red.Step ((x, false) :: tl)) ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
x✝ : α × Bool
tl : List (α × Bool)
ih : (lift f) (Quot.mk Red.Step tl) ∈ s
x : α
b : Bool
⊢ (lift f) (Quot.mk Red.Step ((x, true) :: tl)) ∈ s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
⊢ (lift f).range ≤ s

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₂ \ s₁, a ∉ s₂ ∩ s₁ → g a = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
a : α
⊢ (lift f) (of a) = f a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ (lift f).range = Subgroup.closure (Set.range f)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ Function.Surjective ⇑(lift f) ↔ Subgroup.closure (Set.range f) = ⊤

Tactic:
by

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

Goal state before:
pp: β : Type v
inst✝ : Group β
s : Set β
⊢ Subgroup.closure s = (lift Subtype.val).range

Tactic:
by

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

Goal state before:
pp: α : Type u_1
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
by

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

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

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 α
L₁ L₂ : List (α × Bool)
H : Red.Step L₁ L₂
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) L₁) (List.map (fun x ↦ (f x.1, x.2)) L₂)

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 α
⊢ ∀ (a b : FreeGroup α),
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (a * b) =
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ a * Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ b

Tactic:
by

Goal state after: