mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ (↑x * ↑y = 1) = (↑x' * ↑y' = 1)

pp: case refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯

Tactic:
·

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ (↑x * ↑y = 1) = (↑x' * ↑y' = 1)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂

Tactic:
·

Goal state after:
case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr.inl
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)

pp: case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
·

Goal state after:
case mpr.inl
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
⊢ ∀ (a : ↑x * ↑y = 1) (a' : ↑x' * ↑y' = 1), a ≍ a' → (fun hyx ↦ f x y ⋯ ⋯) ≍ fun hyx ↦ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂

Tactic:
·

Goal state after:
case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2.refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x = 1) = (↑y' * ↑x' = 1)

pp: case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
·

Goal state after:
case refine_2.refine_1
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ (↑y * ↑x = 1) = (↑y' * ↑x' = 1)
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯

Tactic:
·

Goal state after:
case refine_2.refine_2
M : Type u_1
N : Type u_2
P : Type u_3
α : Type u_4
inst✝ : Monoid M
c : Con M
u : c.Quotientˣ
f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α
Hf :
  ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1) (hyx' : c (y' * x') 1),
    c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'
x y x' y' : M
hx : c x x'
hy : c y y'
Hxy : ↑x * ↑y = 1
Hxy' : ↑x' * ↑y' = 1
⊢ ∀ (a : ↑y * ↑x = 1) (a' : ↑y' * ↑x' = 1), a ≍ a' → f x y ⋯ ⋯ ≍ f x' y' ⋯ ⋯
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x3 : α
b3 : Bool
x4 : α
b4 : Bool
tl x✝⁵ x✝⁴ : List (α × Bool)
x✝³ : α
x✝² : Bool
x✝¹ : α
x✝ : Bool
H : (x3, b3) :: (x4, b4) :: tl ++ (x✝³, x✝²) :: (x✝³, !x✝²) :: x✝⁵ = [] ++ (x✝¹, x✝) :: (x✝¹, !x✝) :: x✝⁴
⊢ (x3, b3) :: (x4, b4) :: tl ++ x✝⁵ = [] ++ x✝⁴ ∨
    ∃ L₅, Step ((x3, b3) :: (x4, b4) :: tl ++ x✝⁵) L₅ ∧ Step ([] ++ x✝⁴) L₅

Tactic:
injections; subst_vars; right; simpa using ⟨_, Red.Step.cons_not, Red.Step.not⟩

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

Goal state before:
pp: case head.inl
α : Type u
LL₁ L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h₁₂ : Step L₁ L
h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = (a, b) :: L → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red L₁ L₂

pp: case head.inr
α : Type u
LL₁ c✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: c✝) L₂

Tactic:
·

Goal state after:
case head.inl
α : Type u
LL₁ L₁ L₂ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h₁₂ : Step L₁ L
h : ReflTransGen Step ((a, b) :: L) ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = (a, b) :: L → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red L₁ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case head.inr
α : Type u
LL₁ c✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: c✝) L₂

Tactic:
·

Goal state after:
case head.inr
α : Type u
LL₁ c✝ L₂ : List (α × Bool)
a : α
b : Bool
h : ReflTransGen Step c✝ ((a, b) :: L₂)
ih : ∀ {L₁ L₂_1 : List (α × Bool)}, (a, b) :: L₁ = c✝ → (a, b) :: L₂_1 = (a, b) :: L₂ → Red L₁ L₂_1
⊢ Red ((a, !b) :: c✝) L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)

pp: case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
·

Goal state after:
case tail.inl
α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ (s' ++ e)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂

Tactic:
·

Goal state after:
case tail.inr
α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ (s ++ e') ∧ Red L₄ L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case nil
α : 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₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

pp: case cons
α : 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₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
·

Goal state after:
case nil
α : 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₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case cons
α : 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₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
·

Goal state after:
case cons
α : 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₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: case mp
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

pp: case mpr
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 }
⊢ s ≤ t →
    { 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

Tactic:
·

Goal state after:
case mp
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
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: case mpr
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 }
⊢ s ≤ t →
    { 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

Tactic:
·

Goal state after:
case mpr
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 }
⊢ s ≤ t →
    { 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
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case refine_1
ι : 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
⊢ {a} ⊆ s

pp: case refine_2
ι : 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, x ∉ {a} → f x = 1

Tactic:
·

Goal state after:
case refine_1
ι : 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
⊢ {a} ⊆ s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case refine_2
ι : 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, x ∉ {a} → f x = 1

Tactic:
·

Goal state after:
case refine_2
ι : 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, x ∉ {a} → f x = 1
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 ι
s : Finset ι
f : ι → M
a : ι
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
h : a ∈ s
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

pp: case neg
ι : 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
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
·

Goal state after:
case pos
ι : 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
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
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)⁻¹ = f (of x)⁻¹ * f (of x) * g (of x)⁻¹

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)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
·

Goal state after:
α : 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)⁻¹ = f (of x)⁻¹ * f (of x) * g (of x)⁻¹
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : 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
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1

Tactic:
·

Goal state after:
case neg
ι : 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
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
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)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
·

Goal state after:
α : 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)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹
Module: Mathlib.GroupTheory.Coset.Defs

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

Tactic:
rw [← image_singleton, preimage_image_mk_eq_mul]

Goal state after:
α : Type u_1
inst✝ : Group α
N : Subgroup α
⊢ {1} * ↑N = ↑N
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₂, f a = ∏ a ∈ s₂, g a

Tactic:
conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]

Goal state after:
ι : 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₂, f a = ∏ a ∈ s₁ ∩ s₂, g a
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

pp: case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)

Tactic:
·

Goal state after:
case pos
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : IsEmpty α
⊢ Function.Injective ⇑(map f)
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
·

Goal state after:
case neg
α : Type u
β : Type v
f : α → β
hf : Function.Injective f
h : Nonempty α
⊢ Function.Injective ⇑(map f)
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
h₂ : b ∈ 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
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

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
h₂ : b ∈ 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
h₂ : b ∉ 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
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

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
h₂ : b ∈ 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
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
·

Goal state after:
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
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a * f b
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
h₂ : b ∈ 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
h₂ : b ∉ 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
h₂ : b ∈ s
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
·

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