mathlib-initiative/mathlib-tactics huggingface dataset:
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 α)]
    constructor
    · rintro ⟨a, b, c, d, t, hsub, hab, hac, had, hbc, hbd, hcd, rfl⟩
      exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩
    · rintro ⟨a, b, c, d, ha, hb, hc, hd, hab, hac, had, hbc, hbd, hcd⟩
      exact ⟨a, b, c, d, {a, b, c, d}, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: α : Type u_4
inst✝ : Fintype α
x : α
h : Fintype.card α = 1
⊢ #univ ≤ #{x}

Tactic:
simp [h]

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

Goal state before:
pp: case inr
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs✝ : s.Nonempty
hs : s.Nontrivial
⊢ p s hs✝

Tactic:
refine h₁ hs fun t ht hts ↦ ?_

Goal state after:
case inr
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs✝ : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
⊢ p t ht
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
simp [Ne.symm]

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

Goal state before:
pp: case succ.inr
α : Type u_1
inst✝ : Infinite α
n : ℕ
IH : ∀ (s : Finset α), #s ≤ n → ∃ t, s ⊆ t ∧ #t = n
s : Finset α
hn : #s ≤ n + 1
hn' : #s < n + 1
t : Finset α
hs : s ⊆ t
ht : #t = n
x : α
hx : x ∉ t
⊢ #(cons x t hx) = n + 1

Tactic:
simp [ht]

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

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
h : r a b
⊢ orderedInsert r a (b :: l) ~ a :: b :: l

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∉ s
⊢ a ∉ s.toFinset.val

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
a : α
s : Set α
inst✝ : Fintype ↑s
h : a ∈ s
⊢ ∀ (x : α), x ∈ s.toFinset ↔ x ∈ insert a s

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s ∈ Set.range SetLike.coe → s.Finite

Tactic:
rintro ⟨t, rfl⟩
    simp

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

Goal state before:
pp: case p
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1)
⊢ cons a p j = cons a (i.insertNth x p) (i.succ.succAbove j)

Tactic:
cases j using Fin.cases <;> simp

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f (p.succAbove i) x) = update (p.removeNth f) i x

Tactic:
by
  ext j
  rcases eq_or_ne j i with rfl | hne <;> simp [removeNth, *]

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

Goal state before:
pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

pp: case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
swap

Goal state after:
case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
Module: Mathlib.Data.List.Lex

Goal state before:
pp: case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) l' l
hl : ¬l = []
⊢ l'.head! ≤ l.head!

Tactic:
rw [← List.cons_head!_tail hl', ← List.cons_head!_tail hl] at h

Goal state after:
case neg
α : Type u
inst✝¹ : Preorder α
inst✝ : Inhabited α
l l' : List α
hl' : l' ≠ []
h : Lex (fun x1 x2 ↦ x1 < x2) (l'.head! :: l'.tail) (l.head! :: l.tail)
hl : ¬l = []
⊢ l'.head! ≤ l.head!
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
a b : α
h : Relation.ReflTransGen r a b
⊢ ∀ {a c : α},
    r a c →
      Relation.ReflTransGen r c b →
        (∃ l, IsChain r (c :: l) ∧ (c :: l).getLast ⋯ = b) → ∃ l, IsChain r (a :: l) ∧ (a :: l).getLast ⋯ = b

Tactic:
intro c d e _ ih
    obtain ⟨l, hl₁, hl₂⟩ := ih
    refine ⟨d :: l, .cons_cons e hl₁, ?_⟩
    rwa [getLast_cons_cons]

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ l.rotate (l.length * n) = l

Tactic:
by
  rw [rotate_eq_rotate', rotate'_length_mul]

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

Goal state before:
pp: α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l = l'.rotate (l'.length - n % l'.length)

Tactic:
← @rotate_eq_rotate _ l _ n,

Goal state after:
α : Type u
l l' : List α
n : ℕ
⊢ l.rotate n = l' ↔ l.rotate n = (l'.rotate (l'.length - n % l'.length)).rotate n
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
⊢ map Prod.swap (s ×ˢ t) = t ×ˢ s

Tactic:
induction s using Multiset.induction <;> simp_all

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

Goal state before:
pp: α : Type u_1
β : Type v
M : Type u_4
inst✝ : CommMonoid M
s : Multiset α
t : Multiset β
f : α × β → M
⊢ (map f (s ×ˢ t)).prod = (map (fun i ↦ (map (fun j ↦ f (i, j)) t).prod) s).prod

Tactic:
induction s using Multiset.induction <;> simp_all

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

Tactic:
by_cases h : a' = a

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : a' = a
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'

case neg
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
f : (a' : α) → a' ∈ a ::ₘ m → δ a'
a' : α
h' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ cons m a (f a ⋯) (fun a' ha' ↦ f a' ⋯) a' h' = f a' h'
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : k ≤ n
⊢ k ! * (n - k)! ∣ n !

Tactic:
by
  rw [← choose_mul_factorial_mul_factorial hk, Nat.mul_assoc]; exact Nat.dvd_mul_left _ _

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

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

Tactic:
by
  rcases lt_trichotomy k n with hk | rfl | hk
  · grind [k.choose_mono hk]
  · simp
  · grind

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

Goal state before:
pp: case cons.mp
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
⊢ Pi.cons m a b f' a' ha' ∈ t a'

Tactic:
by_cases h : a' = a

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'

case neg
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
b : β a
hb : b ∈ t a
f' : (a : α) → a ∈ m → β a
hf' : ∀ (a : α) (h : a ∈ m), f' a h ∈ t a
a' : α
ha' : a' ∈ a ::ₘ m
h : ¬a' = a
⊢ Pi.cons m a b f' a' ha' ∈ t a'
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
x✝ : IsConj 1 a
c : αˣ
h : ↑c = a * ↑c
⊢ a = 1

Tactic:
exact c.isUnit.mul_eq_right.mp h.symm

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
S : Subsemigroup M
hn : Nonempty M
h : ⊥ = ⊤
x : M
⊢ x ∈ ⊥

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
p : α → Prop
x✝ : Subtype p
x : α
h : p x
⊢ ⟨x, h⟩ ∈ univ ↔ ⟨x, h⟩ ∈ ⋃ x, ⋃ (h : p x), {⟨x, h⟩}

Tactic:
simp [h]

Goal state after:
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)
a : α
b : β a
x : γ a b
⊢ uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle ⟨a, b⟩ x

Tactic:
← curry_mulSingle ⟨a, b⟩,

Goal state after:
α : Type u_5
β : α → Type u_6
γ : (a : α) → β a → Type u_7
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (β a)
inst✝ : (a : α) → (b : β a) → One (γ a b)
a : α
b : β a
x : γ a b
⊢ uncurry (curry (Pi.mulSingle ⟨a, b⟩ x)) = Pi.mulSingle ⟨a, b⟩ x
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (Prod.mk '' s).seq t = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
by
  rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp]; rfl

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
H✝ : Subgroup G
inst✝ : IsMulCommutative G
H : Subgroup G
⊢ ∀ (n : G), n ∈ H → ∀ (g : G), g * n * g⁻¹ ∈ H

Tactic:
simp [mul_comm']

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

Goal state before:
pp: n : ℕ
⊢ n.bodd.toNat + 2 * n.div2 = n

Tactic:
by
  cases n using bitCasesOn with
  | bit b n => simpa using (bit_val b n).symm

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

Goal state before:
pp: n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
⊢ (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1 < n

Tactic:
by_cases h : n - s * s < s <;> simp only [h, ↓reduceIte, gt_iff_lt, s]

Goal state after:
case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

pp: case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
swap

Goal state after:
case neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : ¬a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

case pos
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
h₂ : a < b₂
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ max m n ^ 2 + min m n ≤ m * m + m + n

Tactic:
max_eq_left h,

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ m ^ 2 + min m n ≤ m * m + m + n
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(closure (⇑↑(MulAut.conj h) '' s))

Tactic:
← MonoidHom.map_closure

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
s : Set G
hH : ∀ h ∈ H, ∀ g ∈ s, h * g * h⁻¹ ∈ closure s
h : G
hh : h ∈ H
⊢ s ⊆ ↑(map (↑(MulAut.conj h)) (closure s))
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ a • A ⊆ B ↔ A ⊆ a⁻¹ • B

Tactic:
refine image_subset_iff.trans ?_

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
A B : Set β
a : α
⊢ A ⊆ (fun x ↦ a • x) ⁻¹' B ↔ A ⊆ a⁻¹ • B
Module: Mathlib.Algebra.Group.Subgroup.Basic

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
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f (f_inv (x * y)) = f (f_inv x) * f (f_inv y)

Tactic:
simp only [hf _]

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

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) = f x

Tactic:
simp only [hf _]

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

Goal state before:
pp: case cons_cons
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ l₁✝ l₂✝ : List M
a : M
a✝ : l₁✝ <+ l₂✝
ih' : (∀ (a : M), a ∈ l₂✝ → 1 ≤ a) → l₁✝.prod ≤ l₂✝.prod
h₁ : ∀ (a_1 : M), a_1 ∈ a :: l₂✝ → 1 ≤ a_1
⊢ (a :: l₁✝).prod ≤ (a :: l₂✝).prod

Tactic:
| cons_cons a _ ih' =>

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

Goal state before:
pp: case cons
α : 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
⊢ f (a :: l).prod ≤ (map f (a :: l)).prod

Tactic:
rw [prod_cons, map_cons, prod_cons]

Goal state after:
case cons
α : 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
⊢ f (a * l.prod) ≤ f a * (map f l).prod
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mp.left
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
⊢ r ⟨i✝, a⟩.fst ⟨j✝, b⟩.fst ∨ ∃ h, s ⟨j✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨j✝, b⟩.snd

pp: case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ r ⟨i✝, a⟩.fst ⟨i✝, b⟩.fst ∨ ∃ h, s ⟨i✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨i✝, b⟩.snd

Tactic:
· exact Or.inl hij

Goal state after:
case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
hab : s i✝ a b
⊢ r ⟨i✝, a⟩.fst ⟨i✝, b⟩.fst ∨ ∃ h, s ⟨i✝, b⟩.fst (h ▸ ⟨i✝, a⟩.snd) ⟨i✝, b⟩.snd
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : 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)
⊢ ∀ (a b : (i : ι) × α i), Lex r s a b → Lex r s b a → a = b

Tactic:
rintro _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, _, hji⟩ | ⟨_, _, hba⟩)

Goal state after:
case left.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✝ j✝ : ι
a : α i✝
b : α j✝
hij : r i✝ j✝
hji : r j✝ i✝
⊢ ⟨i✝, a⟩ = ⟨j✝, b⟩

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⟩

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.Data.Sigma.Lex

Goal state before:
pp: case mp.left
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
a₁✝ : ι
a : α a₁✝
a₂✝ : ι
b : α a₂✝
hij : r a₁✝ a₂✝
⊢ r ⟨a₁✝, a⟩.fst ⟨a₂✝, b⟩.fst ∨ ∃ h, s ⟨a₂✝, b⟩.fst (h ▸ ⟨a₁✝, a⟩.snd) ⟨a₂✝, b⟩.snd

pp: case mp.right
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r ⟨i, b₁✝⟩.fst ⟨i, b₂✝⟩.fst ∨ ∃ h, s ⟨i, b₂✝⟩.fst (h ▸ ⟨i, b₁✝⟩.snd) ⟨i, b₂✝⟩.snd

Tactic:
· exact Or.inl hij

Goal state after:
case mp.right
ι : Sort u_1
α : ι → Sort u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i : ι
b₁✝ b₂✝ : α i
hab : s i b₁✝ b₂✝
⊢ r ⟨i, b₁✝⟩.fst ⟨i, b₂✝⟩.fst ∨ ∃ h, s ⟨i, b₂✝⟩.fst (h ▸ ⟨i, b₁✝⟩.snd) ⟨i, b₂✝⟩.snd
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
S : Submonoid M
inst✝ : Fintype ↥S
h : S = ⊥
⊢ card ↥S ≤ 1

Tactic:
simp [h]

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, toLex a < b

Tactic:
Prod.forall

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder α
⊢ ∀ (a : α) (b : β), ∃ b_1, toLex (a, b) < b_1
Module: Mathlib.Data.Prod.Lex

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

Tactic:
Prod.forall

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

Goal state before:
pp: M : Type u_1
inst✝³ : Monoid M
N : Type u_4
F : Type u_5
inst✝² : Monoid N
inst✝¹ : FunLike F M N
inst✝ : MonoidHomClass F M N
f : F
m : M
⊢ map f (powers m) = powers (f m)

Tactic:
simp only [powers_eq_closure, map_mclosure f, Set.image_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ inl a ∈ s.disjSum t ↔ a ∈ s

Tactic:
by
  rw [mem_disjSum, or_iff_left]
  · simp only [inl.injEq, exists_eq_right]
  rintro ⟨b, _, hb⟩
  exact inr_ne_inl hb

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

Goal state before:
pp: case cons
α : Type u_2
inst✝ : DecidableEq α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
h : s✝.sup.Nodup ↔ ∀ (a : Multiset α), a ∈ s✝ → a.Nodup
⊢ (a✝ ::ₘ s✝).sup.Nodup ↔ ∀ (a : Multiset α), a ∈ a✝ ::ₘ s✝ → a.Nodup

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : u = s.disjSum t
⊢ u.toLeft = s ∧ u.toRight = t

Tactic:
simp [h]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
l : List α
hd : α
tl : List α
IH : tl ≠ [] → ↑(foldr max ⊥ tl) = tl.maximum
h✝ : hd :: tl ≠ []
h : tl = []
⊢ max ↑hd ↑(foldr max ⊥ tl) = max (↑hd) tl.maximum

Tactic:
simp [h]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (f a :: map f l).sublists = map (map f) (a :: l).sublists

Tactic:
sublists_cons,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (do
      let x ← (map f l).sublists
      [x, f a :: x]) =
    map (map f) (a :: l).sublists
Module: Mathlib.Data.List.Sublists

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

Tactic:
sublists_cons,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ flatMap (fun x ↦ [x, f a :: x]) (map (map f) l.sublists) =
    map (map f) do
      let x ← l.sublists
      [x, a :: x]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ (a :: l₂✝).sublists'

Tactic:
rw [sublists'_cons]

Goal state after:
case cons
α : Type u
l₁ l₂ l₁✝ l₂✝ : List α
a : α
a✝ : l₁✝ <+ l₂✝
ih : l₁✝.sublists' <+ l₂✝.sublists'
⊢ l₁✝.sublists' <+ l₂✝.sublists' ++ map (List.cons a) l₂✝.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
a : α
l : List α
⊢ (a :: l).sublists' ~ l.sublists ++ map (cons a) l.sublists

Tactic:
rw [sublists'_cons]

Goal state after:
α : Type u
a : α
l : List α
⊢ l.sublists' ++ map (cons a) l.sublists' ~ l.sublists ++ map (cons a) l.sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
revzip

Goal state after:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
⊢ l₁ ++ l₂ ~ l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
revzip

Goal state after:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ l₂ ~ l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'

Tactic:
simp_rw [range_succ_eq_map, length, flatMap_cons, flatMap_map, sublistsLen_succ_cons,
      sublists'_cons, List.sublistsLen_zero, List.singleton_append]
    refine ((flatMap_append_perm (range (tl.length + 1)) _ _).symm.cons _).trans ?_
    simp_rw [← List.map_flatMap, ← cons_append]
    rw [← List.singleton_append, ← List.sublistsLen_zero tl]
    refine Perm.append ?_ (l_ih.map _)
    rw [List.range_succ, flatMap_append, flatMap_singleton,
      sublistsLen_of_length_lt (Nat.lt_succ_self _), append_nil,
      ← List.flatMap_map Nat.succ fun n => sublistsLen n tl,
      ← flatMap_cons (f := fun n => sublistsLen n tl), ← range_succ_eq_map]
    exact l_ih

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ map Embedding.some s ⊆ map Embedding.some t ↔ s ⊆ t

Tactic:
map_subset_map

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
⊢ s ⊆ t ↔ s ⊆ t
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: ι : Type u_5
α : Type u_7
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup f = ⊤ ↔ ∃ b ∈ s, f b = ⊤

Tactic:
by
  cases subsingleton_or_nontrivial α
  · simpa [Subsingleton.elim _ (⊤ : α)]
  · exact Finset.sup_eq_top_iff

Goal state after: