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

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ b :: List.filter (fun a ↦ elem a (take n l)) l =
    b :: List.filter (fun a ↦ elem a (b :: List.filter (fun a ↦ elem a (take n l)) l)) l

Tactic:
congr 1

Goal state after:
case e_tail
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
b : α
l : List α
n : ℕ
hl : (b :: l).Nodup
⊢ List.filter (fun a ↦ elem a (take n l)) l =
    List.filter (fun a ↦ elem a (b :: List.filter (fun a ↦ elem a (take n l)) l)) l
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ l₂.erase head✝ <+ l₂

Tactic:
grind [erase_sublist]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
⊢ count a (s ∪ t) = max (count a s) (count a t)

Tactic:
simp [(· ∪ ·), union, Nat.sub_add_eq_max]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
⊢ ∀ (a : α), a ∈ s → p a ∨ ¬p a

Tactic:
· simp only [implies_true, Decidable.em]

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

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

Tactic:
rw [Multiset.mem_toFinset, ← mem_def]

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

Goal state before:
pp: case hl
α : Type u_1
l : List α
n : ℕ
⊢ (take n l).inits.length = (take (n + 1) l.inits).length

Tactic:
(simp [take_take] <;> grind)

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

Goal state before:
pp: case h
α : Type u_1
l : List α
n : ℕ
⊢ ∀ (i : ℕ) (h₁ : i < (take n l).inits.length) (h₂ : i < (take (n + 1) l.inits).length),
    (take n l).inits[i] = (take (n + 1) l.inits)[i]

Tactic:
(simp [take_take] <;> grind)

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ s = {a} ∨ s.Nontrivial

Tactic:
← coe_eq_singleton

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∈ s
⊢ ↑s = {a} ∨ s.Nontrivial
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: case cons.inl
α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
a : α
ha : a ∉ ∅
h : ∀ (hs : ∅.Nonempty), motive ∅ hs
hs : (Finset.cons a ∅ ha).Nonempty
⊢ motive (Finset.cons a ∅ ha) hs

Tactic:
exact singleton a

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

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)

Tactic:
rintro a ⟨_, hp⟩ ⟨_, hq⟩

Goal state after:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ a ∈ image (fun i ↦ f i) (range n)

Tactic:
simp only [mem_image, mem_range]

Goal state after:
case mp
α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
i : ℕ
hi : f i = a
⊢ ∃ a_1 < n, f a_1 = a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : ℕ → α
a : α
n : ℕ
hn : 0 < n
h : ∀ (i : ℕ), f (i % n) = f i
⊢ a ∈ Set.range f ↔ a ∈ image (fun i ↦ f i) (range n)

Tactic:
by
  constructor
  · rintro ⟨i, hi⟩
    simp only [mem_image, mem_range]
    exact ⟨i % n, Nat.mod_lt i hn, (rfl.congr hi).mp (h i)⟩
  · rintro h
    simp only [mem_image, Set.mem_range, mem_range] at *
    rcases h with ⟨i, _, ha⟩
    exact ⟨i, ha⟩

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h : j ≤ i
⊢ i = j

Tactic:
obtain h | rfl := h.lt_or_eq
    · exact (this hij.symm h).symm
    · rfl

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

Goal state before:
pp: case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a ↦ i ↑a ⋯) s.attach) = #t

Tactic:
congr 1

Goal state after:
case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ image (fun a ↦ i ↑a ⋯) s.attach = t
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i ≤ ↑n

Tactic:
rw [Fin.natCast_eq_last]

Goal state after:
n : ℕ
i : Fin (n + 1)
⊢ i ≤ last n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n a b : ℕ
han : a ≤ n
hbn : b ≤ n
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
rw [← Nat.lt_succ_iff] at han hbn
  simp [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, han, hbn]

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

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

Tactic:
rw [Fin.succAbove_of_castSucc_lt]

Goal state after:
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 = 0

case h
n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = n

Tactic:
refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
  intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
  obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
  exact ⟨u.erase a, by grind⟩

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

Goal state before:
pp: n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
obtain h | h := a.castSucc.lt_or_ge b

Goal state after:
case inl
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

case inr
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #sᶜ + #s = Fintype.card α

Tactic:
by
  rw [Nat.add_comm, card_add_card_compl]

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

Goal state before:
pp: case right
α : Sort u_1
m n : ℕ
xs : Fin m → α
ys : Fin n → α
i✝ : Fin n
⊢ append xs ys (natAdd m i✝) = append (ys ∘ rev) (xs ∘ rev) (Fin.cast ⋯ (natAdd m i✝).rev)

Tactic:
simp [cast_rev, rev_addNat]

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

Goal state before:
pp: case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = l.get (f ⟨0, ⋯⟩) ∧ x = l.get (f ⟨1, ⋯⟩)

Tactic:
← hf,

Goal state after:
case mp
α : Type u_1
l : List α
x : α
f : Fin (replicate 2 x).length ↪o Fin l.length
hf : ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)
⊢ x = (replicate 2 x).get ⟨0, ⋯⟩ ∧ x = l.get (f ⟨1, ⋯⟩)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
h : ∅.Infinite
⊢ False

Tactic:
exact h finite_empty

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

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
h : ∀ (t : Set γ), t.Finite → ∃ c, P c t
⊢ ∃ u, ∀ (n : ℕ), P (u n) (u '' Iio n)

Tactic:
have : Nonempty γ := (h ∅ finite_empty).nonempty
  choose! c hc using h
  set f : (n : ℕ) → (g : (m : ℕ) → m < n → γ) → γ := fun n g => c (range fun k : Iio n => g k.1 k.2)
  set u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
  refine ⟨u, fun n ↦ ?_⟩
  convert! hc (u '' Iio n) ((finite_lt_nat _).image _)
  rw [image_eq_range]
  exact Nat.strongRecOn_eq f n

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
⊢ Pairwise (fun a b ↦ decide (r a b) = true) l'

Tactic:
by simpa using h'

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a c : α
l₁ l₂ : List α
⊢ IsChain R (a :: (l₁ ++ c :: l₂)) ↔ IsChain R (a :: (l₁ ++ [c])) ∧ IsChain R (c :: l₂)

Tactic:
← cons_append,

Goal state after:
α : Type u_1
R : α → α → Prop
a c : α
l₁ l₂ : List α
⊢ IsChain R (a :: l₁ ++ c :: l₂) ↔ IsChain R (a :: l₁ ++ [c]) ∧ IsChain R (c :: l₂)
Module: Mathlib.Data.List.Chain

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

Tactic:
← cons_append,

Goal state after:
α : Type u_1
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ R a b ∧ IsChain R (b :: l₁ ++ l₂) ↔
    (R a b ∧ IsChain R (b :: l₁)) ∧
      IsChain R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: case cons
M : Type u_8
inst✝ : CommMonoid M
m : M
L : List M
ih : IsUnit L.prod → ∀ (m : M), m ∈ L → IsUnit m
h : IsUnit (m :: L).prod
⊢ ∀ (m_1 : M), m_1 ∈ m :: L → IsUnit m_1

Tactic:
| cons m L ih =>

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

Goal state before:
pp: case cons
α : 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 +
      (map (fun i ↦ if (a == i) = true then 1 else 0) (filter p (a :: as).dedup)).sum =
    countP p as + if p a = true then 1 else 0

Tactic:
congr 1

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 ↦ count i as) (filter p (a :: as).dedup)).sum = countP p as

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.Data.List.Rotate

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

Tactic:
congr 1

Goal state after:
case inr.e_a
α : Type u
l : List α
n m : ℕ
hml : m < l.length
hm : (drop (n % l.length) l).length ≤ m
hlt : n % l.length < l.length
⊢ m - (l.length - n % l.length) = (m + n) % l.length
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
⊢ ∀ (l : List M), op l.prod = (map op l).reverse.prod

Tactic:
by
  intro l; induction l with
  | nil => rfl
  | cons x xs ih =>
    rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

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

Goal state before:
pp: case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
specialize acc a _

Goal state after:
case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : ∀ (a_1 : α), a_1 ∈ (↑⟨a :: l, hl⟩).head? → Acc r a_1
⊢ a ∈ (↑⟨a :: l, hl⟩).head?

case cons
α : Type u_1
r : α → α → Prop
a : α
l : List α
hl : List.IsChain (flip r) (a :: l)
acc : Acc r a
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ ∀ (a : List α),
    (bind (Quot.mk (⇑(List.isSetoid α)) a) f).Nodup ↔
      (∀ (a_1 : α), a_1 ∈ Quot.mk (⇑(List.isSetoid α)) a → (f a_1).Nodup) ∧
        Pairwise (fun x y ↦ Disjoint (f x) (f y)) (Quot.mk (⇑(List.isSetoid α)) a)

Tactic:
simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise]

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

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (if x ∈ s.dedup.bind f then 1 else 0) = if x ∈ s.bind f then 1 else 0

Tactic:
congr 1

Goal state after:
case e_c
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (x ∈ s.dedup.bind f) = (x ∈ s.bind f)
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ (map (fun i ↦ f i - g i + g i) l).sum = (map f l).sum

Tactic:
congr 1

Goal state after:
ι : Type u_2
M : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : ExistsAddOfLE M
inst✝³ : AddLeftMono M
inst✝² : AddLeftReflectLE M
inst✝¹ : Sub M
inst✝ : OrderedSub M
l : Multiset ι
f g : ι → M
hfg : ∀ (x : ι), x ∈ l → g x ≤ f x
⊢ map (fun i ↦ f i - g i + g i) l = map f l
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
a : α
l : List α
⊢ flatMap (fun x ↦ map (Prod.mk x.fst) ((a :: l).eraseIdx x.snd)) ((a, 0) :: map (Prod.map id fun x ↦ x + 1) l.zipIdx) ~
    map (fun x ↦ (a, x)) l ++ map (fun x ↦ (x, a)) l ++
      flatMap (fun x ↦ map (Prod.mk x.fst) (l.eraseIdx x.snd)) l.zipIdx

