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

Goal state before:
pp: α : Type u_1
l₁ : List α
inst✝ : DecidableEq α
a : α
⊢ l₁.bagInter [a] = if a ∈ l₁ then [a] else []

Tactic:
by
  induction l₁ <;> grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
⊢ (map f s.dedup).dedup = (map f s).dedup

Tactic:
simp [dedup_ext]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
hf : Injective f
x : α
H : ¬x ∈ s
⊢ count (f x) (map f s) = count x s

Tactic:
rw [count_eq_zero_of_notMem H, count_eq_zero, mem_map]
    rintro ⟨k, hks, hkx⟩
    rw [hf hkx] at hks
    contradiction

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

Goal state before:
pp: α : Type u_1
s : List α
⊢ s ∈ [].tails ↔ s <:+ []

Tactic:
by
    simp only [tails, mem_singleton, suffix_nil]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.tails.length = l.length + 1

Tactic:
by
  induction l with
  | nil => simp
  | cons x l IH => simpa using IH

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Fintype α
s : Finset α
⊢ (↑s).toFinset = s

Tactic:
by convert! Finset.toFinset_coe s

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

Goal state before:
pp: case mpr
α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
a : α
⊢ (∃ i, ∃ (hi : i ∈ range n), f i ⋯ = a) → a ∈ s

Tactic:
rintro ⟨i, hi, rfl⟩; apply hf'

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
hns : n ≤ #s
⊢ ∃ t ⊆ s, #t = n

Tactic:
by
  simpa using exists_subsuperset_card_eq s.empty_subset (by simp) hns

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

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
⊢ append u v = u ∘ Fin.cast ⋯

Tactic:
refine funext (Fin.addCases (fun l => ?_) fun r => ?_)

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
l : Fin m
⊢ append u v (castAdd n l) = (u ∘ Fin.cast ⋯) (castAdd n l)

case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hv : n = 0
r : Fin n
⊢ append u v (natAdd m r) = (u ∘ Fin.cast ⋯) (natAdd m r)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
⊢ append u v = v ∘ Fin.cast ⋯

Tactic:
refine funext (Fin.addCases (fun l => ?_) fun r => ?_)

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

case refine_2
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
r : Fin n
⊢ append u v (natAdd m r) = (v ∘ Fin.cast ⋯) (natAdd m r)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ ↑((i.succAbove j).succAbove ((j.predAbove i).succAbove k)) = ↑(i.succAbove (j.succAbove k))

Tactic:
simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, val_pred, coe_castPred,
    dite_eq_ite, apply_ite Fin.val, val_succ]

Goal state after:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
⊢ (if (if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1) < if ↑j < ↑i then ↑j else ↑j + 1 then
      if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1
    else (if ↑k < if ↑j < ↑i then ↑i - 1 else ↑i then ↑k else ↑k + 1) + 1) =
    if (if ↑k < ↑j then ↑k else ↑k + 1) < ↑i then if ↑k < ↑j then ↑k else ↑k + 1
    else (if ↑k < ↑j then ↑k else ↑k + 1) + 1
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
e : α ≃ β
this : Injective (⇑e.symm ∘ f) ↔ Surjective (⇑e.symm ∘ f)
hsurj : Surjective f
⊢ Injective f

Tactic:
simpa [Function.comp] using e.injective.comp (this.2 (e.symm.surjective.comp hsurj))

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

Goal state before:
pp: α : Type u_1
l : List α
x y : α
⊢ x ∈+ y :: l ↔ y = x ∧ x ∈ l ∨ x ∈+ l

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

Goal state after:
case refine_1
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
⊢ y = x ∧ x ∈ l ∨ x ∈+ l

case refine_2
α : Type u_1
l : List α
x y : α
h : y = x ∧ x ∈ l ∨ x ∈+ l
⊢ x ∈+ y :: l
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth x p j = ⋯ ▸ p (j.pred ⋯)

Tactic:
by
  rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]

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

Goal state before:
pp: case mpr
α : Type u_1
l l' : List α
⊢ (∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)) → ∃ f, ∀ (ix : ℕ), l[ix]? = l'[f ix]?

Tactic:
· rintro ⟨f, hf⟩
    refine
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          ?_,
        ?_⟩
    · intro i j h
      dsimp only
      split_ifs with hi hj hj
      · rwa [Fin.val_fin_lt, f.lt_iff_lt]
      · lia
      · exact absurd (h.trans hj) hi
      · simpa using h
    · grind

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
⊢ R a b

Tactic:
if heq : a = b then
    cases heq; apply refl
  else
    apply h <;> try (apply hab.subset; simp)
    exact heq

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
a : α
h : Pairwise (fun b a ↦ R a b) l.reverse
ha : a ∈ l.dropLast
⊢ a ∈ l.reverse.tail

Tactic:
by rwa [tail_reverse, mem_reverse]

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

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l₁ : List α
b : α
l₂ : List α
⊢ Decidable (Lex r (a :: l₁) (b :: l₂))

Tactic:
by
    haveI := decidableRel r l₁ l₂
    refine decidable_of_iff (r a b ∨ a = b ∧ Lex r l₁ l₂) ⟨fun h => ?_, fun h => ?_⟩
    · rcases h with (h | ⟨rfl, h⟩)
      · exact Lex.rel h
      · exact Lex.cons h
    · rcases h with (_ | h | h)
      · exact Or.inl h
      · exact Or.inr ⟨rfl, h⟩

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

Goal state before:
pp: 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

Tactic:
rw [length_drop] at hm

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ l.rotate (n + 1) = l

Tactic:
← l.rotate_rotate,

