mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
ι : Type u_2
p : ι → Prop
K : ι → Subgroup G
i : ι
hp : p i
hK : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on K) {i | p i}
x : G
⊢ x ∈ ⨆ i, ⨆ (_ : p i), K i → ∃ i, p i ∧ x ∈ K i

Tactic:
suffices x ∈ closure (⋃ i, ⋃ (_ : p i), (K i : Set G)) → ∃ i, p i ∧ x ∈ K i by
      simpa only [closure_iUnion, closure_eq (K _)] using this
    refine fun hx ↦ closure_induction (fun _ ↦ ?_) ?_ ?_ ?_ hx
    · simp
    · exact ⟨i, hp, (K i).one_mem⟩
    · rintro x y _ _ ⟨i, hip, hi⟩ ⟨j, hjp, hj⟩
      rcases hK i hip j hjp with ⟨k, hk, hki, hkj⟩
      exact ⟨k, hk, mul_mem (hki hi) (hkj hj)⟩
    · rintro _ _ ⟨i, hi', hi⟩
      exact ⟨i, hi', inv_mem hi⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
h : f.ker ≤ H
⊢ comap f (map f H) = H

Tactic:
by
  rwa [comap_map_eq, sup_eq_left]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case inl
n : ℕ
h : n % 2 = 0
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
simp [h, add_mod]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case inr
n : ℕ
h : n % 2 = 1
⊢ n.succ.testBit 0 = !n.testBit 0

Tactic:
simp [h, add_mod]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m * (n + 1)).bodd = (m.bodd && (n + 1).bodd)

Tactic:
simp only [mul_succ, bodd_add, IH, bodd_succ]
    cases bodd m <;> cases bodd n <;> rfl

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.op.Normal ↔ H.Normal

Tactic:
simp only [← normalizer_eq_top_iff, ← op_normalizer, op_eq_top]

Goal state after:
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case inl
m n : ℕ
h : m < n
⊢ max m n ^ 2 + min m n ≤ n * n + m

Tactic:
max_eq_right h.le,

Goal state after:
case inl
m n : ℕ
h : m < n
⊢ n ^ 2 + min m n ≤ n * n + m
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
x : G
⊢ ⇑Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))

Tactic:
ext
  exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
inst✝ : IsMulTorsionFree G
n : ℕ
hn : n ≠ 0
a b : ↥H
⊢ (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b → a = b

Tactic:
have := pow_left_injective hn (M := G) (a₁ := a) (a₂ := b)

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type u_5
inst✝² : Group N
P : Type u_6
inst✝¹ : Group P
inst✝ : IsMulTorsionFree G
n : ℕ
hn : n ≠ 0
a b : ↥H
this : (fun a ↦ a ^ n) ↑a = (fun a ↦ a ^ n) ↑b → ↑a = ↑b
⊢ (fun a ↦ a ^ n) a = (fun a ↦ a ^ n) b → a = b
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b : (i : ι) × α i
inst✝¹ : Std.Irrefl r
inst✝ : ∀ (i : ι), Std.Irrefl (s i)
i✝ : ι
a : α i✝
ha : s i✝ a a
⊢ False

Tactic:
· exact irrefl _ ha

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x : M
⊢ ⇑Additive.ofMul '' ↑(Submonoid.powers x) = ↑(AddSubmonoid.multiples (Additive.ofMul x))

Tactic:
ext
  exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Top α
inst✝² : Top β
inst✝¹ : Top γ
inst✝ : Top δ
f g : TopHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f; cases g; congr

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : Max α
inst✝² : Max β
inst✝¹ : Max γ
inst✝ : Max δ
f g : SupHom α β
h : f.toFun = g.toFun
⊢ f = g

Tactic:
cases f; cases g; congr

Goal state after:
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← SupHom.comp_apply, h, SupHom.comp_apply]

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
r : List (List α)
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) [] r = (Array.foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r.toArray).toList

Tactic:
have := foldl_hom Array.toList (g₁ := fun r l => (r.push l).push (a :: l))
    (g₂ := fun r l => r ++ [l, a :: l]) (l := r) (init := #[]) (by simp)

Goal state after:
α : Type u
a : α
r : List (List α)
this : foldl (fun r l ↦ r ++ [l, a :: l]) #[].toList r = (foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r).toList
⊢ foldl (fun r l ↦ r ++ [l, a :: l]) [] r = (Array.foldl (fun r l ↦ (r.push l).push (a :: l)) #[] r.toArray).toList
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ map (fun x ↦ x ++ []) l.sublists ++
      (map (fun x ↦ x ++ [a]) l.sublists ++ flatMap (fun x ↦ map (fun x_1 ↦ x_1 ++ x) l.sublists) []) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
flatMap_nil,

Goal state after:
α : Type u
l : List α
a : α
⊢ map (fun x ↦ x ++ []) l.sublists ++ (map (fun x ↦ x ++ [a]) l.sublists ++ []) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∀ (n : { x // x ∈ s }), (↑n).Pairwise r) ↔ ∀ a ∈ s, a.Pairwise r

Tactic:
SetCoe.forall

Goal state after:
α : Type u_1
r : α → α → Prop
s : Set (Set α)
hd : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) s
⊢ (∀ (x : Set α) (h : x ∈ s), (↑⟨x, h⟩).Pairwise r) ↔ ∀ a ∈ s, a.Pairwise r
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ici a = Ico ↑a ⊤

Tactic:
← preimage_coe_Ici,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' some ⁻¹' Ici ↑a = Ico ↑a ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨅ i ∈ s, f i
⊢ a < ⨅ i ∈ s, f i

Tactic:
rw [← hx]

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, f x ≤ sInf ∅
H : ∀ x ∈ s, a < f x
w✝ : ι
hmem : w✝ ∈ s
hx : f w✝ = ⨅ i ∈ s, f i
⊢ a < f w✝
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ i, s i ≤ ⨆ t, ⨆ i ∈ t, s i

case refine_2
α : Type u_2
ι : Type u_5
inst✝ : CompleteLattice α
s : ι → α
⊢ ⨆ t, ⨆ i ∈ t, s i ≤ ⨆ i, s i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (sSup (range fun i ↦ f i)) = ⨆ i, l (f i)

Tactic:
gc.l_csSup (range_nonempty _) hf,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ ⨆ x, l ↑x = ⨆ i, l (f i)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (TransGen fun x1 x2 ↦ x1 ⩿ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
by
  rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | ¬x ≤ a} ↔ a < x

Tactic:
by rw [mem_filter, mem_Ici, lt_iff_le_not_ge]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ k, ⨆ (_ : k ≤ n), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n

Tactic:
biSup_le_eq_sup

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → ¬a n < a m) ↔ ∀ (a : ℕ →o α), ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m

Tactic:
congrm ∀ a, ∃ n, ∀ m h, ?_
  rw [lt_iff_le_and_ne]
  simp [a.mono h]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | ∀ m ≥ x, P m}
n : ℕ
hn : ∀ m > n, P m
⊢ False

Tactic:
specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)

Goal state after:
P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b : ℕ
hb : b ∈ upperBounds {x | ∀ m ≥ x, P m}
n : ℕ
hn : ∀ m > n, P m
m : ℕ
hm : m ≥ n + b + 1
⊢ m > n

P : ℕ → Prop
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n✝ b n : ℕ
hb : n + b + 1 ≤ b
hn : ∀ m > n, P m
⊢ False
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ Finset.subtype p (Ioo ↑a ↑b) ↔ a < x ∧ x < b

Tactic:
by simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
h : a ≤ b
⊢ Ioi b ⊆ Ioi a

Tactic:
simpa [← coe_subset] using Set.Ioi_subset_Ioi h

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #∅ = #(Icc a b) - 1

Tactic:
Icc_eq_empty h,

Goal state after:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ #∅ = #∅ - 1
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r ((f (g (m - g 0))).head! :: (f (g (m - g 0))).tail) ((f (g n')).head! :: (f (g n')).tail)

Tactic:
exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h = g * h * g⁻¹

Tactic:
simpa using hg _ hh

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ normalizer {g} → h ∈ centralizer {g}

pp: case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}

Tactic:
· rintro hh g rfl
    exact mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ MulAut.conj h • H = H

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ MulAut.conj h • H ≤ H

case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ H ≤ MulAut.conj h • H
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H ≤ (MulAut.conj ↑h • P).subgroupOf H

case refine_2
G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ (MulAut.conj ↑h • P).subgroupOf H ≤ MulAut.conj h • P.subgroupOf H
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case hac.hab
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (f y)

pp: case hac
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)

pp: case hbc.hab
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

pp: case hac
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)

Tactic:
· exact comm_ff.of_refl hx hy

Goal state after:
case hac
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)

case hbc.hab
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

case hac
α : 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 : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
f : ι → M
⊢ (cons a s h).prod f = f a * ∏ x ∈ s, f x

Tactic:
Finset.prod_cons h

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝ : CommMonoid M
h : a ∉ s
f : ι → M
⊢ f a * ∏ x ∈ s, f x = f a * ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
⊢ Red LL₁ (p :: L₂) → Red L₁ L₂

Tactic:
generalize eq₂ : (p :: L₂ : List _) = LL₂

Goal state after:
α : Type u
L₁ L₂ : List (α × Bool)
p : α × Bool
LL₁ : List (α × Bool)
eq₁ : p :: L₁ = LL₁
LL₂ : List (α × Bool)
eq₂ : p :: L₂ = LL₂
⊢ Red LL₁ LL₂ → Red L₁ 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 t : Finset ι
h : IsCompl s t
f : ι → M
⊢ ∏ x ∈ s.disjUnion t ⋯, f x = ∏ i, f i

Tactic:
rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
s t : Finset ι
h : IsCompl s t
f : ι → M
⊢ ∏ x ∈ ⊤, f x = ∏ i, f i
Module: Mathlib.GroupTheory.Congruence.Hom

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

Tactic:
dsimp +instances [Setoid.ker, onFun] at *
    rw [map_mul, h1, h2, map_mul]

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

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

Tactic:
dsimp only [← coe_mul, Con.liftOn_coe]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ f (m * n) = f m * f n
Module: Mathlib.GroupTheory.FreeGroup.Basic

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

Tactic:
induction L1 with

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : ¬(x ∈ s ∧ p x)
⊢ (if p x then f x else 1) = 1

Tactic:
not_and

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
x : ι
hs : x ∈ s
h : x ∈ s → ¬p x
⊢ (if p x then f x else 1) = 1
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:
replace h₀ : ∀ b ∈ s, f b = 1 := by grind

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : a ∉ s
h₀ : ∀ b ∈ s, f b = 1
⊢ ∏ x ∈ s, f x = if a ∈ s then f a else 1
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 c.mul (c.refl x) (c.symm h)

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

Goal state before:
pp: 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, g (f j)

Tactic:
exact fun n hnI => (prod_filter_of_pairwise_eq_one hnI hf).symm

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

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
intro p hp q hq

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅f p, f q⁆ ∈ ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
prod_le_iff

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
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
⊢ ∀ {x y : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) → ∃ u v, u • x.fst = v • y.fst ∧ ↑u * ↑x.snd = v * ↑y.snd

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
⊢ ∀ {x y z : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) →
      (∃ u v, u • z.fst = v • y.fst ∧ ↑u * ↑z.snd = v * ↑y.snd) →
        ∃ u v, u • z.fst = v • x.fst ∧ ↑u * ↑z.snd = v * ↑x.snd

Tactic:
· rintro ⟨r, s⟩ ⟨r', s'⟩ ⟨u, v, hru, hsu⟩; dsimp only at *
      rcases oreCondition (s : R) s' with ⟨r₂, s₂, h₁⟩
      rcases oreCondition r₂ u with ⟨r₃, s₃, h₂⟩
      have : r₃ * v * s = s₃ * s₂ * s := by
        -- Porting note: the proof used `assoc_rw`
        rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]
      rcases ore_right_cancel (r₃ * v) (s₃ * s₂) s this with ⟨w, hw⟩
      refine ⟨w * (s₃ * s₂), w * (r₃ * u), ?_, ?_⟩ <;>
        simp only [Submonoid.coe_mul, Submonoid.smul_def, ← hw]
      · simp only [mul_smul, hru, ← Submonoid.smul_def]
      · simp only [mul_assoc, hsu]

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
⊢ ∀ {x y z : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) →
      (∃ u v, u • z.fst = v • y.fst ∧ ↑u * ↑z.snd = v * ↑y.snd) →
        ∃ u v, u • z.fst = v • x.fst ∧ ↑u * ↑z.snd = v * ↑x.snd
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * r₁ * r * r₂ = r₁' * ↑t * r * r₂

Tactic:
by rw [hr₁]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r' * r₂ = ↑t' * r₁ * r' * r₂

Tactic:
by rw [hr₁]

Goal state after:
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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
⊢ ↑s₃' * ↑s₁' * r = r₃' * r₂' * r₂ * ↑s'

Tactic:
h₃,

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
⊢ r₃' * ↑s₂' * r = r₃' * r₂' * r₂ * ↑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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (f.map hy k) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩

Tactic:
map,

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
x : M
y : ↥S
⊢ (f.lift ⋯) (f.mk' x y) = k.mk' (g x) ⟨g ↑y, ⋯⟩