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

Goal state before:
pp: case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
⊢ hd :: tl <+ l'

Tactic:
let f' : ℕ ↪o ℕ :=
    OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b => by
      rw [Nat.sub_le_sub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos

Goal state after:
case cons
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
⊢ hd :: tl <+ l'
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: case mp.slnil
α : Type u_1
l l' : List α
⊢ ∃ f, ∀ (ix : ℕ), [][ix]? = [][f ix]?

Tactic:
| slnil =>

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

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ #(range n) = n

Tactic:
card_range

Goal state after:
α : Type u_4
inst✝ : Infinite α
n : ℕ
⊢ n = n
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : (i.succAbove j).castPred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
rw [castPred_succAbove _ _ hlt] at hk

Goal state after:
case pos
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : j.castSucc < i
H₁ : i.succAbove j ≠ last n
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : 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
this : ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'
⊢ Pairwise r (List.orderedInsert r a (b :: l))

Tactic:
simpa [orderedInsert_cons, h', h.of_cons.orderedInsert a l]

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

Goal state before:
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
⊢ ∀ (b' : α), b' ∈ List.orderedInsert r a l → r b b'

Tactic:
intro b'

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
b' : α
⊢ b' ∈ List.orderedInsert r a l → r b b'
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: γ : Type u_1
P : γ → Set γ → Prop
this : Nonempty γ
c : Set γ → γ
hc : ∀ (t : Set γ), t.Finite → P (c t) t
f : (n : ℕ) → ((m : ℕ) → m < n → γ) → γ := fun n g ↦ c (range fun k ↦ g ↑k ⋯)
u : ℕ → γ := fun n ↦ Nat.strongRecOn n f
n : ℕ
⊢ u n = c (range fun x ↦ u ↑x)

Tactic:
exact Nat.strongRecOn_eq f n

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

Goal state before:
pp: α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑s + 1

Tactic:
rw [← card_fintypeInsertOfNotMem s h]

Goal state after:
α : Type u
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
d : Fintype ↑(insert a s)
⊢ Fintype.card ↑(insert a s) = Fintype.card ↑(insert a s)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
s : Set β
f : α → β
hi : Injective f
hf : ∀ (x : α), f x ∈ s
⊢ s.Infinite

Tactic:
rw [← range_subset_iff] at hf
  exact (infinite_range_of_injective hi).mono hf

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i < Fin.find p h ↔ ∀ (m : Fin n), m ≤ i → ¬p m

Tactic:
by
  simp_rw [← not_le, find_le_iff, not_exists, not_and]

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

Goal state before:
pp: case inr.inl
n : ℕ
α : Sort u_1
β : Sort u_2
opα : α → α → α
opβ : β → β → β
f : α → β
hf : ∀ (x y : α), f (opα x y) = opβ (f x) (f y)
j : Fin (n + 1)
g : Fin (n + 1) → α
x : Fin n
h : ↑x = ↑j
⊢ (f ∘ j.contractNth opα g) x = j.contractNth opβ (f ∘ g) x

Tactic:
simp only [Function.comp_apply, contractNth_apply_of_eq, h, hf]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
l₁ : List α
h : Lex r l₁ []
⊢ False

Tactic:
by cases h

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

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

Tactic:
simp_rw [isChain_iff_forall₂, dropLast_concat, cons_append, tail_cons]

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

Goal state before:
pp: α : Type u_1
l : List α
p : α → Prop
h : ∀ (x : α), x ∈ l → p x
r : { a // p a } → { a // p a } → Prop
⊢ IsChain r (l.attachWith p h) ↔ IsChain (fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩) l

Tactic:
by
  induction l with grind +splitIndPred

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

Tactic:
rcases l.length.zero_le.eq_or_lt with hl | hl

Goal state after:
case inl
α : Type u
l : List α
n : ℕ
hl : 0 = l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l

case inr
α : Type u
l : List α
n : ℕ
hl : 0 < l.length
⊢ l.rotate n = drop (n % l.length) l ++ take (n % l.length) l
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
n : ℕ
h0 : n ≠ 0
⊢ a ∈ n • s ↔ a ∈ s

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : β → Multiset γ
f : α → β
⊢ ∀ (a : α) (s : Multiset α),
    ((map f s).bind n = s.bind fun a ↦ n (f a)) → (map f (a ::ₘ s)).bind n = (a ::ₘ s).bind fun a ↦ n (f a)

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
s : Multiset α
f : α → Multiset β
g : β → Multiset γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind f).bind g = s.bind fun a ↦ (f a).bind g) → ((a ::ₘ s).bind f).bind g = (a ::ₘ s).bind fun a ↦ (f a).bind g

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → Multiset γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind fun a ↦ n.bind fun b ↦ f a b) = n.bind fun b ↦ s.bind fun a ↦ f a b) →
      ((a ::ₘ s).bind fun a ↦ n.bind fun b ↦ f a b) = n.bind fun b ↦ (a ::ₘ s).bind fun a ↦ f a b

Tactic:
by simp +contextual

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind fun a ↦ map (fun b ↦ f a b) n) = n.bind fun b ↦ map (fun a ↦ f a b) s) →
      ((a ::ₘ s).bind fun a ↦ map (fun b ↦ f a b) n) = n.bind fun b ↦ map (fun a ↦ f a b) (a ::ₘ s)

Tactic:
by simp +contextual

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

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

Tactic:
← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)

Goal state after:
n k : ℕ
hk : k.succ ≤ n + 1
hk₁ : k.succ < n + 1
h : n.choose k * k.succ ! * (n - k)! = (k + 1) * n !
h₁ : (n - k)! = (n - k) * (n - k.succ)!
⊢ n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * (n.choose k.succ * k.succ ! * (n - k.succ)!)
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
have h : choose n k * k.succ ! * (n - k)! = (k + 1) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_succ_le_succ hk)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
      have h₁ : (n - k)! = (n - k) * (n - k.succ)! := by
        rw [← succ_sub_succ, succ_sub (le_of_lt_succ hk₁), factorial_succ]
      have h₂ : choose n (succ k) * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n ! := by
        rw [← choose_mul_factorial_mul_factorial (le_of_lt_succ hk₁)]
        simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]
      have h₃ : k * n ! ≤ n * n ! := Nat.mul_le_mul_right _ (le_of_succ_le_succ hk)
      rw [choose_succ_succ, Nat.add_mul, Nat.add_mul, succ_sub_succ, h, h₁, h₂, Nat.add_mul,
        Nat.mul_sub_right_distrib, factorial_succ, ← Nat.add_sub_assoc h₃, Nat.add_assoc,
        ← Nat.add_mul, Nat.add_sub_cancel_left, Nat.add_comm]

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
b : β
⊢ DependsOn (fun x ↦ b) ∅

Tactic:
by simp [DependsOn]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ f₁ a' h' = cons s a b f₁ a' this

Tactic:
by rw [Pi.cons_ne this ne.symm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
a : α
b : δ a
s : Multiset α
hs : ¬a ∈ s
f₁ f₂ : (a : α) → a ∈ s → δ a
eq : cons s a b f₁ = cons s a b f₂
a' : α
h' : a' ∈ s
ne : a ≠ a'
this : a' ∈ a ::ₘ s
⊢ cons s a b f₂ a' this = f₂ a' h'

Tactic:
by rw [Pi.cons_ne this ne.symm]

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

Goal state before:
pp: case neg.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
⊢ ∀ (a_1 : β a'),
    a_1 ∈ t a' →
      map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' a_1 x)) n ≍
        map (fun x ↦ Pi.cons (a ::ₘ m) a' a_1 (Pi.cons m a b x)) n

Tactic:
intro b'

Goal state after:
case neg.hf.hf
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m✝ : Multiset α
t : (a : α) → Multiset (β a)
a a' : α
m : Multiset α
n : Multiset ((a : α) → a ∈ m → β a)
eq : ¬a = a'
b : β a
a✝ : b ∈ t a
b' : β a'
⊢ b' ∈ t a' →
    map (fun x ↦ Pi.cons (a' ::ₘ m) a b (Pi.cons m a' b' x)) n ≍
      map (fun x ↦ Pi.cons (a ::ₘ m) a' b' (Pi.cons m a b x)) n
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ ((p + 1) * n).choose n = (p + 1) * ((p + 1) * n - 1).choose (n - 1)

Tactic:
rw [Nat.add_mul, Nat.one_mul, choose_mul_add hn]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
⊢ ∀ (a : α) (s : Multiset α),
    (s.pi t).card = (map (fun a ↦ (t a).card) s).prod →
      ((a ::ₘ s).pi t).card = (map (fun a ↦ (t a).card) (a ::ₘ s)).prod

Tactic:
by simp +contextual

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (f a)

Tactic:
exact ⟨ConjClasses.mk a, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t

Tactic:
compl_union,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
s : Set M
inst✝ : Mul N
f g : M →ₙ* N
a✝ b✝ : M
hx : f a✝ = g a✝
hy : f b✝ = g b✝
⊢ a✝ * b✝ ∈ {x | f x = g x}

Tactic:
simp [*]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
s : Set M
inst✝ : MulOneClass N
f g : M →* N
a✝ b✝ : M
hx : f a✝ = g a✝
hy : f b✝ = g b✝
⊢ a✝ * b✝ ∈ {x | f x = g x}

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = (Prod.mk '' s).seq t

Tactic:
by
  rw [seq_eq_image2, image2_image_left, image2_mk_eq_prod]

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
P : C → Prop
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]

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

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (fun n ↦ (decode n).getD d) (encode x) = x

Tactic:
simp_rw [Encodable.encodek]

Goal state after:
α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (some x).getD d = x
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ ↑a.unop} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}

Tactic:
Subgroup.coe_unop

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ sInf {a | s ⊆ MulOpposite.op ⁻¹' ↑a} = sInf {K | MulOpposite.unop ⁻¹' s ⊆ ↑K}
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s ↔ ⇑(MulAut.conj g) '' s = s

Tactic:
mem_set_normalizer_iff'',

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ (∀ (h : G), h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ⇑(MulAut.conj g) '' s = s
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
x✝ : IsIdempotentElem (a ^ n)
⊢ a ^ n.succ * a ^ n.succ = (a * a) ^ n.succ

Tactic:
rw [← sq, ← sq, ← pow_mul, ← pow_mul']

Goal state after:
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : CancelMonoid M
a : M
⊢ IsIdempotentElem a ↔ a = 1

Tactic:
by simp [IsIdempotentElem]

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

Goal state before:
pp: case nil
α : Type u_1
⊢ toList [].prod = (List.map ⇑toList []).flatten

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u_1
head✝ : FreeMonoid α
tail✝ : List (FreeMonoid α)
tail_ih✝ : toList tail✝.prod = (List.map (⇑toList) tail✝).flatten
⊢ toList (head✝ :: tail✝).prod = (List.map (⇑toList) (head✝ :: tail✝)).flatten

Tactic:
simp [*]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A' A B : Subgroup G
hN : (A'.subgroupOf A).Normal
⊢ ((A' ⊓ B).subgroupOf (A ⊓ B)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
  rw [inf_inf_inf_comm, inf_idem]
  exact le_trans (inf_le_inf hN B.le_normalizer) inf_normalizer_le_normalizer_inf

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

Goal state before:
pp: case slnil
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h₁ : ∀ (a : M), a ∈ [] → 1 ≤ a
⊢ [].prod ≤ [].prod

Tactic:
| slnil =>

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

Goal state before:
pp: case neg
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
hl_empty : ¬l = []
hla_restrict : ∀ (x : α), x ∈ l → p x
hp_sup : p l.prod
hp_a : p a
⊢ f (a * l.prod) ≤ f a * (map f l).prod

Tactic:
grw [h_mul a _ hp_a hp_sup, ← ih hl_empty hla_restrict]

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

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯
one : motive 1 ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯
x : M
hx : x ∈ ⨆ i, S i
⊢ ∃ (hm : 1 ∈ ⨆ i, S i), motive 1 hm

Tactic:
exact ⟨_, one⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
⊢ ∃ b_1, toLex (a, b) < b_1

Tactic:
obtain ⟨c, h⟩ := exists_gt a

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
a : α
b : β
c : α
h : a < c
⊢ ∃ b_1, toLex (a, b) < b_1
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
k : ℕ
⊢ ↑(⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩ ^ (n - 1) * ⟨(fun x_1 ↦ x ^ x_1) k, ⋯⟩) = ↑1

Tactic:
simp only [coe_one, coe_mul, SubmonoidClass.coe_pow]

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
k : ℕ
⊢ (x ^ k) ^ (n - 1) * x ^ k = 1
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ x ∈ s ⊔ t, P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]

Goal state after:
N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∀ (x x_1 : N), x_1 ∈ s → ∀ x_2 ∈ t, x_1 * x_2 = x → P x) ↔ ∀ x₁ ∈ s, ∀ x₂ ∈ t, P (x₁ * x₂)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
simp [mem_sup]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder β
f : α → β
a : α
l hd : List α
tl : α
ih : argmax f (a :: hd) = Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a
⊢ argmax f (a :: (hd ++ [tl])) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a

Tactic:
rw [← cons_append, argmax_concat, ih, argmax_concat]
    rcases h : argmax f hd with - | m
    · simp
    dsimp
    rw [← apply_ite, ← apply_ite]
    grind -abstractProof

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ ∃ a ∈ decodeSum n, encodeSum a = bit n.bodd n.div2

Tactic:
simp only [decodeSum, decode_eq_ofNat, Option.map_some, Sum.exists]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Denumerable α
inst✝ : Denumerable β
n : ℕ
⊢ (∃ a,
      (Sum.inl a ∈
          match n.bodd, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inl a) = bit n.bodd n.div2) ∨
    ∃ b,
      (Sum.inr b ∈
          match n.bodd, n.div2 with
          | false, m => some (Sum.inl (ofNat α m))
          | x, m => some (Sum.inr (ofNat β m))) ∧
        encodeSum (Sum.inr b) = bit n.bodd n.div2
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
⊢ Denumerable α

Tactic:
by
  letI := @decidableRangeEncode α _
  letI : Infinite (Set.range (@encode α _)) :=
    Infinite.of_injective _ (Equiv.ofInjective _ encode_injective).injective
  letI := Nat.Subtype.denumerable (Set.range (@encode α _))
  exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)

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

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
hx : x ∈ []
⊢ a ≤ foldr max b []

Tactic:
exact absurd hx List.not_mem_nil

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a ≤ f b

Tactic:
← sup_eq_right,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeSup α
inst✝¹ : SemilatticeSup β
inst✝ : SupHomClass F α β
f : F
a b : α
h : a ≤ b
⊢ f a ⊔ f b = f b
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : Max α
inst✝ : SemilatticeSup β
f g : SupHom α β
a b : α
⊢ (⇑f ⊔ ⇑g) (a ⊔ b) = (⇑f ⊔ ⇑g) a ⊔ (⇑f ⊔ ⇑g) b

Tactic:
rw [Pi.sup_apply, map_sup, map_sup]
      exact sup_sup_sup_comm _ _ _ _

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

Goal state before:
pp: case succ.slnil
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
⊢ sublistsLen (n + 1) [] <+ sublistsLen (n + 1) []

Tactic:
| slnil =>

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

Goal state before:
pp: case slnil
α : Type u
l l' : List α
⊢ [] ∈ sublistsLen [].length []

Tactic:
| slnil =>

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists.Nodup ↔ l.Nodup

Tactic:
nodup_sublists,

Goal state after:
α : Type u
l : List α
⊢ l.reverse.Nodup ↔ l.Nodup
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 1 ⟦l⟧ = map singleton ⟦l⟧

Tactic:
by
    simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]

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

Goal state before:
pp: case nil
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) []) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) [])

Tactic:
simp [*]

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

Goal state before:
pp: case cons
α : Type u
β : Type v
f : α → β
a : α
l head✝ : List α
tail✝ : List (List α)
tail_ih✝ :
  flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) tail✝) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) tail✝)
⊢ flatMap (fun x ↦ [x, f a :: x]) (flatMap (fun x ↦ [map f x]) (head✝ :: tail✝)) =
    flatMap (fun x ↦ [map f x]) (flatMap (fun x ↦ [x, a :: x]) (head✝ :: tail✝))

Tactic:
simp [*]

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

Goal state before:
pp: case slnil
α : Type u
l₁ l₂ : List α
⊢ [].sublists' <+ [].sublists'

Tactic:
| slnil =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∈ s.ssubsets ↔ t ⊂ s

Tactic:
rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case empty
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
⊢ ∅.sup f = ⊥ ↔ ∀ s ∈ ∅, f s = ⊥

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case insert
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
f : β → α
a✝² : β
s✝ : Finset β
a✝¹ : a✝² ∉ s✝
a✝ : s✝.sup f = ⊥ ↔ ∀ s ∈ s✝, f s = ⊥
⊢ (insert a✝² s✝).sup f = ⊥ ↔ ∀ s ∈ insert a✝² s✝, f s = ⊥

Tactic:
simp [*]

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
h : a ∈ none
⊢ a ∈ s

Tactic:
by cases h

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup γ
s : Finset β
H : s.Nonempty
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
a✝ : β
⊢ g ({a✝}.sup' ⋯ f) = {a✝}.sup' ⋯ (g ∘ f)

Tactic:
simp [*]

Goal state after: