mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ map (Embedding.subtype p) univ = filter p univ

Tactic:
by
  rw [← subtype_map, subtype_univ]

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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s.toFinset = ∅.toFinset ↔ s = ∅

Tactic:
toFinset_inj

Goal state after:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
A : Fintype ↑∅ := Fintype.ofIsEmpty
⊢ s = ∅ ↔ s = ∅
Module: Mathlib.Data.Int.DivMod

Goal state before:
pp: m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ m / n / k = m / (n * k)

Tactic:
ediv_ediv_of_nonneg hn

Goal state after:
m n k : Int
hn : 0 ≤ n
hk : 0 ≤ k
⊢ m / (n * k) = m / (n * k)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset { x // p x }
a : α
h : a ∈ map (Embedding.subtype fun x ↦ p x) s
⊢ p a

Tactic:
rcases mem_map.1 h with ⟨x, _, rfl⟩
  exact x.2

Goal state after:
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i.rev ≤ j ↔ j.rev ≤ i

Tactic:
← rev_le_rev,

Goal state after:
n : ℕ
i j : Fin n
⊢ j.rev ≤ i.rev.rev ↔ j.rev ≤ i
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ i ≤ j.rev ↔ j ≤ i.rev

Tactic:
← rev_le_rev,

Goal state after:
n : ℕ
i j : Fin n
⊢ j.rev.rev ≤ i.rev ↔ j ≤ i.rev
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: α : Sort u_1
k l : ℕ
h : k = l
f : Fin k → α
g : Fin l → α
⊢ f ≍ g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩

Tactic:
by
  subst h
  simp [funext_iff]

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
this : s = image (fun i ↦ f ↑i ⋯) (range n).attach
⊢ #s = #(image (fun i ↦ f ↑i ⋯) (range n).attach)

Tactic:
rw [this]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ #(image f s) = #t

Tactic:
rw [this]

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

Goal state before:
pp: case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n).succ) =
    (f (Fin.castSucc 0) :: ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
concat_cons,

Goal state after:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i ↦ f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i ↦ f i.castSucc.succ).concat (f (Fin.last n).succ) =
    f (Fin.castSucc 0) :: (ofFn fun i ↦ f i.succ.castSucc).concat (f (Fin.last (n + 1)))
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
a b : Fin m
hb : ↑b < n
h : a < b
⊢ ↑(a.castLT ⋯ - b.castLT hb) = ↑(a - b) + n - m

Tactic:
by
  simp only [val_sub, val_castLT]
  repeat rw [Nat.mod_eq_of_lt (by omega)]
  have h' : a.val < b.val := h
  omega

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rcases castSucc_lt_or_lt_succ p i with H | H
  · rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]
    exact Fin.not_lt.2 <| Fin.le_of_lt H
  · rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ

Tactic:
exact succ_succAbove_succ i 0

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

Goal state before:
pp: α : Type u_4
inst✝ : Finite α
⊢ Nonempty (Fintype α)

Tactic:
by
  rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
  exact ⟨.ofEquiv _ e.symm⟩

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ insert (cons x b 0) (Set.range (tail (cons x b))) = insert x (Set.range b)

Tactic:
cons_zero,

Goal state after:
α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ insert x (Set.range (tail (cons x b))) = insert x (Set.range b)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (if (if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1) < if ↑j < ↑i then ↑j else ↑j + 1 then
      if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1
    else (if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1) + 1) =
    if (if ↑k < ↑j then ↑k else ↑k + 1) < ↑i then if ↑k < ↑j then ↑k else ↑k + 1
    else (if ↑k < ↑j then ↑k else ↑k + 1) + 1

Tactic:
split_ifs <;> lia

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i : Fin (m + n)
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) i = v i

Tactic:
cases i using addCases

Goal state after:
case left
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin m
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (castAdd n i✝) = v (castAdd n i✝)

case right
m n : ℕ
γ : Fin (m + n) → Sort u_2
v : (i : Fin (m + n)) → γ i
i✝ : Fin n
⊢ addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) (natAdd m i✝) = v (natAdd m i✝)
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: P : (α : Type u_4) → [Fintype α] → Prop
α : Type u_4
inst✝ : Fintype α
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
hn : card α = n
⊢ P α

Tactic:
induction n using Nat.strong_induction_on generalizing α with | _ n ih

Goal state after:
case h
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
⊢ P α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
a : Fin n → α
m : ℕ
⊢ «repeat» m.succ a = append a («repeat» m a) ∘ Fin.cast ⋯

Tactic:
by
  generalize_proofs h
  apply funext
  rw [(Fin.rightInverse_cast h.symm).surjective.forall]
  refine Fin.addCases (fun l => ?_) fun r => ?_
  · simp [modNat, Nat.mod_eq_of_lt l.is_lt]
  · simp [modNat]

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

Goal state before:
pp: m n : ℕ
h : m ≤ n
⊢ { i // ↑i < m } ≃ Fin m

Tactic:
exact { toFun := fun ⟨⟨i, _⟩, hi⟩ ↦ ⟨i, hi⟩
          invFun := fun ⟨i, hi⟩ ↦ ⟨⟨i, lt_of_lt_of_le hi h⟩, hi⟩ }

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ card α = 1 ↔ ∃ x, ∀ (y : α), y = x

Tactic:
← card_unit,

Goal state after:
α : Type u_1
inst✝ : Fintype α
⊢ card α = card Unit ↔ ∃ x, ∀ (y : α), y = x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
⊢ Injective (snoc x x₀) ↔ Injective x ∧ ¬x₀ ∈ Set.range x

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩
  · simpa [Function.comp] using h.comp (Fin.castSucc_injective _)
  · rintro ⟨i, hi⟩
    rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i,
      h.eq_iff] at hi
    exact ne_last_of_lt i.castSucc_lt_last hi

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
⊢ (f '' f ⁻¹' s).Finite

Tactic:
exact Finite.image f h

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : p 0
⊢ Fin.find p h = 0

pp: case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
· grind [find_eq_zero]

Goal state after:
case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ k.castSucc < j

Tactic:
Fin.lt_def

Goal state after:
case inl.h
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ ↑k.castSucc < ↑j
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: M : Type u_3
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
⊢ a ^ count a s = (filter (Eq a) s).prod

Tactic:
by
  rw [filter_eq, prod_replicate]

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

Goal state before:
pp: α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n (l ++ [a]) ++ take n (l ++ [a]) = drop (n + 1) (a :: l) ++ take (n + 1) (a :: l)

Tactic:
drop,

Goal state after:
α : Type u
a : α
l : List α
n : ℕ
h : n + 1 ≤ (a :: l).length
hnl : n ≤ l.length
hnl' : n ≤ (l ++ [a]).length
⊢ drop n (l ++ [a]) ++ take n (l ++ [a]) = drop n l ++ take (n + 1) (a :: l)
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 ↦ count i as) (filter p (a :: as).dedup)).sum = countP p as

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) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
· refine _root_.trans ?_ h
      by_cases ha : a ∈ as
      · simp [dedup_cons_of_mem ha]
      · simp only [dedup_cons_of_notMem ha, List.filter]
        match p a with
        | true => simp only [List.map_cons, List.sum_cons, List.count_eq_zero.2 ha, zero_add]
        | false => simp only

Goal state after:
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) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0
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) = true then 1 else 0) (filter p (a :: as).dedup)).sum = if p a = true then 1 else 0

Tactic:
simp only [beq_iff_eq]

Goal state after:
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
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ a > b

Tactic:
cases as with
    | nil =>
      simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas
      exact (List.not_lt_nil _ hmas).elim
    | cons a' as =>
      rw [List.isChain_cons_cons] at ha
      refine lt_of_le_of_lt ?_ ha.1
      rw [le_iff_lt_or_eq] at hmas
      rcases hmas with hmas | hmas
      · exact head_le_of_lt hmas
      · simp_all only [List.cons.injEq, le_refl]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0 • s
⊢ a ∈ s

Tactic:
rw [zero_nsmul] at h

Goal state after:
case zero
α : Type u_1
a : α
s : Multiset α
h : a ∈ 0
⊢ a ∈ s
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ (n • m + m).prod = m.prod ^ (n + 1)

Tactic:
pow_add,

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
m : Multiset M
n : ℕ
⊢ (n • m + m).prod = m.prod ^ n * m.prod ^ 1
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
⊢ ((Option.map singleton (f a)).getD 0).bind g = (Option.map g (f a)).getD 0

Tactic:
cases f a with
  | none => simp
  | some b => simp

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

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
by
  induction s using Multiset.induction <;> simp [Int.mul_emod, *]

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ List.count a l + List.count a l ≤ List.count a l * List.count a l

Tactic:
rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h

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

Goal state before:
pp: α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
s' : Multiset α
h : s' = a ::ₘ s.val
⊢ (s'.pi fun a ↦ (t a).val).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup

Tactic:
subst s'

Goal state after:
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ ((a ::ₘ s.val).pi fun a ↦ (t a).val).dedup =
    ((t a).val.bind fun b ↦
        (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup).dedup
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i

Tactic:
rw [this]

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ i, s i)
inhabited_h : Inhabited ι
y : β
x : ι → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x i ∈ s i
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: I : Type u
f : I → Type v
inst✝¹ : DecidableEq I
inst✝ : (i : I) → MulOneClass (f i)
⊢ Pairwise fun i j ↦ ∀ (x : f i) (y : f j), Commute (mulSingle i x) (mulSingle j y)

Tactic:
by
  intro i j hij x y; ext k
  by_cases i = k <;> simp_all

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
p q : Subgroup G
h : (fun s ↦ s.carrier) p = (fun s ↦ s.carrier) q
⊢ p = q

Tactic:
obtain ⟨⟨⟨hp, _⟩, _⟩, _⟩ := p
    obtain ⟨⟨⟨hq, _⟩, _⟩, _⟩ := q
    congr

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ S = ⊥

Tactic:
rw [eq_bot_iff_forall]

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
S : Submonoid M
inst✝ : Subsingleton ↥S
⊢ ∀ x ∈ S, x = 1
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ (decodeSum n).bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Tactic:
rw [this]

Goal state after:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ none.bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none
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
⊢ conjugatesOf a ⊆ ↑N

Tactic:
by
  rintro a hc
  obtain ⟨c, rfl⟩ := isConj_iff.1 hc
  exact tn.conj_mem a h c

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ ⊤ ≤ normalizer ↑(Subgroup.map f H)

Tactic:
← f.range_eq_top_of_surjective hf,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ f.range ≤ normalizer ↑(Subgroup.map f H)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ comap f (normalizer ↑H) = ⊤ ↔ H.Normal

Tactic:
← comap_top f,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ comap f (normalizer ↑H) = comap f ⊤ ↔ H.Normal
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: ⊢ ofNat (ℕ × ℕ) = unpair

Tactic:
funext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
by simp [Finset.ext_iff]

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

Goal state before:
pp: α : Type u_4
β : Type u_5
x✝³ x✝² : Finset α
x✝¹ x✝ : Finset β
⊢ x✝³.disjSum x✝¹ = x✝².disjSum x✝ → x✝³ = x✝² ∧ x✝¹ = x✝

Tactic:
by simp [Finset.ext_iff]

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

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

Tactic:
SupHom.comp_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Max α
inst✝¹ : Max β
inst✝ : Max γ
g : SupHom β γ
f₁ f₂ : SupHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₂ a) = g (f₂ a)
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : Lattice α
inst✝⁵ : Lattice β
inst✝⁴ : FunLike F α β
inst✝³ : OrderBot α
inst✝² : OrderBot β
inst✝¹ : BotHomClass F α β
inst✝ : InfHomClass F α β
a b : α
f : F
h : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
rw [disjoint_iff, ← map_inf, h.eq_bot, map_bot]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
⊢ IsGLB (↑s) i ↔ IsLeast (↑s) i

Tactic:
refine ⟨fun his => ?_, IsLeast.isGLB⟩

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
⊢ IsLeast (↑s) i
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) i

Tactic:
rw [this]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) (s.min' hs)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ sublistsLen 1 (a :: s) = map (fun x ↦ [x]) (a :: s).reverse

Tactic:
rw [sublistsLen_succ_cons, ih, reverse_cons, map_append, sublistsLen_zero]

Goal state after:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) [[]] = map (fun x ↦ [x]) s.reverse ++ map (fun x ↦ [x]) [a]
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:
rw [revzip] at h
  induction l using List.reverseRecOn generalizing l₁ l₂ with
  | nil =>
    have : l₁ = [] ∧ l₂ = [] := by simpa using h
    simp [this]
  | append_singleton l' a ih =>
    rw [sublists_concat, reverse_append, zip_append (by simp), ← map_reverse, zip_map_right,
      zip_map_left] at *
    simp only [Prod.mk_inj, mem_map, mem_append, Prod.map_apply, Prod.exists] at h
    rcases h with (⟨l₁, l₂', h, rfl, rfl⟩ | ⟨l₁', l₂, h, rfl, rfl⟩)
    · rw [← append_assoc]
      exact (ih _ _ h).append_right _
    · rw [append_assoc]
      apply (perm_append_comm.append_left _).trans
      rw [← append_assoc]
      exact (ih _ _ h).append_right _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x : α
s : Finset α
h : x ∉ s
n : ℕ
⊢ powersetCard n.succ (insert x s) = powersetCard n.succ s ∪ image (insert x) (powersetCard n s)

Tactic:
rw [powersetCard_eq_filter, powerset_insert, filter_union, ← powersetCard_eq_filter]
  grind

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ (powersetCard n s).Nonempty ↔ n ≤ #s

Tactic:
by
  aesop (add simp [Finset.Nonempty, exists_subset_card_eq, card_le_card])

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ u

Tactic:
← insert_erase hx,

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
t : Finset α
ht : t ∈ powersetCard n (u.erase x)
⊢ insert x t ∈ powersetCard n.succ (insert x (u.erase x))
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case mp.empty
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ a < ∅.sup f → ∃ b ∈ ∅, a < f b

Tactic:
exact (absurd · not_lt_bot)

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

Goal state before:
pp: ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)

Tactic:
have : Nonempty ι := Nonempty.intro j

Goal state after:
ι : Type u_5
s : Set ι
α : Type u_6
inst✝ : CompleteLattice α
f : ι → α
j : ι
hj : j ∈ s
this : Nonempty ι
⊢ ↑(⨆ i ∈ s, f i) = ⨆ i ∈ s, ↑(f i)
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this✝ : Nonempty ι
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i
⊢ f ⟨i, h⟩ ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩

Tactic:
rw [this]

Goal state after:
case inr.refine_1
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Subtype p → α
hf : BddAbove (range f)
hf' : sSup ∅ ≤ iSup f
h✝ : Nonempty (Subtype p)
this✝ : Nonempty ι
i : ι
h : p i
this : f ⟨i, h⟩ = (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i
⊢ (fun i ↦ ⨆ (h : p i), f ⟨i, h⟩) i ≤ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : ι → Set α
c : Set ι
hn : c.Nonempty
hc : DirectedOn (fun i j ↦ f i ⊆ f j) c
s : Finset α
hs : ↑s ⊆ ⋃ i ∈ c, f i
⊢ ∃ i ∈ c, ↑s ⊆ f i

Tactic:
rw [Set.biUnion_eq_iUnion] at hs
  have := hn.coe_sort
  simpa using (directed_comp.2 hc.directed_val).exists_mem_subset_of_finset_subset_biUnion hs

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
a : α
s : Finset α
ha : a ∈ s
⊢ ∃ b ∈ s, a ≤ b ∧ ?m.24 b

Tactic:
simpa [Maximal, and_assoc] using {x ∈ s | a ≤ x}.exists_maximal ⟨a, mem_filter.2 ⟨ha, le_rfl⟩⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
s : Set α
inst✝ : Preorder α
h : s.Subsingleton
⊢ Minimal (fun x ↦ x ∈ s) x ↔ x ∈ s

Tactic:
obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton

Goal state after:
case inl
α : Type u_2
x : α
inst✝ : Preorder α
h : ∅.Subsingleton
⊢ Minimal (fun x ↦ x ∈ ∅) x ↔ x ∈ ∅

case inr
α : Type u_2
x✝ : α
inst✝ : Preorder α
x : α
h : {x}.Subsingleton
⊢ Minimal (fun x_1 ↦ x_1 ∈ {x}) x✝ ↔ x✝ ∈ {x}