mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ (s + t).dedup = t.dedup

Tactic:
induction s, t using Quot.induction_on₂
  exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.dedup_append_right h

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ filter (fun x ↦ x ∈ t₁) s ∪ filter (fun x ↦ x ∉ t₁) s = s

pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
· grind

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∈ t₁) s) ⊆ t₁

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁

Tactic:
· grind

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
t₁ t₂ : Set α
h : ↑s ⊆ t₁ ∪ t₂
⊢ ↑(filter (fun x ↦ x ∉ t₁) s) ⊆ t₂ \ t₁
Module: Mathlib.Data.Finset.BooleanAlgebra

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ s ⊆ {a}ᶜ ↔ a ∉ s

Tactic:
subset_compl_comm,

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ {a} ⊆ sᶜ ↔ a ∉ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α ↪ β
g : β ↪ γ
s : Finset α
⊢ (map g (map f s)).val = (map (f.trans g) s).val

Tactic:
simp only [map_val, Multiset.map_map]; rfl

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

Goal state before:
pp: α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p ↔ x ∈ s

Tactic:
H

Goal state after:
α : Type u_1
p : Set α
s : Finset α
H : ∀ (x : α), x ∈ s ↔ x ∈ p
x : α
⊢ x ∈ p ↔ x ∈ p
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
⊢ (∃ s', ↑s' ⊆ s ∧ image f s' = t) → ↑t ⊆ f '' s

Tactic:
· grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).dedup = Multiset.map f s.val
⊢ Set.InjOn f ↑s

Tactic:
Multiset.dedup_eq_self

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
H : (Multiset.map f s.val).dedup.card = s.val.card
this : (Multiset.map f s.val).Nodup
⊢ Set.InjOn f ↑s
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ 0 = ⊤ ↔ n = 1

Tactic:
← bot_eq_zero,

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ ⊥ = ⊤ ↔ n = 1
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
j k : Fin n
⊢ ↑↑j < ↑↑k ↔ j < k

Tactic:
by
  simp only [coe_eq_castSucc, castSucc_lt_castSucc_iff]

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < b ↔ a ≤ b

Tactic:
by
  rw [castSucc_pred_eq_pred_castSucc, pred_castSucc_lt_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hinj : ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s), f a₁ ha₁ = f a₂ ha₂ → a₁ = a₂
hst : #t ≤ #s
f' : ↥s → β := fun a ↦ f ↑a ⋯
hinj' : Set.InjOn f' ↑s.attach
hmapsto' : Set.MapsTo f' ↑s.attach ↑t
a : ↥s
ha : a ∈ ↑s.attach
hb : f' a ∈ t
⊢ ∃ a_1, ∃ (ha : a_1 ∈ s), f' a = f a_1 ha

Tactic:
exact ⟨a, a.2, rfl⟩

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

Goal state before:
pp: α : Type u
m n : ℕ
f : Fin (m * n) → α
i : Fin n
j : Fin m
⊢ m * ↑i + m = m * (↑i + 1)

Tactic:
rw [Nat.mul_add, Nat.mul_one]

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

Goal state before:
pp: case mp
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t

pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t

Tactic:
· grind

Goal state after:
case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case inr.refine_1
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∃ a, s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b

pp: case inr.refine_2
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ a, s = {a}

Tactic:
· grind

Goal state after:
case inr.refine_2
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ a, s = {a}
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inr
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y, x ≠ y ∧ s = {x, y}) → #s = 2

Tactic:
· grind

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3

Tactic:
· grind

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ (∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4

Tactic:
· grind

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

Goal state before:
pp: α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ {z | r z x} ⊂ {z | r z y}

Tactic:
simp_rw [lt_iff_le_not_ge, Finset.subset_iff, mem_filter_univ]

Goal state after:
α : Type u_1
inst✝² : Finite α
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : Std.Irrefl r
val✝ : Fintype α
x y : α
hxy : r x y
⊢ (∀ ⦃x_1 : α⦄, r x_1 x → r x_1 y) ∧ ¬∀ ⦃x_1 : α⦄, r x_1 y → r x_1 x
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons_mem
α : Type u_1
l : List α
x : α
l✝ : List α
a✝ : x ∈ l✝
⊢ x ∈ x :: l✝

Tactic:
exact mem_cons_self

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this✝ : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
this : ∀ (i j : ℕ), j ≤ i → (#(g i) - 1 = #(g j) - 1 ↔ g i = g j)
hij : ¬j ≤ i
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j

pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
hij : j ≤ i
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j

Tactic:
· grind

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
hg : Antitone g
i j : ℕ
hij : j ≤ i
⊢ #(g i) - 1 = #(g j) - 1 ↔ g i = g j
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 ∈ b :: m

Tactic:
exact mem_cons_self

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

Goal state before:
pp: case mpr.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ ∀ (ix : ℕ),
    l[ix]? = l'[(OrderEmbedding.ofStrictMono (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ⋯) ix]?

Tactic:
· grind

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
⊢ a :: orderedInsert r x as <+ x :: b :: bs

Tactic:
have hba := pairwise_cons.mp hb |>.left _ (mem_of_cons_sublist ‹a :: as <+ bs›)

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
x a : α
as : List α
b : α
bs : List α
hb : Pairwise r (b :: bs)
a✝ : a :: as <+ bs
hr : ¬r x a
h✝ : r x b
hba : r b a
⊢ a :: orderedInsert r x as <+ x :: b :: bs
Module: Mathlib.Data.List.Sort

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

pp: case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
· grind

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
a b : α
l : List α
h : Pairwise r (b :: l)
h' : ¬r a b
⊢ Pairwise r (List.orderedInsert r a (b :: l))
Module: Mathlib.Data.List.Range

Goal state before:
pp: a : ℕ
l : List ℕ
hl : map length l.ranges = l
| l

Tactic:
rw [← hl]

Goal state after:
a : ℕ
l : List ℕ
hl : map length l.ranges = l
| map length l.ranges
Module: Mathlib.Data.List.ProdSigma

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
l₂ : List β
x : α
l₁ : List α
IH : (l₁ ×ˢ l₂).length = l₁.length * l₂.length
⊢ ((x :: l₁) ×ˢ l₂).length = (x :: l₁).length * l₂.length

Tactic:
| cons x l₁ IH =>

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
hs : s ≠ ∅
p_s : ∀ (a : M), a ∈ s → p a
⊢ p s.prod

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: α : Type u
l : List α
a : α
n : ℕ
⊢ (a :: l).rotate' (n + 1) = (l ++ [a]).rotate' n

Tactic:
rotate'_cons_succ

Goal state after:
α : Type u
l : List α
a : α
n : ℕ
⊢ (l ++ [a]).rotate' n = (l ++ [a]).rotate' n
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (hd :: tl).rotate' (n + 1) ~ hd :: tl

Tactic:
rotate'_cons_succ

Goal state after:
case succ.cons
α : Type u
n : ℕ
hn : ∀ (l : List α), l.rotate' n ~ l
hd : α
tl : List α
⊢ (tl ++ [hd]).rotate' n ~ hd :: tl
Module: Mathlib.Data.List.Chain

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

Tactic:
cases m with
  | nil => grind
  | cons b bs =>
    apply hm.cons_cons
    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.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
α : Type u_2
σ : α → Type u_8
l₂ : (a : α) → List (σ a)
x : α
l₁ : List α
IH : (l₁.sigma l₂).length = (map (fun a ↦ (l₂ a).length) l₁).sum
⊢ ((x :: l₁).sigma l₂).length = (map (fun a ↦ (l₂ a).length) (x :: l₁)).sum

Tactic:
| cons x l₁ IH =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
s : Multiset α
⊢ f s = g s

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]

Tactic:
getElem_rotate

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = l[((l.length - n % l.length + k) % l.length + n) % l.length]
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False

Tactic:
exact hne rfl

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
ι : Type u_4
s : Multiset ι
t : ι → Multiset α
b : ι → α
b₀ : α
⊢ fold op (fold op b₀ (map b s)) (s.bind t) = fold op b₀ (map (fun i ↦ fold op (b i) (t i)) s)

Tactic:
induction s using Multiset.induction_on with

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

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l.cyclicPermutations ~r l'.cyclicPermutations

Tactic:
by
  obtain ⟨k, rfl⟩ := h
  exact ⟨k, by simp⟩

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

Goal state before:
pp: case inl
n k s : ℕ
hsk : s ≤ k
hnk : n < k
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

pp: case inr
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)