Goal state after:
α : Type u
inst✝ : Nonempty α
l : List α
h : l.rotate 1 = l
n✝ n : ℕ
hn : l.rotate n = l
⊢ (l.rotate n).rotate 1 = l
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 : Acc r a
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
induction acc generalizing l with
  | intro a _ ih =>
    /- Bundle l with a proof that it is r-decreasing to form l' -/
    have hl' := (List.isChain_cons.1 hl).2
    let l' : List.chains r := ⟨l, hl'⟩
    have : Acc (List.lex_chains r) l' := by
      rcases l with - | ⟨b, l⟩
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      /- l' is accessible by induction hypothesis -/
      · apply ih b (List.isChain_cons_cons.1 hl).1
    /- make l' a free variable and induct on l' -/
    revert hl
    rw [(by rfl : l = l'.1)]
    clear_value l'
    induction this with
    | intro l _ ihl =>
      intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b hr
      · apply ihl ⟨m, (List.isChain_cons.1 hm).2⟩ hr

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
s : Finset α
t : Finset β
inst✝¹ : Nonempty α
inst✝ : Nonempty β
⊢ s ×ˢ t = univ ↔ s = univ ∧ t = univ

Tactic:
by
  simp [eq_univ_iff_forall, forall_and]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
⊢ IsConj 1 a ↔ a = 1

Tactic:
by
  refine ⟨fun ⟨c, h⟩ => ?_, fun h => by rw [h]⟩
  rw [SemiconjBy, mul_one] at h
  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
inst✝ : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := mul_mem' } = ⊤ ↔ carrier = Set.univ

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
carrier : Set M
mul_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
⊢ { carrier := carrier, mul_mem' := mul_mem' } = ⊥ ↔ carrier = ∅

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
toSubsemigroup : Subsemigroup M
one_mem' : 1 ∈ toSubsemigroup.carrier
⊢ { toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } = ⊥ ↔ ↑toSubsemigroup = {1}

Tactic:
by
  simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
a : α
⊢ a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Tactic:
simp only [mem_inv, inv_inv]

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
s t : Set α
n : ℕ
⊢ (s ∩ t) ^ n ⊆ s ^ n ∩ t ^ n

Tactic:
by apply subset_inter <;> gcongr <;> simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
hm : Injective ⇑m
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ ⇑m '' ⇑m ⁻¹' (s * t) = ⇑m '' (⇑m ⁻¹' s * ⇑m ⁻¹' t)

Tactic:
rw [image_mul, image_preimage_eq_iff.2 hs, image_preimage_eq_iff.2 ht,
      image_preimage_eq_iff.2 (mul_subset_range m hs ht)]

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
S : Set G
a b : G
ha : ∀ (n : G), n ∈ S ↔ a * n * a⁻¹ ∈ S
hb : ∀ (n : G), n ∈ S ↔ b * n * b⁻¹ ∈ S
n : G
⊢ a * (b * n * b⁻¹) * a⁻¹ ∈ S ↔ a * b * n * (a * b)⁻¹ ∈ S

Tactic:
simp only [mul_assoc, mul_inv_rev]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝ : ∃ g, ↑H = {g}
g : G
hg : ↑H = {g}
⊢ Subsingleton ↑↑H

Tactic:
rw [hg]
      infer_instance

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ f.range = ⊥ ↔ f = 1

Tactic:
by
  rw [← le_bot_iff, f.range_eq_map, map_le_iff_le_comap, top_le_iff, comap_bot, ker_eq_top_iff]

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

Goal state before:
pp: N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MonoidHom.snd M N) s

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

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

Goal state before:
pp: n : ℕ
⊢ n.bodd = n.bits.headI

Tactic:
induction n using Nat.binaryRec' with
  | zero => simp
  | bit _ _ h => simp [bodd_bit, bits_append_bit _ _ h]

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

Goal state before:
pp: a b₁ b₂ : ℕ
h : b₁ < b₂
⊢ pair a b₁ < pair a b₂

Tactic:
by
  by_cases h₁ : a < b₁
  · simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h
  · simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
    by_cases h₂ : a < b₂; swap; · simp [h₂, h]
    simp only [h₂, ↓reduceIte]
    rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
    rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
    exact le_trans (not_lt.mp h₁) (Nat.le_add_left _ _)

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup N
x : G × N
⊢ x ∈ ⊤.prod H ↔ x ∈ comap (MonoidHom.snd G N) H

Tactic:
simp [mem_prod, MonoidHom.coe_snd]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : FreeMonoid α
e : α ≃ β
⊢ (map ⇑e.symm) ((map ⇑e) x) = x

Tactic:
by simp [map_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : FreeMonoid β
e : α ≃ β
⊢ (map ⇑e) ((map ⇑e.symm) x) = x

Tactic:
by simp [map_map]

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_one : f 1 ≤ 1
hp_one : p 1
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 : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod

Tactic:
have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
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 : α
s : List α
ih : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpl : ∀ (a_1 : α), a_1 ∈ a :: s → p a_1
hpla : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f (a :: s).prod ≤ (map f (a :: s)).prod
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

pp: case refine_3
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
x y : M
⊢ (∃ (hm : x ∈ ⨆ i, S i), motive x hm) →
    (∃ (hm : y ∈ ⨆ i, S i), motive y hm) → ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm

Tactic:
· exact ⟨_, one⟩

Goal state after:
case refine_3
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
x y : M
⊢ (∃ (hm : x ∈ ⨆ i, S i), motive x hm) →
    (∃ (hm : y ∈ ⨆ i, S i), motive y hm) → ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m

Tactic:
intro b m o hb ho

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
b m : α
o : Option α
hb : b ∈ tl ++ [a]
ho : m ∈ foldl (argAux r) o (tl ++ [a])
⊢ ¬r b m
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✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ f (x ⊓ y) = f x

Tactic:
map_inf,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : SemilatticeInf α
inst✝¹ : SemilatticeInf β
f : F
inst✝ : InfHomClass F α β
hf : Injective ⇑f
x y : α
h : f x ≤ f y
⊢ f x ⊓ f y = f x
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ⊓ bᶜ) = f a ⊓ (f b)ᶜ

Tactic:
map_inf,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f a ⊓ f bᶜ = f a ⊓ (f b)ᶜ
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ Forall₂ (fun p s ↦ p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)

Tactic:
rw [forall₂_map_right_iff, forall₂_same]

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ ∀ (x : Multiset α × Multiset α), x ∈ l'.revzip → x = (x.1, ↑l - x.1)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ s

Tactic:
rw [← mem_coe]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
his : IsGLB (↑s) i
hs : s.Nonempty
⊢ i ∈ ↑s
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = map f (sublistsLenAux n l id []) ++ r

Tactic:
← sublistsLenAux_append

Goal state after:
α : Type u
β : Type v
l : List α
n : ℕ
f : List α → β
r : List β
⊢ sublistsLenAux n l f r = sublistsLenAux n l (f ∘ id) (map f [] ++ r)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
⊢ Function.Injective powerset

Tactic:
by
  intro a₁ a₂ a
  exact le_antisymm
    (powerset_le_powerset_iff_le.mp (le_of_eq a))
    (powerset_le_powerset_iff_le.mp (le_of_eq a.symm))

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

Goal state before:
pp: α : Type u
l : List α
⊢ (finRange l.length).sublists'.Nodup

Tactic:
· exact (nodup_sublists'.mpr (nodup_finRange _))

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_5
inst✝⁵ : SemilatticeSup α
inst✝⁴ : OrderBot α
inst✝³ : SemilatticeSup β
inst✝² : OrderBot β
inst✝¹ : FunLike F α β
inst✝ : SupBotHomClass F α β
f : F
s✝ : Finset ι
g : ι → α
i : ι
s : Finset ι
x✝ : i ∉ s
h : f (s.sup g) = s.sup (⇑f ∘ g)
⊢ f ((cons i s x✝).sup g) = (cons i s x✝).sup (⇑f ∘ g)

Tactic:
rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]

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⟩

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
⊢ (Disjoint on fun i ↦ ⨆ i' ∈ t, f (i, i')) i j

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
⊢ (Disjoint on fun i' ↦ ⨆ i ∈ s, f (i, i')) i j
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompletePartialOrderSup α
hι : Nonempty ι
a : α
⊢ ⨆ x, a = a

