mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : 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
i : ι
left✝¹ : i ∈ s
hx : g i ∈ ↑t
left✝ : i ∈ s
hy : g i ∈ ↑t
hne : g i ≠ g i
⊢ False

Tactic:
;

Goal state after:
case h
ι : 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
i : ι
left✝¹ : i ∈ s
hx : g i ∈ ↑t
left✝ : i ∈ s
hy : g i ∈ ↑t
hne : g i ≠ g i
⊢ False
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
x✝ : M
⊢ ((c.lift f H).comp c.mk') x✝ = f x✝

Tactic:
;

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ((c.lift f H).comp c.mk') x✝ = f x✝
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
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x

Tactic:
;

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x
Module: Mathlib.GroupTheory.Congruence.Hom

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

Tactic:
;

Goal state after:
case mk
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : c.Quotient →* P
x : c.Quotient
a✝ : M
⊢ (c.lift (f.comp c.mk') ⋯) (Quot.mk (⇑c.toSetoid) a✝) = f (Quot.mk (⇑c.toSetoid) a✝)
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 (fun x ↦ f x * g x) s

Tactic:
;

Goal state after:
ι : 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 (fun x ↦ f x * g x) s
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝

Tactic:
;

Goal state after:
case not
α : Type u
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ L₁✝ ++ L₂✝ <+ L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case hc
ι : 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}
⊢ p a

Tactic:
;

Goal state after:
case hc
ι : 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}
⊢ p a
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
this✝ : DecidableEq ι
b : ι
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
this✝ : DecidableEq ι
b : ι
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk.mk.mk
α : Type u
L L₁✝ L₂✝ L₃✝ L₄ : List (α × Bool)
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
c✝ : FreeGroup α
L₃ : List (α × Bool)
⊢ Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃ =
    Quot.mk Red.Step L₁ * (Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃)

Tactic:
;

Goal state after:
case mk.mk.mk
α : Type u
L L₁✝ L₂✝ L₃✝ L₄ : List (α × Bool)
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
c✝ : FreeGroup α
L₃ : List (α × Bool)
⊢ Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃ =
    Quot.mk Red.Step L₁ * (Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ 1 * Quot.mk Red.Step L = Quot.mk Red.Step L

Tactic:
;

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ 1 * Quot.mk Red.Step L = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ Quot.mk Red.Step L * 1 = Quot.mk Red.Step L

Tactic:
;

Goal state after:
case mk
α : Type u
L✝ L₁ L₂ L₃ L₄ : List (α × Bool)
a✝ : FreeGroup α
L : List (α × Bool)
⊢ Quot.mk Red.Step L * 1 = Quot.mk Red.Step L
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
⊢ ∏ a with a ∈ s, f a = ∏ i ∈ s, f i

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ a with a ∈ s, f a = ∏ i ∈ s, f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case e_s
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {a | a ∈ s} = s

Tactic:
;

Goal state after:
case e_s
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ι → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {a | a ∈ s} = s
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝

Tactic:
;

Goal state after:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b : Bool
⊢ Lift.aux f (L₁✝ ++ (x✝, b) :: (x✝, !b) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁) * Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₂)

Tactic:
;

Goal state after:
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₁) * Quot.lift (Lift.aux f) ⋯ (Quot.mk Red.Step L₂)
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 : α → β
x✝ : α
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) x✝ = f x✝

Tactic:
;

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
x✝ : α
⊢ (fun g ↦ ⇑g ∘ of) ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) f) x✝ = f x✝
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 α →* β
a✝ : α
⊢ ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g)) (of a✝) = g (of a✝)

Tactic:
;

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f : α → β
x y : FreeGroup α
g : FreeGroup α →* β
a✝ : α
⊢ ((fun f ↦ MonoidHom.mk' (Quot.lift (Lift.aux f) ⋯) ⋯) ((fun g ↦ ⇑g ∘ of) g)) (of a✝) = g (of a✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝))
    (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ L₂✝))

Tactic:
;

Goal state after:
case not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝))
    (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ L₂✝))
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁) *
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₂)

Tactic:
;

Goal state after:
case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁) *
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₂)
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:
;

Goal state after:
case mk
α : Type u
x : FreeGroup α
L : List (α × Bool)
⊢ (map _root_.id) (Quot.mk Red.Step L) = Quot.mk Red.Step L
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mk
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ (map g) ((map f) (Quot.mk Red.Step L)) = (map (g ∘ f)) (Quot.mk Red.Step L)

Tactic:
;

Goal state after:
case mk
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeGroup α
L : List (α × Bool)
⊢ (map g) ((map f) (Quot.mk Red.Step L)) = (map (g ∘ f)) (Quot.mk Red.Step L)
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
;

Goal state after:
α : Type u
β : Type v
f : α → β
a✝ : α
⊢ (map f) (of a✝) = (lift (of ∘ f)) (of a✝)
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 ι
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
;

Goal state after:
ι : 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 ι
⊢ ∏ x ∈ s, f x = f a * f b
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:
← lift_unique (prod.comp (map f)) (by simp),

Goal state after:
α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ (prod.comp (map f)) x = prod ((map f) x)
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
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
;

Goal state after:
ι : 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 ι
⊢ ∏ x ∈ s, f x = f a * f b
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₂ : 1 ≠ 1
H : g b = 1
⊢ False

Tactic:
;

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₂)
b : κ
hb : b ∈ {x ∈ t | g x ≠ 1}
h₁ : b ∈ t
h₂ : 1 ≠ 1
H : g b = 1
⊢ False
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:
;

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 ↔ x✝ ∈ ⊤
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:
;

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 ↔ x✝ ∈ ⊤
Module: Mathlib.GroupTheory.QuotientGroup.Defs

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

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x✝ : ↥N
⊢ ((mk' N).comp N.subtype) x✝ = 1 x✝
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
;

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ Submonoid.closure Set.univ = ⊤
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 rw [Finset.coe_image, MonoidHom.map_mclosure]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure Set.univ = ⊤

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
inst✝³ : Monoid M
G : Type u_3
H : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup H
inst✝ : Finite G
val✝ : Fintype G
⊢ Subgroup.closure Set.univ = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 = 0 + f 0

Tactic:
;

Goal state after:
M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ f 0 = 0 + f 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a ∪ s.biUnion t) ≤ #(t a) + #(s.biUnion t)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
⊢ ∏ x, f x = f a

Tactic:
by
  have : Unique ι := uniqueOfSubsingleton a
  rw [prod_unique f, Subsingleton.elim default a]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • (r', s').fst = v • (r, s).fst
hsu : ↑u * ↑(r', s').snd = v * ↑(r, s).snd
⊢ ∃ u v, u • (r, s).fst = v • (r', s').fst ∧ ↑u * ↑(r, s).snd = v * ↑(r', s').snd

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • (r', s').fst = v • (r, s).fst
hsu : ↑u * ↑(r', s').snd = v * ↑(r, s).snd
⊢ ∃ u v, u • (r, s).fst = v • (r', s').fst ∧ ↑u * ↑(r, s).snd = v * ↑(r', s').snd
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : ↑u * ↑(r₂, s₂).snd = v * ↑(r₁, s₁).snd
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : ↑u' * ↑(r₃, s₃).snd = v' * ↑(r₂, s₂).snd
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ∃ u v, u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ ↑u * ↑(r₃, s₃).snd = v * ↑(r₁, s₁).snd

Tactic:
;

Goal state after:
case refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
r₃ : X
s₃ u : ↥S
v : R
hur₁ : u • (r₂, s₂).fst = v • (r₁, s₁).fst
hs₁u : ↑u * ↑(r₂, s₂).snd = v * ↑(r₁, s₁).snd
u' : ↥S
v' : R
hur₂ : u' • (r₃, s₃).fst = v' • (r₂, s₂).fst
hs₂u : ↑u' * ↑(r₃, s₃).snd = v' * ↑(r₂, s₂).snd
r' : R
s' : ↥S
h : ↑s' * v' = r' * ↑u
⊢ ∃ u v, u • (r₃, s₃).fst = v • (r₁, s₁).fst ∧ ↑u * ↑(r₃, s₃).snd = v * ↑(r₁, s₁).snd
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α✝ : Type u
G : Type u_1
β✝ : Type v
γ : Type w
α : Type u_2
β : Type u_3
f : α ≃ β
x : FreeAbelianGroup β
⊢ (map ⇑f) ((map ⇑f.symm) x) = x

Tactic:
rw [← map_comp_apply, Equiv.self_comp_symm, map_id, AddMonoidHom.id_apply]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk (m₁ * ↑s₂) (s₁ * ⟨m₂, ⋯⟩) = mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
m₁ m₂ : M
s₁ s₂ : ↥⊤
⊢ mk (m₁ * ↑s₂) (s₁ * ⟨m₂, ⋯⟩) = mk (m₁ * ↑s₂) ⟨↑s₁ * m₂, ⋯⟩
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x✝ : M
⊢ ((fun f ↦ f.comp of) ((fun f ↦ (monoidOf ⊤).lift ⋯) f)) x✝ = f x✝

Tactic:
;

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x✝ : M
⊢ ((fun f ↦ f.comp of) ((fun f ↦ (monoidOf ⊤).lift ⋯) f)) x✝ = f x✝
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : GrothendieckGroup M →* G
x✝ : Localization ⊤
⊢ ((fun f ↦ (monoidOf ⊤).lift ⋯) ((fun f ↦ f.comp of) f)) x✝ = f x✝

Tactic:
;

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : GrothendieckGroup M →* G
x✝ : Localization ⊤
⊢ ((fun f ↦ (monoidOf ⊤).lift ⋯) ((fun f ↦ f.comp of) f)) x✝ = f x✝
Module: Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x : GrothendieckGroup M
⊢ ↑((IsUnit.liftRight (f.domRestrict ⊤) ⋯) ((monoidOf ⊤).sec x).2) = f ↑((monoidOf ⊤).sec x).2

Tactic:
;

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
f : M →* G
x : GrothendieckGroup M
⊢ ↑((IsUnit.liftRight (f.domRestrict ⊤) ⋯) ((monoidOf ⊤).sec x).2) = f ↑((monoidOf ⊤).sec x).2
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑(s' * s) ∈ S

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r : X
s s' : ↥S
⊢ ↑(s' * s) ∈ S
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)
⊢ g (f.sec 1).1 = g ↑(f.sec 1).2

Tactic:
;

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
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ g (f.sec 1).1 = g ↑(f.sec 1).2
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
s₁vS : v * ↑s₁ ∈ S
⊢ ↑(u * s₂) = ↑⟨v * ↑s₁, s₁vS⟩

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
hs₂ : ↑u * ↑s₂ = v * ↑s₁
s₁vS : v * ↑s₁ ∈ S
⊢ ↑(u * s₂) = ↑⟨v * ↑s₁, s₁vS⟩
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ ↑(u * s₂) ∈ S

Tactic:
;

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ ↑(u * s₂) ∈ S