Tactic:
· grind

Goal state after:
case inr
n k s : ℕ
hsk : s ≤ k
hkn : k ≤ n
⊢ n.choose k * k.choose s = n.choose s * (n - s).choose (k - s)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
rwa [Nat.add_sub_cancel_left i j] at this

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

Goal state before:
pp: α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(s.piDiag ι) = #s

Tactic:
by rw [piDiag, card_image_of_injective _ const_injective]

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

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

Tactic:
apply Nat.mul_right_cancel (n + k - k).factorial_pos

Goal state after:
n k : ℕ
⊢ (n + 1).ascFactorial k * (n + k - k)! = (n + k).choose k * k ! * (n + k - k)!
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr.inr
n k : ℕ
hk : n < k
⊢ n.choose k = 1 ↔ k = 0 ∨ n = k

Tactic:
· grind

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
cases n <;> aesop

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_2
p : ι → Subgroup G
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
closure_iUnion,

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_2
p : ι → Subgroup G
⊢ ⨆ i, p i = ⨆ i, closure ↑(p i)
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
h : f.ker = ⊥
x y : G
hxy : f x = f y
⊢ x = y

Tactic:
eq_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y⁻¹ * x ∈ f.ker
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case refine_4
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h : x ∈ closure (↑s ∪ ↑t)
y : C
hy : y ∈ s
z : C
hz : z ∈ t
hx✝ : y * z ∈ closure (↑s ∪ ↑t)
⊢ ∃ y_1 ∈ s, ∃ z_1 ∈ t, y_1 * z_1 = (y * z)⁻¹

Tactic:
exact ⟨_, inv_mem hy, _, inv_mem hz, mul_comm z y ▸ (mul_inv_rev z y).symm⟩

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

Goal state before:
pp: case succ
m n : ℕ
IH : (m * n).bodd = (m.bodd && n.bodd)
⊢ (m.bodd && n.bodd ^^ m.bodd) = (m.bodd && !n.bodd)

Tactic:
cases bodd m <;> cases bodd n <;> rfl

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (decode₂ α x).isSome = true

Tactic:
← hn,

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝ : Encodable α
x : ℕ
x✝ : (fun x ↦ x ∈ Set.range encode) x
n : α
hn : encode n = x
⊢ (decode₂ α (encode n)).isSome = true
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
s : Set G
N : Subgroup G
inst✝ : N.Normal
h : s ⊆ ↑N
⊢ normalClosure s ≤ N

Tactic:
intro a w
  refine closure_induction (fun x hx => ?_) ?_ (fun x y _ _ ihx ihy => ?_) (fun x _ ihx => ?_) w
  · exact conjugatesOfSet_subset h hx
  · exact one_mem _
  · exact mul_mem ihx ihy
  · exact inv_mem ihx

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

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : αᵐᵒᵖ
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ s ∧ b ∈ t) ∧ a⁻¹ * b = unop x

Tactic:
constructor
  · rintro ⟨a, h, ha⟩
    obtain ⟨b, hb, rfl⟩ := mem_smul_set.mp h
    exact ⟨b, x • b, ⟨hb, ha⟩, by simp⟩
  · rintro ⟨a, b, ⟨ha, hb⟩, H⟩
    have : MulOpposite.op (a⁻¹ * b) = x := congr_arg MulOpposite.op H
    exact ⟨b, mem_inter (mem_smul_set.mpr ⟨a, ha, by simp [← this]⟩) hb⟩

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ Sum.inr ⟨↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x), ⋯⟩ = Sum.inr x

pp: case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)

Tactic:
· grind

Goal state after:
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
s : Submonoid M
hs : s ∈ S
⊢ ∀ {x : M}, x ∈ s → x ∈ sSup S

Tactic:
rw [← SetLike.le_def]
  exact le_sSup hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
u : Finset (α ⊕ β)
⊢ map Embedding.inr t ⊆ u ↔ t ⊆ u.toRight

Tactic:
by
  simp [← empty_disjSum, disjSum_subset]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l₁ l₂ : List α
⊢ (l₁ ++ l₂).maximum = max l₁.maximum l₂.maximum

Tactic:
by
  induction l₁ with
  | nil => simp
  | cons _ _ ih => rw [maximum_cons, cons_append, maximum_cons, ih, ← max_assoc]

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

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

Tactic:
by rw [← TopHom.comp_apply, h, TopHom.comp_apply]

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

Goal state before:
pp: case empty
α : Type u_2
inst✝ : LinearOrder α
a✝ : α
⊢ ∅.max = ↑a✝ → a✝ ∈ ∅

Tactic:
H

Goal state after:
case empty
α : Type u_2
inst✝ : LinearOrder α
a✝ : α
H : ∅.max = ↑a✝
⊢ a✝ ∈ ∅
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
⊢ powersetCardAux n l = List.map ofList (sublistsLen n l)

Tactic:
rw [powersetCardAux, sublistsLenAux_eq, append_nil]

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.sublists ~ l.sublists'

Tactic:
← map_get_finRange l,

Goal state after:
α : Type u
l : List α
⊢ (map l.get (finRange l.length)).sublists ~ (map l.get (finRange l.length)).sublists'
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inr.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i ↦ ⨆ i' ∈ t, f (i, i')) (j, j').1

Tactic:
convert! le_iSup₂ (α := α) j' hj.2; rfl

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

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
⊢ (s ×ˢ t).PairwiseDisjoint f ↔
    (s.PairwiseDisjoint fun i ↦ ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' ↦ ⨆ i ∈ s, f (i, i')

Tactic:
refine
      ⟨fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩, fun h => h.1.prod_left h.2⟩ <;>
    simp_rw [Function.onFun, iSup_disjoint_iff, disjoint_iSup_iff]

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
⊢ ∀ i_1 ∈ t, ∀ i_3 ∈ t, Disjoint (f (i, i_1)) (f (j, i_3))

case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
⊢ ∀ i_1 ∈ s, ∀ i_3 ∈ s, Disjoint (f (i_1, i)) (f (i_3, j))
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ∈ powersetCard n (map f s) ↔ t ∈ map (mapEmbedding f).toEmbedding (powersetCard n s)

Tactic:
simp only [mem_powersetCard, mem_map]

Goal state after:
α : Type u_1
β : Type u_2
f : α ↪ β
n : ℕ
s : Finset α
t : Finset β
⊢ t ⊆ map f s ∧ #t = n ↔ ∃ a, (a ⊆ s ∧ #a = n) ∧ (mapEmbedding f).toEmbedding a = t
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) = ⨆ a ∈ s, f a

Tactic:
← ciSup_subtype_fun hf hf',

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 (f '' s) = ⨆ i, f ↑i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → x = b → α
⊢ f b ⋯ ∈ upperBounds (⋃ i, range (f i))

Tactic:
rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → x = b → α
⊢ f b ⋯ ≤ f b ⋯
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ∈ upperBounds (⋃ i, range (f i))

Tactic:
rintro a ⟨_, ⟨b, rfl⟩, ⟨rfl, rfl⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
b : β
f : (x : β) → b = x → α
⊢ f b ⋯ ≤ f b ⋯
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
a : α
b₁ b₂ : β
⊢ (a, b₁) ⋖ (a, b₂) ↔ b₁ ⋖ b₂

Tactic:
simp_rw [covBy_iff_wcovBy_and_lt, mk_wcovBy_mk_iff_right, mk_lt_mk_iff_right]

Goal state after:
Module: Mathlib.Order.Cover

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

Tactic:
exact Or.inl ⟨mk_covBy_mk_iff_left.1 h, rfl⟩

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

Goal state before:
pp: case inr
s : Set ℕ
m : ℕ
hm : m < sInf s
h : s.Nonempty
⊢ m ∉ s

Tactic:
rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm

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

Goal state before:
pp: ⊢ sSup ∅ = ⊥

Tactic:
simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
        not_false_iff, exists_const]

Goal state after:
⊢ Nat.find ⋯ = ⊥