mathlib-initiative/mathlib-tactics huggingface dataset:
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:
simpa using

Goal state after:
α : 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
⊢ y ∈ s
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:
simpa using

Goal state after:
α : 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
⊢ z ∈ N
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:
simpa using

Goal state after:
α : 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
⊢ (f x)⁻¹ * (List.map (fun x ↦ bif x.2 then f x.1 else (f x.1)⁻¹) tl).prod ∈ s
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:
simpa using

Goal state after:
α : 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
⊢ f x * (List.map (fun x ↦ bif x.2 then f x.1 else (f x.1)⁻¹) tl).prod ∈ s
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk
α : Type u
x : FreeGroup α
L : List (α × Bool)
⊢ (map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L

Tactic:
simp [List.map_id']

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

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

Tactic:
simpa using

Goal state after:
case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℕ
hx : (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) ↑x) = ↑x
⊢ (of 1 ^ x).sum = ↑x
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
simpa using

Goal state after:
case pred
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : ℕ
hx : (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) (-↑x)) = -↑x
⊢ (of 1 ^ x).sum = ↑x
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 ∈ s, p x

Tactic:
simpa using

Goal state after:
ι : 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 ∈ s, p x
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:
simpa using

Goal state after:
ι : 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
Module: Mathlib.GroupTheory.QuotientGroup.Defs

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

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ (∀ (x x_1 : G), x_1⁻¹ * x ∈ N) ↔ N = ⊤
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
x✝ : G
⊢ x✝ ∈ N ↔ x✝ ∈ ⊤

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x_1⁻¹ * x ∈ N
x✝ : G
⊢ x✝ ∈ N
Module: Mathlib.GroupTheory.QuotientGroup.Defs

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

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
⊢ (∀ (x x_1 : G), x * x_1⁻¹ ∈ N) ↔ N = ⊤
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
x✝ : G
⊢ x✝ ∈ N ↔ x✝ ∈ ⊤

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
h : ∀ (x x_1 : G), x * x_1⁻¹ ∈ N
x✝ : G
⊢ x✝ ∈ N
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:
simpa using

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

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

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
ι : Sort u_3
inst✝ : Finite ι
P : ι → Submonoid M
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG
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:
simpa using

Goal state after:
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}
⊢ c (a✝ * b✝) 1
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:
simpa using

Goal state after:
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}
⊢ c x✝⁻¹ 1
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
hx : x ∈ c.subgroup
g : G
⊢ g * x * g⁻¹ ∈ c.subgroup

Tactic:
simpa using

Goal state after:
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
hx : x ∈ c.subgroup
g : G
⊢ c (g * x * g⁻¹) 1
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
hx : x ∈ c.subgroup
g : G
⊢ g * x * g⁻¹ ∈ c.subgroup

Tactic:
by simpa using (c.mul (c.mul (c.refl g) hx) (c.refl g⁻¹))

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
h : c (x⁻¹ * y) 1
⊢ c x y

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
h : c (x⁻¹ * y) 1
⊢ c x y
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
h : c x y
⊢ c (x⁻¹ * y) 1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
h : c x y
⊢ c (x⁻¹ * y) 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
s : List M
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ count m s

Tactic:
simpa using

Goal state after:
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq M
s : List M
⊢ s.prod = ∏ m ∈ s.toFinset, m ^ count m s
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Finset ι
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
simpa using

Goal state after:
G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Finset ι
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Set ι
hs : s.Finite
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG

Tactic:
simpa using

Goal state after:
G : Type u_3
inst✝ : Group G
ι : Type u_5
s : Set ι
hs : s.Finite
P : ι → Subgroup G
hP : ∀ i ∈ s, (P i).FG
⊢ (⨆ i ∈ s, P i).FG
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
ι : Sort u_5
inst✝ : Finite ι
P : ι → Subgroup G
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG

Tactic:
simpa using

Goal state after:
G : Type u_3
inst✝¹ : Group G
ι : Sort u_5
inst✝ : Finite ι
P : ι → Subgroup G
hP : ∀ (i : ι), (P i).FG
⊢ (_root_.iSup P).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case inl
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
hx' : g x hx = x
⊢ ∏ x ∈ {x, g x hx}, f x = 1

Tactic:
simpa using

Goal state after:
case inl
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
hx' : g x hx = x
⊢ f x = 1
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
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h₃ : ∀ (a : ι) (ha : a ∈ s \ {x, g x hx}), g a ⋯ ∈ s \ {x, g x hx}
⊢ x ∉ s \ {x, g x hx} ∧ insert x (s \ {x, g x hx}) ⊆ s

Tactic:
by simp [insert_subset_iff, hx]

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
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
classical
  let t' k := (t k).filter (fun i ↦ f i ≠ 1)
  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
  rw [← prod_filter_ne_one, ← this, prod_biUnion]
  swap
  · intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim
  exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))

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 ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
prod_image'

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∏ i ∈ I, ?h i = ∏ i ∈ I, g (f i)

case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ κ → M

case eq
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∀ i ∈ I, g (f i) = ∏ j ∈ I with f j = f i, ?h j
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:
try rw [ih]

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.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:
try rw [ih]

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 >>= fun x ↦ f x >>= g) = -pure x >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_5
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
⊢ ∑ j ∈ t, #({i ∈ s | g i = j}) = #({i ∈ s | g i ∈ t})

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_5
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
⊢ ∑ x ∈ t, ∑ x ∈ s with g x = x, 1 = ∑ x ∈ s with g x ∈ t, 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : DecidableEq M
t : ι → Finset M
h : (↑s).PairwiseDisjoint t
⊢ #(s.biUnion t) = ∑ u ∈ s, #(t u)

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : DecidableEq M
t : ι → Finset M
h : (↑s).PairwiseDisjoint t
⊢ #(s.biUnion t) = ∑ u ∈ s, #(t u)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ i ∈ univ, i ∉ e '' ↑univ → g i = 1

Tactic:
simpa using

Goal state after:
M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ (i : κ), (∀ (x : ι), ¬e x = i) → g i = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
⊢ Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p

Tactic:
rw [map_pure, map_pure, pure_seq, map_pure]

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
l : List ι
⊢ ∑ a ∈ l.toFinset, count a l = l.length

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
l : List ι
⊢ ∑ a ∈ l.toFinset, count a l = l.length
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, count a s = s.card

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, count a s = s.card
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case e_s
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
a : ι
⊢ a ∈ {x ∈ s | count x m ≠ 0} ↔ a ∈ m.toFinset

Tactic:
simpa using

Goal state after:
case e_s
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
a : ι
⊢ a ∈ m → a ∈ s
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
h : 0 * a + 0 * a = 0 * a
⊢ 0 * a = 0

Tactic:
simpa using

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
h : 0 * a + 0 * a = 0 * a
⊢ 0 * a = 0
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

Goal state after:
case cons
M : Type u_4
inst✝ : CommMonoid M
a : M
s : Multiset M
ih : IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a
⊢ IsUnit a → (IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))

Tactic:
rw [mul_add, mul_add, mul_add, ih₁, ih₂]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
m₁ m₂ : M
s₁ s₂ : ↥⊤
h : (r ⊤) (m₁, s₁) (m₂, s₂)
⊢ ⋯ ▸ mk ↑s₁ ⟨m₁, ⋯⟩ = mk ↑s₂ ⟨m₂, ⋯⟩

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
m₁ m₂ : M
s₁ s₂ : ↥⊤
h : (r ⊤) (m₁, s₁) (m₂, s₂)
⊢ ∃ a, a * (m₁ * ↑s₂) = a * (m₂ * ↑s₁)
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
x : α
h : ∀ (f g : F) (x : α), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x
⊢ g x ≤ f x → f x⁻¹ ≤ g x⁻¹

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝⁶ : Group α
inst✝⁵ : Monoid β
F : Type u_6
inst✝⁴ : FunLike F α β
inst✝³ : MonoidHomClass F α β
inst✝² : LE β
inst✝¹ : MulRightMono β
inst✝ : MulLeftMono β
f g : F
x : α
h : ∀ (f g : F) (x : α), f x⁻¹ ≤ g x⁻¹ → g x ≤ f x
⊢ g x ≤ f x → f x⁻¹ ≤ g x⁻¹
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

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

Tactic:
rw [mul_inv_left hg, ← mul_assoc, ← mul_assoc, mul_inv_right hg, mul_comm _ (g (f.sec y).1), ←
      mul_assoc, ← mul_assoc, mul_inv_right hg]
    repeat rw [← g.map_mul]
    refine f.eq_of_eq hg ?_
    simp_rw [map_mul, sec_spec', ← toMonoidHom_apply]
    ac_rfl

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ ((k.lift hl).comp ((f.lift ⋯).comp f.toMonoidHom)) x = l x

Tactic:
lift_comp,

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ ((k.lift hl).comp k.toMonoidHom) x = l x
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Sort u
x : Localization S
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a✝ c✝ : M
b✝ d✝ : ↥S
h : (r S) (a✝, b✝) (c✝, d✝)
⊢ ⋯ ▸ f a✝ b✝ = f c✝ d✝

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
p : Sort u
x : Localization S
f : M → ↥S → p
H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d
a✝ c✝ : M
b✝ d✝ : ↥S
h : (r S) (a✝, b✝) (c✝, d✝)
⊢ f a✝ b✝ = f c✝ d✝
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
⊢ ∃ z' w' d, z * f ↑d = f z' ∧ w * f ↑d = f w'

Tactic:
let ⟨a, ha⟩ := surj f z

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
⊢ ∃ z' w' d, z * f ↑d = f z' ∧ w * f ↑d = f w'
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ f.mk' x 1 = f x

Tactic:
rw [mk', map_one]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ f x * ↑1⁻¹ = f x