mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (Disjoint on fun i ↦ map (Embedding.sigmaMk i) (t i)) i j

Tactic:
rw [Function.onFun, disjoint_left]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → a ∉ map (Embedding.sigmaMk j) (t j)
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
x : α
⊢ x ∈ ↑t → x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t

Tactic:
hx

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
x : α
hx : x ∈ ↑t
⊢ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ k = n

Tactic:
refine ih hk ?_ hkl

Goal state after:
case succ.inr.inl
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
⊢ n ∈ ↑(Ico n (n + a))
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Set.Ioc a b ∪ {a} = Set.Icc a b

Tactic:
Set.Ioc_union_left h

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ Set.Icc a b = Set.Icc a b
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
hpos : ∀ x ∈ s, 1 ≤ x
h : s.IsPWO
⊢ (↑(Submonoid.closure s)).IsPWO

Tactic:
rw [Submonoid.closure_eq_image_prod]
  refine (h.partiallyWellOrderedOn_sublistForall₂ (· ≤ ·)).image_of_monotone_on ?_
  exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
⊢ (orbitRel ↥H ↑x.orbit) a b ↔ (orbitRel (↥H) α) ↑a ↑b

Tactic:
exact orbitRel.Quotient.mem_subgroup_orbit_iff.symm

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ orbit ⟦a⟧
⊢ ↑b ∈ MulAction.orbit ↥H ↑a

Tactic:
rw [orbitRel.Quotient.orbit_eq_orbit_out (⟦a⟧ : orbitRel.Quotient H x.orbit) Quotient.out_eq']
       at hb

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ ↑b ∈ MulAction.orbit ↥H ↑a
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ center G → x ∈ normalizer s

Tactic:
hx

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
x : G
hx : x ∈ center G
⊢ x ∈ normalizer s
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
⊢ x ∈ (ConjClasses.mk g).carrier → ∀ ⦃y : G⦄, y ∈ (ConjClasses.mk g).carrier → x = y

Tactic:
hx

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x : G
hx : x ∈ (ConjClasses.mk g).carrier
⊢ ∀ ⦃y : G⦄, y ∈ (ConjClasses.mk g).carrier → x = y
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
N : Type u_2
inst✝ : Mul N
S : Set M
T : Set N
hS : S.Nonempty
hT : T.Nonempty
x✝ : M × N
⊢ (∀ (a : M) (b : N), a ∈ S ∧ b ∈ T → (a * x✝.1, b * x✝.2) = (x✝.1 * a, x✝.2 * b)) ↔
    (∀ m ∈ S, m * x✝.1 = x✝.1 * m) ∧ ∀ m ∈ T, m * x✝.2 = x✝.2 * m

Tactic:
grind [Set.Nonempty]

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr (fun x ↦ f ↑x) b (List.pmap Subtype.mk l ⋯) = List.foldr f b l

Tactic:
← List.foldr_map

Goal state after:
α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map Subtype.val (List.pmap Subtype.mk l ⋯)) = List.foldr f b l
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)

Tactic:
have h a (ha : a ∈ s) : (closure s : Set G) <• a = closure s :=
    op_smul_coe_set <| subset_closure ha

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
h : ∀ a ∈ s, ↑(closure s) <• a = ↑(closure s)
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
⊢ x ∈ {x | x ∈ ↑tl} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ ↑tl} → x ≠ y → Commute x y

Tactic:
hx

Goal state after:
case cons
α : Type u_3
inst✝ : Monoid α
hd : α
tl : List α
hl : {x | x ∈ ↑tl}.Pairwise Commute → List.foldr (fun x1 x2 ↦ x1 * x2) 1 tl = tl.prod
comm : {x | x ∈ ↑(hd :: tl)}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ ↑tl}
⊢ ∀ ⦃y : α⦄, y ∈ {x | x ∈ ↑tl} → x ≠ y → Commute x y
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x : α
⊢ x ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → ∀ ⦃y : α⦄, y ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → x ≠ y → Commute x y

Tactic:
hx

Goal state after:
case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ ⟦tl⟧}
⊢ ∀ ⦃y : α⦄, y ∈ {x | x ∈ a ::ₘ ⟦tl⟧} → x ≠ y → Commute x y
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
⊢ g * (fun x1 x2 ↦ x1 * x2) h k * g⁻¹ ∈ ↑H * ↑K

Tactic:
refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
⊢ (fun x1 x2 ↦ x1 * x2) (g * h * g⁻¹) (g * k * g⁻¹) = g * (fun x1 x2 ↦ x1 * x2) h k * g⁻¹
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
⊢ x ∈ l → ∀ y ∈ l, x * y = y * x

Tactic:
hx

Goal state after:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm' : ∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
⊢ ∀ y ∈ l, x * y = y * x
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
⊢ x ∈ ↑s → ∀ ⦃y : α⦄, y ∈ ↑s → x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y

Tactic:
hx

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
⊢ ∀ ⦃y : α⦄, y ∈ ↑s → x ≠ y → (fun x y ↦ Commute ((f * g) x) ((f * g) y)) x y
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case trans.inl.inl
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ y✝ z✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ y✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) y✝ z✝
ih1 : Relation.Map (⇑r) f f x✝ y✝
ih2 : Relation.Map (⇑r) f f y✝ z✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ z✝

pp: case trans.inl.inr
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ y✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ y✝
ih1 : Relation.Map (⇑r) f f x✝ y✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) y✝ y✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ y✝

Tactic:
· exact .inl <| r.iseqv.isTrans.map hf |>.trans _ _ _ ih1 ih2

Goal state after:
case trans.inl.inr
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ y✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ y✝
ih1 : Relation.Map (⇑r) f f x✝ y✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) y✝ y✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ y✝
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c✝ d c : Con M
⊢ ∀ (x y : M), id (x * y) = id x * id y

Tactic:
by intros; rfl

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

Goal state before:
pp: case head
α : Type u
LL₁ c✝ L₁ 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
h₁₂ : (∃ L, Step L₁ L ∧ c✝ = (a, b) :: L) ∨ L₁ = (a, !b) :: c✝
⊢ Red L₁ L₂

Tactic:
rcases h₁₂ with (⟨L, h₁₂, rfl⟩ | rfl)

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₂

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.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
⊢ x' ∈ ↑t → ∀ ⦃y : κ⦄, y ∈ ↑t → x' ≠ y → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y

Tactic:
hx

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
⊢ ∀ ⦃y : κ⦄, y ∈ ↑t → x' ≠ y → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y
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
x' : κ
⊢ x' ∈ ↑t → ∀ ⦃y : κ⦄, y ∈ ↑t → x' ≠ y → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y

Tactic:
hx

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
x' : κ
hx : x' ∈ ↑t
⊢ ∀ ⦃y : κ⦄, y ∈ ↑t → x' ≠ y → (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y
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
    simp only [eq_iff_iff]
    apply leftRel_apply

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 simpa using s.mul_mem (s.inv_mem <| H ⟨x, rfl⟩) ih

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
convert! (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

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

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

Tactic:
by exact DFunLike.congr_fun h ⟨x, hx⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
⊢ QuotientGroup.con c.subgroup = c

Tactic:
ext x y

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ (QuotientGroup.con c.subgroup) x y ↔ c x y
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = Subgroup.map (mk' N) (Subgroup.comap (mk' N) (lift N φ HN).ker)

Tactic:
Subgroup.map_comap_eq_self_of_surjective (mk'_surjective N)

Goal state after:
G : Type u_1
M : Type u_4
inst✝¹ : Group G
inst✝ : Monoid M
N : Subgroup G
nN : N.Normal
φ : G →* M
HN : N ≤ φ.ker
⊢ (lift N φ HN).ker = (lift N φ HN).ker
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
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
⊢ x ∈ N → x ∈ ((mk' M).comp f).ker

Tactic:
hx

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
M : Subgroup H
inst✝ : M.Normal
f : G →* H
h : N ≤ Subgroup.comap f M
x : G
hx : x ∈ N
⊢ x ∈ ((mk' M).comp f).ker
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG

Tactic:
simp_rw [fg_iff_submonoid_fg] at *

Goal state after:
ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
⊢ x ∈ s → f x = b

Tactic:
hx

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
hc : #s ≤ 1
f : ι → M
b : M
h : ∏ x ∈ s, f x = b
x : ι
hx : x ∈ s
⊢ f x = b
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 : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
⊢ x ∈ s → f x = 1

Tactic:
hx

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
⊢ f x = 1
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ f 0 = 0

Tactic:
map_zero

Goal state after:
α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ 0 = 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)
⊢ #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
biUnion_insert

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.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
⊢ x ∈ H₁ → ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅x, g₂⁆⁆ = 1

Tactic:
hx

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
⊢ ∀ g₂ ∈ H₂, ∀ h ∈ ↑H₃, ⁅h, ⁅x, g₂⁆⁆ = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
⊢ x ∈ s.toFinset → k • (count x s / k) • {x} = count x s • {x}

Tactic:
hx

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
x : ι
hx : x ∈ s.toFinset
⊢ k • (count x s / k) • {x} = count x s • {x}
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₂ ↦ of (1 * x₂)) x = x

Tactic:
induction x using FreeAbelianGroup.induction_on with
    | zero => rfl
    | of L => rw [lift_apply_of, one_mul]
    | neg L ih => rw [map_neg, ih]
    | add x1 x2 ih1 ih2 => rw [map_add, ih1, ih2]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆

Tactic:
apply congr_arg₂

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range
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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ z * f ↑x.2 = f x.1

Tactic:
hx

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)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
z : N
x : M × ↥S
hx : z * f ↑x.2 = f x.1
v : P
hv : k v = x.1
w : P
hw : k w = ↑x.2
⊢ f x.1 = f x.1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = f ra * (↑(fS s₂) * (↑(fS s₂)⁻¹ * f r₂))

Tactic:
← mul_assoc (fS s₂ : T),

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ f ra * f r₂ = f ra * (↑(fS s₂) * ↑(fS s₂)⁻¹ * f r₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹⁷ : Monoid M
S : Submonoid M
inst✝¹⁶ : OreSet S
inst✝¹⁵ : MulAction M X
inst✝¹⁴ : SMul R✝ X
inst✝¹³ : SMul R✝ M
inst✝¹² : IsScalarTower R✝ M M
inst✝¹¹ : IsScalarTower R✝ M X
inst✝¹⁰ : SMul R' X
inst✝⁹ : SMul R' M
inst✝⁸ : IsScalarTower R' M M
inst✝⁷ : IsScalarTower R' M X
inst✝⁶ : SMul R✝ R'
inst✝⁵ : IsScalarTower R✝ R' M
R : Type ?u.51
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : IsScalarTower R M M
inst✝¹ : MulAction R X
inst✝ : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
⊢ (s₁ * s₂) • x = s₁ • s₂ • x

Tactic:
rw [← smul_eq_mul, smul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
x y : OreLocalization S R
⊢ x * y = y * x

Tactic:
cases x with | _ r₁ s₁
    cases y with | _ r₂ s₂
    rw [oreDiv_mul_oreDiv_comm, oreDiv_mul_oreDiv_comm, mul_comm r₁, mul_comm s₁]

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : α
hmn : m ≤ n
⊢ P n hmn

Tactic:
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
hmn : m ≤ Order.succ^[n] m
⊢ P (Order.succ^[n] m) hmn
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ IsSuccLimit a

Tactic:
by
  refine ⟨?_, hs.isSuccPrelimit_of_notMem ha⟩
  obtain ⟨b, hb⟩ := hs'
  obtain rfl | hb := (hs.1 hb).eq_or_lt
  · contradiction
  · exact hb.not_isMin

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
⊢ a < succ b → a ≤ b

Tactic:
contrapose!
  exact succ_le_of_lt

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
⊢ x ∈ S → x ≤ m

Tactic:
hx

Goal state after:
X : Type u_3
inst✝² : LinearOrder X
inst✝¹ : SuccOrder X
inst✝ : IsSuccArchimedean X
S : Set X
m✝ n : X
hn' : n ≤ m✝
m : X
hmn✝ : n ≤ m
IH : (∀ x ∈ S, x ≤ m) → n ∈ S → m ∉ S → ∃ x, IsGreatest S x
hn : n ∈ S
hm' : succ m ∉ S
hm : ∀ x ∈ S, x = succ m ∨ x ≤ m
x : X
hx : x ∈ S
⊢ x ≤ m
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: case zero
m n : ℕ
ha : 0 ≤ pred 0
⊢ IsMin 0

Tactic:
exact isMin_bot

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2

Tactic:
rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
ha :
  (match ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)) ≤
    ⊤
⊢ IsMax ⊤

Tactic:
exact isMax_top

Goal state after:
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ (Function.invFun g ∘ f) a = b

Tactic:
rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]

Goal state after: