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

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
⊢ l <+ l'

Tactic:
by
  induction l generalizing l' f with
  | nil => simp
  | cons hd tl IH => ?_
  have : some hd = l'[f 0]? := by simpa using hf 0
  rw [eq_comm, List.getElem?_eq_some_iff] at this
  obtain ⟨w, h⟩ := this
  let f' : ℕ ↪o ℕ :=
    OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b => by
      rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos
  have : ∀ ix, tl[ix]? = (l'.drop (f 0 + 1))[f' ix]? := by
    intro ix
    rw [List.getElem?_drop, OrderEmbedding.coe_ofMapLEIff, Nat.add_sub_cancel', ← hf]
    · simp only [getElem?_cons_succ]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact ix.succ_pos
  rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
  apply List.Sublist.append _ (IH _ this)
  rw [List.singleton_sublist, ← h, l'.getElem_take' _ (Nat.lt_succ_self _)]
  exact List.getElem_mem _

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) →
    ∃ n m x_1, x = l.get n ∧ x = l.get m

pp: case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)

Tactic:
· rintro ⟨f, hf⟩
      refine ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩, f.lt_iff_lt.2 (Nat.zero_lt_one), ?_⟩
      rw [← hf, ← hf]; simp

Goal state after:
case mpr
α : Type u_1
l : List α
x : α
⊢ (∃ n m x_1, x = l.get n ∧ x = l.get m) →
    ∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mpr.refine_1.succ.succ
α : Type u_1
l : List α
x : α
n m : Fin l.length
hnm : n < m
h : x = l.get n
h' : x = l.get m
n✝¹ : ℕ
hi✝ : n✝¹ + 1 < (replicate 2 x).length
n✝ : ℕ
hj✝ : n✝ + 1 < (replicate 2 x).length
hi : n✝¹ = 0
hj : n✝ = 0
⊢ ⟨n✝¹ + 1, hi✝⟩ < ⟨n✝ + 1, hj✝⟩ →
    (fun i ↦ if ↑i = 0 then n else m) ⟨n✝¹ + 1, hi✝⟩ < (fun i ↦ if ↑i = 0 then n else m) ⟨n✝ + 1, hj✝⟩

Tactic:
simp [hi, hj]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : (f ⁻¹' s).Finite
hs : s ⊆ range f
⊢ s.Finite

Tactic:
rw [← image_preimage_eq_of_subset hs]
  exact Finite.image f h

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

Goal state before:
pp: case nil
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
h : Pairwise R []
ha : a ∈ []
⊢ R [].head! a

pp: case cons
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
ha : a ∈ head✝ :: tail✝
⊢ R (head✝ :: tail✝).head! a

Tactic:
· contradiction

Goal state after:
case cons
α : Type u_1
R : α → α → Prop
a : α
inst✝¹ : Inhabited α
inst✝ : Std.Refl R
head✝ : α
tail✝ : List α
h : Pairwise R (head✝ :: tail✝)
ha : a ∈ head✝ :: tail✝
⊢ R (head✝ :: tail✝).head! a
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case nil.nil
α : Type u
inst✝ : DecidableEq α
H : [].length ≤ [].length
h : [] ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] []

pp: case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] (b :: l₂)

pp: case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

pp: case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)

Tactic:
· contradiction

Goal state after:
case nil.cons
α : Type u
inst✝ : DecidableEq α
b : α
l₂ : List α
H : [].length ≤ (b :: l₂).length
h : [] ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] (b :: l₂)

case cons.nil
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
H : (head✝ :: tail✝).length ≤ [].length
h : head✝ :: tail✝ ≠ []
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) []

case cons.cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
b : α
l₂ : List α
H : (head✝ :: tail✝).length ≤ (b :: l₂).length
h : head✝ :: tail✝ ≠ b :: l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) (b :: l₂)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate' (n % l.length) = (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length))

Tactic:
by rw [rotate'_length_mul]

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

Goal state before:
pp: case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

pp: case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum

Tactic:
· simp [dedup_cons_of_mem ha]

Goal state after:
case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
ha : ¬a ∈ as
⊢ (map (fun i ↦ count i as) (filter p (a :: as).dedup)).sum = (map (fun x ↦ count x as) (filter p as.dedup)).sum
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons.e_a
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
by_cases hp : p a

Goal state after:
case pos
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

case neg
α : Type u_2
inst✝ : DecidableEq α
p : α → Bool
a : α
as : List α
h : (map (fun x ↦ count x as) (filter p as.dedup)).sum = countP p as
hp : ¬p a = true
⊢ (map (fun i ↦ if a = i then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case inr.inl
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 = n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

pp: case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)

Tactic:
· simp [← hn]

Goal state after:
case inr.inr
α : Type u
l l' : List α
n : ℕ
hl : 0 < l'.length
hn : 0 < n % l'.length
⊢ l.rotate n = l' ↔ l.rotate n = l'.rotate (((l'.length - n % l'.length) % l'.length + n % l'.length) % l'.length)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
rw [← @rotate_eq_rotate _ l _ n, rotate_rotate, ← rotate_mod l', add_mod]
  rcases l'.length.zero_le.eq_or_lt with hl | hl
  · rw [eq_nil_of_length_eq_zero hl.symm, rotate_nil]
  · rcases (Nat.zero_le (n % l'.length)).eq_or_lt with hn | hn
    · simp [← hn]
    · rw [mod_eq_of_lt (Nat.sub_lt hl hn), Nat.sub_add_cancel, mod_self, rotate_zero]
      exact (Nat.mod_lt _ hl).le

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

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ l.cyclicPermutations = (zipWith (fun x1 x2 ↦ x1 ++ x2) l.tails l.inits).dropLast

Tactic:
obtain ⟨hd, tl, rfl⟩ := exists_cons_of_ne_nil h
  exact cyclicPermutations_cons _ _

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk
  rw [choose_succ_right _ _ hn, Nat.add_one_sub_one]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 + 1) * (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1 + 1) * (k + 1 + 1)

Tactic:
rw [choose_succ_succ' (n + 1) (k + 1), Nat.add_mul _ _ (k + 1 + 1), ← add_one_mul_choose_eq n,
      mul_add_one, ← add_one_mul_choose_eq n, Nat.add_right_comm _ _ (_ * _), ← Nat.mul_add,
      ← choose_succ_succ', ← add_one_mul]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!

Tactic:
have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

Goal state after:
case inl
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
⊢ (n + 1).choose k.succ * k.succ ! * (n + 1 - k.succ)! = (n + 1)!
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: case negSucc
α : Type u
inst✝ : Group α
a b : α
a✝ : ℕ
⊢ (a * b * a⁻¹) ^ Int.negSucc a✝ = a * b ^ Int.negSucc a✝ * a⁻¹

Tactic:
simp only [zpow_negSucc, conj_pow, mul_inv_rev, inv_inv]
    rw [mul_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
b : β
⊢ b ∈ f '' s ↔ b ∈ ⋃ i ∈ s, {f i}

Tactic:
simp [@eq_comm β b]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ (fun x ↦ x⁻¹) '' {a} = {a⁻¹}

Tactic:
image_singleton

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ {a⁻¹} = {a⁻¹}
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂ i ∈ T, i) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
exact image2_iInter₂_subset_right ..

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

Goal state before:
pp: case mem.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 z : M
hz : z ∈ s
x✝ : M
h : x✝ ∈ s
⊢ motive x✝ z ⋯ ⋯

Tactic:
exact mem _ _ h hz

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

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

Tactic:
image_singleton

Goal state after:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {a⁻¹ * b} = {a⁻¹ * b}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

Tactic:
image_singleton

Goal state after:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {b * a⁻¹} = {b * a⁻¹}
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ (fun x ↦ a / x) '' {b} = {a / b}

Tactic:
image_singleton

Goal state after:
α : Type u_2
inst✝ : Group α
a b : α
⊢ {a / b} = {a / b}
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mem.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 z : G
hz : z ∈ k
x✝ : G
h : x✝ ∈ k
⊢ p x✝ z ⋯ ⋯

Tactic:
exact mem _ _ h hz

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
⊢ mrange f = ⊤

Tactic:
mrange_eq_top_of_surjective _ hf

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
inst✝ : MonoidHomClass F M N
f : F
hf : Surjective ⇑f
H K : Submonoid M
h : Codisjoint H K
⊢ ⊤ = ⊤
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b n).bodd = b

Tactic:
cases b <;> simp [bodd]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b n).div2 = n

Tactic:
rw [div2_val, bit_div_two]

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

Goal state before:
pp: case pos.h
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ b₁ ≤ a + a

Tactic:
exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ {g} ⊆ ↑H ↔ g ∈ H

Tactic:
Set.singleton_subset_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ g ∈ ↑H ↔ g ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
tn : N.Normal
a : G
h : a ∈ N
c : G
hc : c * a * c⁻¹ ∈ conjugatesOf a
⊢ c * a * c⁻¹ ∈ ↑N

Tactic:
exact tn.conj_mem a h c

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ map (↑(MulAut.conj g)) H.normalCore ≤ map (↑(MulAut.conj g)) H

Tactic:
normalCore_le

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H : Subgroup G
this : (⨅ g, map (↑(MulAut.conj g)) H).Normal
g : G
⊢ map (↑(MulAut.conj g)) H ≤ map (↑(MulAut.conj g)) H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ {⟨g, hg⟩} ⊆
    ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
        (normalClosure {⟨c * g * c⁻¹, hg'⟩}))

Tactic:
Set.singleton_subset_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
hs : Surjective ⇑(((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
⊢ ⟨g, hg⟩ ∈
    ↑(comap (((MulEquiv.toMonoidHom (MulAut.conj c)).domRestrict N).codRestrict N h)
        (normalClosure {⟨c * g * c⁻¹, hg'⟩}))
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
hd : M
tl : List M
IH : f tl.sum ≤ foldr (fun x y ↦ max (f x) y) 0 tl
⊢ f (hd + tl.sum) ≤ max (f hd) (foldr (fun x y ↦ max (f x) y) 0 tl)

Tactic:
exact (hadd _ _).trans (max_le_max le_rfl IH)

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ decode n = some (e.symm (ofNat α n))

Tactic:
rw [decode_ofEquiv e]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Denumerable α
e : β ≃ α
n : ℕ
this : Denumerable β := ofEquiv α e
⊢ Option.map (⇑e.symm) (decode n) = some (e.symm (ofNat α n))
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
hn : n < ↑⊥ ∧ n ∈ s
⊢ False

Tactic:
exact bot_le.not_gt (show (⟨n, hn.2⟩ : s) < ⊥ from hn.1)

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

Goal state before:
pp: case cons
α : Type u
β : Type u_1
γ : Type u_2
f g : α → β → γ
la : List α
lb : List β
a✝¹ : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
hfg : f a✝¹ b✝ = g a✝¹ b✝
a✝ : Forall₂ (fun a b ↦ f a b = g a b) l₁✝ l₂✝
ih : zipWith f l₁✝ l₂✝ = zipWith g l₁✝ l₂✝
⊢ zipWith f (a✝¹ :: l₁✝) (b✝ :: l₂✝) = zipWith g (a✝¹ :: l₁✝) (b✝ :: l₂✝)

Tactic:
| cons hfg _ ih =>

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).max' h = f (s.max' ⋯)

Tactic:
by
  simp only [max', sup'_image]
  exact .symm <| apply_sup'_eq_sup'_comp _ _ fun _ _ ↦ hf.map_max

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

Goal state before:
pp: case cons.mp
α : Type u
a : α
t : List α
IH : ∀ {s : List α}, s ∈ t.sublists' ↔ s <+ t
s : List α
h : s <+ t ∨ ∃ a_1, a_1 <+ t ∧ a :: a_1 = s
⊢ s <+ a :: t

Tactic:
rcases h with (h | ⟨s, h, rfl⟩)
    · exact sublist_cons_of_sublist _ h
    · exact h.cons_cons _

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

Goal state before:
pp: case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetAux' l✝ ++
      (List.map (cons a) (powersetAux' l✝) ++
        (List.map (cons b) (powersetAux' l✝) ++ List.map (cons b ∘ cons a) (powersetAux' l✝))) ~
    powersetAux' l✝ ++
      (List.map (cons b) (powersetAux' l✝) ++
        (List.map (cons a) (powersetAux' l✝) ++ List.map (cons a ∘ cons b) (powersetAux' l✝)))

Tactic:
apply Perm.append_left

Goal state after:
case swap
α : Type u_1
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetAux' l✝) ++
      (List.map (cons b) (powersetAux' l✝) ++ List.map (cons b ∘ cons a) (powersetAux' l✝)) ~
    List.map (cons b) (powersetAux' l✝) ++
      (List.map (cons a) (powersetAux' l✝) ++ List.map (cons a ∘ cons b) (powersetAux' l✝))
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case succ.swap
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ powersetCardAux (n + 1) l✝ ++
      (List.map (cons a) (powersetCardAux n l✝) ++ List.map (cons b) (powersetCardAux n (a :: l✝))) ~
    powersetCardAux (n + 1) l✝ ++
      (List.map (cons b) (powersetCardAux n l✝) ++ List.map (cons a) (powersetCardAux n (b :: l✝)))

Tactic:
apply Perm.append_left

Goal state after:
case succ.swap
α : Type u_1
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ ~ l₂ → powersetCardAux n l₁ ~ powersetCardAux n l₂
l₁ l₂ : List α
a b : α
l✝ : List α
⊢ List.map (cons a) (powersetCardAux n l✝) ++ List.map (cons b) (powersetCardAux n (a :: l✝)) ~
    List.map (cons b) (powersetCardAux n l✝) ++ List.map (cons a) (powersetCardAux n (b :: l✝))
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j

Tactic:
exact H p (mp hm) (np hn) hij

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ #(y ∪ s) = n

Tactic:
rw [card_union_of_disjoint (disjoint_of_subset_left hyt disjoint_sdiff_self_left), hyn]

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
y : Finset α
hyt : y ⊆ t \ s
hyn : #y = n - #s
⊢ n - #s + #s = n
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:
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.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ⨆ j, f ↑j ≤ f ↑⟨a, ⋯⟩

Tactic:
rw [hd.ciSup_le_iff H]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompletePartialOrderSup α
inst✝ : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ f ↑x
H : BddAbove (range fun x ↦ f ↑x)
⊢ ∀ (i : ↑(Iic a)), f ↑i ≤ f ↑⟨a, ⋯⟩
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
⊢ ∃ x, ∀ y ∈ range fun b ↦ ⨆ c, f (b, c), y ≤ x

Tactic:
refine ⟨B, fun y hy ↦ ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
h✝¹ : Nonempty β
h✝ : Nonempty γ
B : α
hB : ∀ y ∈ range f, y ≤ B
y : α
hy : y ∈ range fun b ↦ ⨆ c, f (b, c)
⊢ y ≤ B
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove (range fun i ↦ f ↑i)
hf' : sSup ∅ ≤ ⨆ i, f ↑i
⊢ sSup (f '' s) = sSup (range fun i ↦ f ↑i)

Tactic:
Set.image_eq_range

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
s : Set β
f : β → α
hf : BddAbove (range fun i ↦ f ↑i)
hf' : sSup ∅ ≤ ⨆ i, f ↑i
⊢ sSup (range fun x ↦ f ↑x) = sSup (range fun i ↦ f ↑i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
s : ι → α
a : α
h : BddAbove (range s)
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
by simp [iSup, h, le_csSup_iff', upperBounds]

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

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

Tactic:
by_cases h₂ : x.2 ∈ t₁ x.1

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∈ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁

case neg
ι : Type u_1
α : ι → Type u_3
s₁ s₂ : Set ι
t₁ t₂ : (i : ι) → Set (α i)
x : (i : ι) × α i
h₁ : x.fst ∈ s₁
h₂ : x.snd ∉ t₁ x.fst
⊢ x ∈ s₁.sigma t₁ \ s₂.sigma t₂ ↔ x ∈ s₁.sigma (t₁ \ t₂) ∪ (s₁ \ s₂).sigma t₁