Tactic:
have : map (fun x ↦ (x.fst, a)) l.zipIdx = map (·, a) l := by
    conv_rhs => rw [← zipIdx_map_fst 0 l, map_map, Function.comp_def]

Goal state after:
α : Type u_1
a : α
l : List α
this : map (fun x ↦ (x.fst, a)) l.zipIdx = map (fun x ↦ (x, a)) l
⊢ flatMap (fun x ↦ map (Prod.mk x.fst) ((a :: l).eraseIdx x.snd)) ((a, 0) :: map (Prod.map id fun x ↦ x + 1) l.zipIdx) ~
    map (fun x ↦ (a, x)) l ++ map (fun x ↦ (x, a)) l ++
      flatMap (fun x ↦ map (Prod.mk x.fst) (l.eraseIdx x.snd)) l.zipIdx
Module: Mathlib.Data.Fintype.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
⊢ Infinite ((i : ι) → π i)

Tactic:
choose m n hm using fun i => exists_pair_ne (π i)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
π : ι → Type u_5
inst✝¹ : ∀ (i : ι), Nontrivial (π i)
inst✝ : Infinite ι
m n : (i : ι) → π i
hm : ∀ (i : ι), m i ≠ n i
⊢ Infinite ((i : ι) → π i)
Module: Mathlib.Data.Fintype.Pi

Goal state before:
pp: case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
a : α
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ ∅) = ∅

pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t

Tactic:
· have : Nonempty α := ⟨a⟩
    simp

Goal state after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
β : Type u_5
inst✝ : DecidableEq β
t : Finset β
a : α
ht : t.Nonempty
⊢ image (fun f ↦ f a) (piFinset fun _i ↦ t) = t
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_5
f : α → β → γ
s : Set α
t : ι → Set β
⊢ image2 f s (⋃ i, t i) = ⋃ i, image2 f s (t i)

Tactic:
by
  simp only [← image_prod, prod_iUnion, image_iUnion]

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

Goal state before:
pp: case mem.one
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
⊢ motive 1 z ⋯ ⋯

Tactic:
| one =>

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

Goal state before:
pp: case one
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 : M
hx : x ∈ closure s
⊢ motive x 1 hx ⋯

Tactic:
| one =>

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : MulOneClass M
motive : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ motive 1

Tactic:
| one =>

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

Goal state before:
pp: case one
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p 1

Tactic:
| one =>

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

Goal state before:
pp: case a.one
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
⊢ 1 ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
| one =>

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
by
  simp_rw [Submonoid.closure_iUnion, Submonoid.closure_eq]

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

Goal state before:
pp: case mem.one
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
⊢ p 1 z ⋯ ⋯

Tactic:
| one =>

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

Goal state before:
pp: case one
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 : G
hx : x ∈ closure k
⊢ p x 1 hx ⋯

Tactic:
| one =>

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
N : Type u_5
P : Type u_6
inst✝² : Group N
inst✝¹ : Group P
K : Subgroup G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
x : G
hx : f x = 1
⊢ f x * f x⁻¹ = 1

Tactic:
by rw [← map_mul, mul_inv_cancel, map_one]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
s : Set N
x : G
hx : x ∈ ⇑f ⁻¹' s
⊢ f x ∈ closure s

Tactic:
exact subset_closure hx

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
f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ≤ K ⊔ f.ker

Tactic:
by
  rw [map_le_iff_le_comap, comap_map_eq]

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

Goal state before:
pp: m n : ℕ
⊢ pair m n < (max m n + 1) ^ 2

Tactic:
simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]

Goal state after:
m n : ℕ
⊢ (if m < n then n * n + m else m * m + (m + n)) < max m n * max m n + (max m n + (max m n + 1))
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case mp.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
hb : (map f) 1 = of d
⊢ ∃ a, f a = d

Tactic:
| one =>

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

Goal state before:
pp: case mpr.one
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
⊢ ∃ a, (map f) a = 1

Tactic:
| one =>

Goal state after:
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✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hij : r i✝ i✝
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

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✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

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✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

Tactic:
· exact (irrefl _ hij).elim

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✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hji : r i✝ i✝
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩

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✝¹ : Std.Asymm r
inst✝ : ∀ (i : ι), Std.Antisymm (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
hba : s i✝ b a
⊢ ⟨i✝, a⟩ = ⟨i✝, b⟩
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: case one
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
h : (FreeMonoid.lift Subtype.val) 1 ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) 1) h

Tactic:
| one =>

Goal state after: