mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
⊢ (drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?

Tactic:
· have hlt : n % length l < length l := mod_lt _ (m.zero_le.trans_lt hml)
    rw [getElem?_append_right hm, getElem?_take_of_lt, length_drop]
    · congr 1
      rw [length_drop] at hm
      have hm' := Nat.sub_le_iff_le_add'.1 hm
      have : n % length l + m - length l < length l := by
        rw [Nat.sub_lt_iff_lt_add hm']
        exact Nat.add_lt_add hlt hml
      conv_rhs => rw [Nat.add_comm m, ← mod_add_mod, mod_eq_sub_mod hm', mod_eq_of_lt this]
      lia
    · rwa [Nat.sub_lt_iff_lt_add' hm, length_drop, Nat.sub_add_cancel hlt.le]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l ~r l' ↔ l' ∈ map l.rotate (range (l.length + 1))

Tactic:
simp_rw [mem_map, mem_range, isRotated_iff_mod]
  exact
    ⟨fun ⟨n, hn, h⟩ => ⟨n, Nat.lt_succ_of_le hn, h⟩,
      fun ⟨n, hn, h⟩ => ⟨n, Nat.le_of_lt_succ hn, h⟩⟩

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁.offDiag ~ l₂.offDiag

Tactic:
simp_all [perm_iff_count, count_offDiag_eq_mul_sub_ite]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ ↑(map { toFun := Prod.swap, inj' := ⋯ } (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
by
    push_cast
    exact Set.image_swap_prod _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq (α × β)
s : Finset α
t : Finset β
⊢ ↑(image Prod.swap (t ×ˢ s)) = ↑(s ×ˢ t)

Tactic:
by
    push_cast
    exact Set.image_swap_prod _ _

Goal state after:
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ cons m a (φ b) (fun a' ha' ↦ φ (f a' ha')) a' ha' = φ (cons m a b f a' ha')

Tactic:
refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ (fun h ↦ ⋯ ▸ φ b) = fun h ↦ φ (⋯ ▸ b)
Module: Mathlib.Data.Multiset.Pi

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
⊢ ∀ (a_1 : α) (ha : a_1 ∈ a ::ₘ m), r (cons m a b₁ f₁ a_1 ha) (cons m a b₂ f₂ a_1 ha)

Tactic:
intro a ha

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a✝ : α
r : ⦃a : α⦄ → δ a → δ a → Prop
b₁ b₂ : δ a✝
f₁ f₂ : (a' : α) → a' ∈ m → δ a'
hb : r b₁ b₂
hf : ∀ (a : α) (ha : a ∈ m), r (f₁ a ha) (f₂ a ha)
a : α
ha : a ∈ a✝ ::ₘ m
⊢ r (cons m a✝ b₁ f₁ a ha) (cons m a✝ b₂ f₂ a ha)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: r n : ℕ
h : r < n / 2
⊢ r + r < n

Tactic:
← Nat.mul_two

Goal state after:
r n : ℕ
h : r < n / 2
⊢ r * 2 < n
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: E : Type u_4
F : Type u_5
G : Type u_6
inst✝³ : Monoid E
inst✝² : Monoid F
inst✝¹ : MulAction F G
inst✝ : IsPretransitive F G
f : E →* F
hf : Surjective ⇑f
x✝ : MulAction E G := compHom G f
x : G
e : E
⊢ ∃ g, g • x = f e • x

Tactic:
exact ⟨e, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
κ : ι → Sort u_8
f : α → β
s : (i : ι) → κ i → Set β
⊢ f ⁻¹' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f ⁻¹' s i j

Tactic:
preimage_iInter

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ univ ^ (n + 2) = univ

Tactic:
by rw [pow_succ, univ_pow n.succ_ne_zero, univ_mul_univ]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
κ : ι → Sort u_8
f : α → β → γ
s : (i : ι) → κ i → Set α
t : Set β
⊢ image2 f (⋂ i, ⋂ j, s i j) t ⊆ ⋂ i, ⋂ j, image2 f (s i j) t

Tactic:
simp_rw [image2_subset_iff, mem_iInter]
  exact fun x hx y hy i j => mem_image2_of_mem (hx _ _) hy

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a * x) '' t = (fun x ↦ a⁻¹ * x) ⁻¹' t

Tactic:
image_eq_preimage_of_inverse

Goal state after:
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ ?m.22 ⁻¹' t = (fun x ↦ a⁻¹ * x) ⁻¹' t

case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse ?m.22 fun x ↦ a * x

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse ?m.22 fun x ↦ a * x

α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ α → α
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x * b) '' t = (fun x ↦ x * b⁻¹) ⁻¹' t

Tactic:
image_eq_preimage_of_inverse

Goal state after:
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ ?m.22 ⁻¹' t = (fun x ↦ x * b⁻¹) ⁻¹' t

case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse ?m.22 fun x ↦ x * b

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse ?m.22 fun x ↦ x * b

α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ α → α
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ (fun x ↦ a / x) '' t = (fun x ↦ x⁻¹ * a) ⁻¹' t

Tactic:
image_eq_preimage_of_inverse

Goal state after:
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ ?m.23 ⁻¹' t = (fun x ↦ x⁻¹ * a) ⁻¹' t

case h₁
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ LeftInverse ?m.23 fun x ↦ a / x

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ RightInverse ?m.23 fun x ↦ a / x

α : Type u_2
inst✝ : Group α
t : Set α
a : α
⊢ α → α
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x ↦ x / b) '' t = (fun x ↦ x * b) ⁻¹' t

Tactic:
image_eq_preimage_of_inverse

Goal state after:
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ ?m.20 ⁻¹' t = (fun x ↦ x * b) ⁻¹' t

case h₁
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ LeftInverse ?m.20 fun x ↦ x / b

case h₂
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ RightInverse ?m.20 fun x ↦ x / b

α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ α → α
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a : M
⊢ a ∈ Set.ofPred IsUnit ↔ IsUnit a

Tactic:
rw [Set.mem_ofPred_eq]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x y : G
⊢ x / y ∈ f.ker ↔ f x = f y

Tactic:
constructor <;> intro h
  · rw [← div_mul_cancel x y, map_mul, mem_ker.mp h, one_mul]
  · rw [mem_ker, div_eq_mul_inv, map_mul, h, ← map_mul, mul_inv_cancel, map_one]

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

Goal state before:
pp: b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m (n - k) = bit b (shiftLeft' b m n) >>> 1 >>> k

Tactic:
simp only [shiftLeft'_sub, Nat.le_of_succ_le_succ h, shiftRight_succ, shiftRight_zero]

Goal state after:
b : Bool
m n k : ℕ
h : k + 1 ≤ n + 1
⊢ shiftLeft' b m n >>> k = (bit b (shiftLeft' b m n) / 2) >>> k
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: ⊢ unpair 0 = 0

Tactic:
unpair

Goal state after:
⊢ (if 0 - sqrt 0 * sqrt 0 < sqrt 0 then (0 - sqrt 0 * sqrt 0, sqrt 0) else (sqrt 0, 0 - sqrt 0 * sqrt 0 - sqrt 0)) = 0
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s) ∩ z • (t⁻¹ * t)

Tactic:
smul_mul_assoc

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

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ y :: ys
⊢ x ≤ (y :: ys).prod

Tactic:
simp only [mem_cons] at h₁

Goal state after:
case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x = y ∨ x ∈ ys
⊢ x ≤ (y :: ys).prod
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
⊢ ∀ a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x), a ∈ s

Tactic:
intro a ha

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
a : ℕ
ha : a ∈ List.filter (fun y ↦ decide (y ∈ s)) (List.range x)
⊢ a ∈ s
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList l.sublists

Tactic:
change l.map (((↑) : List α → Multiset α) ∘ pure) <+~ (sublists l).map (↑)

Goal state after:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
⊢ ↑(t.sup f) = t.sup fun x ↦ ↑(f x)

Tactic:
let := Subtype.semilatticeSup Psup
  let := Subtype.orderBot Pbot
  apply apply_sup_eq_sup_comp Subtype.val <;> intros <;> rfl

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

Goal state before:
pp: case refine_2
α : Type u_1
s a : Finset α
ha✝ : a ∈ (range (#s + 1)).disjiUnion (fun i ↦ powersetCard i s) ⋯
i : ℕ
_hi : i ∈ range (#s + 1)
ha : a ∈ powersetCard i s
⊢ a ∈ s.powerset

Tactic:
exact mem_powerset.mpr (mem_powersetCard.mp ha).1

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

Goal state before:
pp: case intro
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P α

Tactic:
refine Fintype.induction_empty_option ?_ ?_ ?_ α

Goal state after:
case intro.refine_1
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α β : Type u) [Fintype β] (e : α ≃ β), P α → P β

case intro.refine_2
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ P PEmpty.{u + 1}

case intro.refine_3
P : Type u → Prop
of_equiv : ∀ {α β : Type u} (a : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ {α : Type u} [Fintype α], P α → P (Option α)
α : Type u
inst✝ : Finite α
val✝ : Fintype α
⊢ ∀ (α : Type u) [Fintype α], P α → P (Option α)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : IsEmpty ι
inst✝ : InfSet α
f : ι → WithTop α
⊢ ⨅ i, f i = ⊤

Tactic:
iInf,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : IsEmpty ι
inst✝ : InfSet α
f : ι → WithTop α
⊢ sInf (range fun i ↦ f i) = ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
iInf,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(sInf (range fun i ↦ f i)) = ⨅ i, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(sInf (range fun i ↦ f i)) = ⨅ i, ↑(f i)

Tactic:
iInf,

Goal state after:
α : Type u_1
ι : Sort u_4
inst✝² : Preorder α
inst✝¹ : Nonempty ι
inst✝ : InfSet α
f : ι → α
hf : BddBelow (range f)
⊢ ↑(sInf (range fun i ↦ f i)) = sInf (range fun i ↦ ↑(f i))
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Tactic:
cases isEmpty_or_nonempty ι
  · simp [iSup_of_empty']
  apply le_antisymm <| ciSup_le fun x ↦ sup_le_sup (le_ciSup Hf x) (le_ciSup Hg x)
  have := bbdAbove_range_sup Hf Hg
  exact sup_le (ciSup_mono this fun _ ↦ le_sup_left) (ciSup_mono this fun _ ↦ le_sup_right)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ f '' ∅, g i = ⨆ x ∈ ∅, g (f x)

Tactic:
Set.image_empty,

Goal state after:
case inl
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
⊢ ⨆ i ∈ ∅, g i = ⨆ x ∈ ∅, g (f x)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ ⨆ i ∈ f '' s, g i = ⨆ x ∈ s, g (f x)

Tactic:
← csSup_image hg hf',

Goal state after:
case inr
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
hf' : sSup ∅ ≤ ⨆ i, g ↑i
⊢ sSup (g '' f '' s) = ⨆ x ∈ s, g (f x)
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ioi a = Ici b

Tactic:
← Ioo_union_Ici_eq_Ioi h.lt,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ⋖ b
⊢ Ioo a b ∪ Ici b = Ici b
Module: Mathlib.Order.Cover

Goal state before:
pp: case refine_1.inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a₁ : α
b₁ b₂ : β
h : (a₁, b₁) ⋖ (a₁, b₂)
⊢ a₁ ⋖ a₁ ∧ b₁ = b₂ ∨ b₁ ⋖ b₂ ∧ a₁ = a₁

Tactic:
exact Or.inr ⟨mk_covBy_mk_iff_right.1 h, rfl⟩

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
h : a ⋖ b
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j

Tactic:
obtain ⟨i, hi⟩ := exists_forall_antisymmRel_of_covBy h

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝ : (i : ι) → PartialOrder (α i)
a b : (i : ι) → α i
h : a ⋖ b
i : ι
hi : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
⊢ ∃ i, ∀ (j : ι), j ≠ i → a j = b j
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
inst✝¹ : LinearOrder α
inst✝ : Finite α
f : α →o α
hf : Function.Injective ⇑f
⊢ Set.range ⇑f = Set.range ⇑id

Tactic:
by
    simpa [Set.range_eq_univ] using Finite.surjective_of_injective hf

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

Goal state before:
pp: n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

Tactic:
obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty

Goal state after:
case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}

case inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
m : ℕ
hm : m ∈ {m | p (m + n)}
⊢ sInf {m | p (m + n)} + n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Nat

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

Tactic:
refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
h : ∃ x, n + m < x ∧ r (f (n + m)) (f x)
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
obtain ⟨n', hn1, hn2⟩ := h

Goal state after:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ ∃ n', n < n' ∧ r (f (n + m)) (f (n' + m))
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 (Icc ↑a ↑b) ↔ a ≤ x ∧ x ≤ b

Tactic:
by simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]

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 α
g : G
a : α
⊢ a ∈ orbit G (g • a)

Tactic:
by
  simp only [orbit_smul, mem_orbit_self]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case pos
α : 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 < n
hmn :
  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)
hn : n < g 0
⊢ False

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 < n
hmn :
  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)
hn : ¬n < g 0
⊢ False

Tactic:
· apply hf1.2 m n mn
    rwa [if_pos hn, if_pos (mn.trans hn)] at hmn

Goal state after:
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 < n
hmn :
  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)
hn : ¬n < g 0
⊢ False
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • (↑(ofConjAct um) * m * ↑(ofConjAct um)⁻¹) = a • (↑(ofConjAct um) * m) * ↑(ofConjAct um)⁻¹

Tactic:
smul_mul_assoc

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Monoid M
inst✝² : SMul α M
inst✝¹ : SMulCommClass α M M
inst✝ : IsScalarTower α M M
a : α
um : ConjAct Mˣ
m : M
⊢ a • (↑(ofConjAct um) * m * ↑(ofConjAct um)⁻¹) = a • (↑(ofConjAct um) * m * ↑(ofConjAct um)⁻¹)
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = a • (ofConjAct ug * g) * (ofConjAct ug)⁻¹

Tactic:
smul_mul_assoc

Goal state after:
α : Type u_1
M : Type u_2
G : Type u_3
inst✝³ : Group G
inst✝² : SMul α G
inst✝¹ : SMulCommClass α G G
inst✝ : IsScalarTower α G G
a : α
ug : ConjAct G
g : G
⊢ a • (ofConjAct ug * g * (ofConjAct ug)⁻¹) = a • (ofConjAct ug * g * (ofConjAct ug)⁻¹)
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
⊢ ((centralizer s).subgroupOf (normalizer s)).Normal

Tactic:
refine (Subgroup.normal_subgroupOf_iff <| centralizer_le_normalizer s).mpr fun c n hc hn ↦ ?_

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
⊢ n * c * n⁻¹ ∈ centralizer s
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ normalizer {g} = centralizer {g}

Tactic:
refine ext fun h ↦ ⟨?_, ?_⟩

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

case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ ⇑(iInf f) = ⨅ i, ⇑(f i)

Tactic:
iInf,

Goal state after:
M : Type u_1
inst✝ : Mul M
ι : Sort u_4
f : ι → Con M
⊢ ⇑(sInf (Set.range f)) = ⨅ i, ⇑(f i)
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 ι
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 * ∏ m ∈ s.toFinset, f m ^ count m s = f a * ∏ x ∈ s.toFinset, f x ^ count x (a :: s)

Tactic:
grind [Finset.prod_congr]

Goal state after:
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
φ : G →* H
hφ : Surjective ⇑φ
HN : N = φ.ker
⊢ Injective ⇑(lift N φ ⋯)

Tactic:
rw [← MonoidHom.ker_eq_bot_iff, ker_lift, ← HN, QuotientGroup.map_mk'_self]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ centralizer Set.univ ↔ H ≤ center G

Tactic:
centralizer_univ

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ center G ↔ H ≤ center G