Tactic:
rw [iSup, range_const, csSup_singleton]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ P x ∧ Q x) x ↔ Minimal P x ∧ Q x

Tactic:
simp_rw [and_iff_left_of_imp (fun x ↦ hPQ x), iff_self_and]

Goal state after:
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Minimal (fun x ↦ P x) x → Q x
Module: Mathlib.Order.Minimal

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : Preorder α
Q : ι → Prop
f : ι → α
i : ι
⊢ MinimalFor Q f i ↔ Q i ∧ ∀ ⦃j : ι⦄, f j < f i → ¬Q j

Tactic:
by
  simp [MinimalFor, lt_iff_le_not_ge, imp.swap]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
y : α
hys : (fun x ↦ x ∈ s) y
⊢ y ≤ a → f a ≤ f y

Tactic:
← hf hys ha

Goal state after:
α : Type u_2
β : Type u_3
a : α
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α → β
ha : a ∈ s
hf : ∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)
h : Minimal (fun x ↦ x ∈ f '' s) (f a)
y : α
hys : (fun x ↦ x ∈ s) y
⊢ f y ≤ f a → f a ≤ f y
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
h : 0 < sInf s
⊢ s.Nonempty

Tactic:
by_contra contra
  rw [Set.not_nonempty_iff_eq_empty] at contra
  have h' : sInf s ≠ 0 := ne_of_gt h
  apply h'
  rw [Nat.sInf_eq_zero]
  right
  assumption

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
k : ℕ
⊢ ¬Acc r (f k)

Tactic:
rw [acc_iff_isEmpty_subtype_mem_range, not_isEmpty_iff]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
f : (fun x1 x2 ↦ x1 > x2) ↪r r
k : ℕ
⊢ Nonempty { f_1 // f k ∈ Set.range ⇑f_1 }
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝ : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
⊢ ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
let S := Set.Icc x y

Goal state after:
α : Type u_2
inst✝ : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
⊢ ∃ a, a 0 = x ∧ ∃ n, a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : LT α
⊢ univ.IsWF ↔ WellFoundedLT α

Tactic:
by
  simp [IsWF, wellFoundedOn_iff, isWellFounded_iff]

Goal state after: