mathlib-initiative/mathlib-tactics huggingface dataset:
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
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K < comap f L ↔ K < L

Tactic:
lt_iff_le_not_ge,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K ≤ comap f L ∧ ¬comap f L ≤ comap f K ↔ K ≤ L ∧ ¬L ≤ K
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : x.1 = y.1 ∧ x.2 = y.2
⊢ x = y

Tactic:
← Prod.ext_iff

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
h : Disjoint H₁ H₂
x y : ↥H₁ × ↥H₂
hxy : x = y
⊢ x = y
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ closure (⇑f '' Set.univ) = mrange f

Tactic:
← map_mclosure,

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ map f (closure Set.univ) = mrange f
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Submonoid M
⊢ (∃ x, ∃ (hx : x ∈ S), ⟨x, hx⟩ ≠ ⟨1, ⋯⟩) ↔ ∃ x ∈ S, x ≠ 1

Tactic:
simp [Ne]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
F : Type u_4
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ Codisjoint (map f H) (map f K)

Tactic:
rw [codisjoint_iff, ← map_sup, codisjoint_iff.mp h, ← MonoidHom.mrange_eq_map,
    mrange_eq_top_of_surjective _ hf]

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

Goal state before:
pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n

Tactic:
· simp only [not_lt] at h
    have s0 : 0 < s := sqrt_pos.2 n1
    exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
a b : α
H : a⁻¹ * b = unop x
ha : a ∈ s
hb : b ∈ t
this : op (a⁻¹ * b) = x
⊢ x • a = b

Tactic:
simp [← this]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < (a :: b :: l).prod

Tactic:
rw [List.prod_cons]

Goal state after:
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
a b : M
l : List M
x✝ : a :: b :: l ≠ []
hl₁ : 1 < a ∧ 1 < b ∧ ∀ (a : M), a ∈ l → 1 < a
⊢ 1 < a * (b :: l).prod
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
← SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ↑(⨆ i, S i), ∀ b ∈ ↑(⨆ i, S i), a * b = b * a
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
← SetLike.mem_coe,

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
induction l using List.reverseRecOn with

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
s t : Submonoid N
x : N
⊢ x ∈ s ⊔ t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x

Tactic:
simp only [sup_eq_range, mem_mrange, coprod_apply, coe_subtype, Prod.exists,
    Subtype.exists, exists_prop]

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
this : idxOf m l = idxOf n l
⊢ m ∈ some n

Tactic:
(idxOf_inj hml).1 this,

Goal state after:
case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
this : idxOf m l = idxOf n l
⊢ n ∈ some n
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
g : BoundedLatticeHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ } = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Lattice α
inst✝⁶ : Lattice β
inst✝⁵ : Lattice γ
inst✝⁴ : Lattice δ
inst✝³ : BoundedOrder α
inst✝² : BoundedOrder β
inst✝¹ : BoundedOrder γ
inst✝ : BoundedOrder δ
toFun✝¹ : α → β
map_sup'✝¹ : ∀ (a b : α), toFun✝¹ (a ⊔ b) = toFun✝¹ a ⊔ toFun✝¹ b
map_inf'✝¹ :
  ∀ (a b : α),
    { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun (a ⊓ b) =
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun a ⊓ { toFun := toFun✝¹, map_sup' := map_sup'✝¹ }.toFun b
map_top'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun ⊤ = ⊤
map_bot'✝¹ : { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹ }.toFun ⊥ = ⊥
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹,
        map_bot' := map_bot'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
⊢ { toFun := toFun✝¹, map_sup' := map_sup'✝¹, map_inf' := map_inf'✝¹, map_top' := map_top'✝¹, map_bot' := map_bot'✝¹ } =
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_bot' := map_bot'✝ }
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ ¬((image (⇑toDual) s).erase (toDual x)).max = ↑(toDual x)

Tactic:
apply max_erase_ne_self

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

Goal state before:
pp: α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) (foldl (fun r l ↦ r ++ [a :: l]) r₂ r₁) [l] = sublists'Aux a r₁ r₂ ++ [a :: l]

Tactic:
foldl

Goal state after:
α : Type u
a : α
r₁✝ r₁ : List (List α)
l : List α
ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁
r₂ : List (List α)
⊢ foldl (fun r l ↦ r ++ [a :: l]) (foldl (fun r l ↦ r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] =
    sublists'Aux a r₁ r₂ ++ [a :: l]
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Multiset α
⊢ ∀ (a : List α), (powersetCard n ⟦a⟧).card = (card ⟦a⟧).choose n

Tactic:
simp [powersetCard_coe]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot β
inst✝ : WellFoundedGT β
f : α → β
h✝ : Nonempty α
t : Finset α
ht : ∀ x ∈ Set.range fun x ↦ x.sup f, ¬(fun x ↦ x.sup f) t < x
a : α
⊢ f a ≤ t.sup f

Tactic:
classical
  have := ht (f a ⊔ t.sup f) ⟨insert a t, by simp⟩
  rwa [right_lt_sup, not_not] at this

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mpr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
ha : ⊥ < a
⊢ (∃ b ∈ s, a ≤ f b) → a ≤ s.sup f

Tactic:
exact fun ⟨b, hb, hle⟩ => le_trans hle (le_sup hb)

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (f ⁻¹' s).Finite

Tactic:
← Set.biUnion_preimage_singleton

Goal state after:
α : Type u
β : Type v
f : α → β
s : Set β
h : s.Finite
hf : ∀ b ∈ s, (f ⁻¹' {b}).Finite
⊢ (⋃ y ∈ s, f ⁻¹' {y}).Finite
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case insert
ι : Type u_1
ι' : Type u_2
α : Type u_3
inst✝³ : Preorder ι'
inst✝² : Nonempty ι'
inst✝¹ : IsDirectedOrder ι'
inst✝ : Order.Frame α
s : Set ι
f : ι → ι' → α
a✝¹ : ι
s✝ : Set ι
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ihs : (∀ i ∈ s✝, Monotone (f i)) → ⨆ j, ⨅ i ∈ s✝, f i j = ⨅ i ∈ s✝, ⨆ j, f i j
hf : ∀ i ∈ insert a✝¹ s✝, Monotone (f i)
⊢ ⨆ j, ⨅ i ∈ insert a✝¹ s✝, f i j = ⨅ i ∈ insert a✝¹ s✝, ⨆ j, f i j

Tactic:
rw [forall_mem_insert] at hf
    simp only [iInf_insert, ← ihs hf.2]
    exact iSup_inf_of_monotone hf.1 fun j₁ j₂ hj => iInf₂_mono fun i hi => hf.2 i hi hj

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ ⨆ x ∈ (↑s).sigma fun i ↦ ↑(t i), f x = ⨆ x ∈ ↑s, ⨆ x_1 ∈ ↑(t x), f ⟨x, x_1⟩

Tactic:
biSup_sigma

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

Goal state before:
pp: α : Type u
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ (t.sigma fun a ↦ s.preimage (Sigma.mk a) ⋯) = s

Tactic:
by
  rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ (∃ y, P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ y, y < x ∧ P y

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u_2
P : α → Prop
x : α
inst✝ : Preorder α
hx : P x
⊢ (∃ y, P y ∧ y ≤ x ∧ ¬x ≤ y) ↔ ∃ y, (y ≤ x ∧ ¬x ≤ y) ∧ P y
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
x : α
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ↪o β
t : Set β
⊢ Minimal (fun x ↦ x ∈ t ∩ range ⇑f) (f x) ↔ Minimal (fun x ↦ f x ∈ t) x

Tactic:
by
  refine ⟨fun h ↦ ⟨h.prop.1, fun y hy ↦ ?_⟩, fun h ↦ ⟨⟨h.prop, mem_range_self x⟩, ?_⟩⟩
  · rw [← f.le_iff_le, ← f.le_iff_le]
    exact h.le_of_le ⟨hy, mem_range_self y⟩
  rintro _ ⟨hyt, ⟨y, rfl⟩⟩
  simp_rw [f.le_iff_le]
  exact h.le_of_le hyt

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ {x ∈ Finset.Ico a b | c ≤ x}.val = Ico c b

Tactic:
Finset.Ico_filter_le_of_left_le hac

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
x✝ : s = ∅ ∨ s.Nonempty
⊢ sInf s = 0 ↔ 0 ∈ s ∨ s = ∅

Tactic:
cases eq_empty_or_nonempty s with

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ a < x ∧ x < b

Tactic:
lt_iff_le_not_ge,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ (a ≤ x ∧ ¬x ≤ a) ∧ x ≤ b ∧ ¬b ≤ x ↔ (a ≤ x ∧ ¬x ≤ a) ∧ x < b
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m < sInf s
x✝ : s = ∅ ∨ s.Nonempty
⊢ m ∉ s

Tactic:
cases eq_empty_or_nonempty s with

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Icc a b) = Icc ↑a ↑b

Tactic:
rw [subtype_Icc_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Icc] at hx
  exact hp hx.1 hx.2 a.prop b.prop

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b

Tactic:
by
  rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x ∈ (closure s)⁻¹ ↔ x⁻¹ ∈ closure s

Tactic:
mem_inv

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
x : G
⊢ x⁻¹ ∈ closure s ↔ x⁻¹ ∈ closure s
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: case single
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y b✝ : α
h : x ⩿ b✝
⊢ x ≤ b✝

Tactic:
exact h.le

Goal state after:
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
hx : x ∈ (ConjClasses.mk g).carrier
y : G
hy : y ∈ (ConjClasses.mk g).carrier
⊢ x = y

Tactic:
simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
x y : G
hx : IsConj x g
hy : IsConj y g
⊢ x = y
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
g : G
hg : g ∈ ↑(centralizer s)
h : G
hh : h ∈ s
⊢ f h * f g = f g * f h

Tactic:
rw [← map_mul, ← map_mul, hg h hh]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
⊢ {y | toLex (a, y) ∈ s}.IsPWO

Tactic:
let f : α ×ₗ β → β := fun x => (ofLex x).2
  have h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a}) := by
    ext x
    simp [f]
  rw [h]
  apply IsPWO.image_of_monotoneOn (hαβ.mono inter_subset_left)
  rintro b ⟨-, hb⟩ c ⟨-, hc⟩ hbc
  simp only [mem_preimage, mem_singleton_iff] at hb hc
  have : (ofLex b).1 < (ofLex c).1 ∨ (ofLex b).1 = (ofLex c).1 ∧ f b ≤ f c :=
    Prod.Lex.toLex_le_toLex.mp hbc
  simp_all only [lt_self_iff_false, true_and, false_or]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) * s ^ (n + 1) = ↑(closure s)

Tactic:
pow_succ',

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) * (s * s ^ n) = ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ z ∈ ↑C

Tactic:
suffices y⁻¹ * (y * z) ∈ C by simpa

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ y⁻¹ * (y * z) ∈ C
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
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a

Tactic:
rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]

Goal state after:
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
n : G
hmem : n ∈ H ⊔ K
g : G
⊢ g * n * g⁻¹ ∈ H ⊔ K

Tactic:
← SetLike.mem_coe,

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
n : G
hmem : n ∈ ↑(H ⊔ K)
g : G
⊢ g * n * g⁻¹ ∈ ↑(H ⊔ K)
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 x y : Con M
h : (fun c ↦ ⇑c.toSetoid) x = (fun c ↦ ⇑c.toSetoid) y
⊢ x = y

Tactic:
by
    rcases x with ⟨⟨x, _⟩, _⟩
    rcases y with ⟨⟨y, _⟩, _⟩
    have : x = y := h
    subst x; rfl

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten

Tactic:
pow_succ',

Goal state after:
α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L * mk L ^ n = mk (List.replicate (n + 1) L).flatten
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 ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
rw [← Finset.prod_subset hu hf]

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 ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s', f x = f a * f b
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x : FreeAddGroup α
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) x) = x

Tactic:
induction x with
    | C1 => simp
    | of x => simp [Unique.default_eq x]
    | neg_of x hx => simp [Unique.default_eq x]
    | add x y hx hy => simp [add_zsmul, hx, hy]

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
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s with p x, f x = ∏ x ∈ s, f x

Tactic:
filter_true_of_mem

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, f x = ∏ x ∈ s, f x

ι : 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
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ Finset.subtype p s, f ↑x = ∏ x ∈ s, f x

Tactic:
by
  rw [prod_subtype_eq_prod_filter, filter_true_of_mem]
  simpa using h

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ ≤ ⊥ ↔ H₁ ≤ centralizer ↑H₂

Tactic:
commutator_le

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
seq_neg,

Goal state after:
case neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
ih : Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p
⊢ -(Prod.mk <$> pure p <*> y) = -((fun b a ↦ (a, b)) <$> y <*> pure p)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ (map (fun i ↦ ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (map (fun i ↦ f i a) m).prod

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]

Goal state after:
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₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
commutator_le

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'
⊢ ∀ g₁ ∈ H₁.prod K₁, ∀ g₂ ∈ H₂.prod K₂, ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
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
⊢ (lift f) x = f ((monoidOf ⊤).sec x).1 / f ↑((monoidOf ⊤).sec x).2

Tactic:
by
  simp [lift, (monoidOf ⊤).lift_apply, div_eq_mul_inv]; congr

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
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ f (f.sec 1).1 = f ↑(f.sec 1).2

Tactic:
← sec_spec,

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)
⊢ 1 * f ↑(f.sec 1).2 = f ↑(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_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
⊢ smul' r₁ s₁ r₂ s₂ = v • r₂ /ₒ (u * s₁)

Tactic:
simp only [smul']

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₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
⊢ oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) = v • r₂ /ₒ (u * s₁)