mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
a b c : α
left✝¹ : c < a
right✝¹ : a ≤ b
left✝ : c < b
right✝ : b ≤ a
⊢ b ≤ a

Tactic:
first | assumption | exact le_of_lt ‹_› | exact le_trans ‹_› (le_of_lt ‹_›)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (range f)

Tactic:
by
  rw [← image_univ]
  exact hf.isChain_image (isChain_of_trichotomous _)

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
⊢ extend f g 1 x = 1

Tactic:
by
    by_cases hf : ∃ a, f a = x
    · rw [extend, dif_pos hf, ← notMem_mulSupport]
      rw [← Classical.choose_spec hf] at hfg
      exact fun hg ↦ hfg ⟨_, hg, rfl⟩
    · rw [extend_apply' _ _ _ hf]; rfl

Goal state after:
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ 0 ≤ 2 • f a

Tactic:
rw [two_nsmul, ← map_one_eq_zero f, ← div_self' a]

Goal state after:
ι : Type u_1
F : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝⁵ : FunLike F α β
inst✝⁴ : Group α
inst✝³ : AddCommMonoid β
inst✝² : LinearOrder β
inst✝¹ : IsOrderedAddMonoid β
inst✝ : GroupSeminormClass F α β
f : F
a : α
⊢ f (a / a) ≤ f a + f a
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ n.descFactorial (k + 1)

Tactic:
by
    rw [descFactorial_succ, Nat.pow_succ, succ_sub_succ, Nat.mul_comm]
    apply Nat.mul_le_mul_left
    exact (le_trans (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) k)
      (pow_sub_le_descFactorial n k))

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
⊢ ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2

Tactic:
exact Int.floor_le (x + 1 / 2)

Goal state after:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ l + (n + 1) • a ≤ l + 0 • a

Tactic:
by gcongr; lia

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋₊ = ↑⌊a⌋

Tactic:
by
  rw [← Int.natCast_floor_eq_floor ha, Int.cast_natCast]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ ↑(z + 1) < y * ↑n

Tactic:
rw [Int.cast_add, Int.cast_one]

Goal state after:
K : Type u_4
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : Archimedean K
x y : K
n : ℕ
h : x < y
nh : (y - x)⁻¹ < ↑n
z : ℤ
zh : ∀ (z_1 : ℤ), z_1 ≤ z ↔ ↑z_1 ≤ x * ↑n
n0' : 0 < ↑n
⊢ ↑z + 1 < y * ↑n
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a : α
⊢ a ∈ a ::ₘ 0

Tactic:
exact mem_cons_self _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : s ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
← cons_erase m

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)

Tactic:
by
  rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
x : α
t : Multiset α
ih : ∀ {s u : Multiset α}, Rel r s t → Rel r t u → Rel r s u
a : α
as : Multiset α
ha1 : r a x
ha2 : Rel r as t
r1 : Rel r (a ::ₘ as) (x ::ₘ t)
b : α
bs : Multiset α
hb1 : r x b
hb2 : Rel r t bs
r2 : Rel r (x ::ₘ t) (b ::ₘ bs)
⊢ Rel r (a ::ₘ as) (b ::ₘ bs)

Tactic:
exact Multiset.Rel.cons (_root_.trans ha1 hb1) (ih ha2 hb2)

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝ : DecidableEq α
f : α → β
s : Multiset α
t : Multiset β
b : β
h : map f s = b ::ₘ t
⊢ b ∈ b ::ₘ t

Tactic:
exact mem_cons_self _ _

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t = s + t

Tactic:
by
  apply _root_.le_antisymm
  · rw [union_add_distrib]
    refine union_le (Multiset.add_le_add_left inter_le_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right inter_le_left
  · rw [Multiset.add_comm, add_inter_distrib]
    refine le_inter (Multiset.add_le_add_right le_union_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right le_union_left

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → Option β
a : α
s : Multiset α
⊢ filterMap f (a ::ₘ s) = (Option.map singleton (f a)).getD 0 + filterMap f s

Tactic:
by
  cases h : f a with
  | none => simp [filterMap_cons_none a s h]
  | some b => simp [filterMap_cons_some f a s h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.val.toFinset = s

Tactic:
ext
  rw [Multiset.mem_toFinset, ← mem_def]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ Set.SurjOn toFinset {l | l.Nodup} Set.univ

Tactic:
by
  rintro ⟨⟨l⟩, hl⟩ _
  exact ⟨l, hl, (toFinset_eq hl).symm⟩

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

Goal state before:
pp: α : Type u_1
a : α
⊢ ¬a ∈ ∅

Tactic:
simp only [mem_def, empty_val, notMem_zero, not_false_iff]

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
x✝¹ x✝ : List α
⊢ (⟦x✝¹⟧ + ⟦x✝⟧).Nodup ↔ Nodup ⟦x✝¹⟧ ∧ Nodup ⟦x✝⟧ ∧ _root_.Disjoint ⟦x✝¹⟧ ⟦x✝⟧

Tactic:
simp [nodup_append, disjoint_iff_ne]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
p : α → Prop
inst✝ : DecidablePred p
⊢ count True (map p s) = (filter p s).card

Tactic:
by
  simp only [count_eq_card_filter_eq, eq_iff_iff, true_iff, filter_map, comp_apply, card_map]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun x ↦ x \ s) {t | s ⊆ t}

Tactic:
grind [Set.InjOn, sdiff_union_of_subset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
f : α → β
⊢ (Multiset.map f univ.val).Nodup ↔ Injective f

Tactic:
by
  rw [nodup_map_iff_injOn, coe_univ, Set.injOn_univ]

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

Goal state before:
pp: α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p s = ∅ ↔ ∀ x ∈ s, ¬p x

Tactic:
filter_eq_empty_iff

Goal state after:
α : Type u_1
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
⊢ (∀ ⦃x : α⦄, x ∈ s → ¬p x) ↔ ∀ x ∈ s, ¬p x
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : i.succ < p
hij : i.succ = j.castSucc
⊢ i = j

Tactic:
cases hi <| Nat.lt_trans i.castSucc_lt_succ hj

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃! a, a ∈ s

Tactic:
simp [card_eq_one, Finset.singleton_iff_unique_mem]

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

Goal state before:
pp: n : ℕ
⊢ image (succAbove 0) univ = {0}ᶜ

Tactic:
Fin.image_succAbove_univ

Goal state after:
n : ℕ
⊢ {0}ᶜ = {0}ᶜ
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: n : ℕ
⊢ image (last n).succAbove univ = {last n}ᶜ

Tactic:
Fin.image_succAbove_univ

Goal state after:
n : ℕ
⊢ {last n}ᶜ = {last n}ᶜ
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
l : List α
h : l.Nodup
⊢ l.length ≤ Fintype.card α

Tactic:
classical exact List.toFinset_card_of_nodup h ▸ l.toFinset.card_le_univ

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 3 < #s ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_four,
      ← exists_and_left, exists_comm (α := Finset α)]

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ b b_1 b_2 b_3, ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b ≠ b_3 ∧ b_1 ≠ b_2 ∧ b_1 ≠ b_3 ∧ b_2 ≠ b_3 ∧ a = {b, b_1, b_2, b_3}) ↔
    ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x y : (i : Fin n) → α i.castSucc
xₙ yₙ : α (last n)
h : snoc x xₙ = snoc y yₙ
i : Fin n
⊢ x i = y i

Tactic:
simpa using congr_fun h (castSucc i)

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
⊢ ∃ t, s ⊆ t ∧ #t = n + 1

Tactic:
rcases hn.eq_or_lt with hn' | hn'
    · exact ⟨s, subset_rfl, hn'⟩
    obtain ⟨t, hs, ht⟩ := IH _ (Nat.le_of_lt_succ hn')
    obtain ⟨x, hx⟩ := exists_notMem_finset t
    refine ⟨Finset.cons x t hx, hs.trans (Finset.subset_cons _), ?_⟩
    simp [ht]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ insertionSort r l

Tactic:
rw [hi]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
s : Finset α
f g : α → β
b₁ b₂ : β
⊢ fold op (op b₁ b₂) (fun x ↦ op (f x) (g x)) s = op (fold op b₁ f s) (fold op b₂ g s)

Tactic:
simp only [fold, fold_distrib]

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

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

Tactic:
| head =>

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
l : List α
⊢ IsChain R ([a] ++ l) ↔ IsChain R [a] ∧ IsChain R l ∧ ∀ (x : α), x ∈ [a].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
simp [isChain_cons, and_comm]

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

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l' : List α), (tail✝ ++ l').rotate' tail✝.length = l' ++ tail✝
l' : List α
⊢ (head✝ :: tail✝ ++ l').rotate' (head✝ :: tail✝).length = l' ++ head✝ :: tail✝

Tactic:
simp_all [rotate']

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

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

Tactic:
getElem?_drop,

Goal state after:
case inl
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : m < (drop (n % l.length) l).length
⊢ l[n % l.length + m]? = l[(m + n) % l.length]?
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
l₁ l₂ : List M
h : l₁ <+ l₂
⊢ l₁.prod ∣ l₂.prod

Tactic:
by
  obtain ⟨l, hl⟩ := h.exists_perm_append
  rw [hl.prod_eq, prod_append]
  exact dvd_mul_right _ _

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

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s t : Multiset M
h : s ≤ t
⊢ s.prod ∣ t.prod

Tactic:
obtain ⟨z, rfl⟩ := exists_add_of_le h

Goal state after:
M : Type u_5
inst✝ : CommMonoid M
s z : Multiset M
h : s ≤ s + z
⊢ s.prod ∣ (s + z).prod
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
G : Type u_4
inst✝ : DivisionCommMonoid G
m : Multiset ι
f : ι → G
n : ℤ
⊢ (map (fun i ↦ f i ^ n) m).prod = (map f m).prod ^ n

Tactic:
by
  convert! (m.map f).prod_hom (zpowGroupHom n : G →* G)
  simp only [map_map, Function.comp_apply, zpowGroupHom_apply]

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

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
h : n < (a :: l).cyclicPermutations.length
⊢ n ≤ (a :: l).length

Tactic:
by simpa using h.le

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

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

Tactic:
by
  obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ (s ×ˢ t).Nontrivial ↔ 0 < #s ∧ 0 < #t ∧ (s.Nontrivial ∨ t.Nontrivial)

Tactic:
← one_lt_card_iff_nontrivial,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ 1 < #(s ×ˢ t) ↔ 0 < #s ∧ 0 < #t ∧ (1 < #s ∨ 1 < #t)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ i ! * j ! ∣ (i + j)!

Tactic:
suffices i ! * (i + j - i)! ∣ (i + j)! by
    rwa [Nat.add_sub_cancel_left i j] at this

Goal state after:
i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
ht : ∀ (b : α), a ≠ b → (t b).Nonempty
x : δ a
h : x ∈ t a
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x

Tactic:
choose f hf using ht

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
a : α
inst✝ : DecidableEq (δ a)
x : δ a
h : x ∈ t a
f : (b : α) → a ≠ b → δ b
hf : ∀ (b : α) (a : a ≠ b), f b a ∈ t b
⊢ ∃ a_1 ∈ piFinset t, a_1 a = x
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : ConjClasses α
⊢ a ∈ b.carrier ↔ ConjClasses.mk a = b

Tactic:
revert b

Goal state after:
α : Type u
inst✝ : Monoid α
a : α
⊢ ∀ {b : ConjClasses α}, a ∈ b.carrier ↔ ConjClasses.mk a = b
Module: Mathlib.Algebra.Group.Pi.Lemmas

Goal state before:
pp: α : Type u_5
β : α → Type u_6
γ : (a : α) → β a → Type u_7
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : (a : α) → (b : β a) → One (γ a b)
i : (a : α) × β a
x : γ i.fst i.snd
⊢ curry (Pi.mulSingle i x) = Pi.mulSingle i.fst (Pi.mulSingle i.snd x)

Tactic:
simp only [Pi.mulSingle, Sigma.curry_update, Sigma.curry_one, Pi.one_apply]

Goal state after:
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
g : N →* P
iso : G ≃* N
⊢ (g.comp ↑iso).ker = map (↑iso.symm) g.ker

Tactic:
← comap_ker,

Goal state after:
G : Type u_1
inst✝² : Group G
N : Type u_5
inst✝¹ : Group N
P : Type u_8
inst✝ : MulOneClass P
g : N →* P
iso : G ≃* N
⊢ comap (↑iso) g.ker = map (↑iso.symm) g.ker
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:
← comap_ker,

Goal state after:
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
⊢ comap f g.ker = f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) ↔ ∃ y z, ↑y * ↑z = x

Tactic:
simp only [SetLike.exists, exists_prop]

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
mc : MonoidHomClass F M N
f : F
⊢ map f (closure Set.univ) = map f ⊤

Tactic:
closure_univ

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ map f ⊤ = map f ⊤
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : α
⊢ decodeSum (encodeSum (Sum.inl val✝)) = some (Sum.inl val✝)

Tactic:
simp [encodeSum, div2_val, decodeSum, encodek]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
val✝ : β
⊢ decodeSum (encodeSum (Sum.inr val✝)) = some (Sum.inr val✝)

Tactic:
simp [encodeSum, div2_val, decodeSum, encodek]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = ⊥ ↔ g = 1

Tactic:
by rw [eq_bot_iff, zpowers_le, mem_bot]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
h : G
⊢ h * g * h⁻¹ ∈ iInf a

Tactic:
rw [Subgroup.mem_iInf] at g_in_iInf ⊢

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : ∀ (i : ι), g ∈ a i
h : G
⊢ ∀ (i : ι), h * g * h⁻¹ ∈ a i
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case left.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
c : α j✝
hc : s j✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

pp: case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨i✝, c⟩

Tactic:
· exact Lex.left _ _ hij

Goal state after:
case right.left
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
j✝ : ι
c : α j✝
hk : r i✝ j✝
⊢ Lex r s ⟨i✝, a⟩ ⟨j✝, c⟩

case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨i✝, c⟩
Module: Mathlib.Data.Finset.Max

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

Tactic:
WithTop.map_coe

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ ¬((image (⇑toDual) s).erase (toDual x)).max = ↑(toDual x)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case nil
α : Type u
s : List α
⊢ s ∈ [].sublists' ↔ s <+ []

Tactic:
simp only [sublists'_nil, mem_singleton]
    exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩

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

Goal state before:
pp: case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
⊢ motive (Insert.insert a (s.erase a))

Tactic:
refine insert _ _ (notMem_erase a s) (fun x hx => ?_) (ihs a has)

Goal state after:
case H.inr
α : Type u_2
ι : Type u_5
inst✝¹ : LinearOrder α
inst✝ : DecidableEq ι
f : ι → α
motive : Finset ι → Prop
empty : motive ∅
insert : ∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (Insert.insert a s)
s : Finset ι
ihs : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : (image f s).Nonempty
a : ι
has : a ∈ s
hfa : f a = (image f s).max' hne
x : ι
hx : x ∈ s.erase a
⊢ f x ≤ f a
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
c : ι'
hc : c ∈ s
ha : a ∈ g c
⊢ (Disjoint on f) a b

Tactic:
obtain ⟨d, hd, hb⟩ := hb

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
⊢ (Disjoint on f) a b
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hinj : Set.InjOn (fun x ↦ x ∪ s) ↑(powersetCard (n - #s) (t \ s))
⊢ #({x ∈ powersetCard n t | s ⊆ x}) = (#t - #s).choose (n - #s)

Tactic:
simp only [filter_powersetCard_subset s t n hst hsn, card_image_of_injOn hinj,
             card_powersetCard, card_sdiff_of_subset hst]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image (⇑Embedding.some) (eraseNone s) = s.erase none

Tactic:
Embedding.some_apply,

Goal state after:
α : Type u_1
inst✝ : DecidableEq (Option α)
s : Finset (Option α)
⊢ image some (eraseNone s) = s.erase none
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: case mp
α : Type u_1
s a✝ : Finset α
⊢ a✝ ⊆ s ∧ #a✝ = #s → a✝ = s

Tactic:
exact fun ⟨hs, hc⟩ => eq_of_subset_of_card_le hs hc.ge

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
⊢ Trunc (P α)

Tactic:
by
    apply Trunc.bind (this (Fintype.card α))
    intro h
    apply Trunc.map _ (Fintype.truncEquivFin α)
    intro e
    exact of_equiv (Equiv.ulift.trans e.symm) h

Goal state after: