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

Goal state before:
pp: case mem
M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
z : M
hz : z ∈ s
⊢ motive x z hx ⋯

Tactic:
| mem z hz =>

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
⊢ ⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)

Tactic:
by
  rintro _ ⟨_, _, _, _, rfl⟩
  exact ⟨_, ‹_›, _, ‹_›, (map_mul m ..).symm⟩

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

Goal state before:
pp: case mem
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
z : G
hz : z ∈ k
⊢ p x z hx ⋯

Tactic:
| mem z hz =>

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

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
f : G →* N
H : Subgroup G
⊢ ∀ {x : N}, x ∈ ⇑f '' ↑H → x⁻¹ ∈ ⇑f '' ↑H

Tactic:
rintro _ ⟨x, hx, rfl⟩
      exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ x ∈ ↑(comap f (closure s))

Tactic:
rw [SetLike.mem_coe, mem_comap]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ f x ∈ closure s
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
P : Type u_8
inst✝ : MulOneClass P
f : G →* N
g : N →* P
hg : Injective ⇑g
⊢ (g.comp f).ker = f.ker

Tactic:
by
  rw [← comap_ker, g.ker_eq_bot hg, comap_bot]

Goal state after:
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 : y.1 = x.1 ∧ x.2 = y.2
⊢ x = y

Tactic:
eq_comm,

Goal state after:
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
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp.left
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (fst M N) u ≤ s

Tactic:
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩

Goal state after:
case mp.left
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ (fst M N) (y1, y2) ∈ s
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
⊢ map (snd M N) u ≤ t

Tactic:
rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩

Goal state after:
case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : u ≤ s.prod t
y1 : M
y2 : N
hy1 : (y1, y2) ∈ ↑u
⊢ (snd M N) (y1, y2) ∈ t
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: a b k : ℤ
⊢ (fun x ↦ x • a) k = b ↔ b = k * a

Tactic:
eq_comm,

Goal state after:
a b k : ℤ
⊢ b = (fun x ↦ x • a) k ↔ b = k * a
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ normalizer s ≤ normalizer ↑(closure s)

Tactic:
intro g hg
  rw [mem_normalizer_iff_conj_image_eq] at hg
  rw [mem_normalizer_iff_map_conj_eq, MonoidHom.map_closure, MonoidHom.coe_coe, hg]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun x ↦ a • x) ⁻¹' B ↔ A ⊆ a⁻¹ • B

Tactic:
congr! 1

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ (fun x ↦ a • x) ⁻¹' B = a⁻¹ • B
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun x ↦ a⁻¹ • x) ⁻¹' B ↔ A ⊆ a • B

Tactic:
congr! 1

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ (fun x ↦ a⁻¹ • x) ⁻¹' B = a • B
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f : α → β
⊢ Function.Surjective ⇑(map f) → Function.Surjective f

Tactic:
intro fs d
    rcases fs (FreeMonoid.of d) with ⟨b, hb⟩
    induction b using FreeMonoid.inductionOn' with
    | one =>
      have H := congr_arg length hb
      simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
    | of_mul head _ _ =>
      simp only [map_mul, map_of] at hb
      use head
      have H := congr_arg length hb
      simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
      rw [H, mul_one] at hb
      exact FreeMonoid.of_injective hb

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

Goal state before:
pp: case mpr.inl
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
i : ι
a : α i
h : r i b.fst
⊢ Lex r s ⟨i, a⟩ b

Tactic:
exact Lex.left _ _ h

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

Goal state before:
pp: case mp.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : Function.swap r i✝ j✝
⊢ Lex r (fun i ↦ Function.swap (s i)) ⟨j✝, b⟩ ⟨i✝, a⟩

Tactic:
exact Lex.left _ _ h

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

Goal state before:
pp: case mpr.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
h : r i✝ j✝
⊢ Lex (Function.swap r) s ⟨j✝, b⟩ ⟨i✝, a⟩

Tactic:
exact Lex.left _ _ h

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:
apply one_lt_mul_of_lt_of_le' hl₁.1

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 ≤ (b :: l).prod
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LE β
x y : α × β
⊢ toLex y ≤ toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 ≤ x.2

Tactic:
eq_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LE β
x y : α × β
⊢ toLex y ≤ toLex x ↔ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 ≤ x.2
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x y : α × β
⊢ toLex y < toLex x ↔ y.1 < x.1 ∨ x.1 = y.1 ∧ y.2 < x.2

Tactic:
eq_comm,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x y : α × β
⊢ toLex y < toLex x ↔ y.1 < x.1 ∨ y.1 = x.1 ∧ y.2 < x.2
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr.inl
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) ×' α i
i : ι
a : α i
h : r i b.fst
⊢ Lex r s ⟨i, a⟩ b

Tactic:
exact Lex.left _ _ h

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
cases x with | h x
     =>  _ 

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)

Tactic:
exact congrArg _ (funext <| FreeMonoid.lift_apply _)

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : Lex (α × β)
h : x < y
⊢ ∃ a, x < a ∧ a < y

Tactic:
cases x with | h x
     =>  _ 

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
y : Lex (α × β)
x : α × β
h : toLex x < y
⊢ ∃ a, toLex x < a ∧ a < y
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ max (↑head✝) (max tail✝.maximum l₂.maximum) = max (max (↑head✝) tail✝.maximum) l₂.maximum

Tactic:
← max_assoc

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ max (max (↑head✝) tail✝.maximum) l₂.maximum = max (max (↑head✝) tail✝.maximum) l₂.maximum
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
← BoundedOrderHom.comp_apply,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedOrderHom β γ
f₁ f₂ : BoundedOrderHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ (g.comp f₁) a = g (f₂ a)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₂ : List α
a : α
l₁ : List α
ih :
  foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      l₁ =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₁)
⊢ foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂)
      (a :: l₁) =
    do
    let x ← foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] l₂
    map (fun x_1 ↦ x_1 ++ x) (foldr (fun a acc ↦ flatMap (fun x ↦ [x, a :: x]) acc) [[]] (a :: l₁))

Tactic:
| cons a l₁ ih =>

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

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
by
  rw [revzip] at h
  induction l generalizing l₁ l₂ with
  | nil =>
    simp_all only [sublists'_nil, reverse_cons, reverse_nil, nil_append, zip_cons_cons,
      zip_nil_right, mem_singleton, Prod.mk.injEq, append_nil, Perm.refl]
  | cons a l IH =>
    rw [sublists'_cons, reverse_append, zip_append, ← map_reverse, zip_map_right, zip_map_left] at *
      <;> [simp only [mem_append, mem_map, Prod.map_apply, id_eq, Prod.mk.injEq, Prod.exists,
        exists_eq_right_right] at h; simp]
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', h, rfl⟩)
    · exact perm_middle.trans ((IH _ _ h).cons _)
    · exact (IH _ _ h).cons _

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : Option α → Prop
⊢ (∀ a ∈ insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)

Tactic:
simp [Option.forall]

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
s : Set ι
⊢ s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j

Tactic:
by
  simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _),
    not_disjoint_iff_nonempty_inter]

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

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Infinite
⊢ (⋃ i, ↑i).Infinite

Tactic:
have _ := hs.to_subtype

Goal state after:
α : Type u
s : Set (Set α)
hs : s.Infinite
x✝ : Infinite ↑s
⊢ (⋃ i, ↑i).Infinite
Module: Mathlib.Order.Cover

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

Tactic:
by
  ext x y; simp_rw [wcovBy_iff_eq_or_covBy, @eq_comm _ x, reflGen_iff]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ b = Function.update a i (b i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ b = Function.update a i (b i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
i : ι
hi : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ a = Function.update b i (a i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
inst✝ : DecidableEq ι
i : ι
hi : a i ⋖ b i
h : ∀ (j : ι), j ≠ i → a j = b j
⊢ a = Function.update b i (a i)

Tactic:
simpa [Function.eq_update_iff, eq_comm] using h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b

Tactic:
rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl

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

Goal state before:
pp: case zero
a k l : ℕ
hkl : k % a = l % a
hk : k < a
hl : l < a
⊢ k = l

Tactic:
rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableLE (α × β)
a x : α × β
⊢ x ∈ Ici a.1 ×ˢ Ici a.2 ↔ a ≤ x

Tactic:
by
    rw [mem_product, mem_Ici, mem_Ici, le_def]

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

Goal state before:
pp: P : ℕ → Prop
base : ∃ n, ∀ m > n, P m
step : ∀ (n : ℕ), (∀ m > n, P m) → P n
n : ℕ
⊢ ¬BddAbove {x | ∀ m ≥ x, P m}

Tactic:
rintro ⟨b, hb⟩
    rcases base with ⟨n, hn⟩
    specialize @hb (n + b + 1) (fun m hm ↦ hn _ _)
    all_goals lia

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
rw [image_eq_range]

Goal state after:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (range fun x ↦ f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ (a✝ * b✝)⁻¹ ∈ ↑S

Tactic:
mul_inv_rev

Goal state after:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ b✝⁻¹ * a✝⁻¹ ∈ ↑S
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ (Ici a).erase a ↔ a✝ ∈ Ioi a

Tactic:
simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ (univ.pi s).PartiallyWellOrderedOn fun a b ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
rw [partiallyWellOrderedOn_iff_exists_monotone_subseq]

Goal state after:
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝¹ : Fintype ι
this✝ : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
⊢ ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ), f n ∈ univ.pi s) → ∃ g, ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f (g m) i) (f (g n) i)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
by
  rw [mem_Icc] at ha hb
  exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
⊢ { g // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }

Tactic:
refine ⟨Classical.choose (Nat.find_spec h), h1, by convert! h2, fun g hg1 hg2 con => ?_⟩

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r✝ r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ k g, (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 : ∀ m < n, f m = Classical.choose ⋯ m
h2 : IsBadSeq r s (Classical.choose ⋯)
h3 : rk (Classical.choose ⋯ n) = Nat.find h
g : ℕ → α
hg1 : ∀ m < n, Classical.choose ⋯ m = g m
hg2 : rk (g n) < rk (Classical.choose ⋯ n)
con : IsBadSeq r s g
⊢ False
Module: Mathlib.Data.Finset.NoncommProd

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

Tactic:
simp only [quot_mk_to_coe, mem_coe, coe_erase, noncommProd_coe] at comm h ⊢

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
⊢ a * (l.erase a).prod = l.prod
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
⊢ ↑H * {h} = ↑H

Tactic:
simp [preimage, mul_mem_cancel_right (inv_mem hh)]

Goal state after:
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:
simp only [eq_iff_iff]
    apply leftRel_apply

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out ↑g = g * ↑⟨g⁻¹ * Quotient.out ↑g, ⋯⟩

Tactic:
mul_inv_cancel_left

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out ↑g = Quotient.out ↑g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∀ x ∈ s, x ∉ {a} → f x = 1

Tactic:
simpa only [mem_singleton]

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

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
simp_rw [← _root_.map_mul, inv_mul_cancel, _root_.map_one, one_mul]

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a ^ (count a s + 1) * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
pow_succ'

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x s =
    f a * f a ^ count a s * ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG → P.FG

Tactic:
rintro ⟨S, hS⟩

Goal state after:
case mpr
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ P.FG
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
ih₂

Goal state after:
case of.of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ x₁ * (of L2 * of L3) + x₂ * (of L2 * of L3) = x₁ * (of L2 * of L3) + x₂ * (of L2 * of L3)