mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).Finite

Tactic:
rw [Set.Finite] at hs ht
  apply toFinite

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ {a} ∪ fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = insert a s

Tactic:
ih,

Goal state after:
case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
has : a ∉ s
ih : fold (fun x1 x2 ↦ x1 ∪ x2) ∅ singleton s = s
⊢ {a} ∪ s = insert a s
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
s : Finset α
inst✝ : LinearOrder β
c : β
⊢ fold min b f s ≤ c ↔ b ≤ c ∨ ∃ x ∈ s, f x ≤ c

Tactic:
by
  change _ ≥ _ ↔ _
  apply fold_op_rel_iff_or
  intro x y z
  change _ ≤ _ ↔ _
  exact min_le_iff

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
l₁ l₂ : List α
H : l₁.length ≤ l₂.length
h : l₁ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) l₁ l₂

Tactic:
induction l₁ generalizing l₂

Goal state after:
case nil
α : Type u
inst✝ : DecidableEq α
l₂ : List α
H : [].length ≤ l₂.length
h : [] ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) [] l₂

case cons
α : Type u
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, tail✝.length ≤ l₂.length → tail✝ ≠ l₂ → Lex (fun x1 x2 ↦ x1 ≠ x2) tail✝ l₂
l₂ : List α
H : (head✝ :: tail✝).length ≤ l₂.length
h : head✝ :: tail✝ ≠ l₂
⊢ Lex (fun x1 x2 ↦ x1 ≠ x2) (head✝ :: tail✝) l₂
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Defs

Goal state before:
pp: case neg
M : Type u_3
inst✝ : CommMonoid M
s✝ : Multiset M
p : M → Prop
p_mul : ∀ (a b : M), p a → p b → p (a * b)
a : M
s : Multiset M
hsa : s ≠ ∅ → (∀ (a : M), a ∈ s → p a) → p s.prod
hs : a ::ₘ s ≠ ∅
p_s : ∀ (a_1 : M), a_1 ∈ a ::ₘ s → p a_1
hs_empty : ¬s = ∅
hps : ∀ (x : M), x ∈ s → p x
⊢ p (a * s.prod)

Tactic:
exact p_mul a s.prod (p_s a (mem_cons_self a s)) (hsa hs_empty hps)

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

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

Tactic:
induction L with
  | nil => exact fun m' h' => False.elim (not_mem_nil h')
  | cons m L ih =>
    rw [prod_cons, IsUnit.mul_iff] at h
    exact fun m' h' ↦ Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H

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

Goal state before:
pp: l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n < l.sum

Tactic:
← mem_range,

Goal state after:
l : List ℕ
n : ℕ
⊢ (∃ s, s ∈ l.ranges ∧ n ∈ s) ↔ n ∈ range l.sum
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + filter p (n • ha) = n • filter p (a ::ₘ ha)

Tactic:
ih,

Goal state after:
case refine_2
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • {a}) + n • filter p ha = n • filter p (a ::ₘ ha)
Module: Mathlib.Data.List.Rotate

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

Tactic:
length_reverse

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.reverse = l.reverse.rotate (l.length - (l.length - n % l.length) % l.length + (l.length - n % l.length))
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
n k' : ℕ
x : α
l : List α
k : ℕ := n % (x :: l).reverse.length
hk' : k = k' + 1
⊢ 0 < n % (x :: l).reverse.length

Tactic:
simp_all! [k]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ Function.Injective fun x_1 ↦ (x, x_1)

Tactic:
by simp [Function.Injective]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ Function.Injective fun x ↦ (x, y)

Tactic:
by simp [Function.Injective]

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

Goal state before:
pp: case succ
n : ℕ
ih : n.choose 2 = n * (n - 1) / 2
⊢ (n + 1).choose 2 = (n + 1) * (n + 1 - 1) / 2

Tactic:
rw [triangle_succ n, choose, ih]
    simp [Nat.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ x ∈ Set.univ.pi fun a ↦ ↑(t a)

Tactic:
Set.mem_univ_pi

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
δ : α → Type u_4
t : (a : α) → Finset (δ a)
x : (a : α) → δ a
⊢ x ∈ ↑(piFinset t) ↔ ∀ (i : α), x i ∈ ↑(t i)
Module: Mathlib.Data.Finite.Prod

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
⊢ Finite ((a : α) → β a)

Tactic:
have := Fintype.ofFinite (PLift α)

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
α : Sort u_3
β : α → Sort u_4
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Finite (β a)
this : Fintype (PLift α)
⊢ Finite ((a : α) → β a)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: case succ
α : Type u
inst✝ : Group α
a b : α
i : ℕ
hi : (a * b * a⁻¹) ^ i = a * b ^ i * a⁻¹
⊢ (a * b * a⁻¹) ^ (i + 1) = a * b ^ (i + 1) * a⁻¹

Tactic:
simp [pow_succ, hi]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (range f)ᶜ ⊆ kernImage f s

Tactic:
rw [← kernImage_empty]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f ∅ ⊆ kernImage f s
Module: Mathlib.Algebra.Group.Submonoid.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
ha : a✝ ∈ {1}
hb : b✝ ∈ {1}
⊢ a✝ * b✝ ∈ {1}

Tactic:
push _ ∈ _ at *

Goal state after:
M : Type u_1
N : Type u_2
inst✝ : MulOneClass M
s : Set M
S : Submonoid M
a✝ b✝ : M
hb : b✝ = 1
ha : a✝ = 1
⊢ a✝ * b✝ = 1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : One α
inst✝ : One β
x✝ : α × β
⊢ x✝ ∈ 1 ×ˢ 1 ↔ x✝ ∈ 1

Tactic:
simp [Prod.ext_iff]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ a⁻¹ * x) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ x * a) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]

Goal state after:
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 β
⊢ ∀ (x : α), (∀ (i : ι), x ∈ s i) → ∀ y ∈ t, ∀ (i : ι), f x y ∈ image2 f (s i) t

Tactic:
exact fun x hx y hy i => mem_image2_of_mem (hx _) hy

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ (((fun x ↦ x * a⁻¹) '' s)⁻¹ ∩ t⁻¹).Nonempty ↔ ((fun x ↦ a * x) '' s⁻¹ ∩ t⁻¹).Nonempty

Tactic:
simp_rw [← image_inv_eq_inv, image_image, mul_inv_rev, inv_inv]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : DivisionMonoid α
s✝ t✝ : Set α
n : ℤ
s t : Set α
h : s * t = 1
⊢ s⁻¹ = t

Tactic:
obtain ⟨a, b, rfl, rfl, hab⟩ := Set.mul_eq_one_iff.1 h
      rw [inv_singleton, inv_eq_of_mul_eq_one_right hab]

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
by
  constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Set.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.set

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s : Set α
hs : s.Nonempty
n : ℕ
⊢ (s ^ Int.negSucc n).Nonempty

Tactic:
by simpa using hs.pow

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

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩

Goal state after:
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
y : C
hy : y ∈ s
z : C
hz : z ∈ t
⊢ y * z ∈ s ⊔ t
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
⊢ (∃ y ∈ s, ∃ z ∈ t, y * z = x) → x ∈ s ⊔ t

Tactic:
rintro ⟨y, hy, z, hz, rfl⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
y : G
hy : y ∈ s
z : G
hz : z ∈ t
⊢ y * z ∈ s ⊔ t
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ closure (Set.range ⇑f) = mrange f

Tactic:
by
  rw [← Set.image_univ, ← map_mclosure, mrange_eq_map, closure_univ]

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

Goal state before:
pp: b : Bool
n : ℕ
⊢ (bit b n).bodd = b

Tactic:
cases b

Goal state after:
case false
n : ℕ
⊢ (bit false n).bodd = false

case true
n : ℕ
⊢ (bit true n).bodd = true
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ bit b n % 2 = (bit b n).bodd.toNat

Tactic:
cases b

Goal state after:
case bit.false
n : ℕ
⊢ bit false n % 2 = (bit false n).bodd.toNat

case bit.true
n : ℕ
⊢ bit true n % 2 = (bit true n).bodd.toNat
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b : Bool
n : ℕ
⊢ (bit b n + 1).div2 = bif (bit b n).bodd then (bit b n).div2.succ else (bit b n).div2

Tactic:
cases b

Goal state after:
case bit.false
n : ℕ
⊢ (bit false n + 1).div2 = bif (bit false n).bodd then (bit false n).div2.succ else (bit false n).div2

case bit.true
n : ℕ
⊢ (bit true n + 1).div2 = bif (bit true n).bodd then (bit true n).div2.succ else (bit true n).div2
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
⊢ 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m

Tactic:
rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]

Goal state after:
m n : ℕ
⊢ m * 2 ^ n.succ = 2 ^ (n + 1) * m
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b n).testBit m.succ = n.testBit m

Tactic:
have : bodd (((bit b n) >>> 1) >>> m) = bodd (n >>> m) := by
    simp only [shiftRight_eq_div_pow]
    simp [← div2_val, div2_bit]

Goal state after:
m : ℕ
b : Bool
n : ℕ
this : (bit b n >>> 1 >>> m).bodd = (n >>> m).bodd
⊢ (bit b n).testBit m.succ = n.testBit m
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
h : n ≠ 0
⊢ bit b n ≠ 0

Tactic:
cases b

Goal state after:
case false
n : ℕ
h : n ≠ 0
⊢ bit false n ≠ 0

case true
n : ℕ
h : n ≠ 0
⊢ bit true n ≠ 0
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: m n : ℕ
a b : Bool
h : m < n
⊢ 2 * n ≤ bit b n

Tactic:
cases b

Goal state after:
case false
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit false n

case true
m n : ℕ
a : Bool
h : m < n
⊢ 2 * n ≤ bit true n
Module: Mathlib.Algebra.Group.Idempotent

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a ^ (n + 1) * a = a

Tactic:
ih,

Goal state after:
M : Type u_1
inst✝ : Monoid M
a : M
n✝ : ℕ
h : IsIdempotentElem a
n : ℕ
ih : a ^ (n + 1) = a
⊢ a * a = a
Module: Mathlib.Algebra.Group.Idempotent

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

Tactic:
rw [pow_succ, ih, h.eq]

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
f : G →* N
hf : Surjective ⇑f
H : Subgroup N
⊢ (comap f H).Normal ↔ H.Normal

Tactic:
by
  rw [← normalizer_eq_top_iff, ← comap_normalizer_eq_of_surjective H hf, ← comap_top f,
    (comap_injective hf).eq_iff, normalizer_eq_top_iff]

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

Goal state before:
pp: case cons
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x y : M
ys : List M
ih : x ∈ ys → x ≤ ys.prod
h₁ : x ∈ y :: ys
⊢ x ≤ (y :: ys).prod

Tactic:
simp only [mem_cons] at h₁
    rcases h₁ with (rfl | h₁)
    · simp
    · specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : M → Prop
hs : closure s = ⊤
x : M
one : motive 1
mul_right : ∀ (x y : M), y ∈ s → motive x → motive (x * y)
this : x ∈ closure s
⊢ motive x

Tactic:
induction this using closure_induction_right with
  | one => exact one
  | mul_right x _ y hy ih => exact mul_right x y hy ih

Goal state after:
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
m : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ ↑m.succ) = ↑(x ^ ↑m * x)

Tactic:
by
    simp_rw [HPow.hPow, Pow.pow]
    obtain ⟨_, k, rfl⟩ := x
    simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow, coe_mul]
    norm_cast
    iterate 2 rw [Int.toNat_natCast, mul_comm, pow_mul, ← pow_eq_pow_mod _ hx]
    rw [← pow_mul _ m, mul_comm, pow_mul, ← pow_succ, ← pow_mul, mul_comm, pow_mul]

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
⊢ (Option.casesOn (argmax f (a :: hd)) (some tl) fun c ↦ if f c < f tl then some tl else some c) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a

Tactic:
ih,

Goal state after:
α : 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
⊢ (Option.casesOn (Option.casesOn (argmax f hd) (some a) fun c ↦ if f a < f c then some c else some a) (some tl) fun c ↦
      if f c < f tl then some tl else some c) =
    Option.casesOn (argmax f (hd ++ [tl])) (some a) fun c ↦ if f a < f c then some c else some a
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:
mem_disjSum,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
a : α
⊢ ((∃ a_1, a_1 ∈ s ∧ inl a_1 = inl a) ∨ ∃ b, b ∈ t ∧ inr b = inl a) ↔ a ∈ s
Module: Mathlib.Data.Multiset.Sum

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

Tactic:
mem_disjSum,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ ((∃ a, a ∈ s ∧ inl a = inr b) ∨ ∃ b_1, b_1 ∈ t ∧ inr b_1 = inr b) ↔ b ∈ t
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)

Tactic:
disjoint_map_map

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → inl a ≠ inr b
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (a :: tl).maximum ↑hd = max (↑a) (tl ++ [hd]).maximum

Tactic:
ih,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : α
l tl : List α
hd : α
ih : (a :: tl).maximum = max (↑a) tl.maximum
⊢ max (max (↑a) tl.maximum) ↑hd = max (↑a) (tl ++ [hd]).maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ max (↑head✝) (tail✝ ++ l₂).maximum = max (max (↑head✝) tail✝.maximum) l₂.maximum

Tactic:
ih,

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
l₂ : List α
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).maximum = max tail✝.maximum l₂.maximum
⊢ max (↑head✝) (max tail✝.maximum l₂.maximum) = max (max (↑head✝) tail✝.maximum) l₂.maximum
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → ↑a ≤ b
⊢ l.maximum ≤ b

Tactic:
induction l with
  | nil => simp
  | cons a l ih =>
    simp only [maximum_cons, max_le_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

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

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ (some z).getD d = y

Tactic:
Option.getD_some

Goal state after:
case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ z = y
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({y ∈ range ↑(succ (ofNat s n)) | y ∈ s}) = n + 1

Tactic:
conv =>

Goal state after:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
h₁ : ↑(ofNat s n) ∉ {x ∈ range ↑(ofNat s n) | x ∈ s}
h₂ : {x ∈ range ↑(succ (ofNat s n)) | x ∈ s} = insert (↑(ofNat s n)) ({x ∈ range ↑(ofNat s n) | x ∈ s})
ih : #({y ∈ range ↑(ofNat s n) | y ∈ s}) = n
| #({x ∈ range ↑(succ (ofNat s n)) | x ∈ s})
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.unzip.fst = l

Tactic:
unzip_revzip

Goal state after:
α : Type u
l : List α
⊢ (l, l.reverse).fst = l
Module: Mathlib.Data.List.Zip

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.unzip.snd = l.reverse

Tactic:
unzip_revzip

Goal state after:
α : Type u
l : List α
⊢ (l, l.reverse).snd = l.reverse
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
⊢ l.reverse.sublists = map reverse l.sublists'

Tactic:
by
  induction l with
  | nil => rfl
  | cons hd tl ih =>
    simp only [reverse_cons, sublists_append, sublists'_cons, map_append, ih, sublists_singleton,
      bind_eq_flatMap, map_map, flatMap_cons, append_nil, flatMap_nil, Function.comp_def]

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

Goal state before:
pp: α : Type u
l : List α
⊢ [] = map (fun x ↦ [x]) [].reverse

Tactic:
reverse_nil,

Goal state after:
α : Type u
l : List α
⊢ [] = map (fun x ↦ [x]) []
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ sublistsLen (0 + 1) s ++ map (cons a) (sublistsLen 0 s) = map (fun x ↦ [x]) (a :: s).reverse

Tactic:
ih,

Goal state after:
α : Type u
l : List α
a : α
s : List α
ih : sublistsLen 1 s = map (fun x ↦ [x]) s.reverse
⊢ map (fun x ↦ [x]) s.reverse ++ map (cons a) (sublistsLen 0 s) = map (fun x ↦ [x]) (a :: s).reverse
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c) ⊔ g (t.sup f) = (g ∘ f) c ⊔ t.sup (g ∘ f)

Tactic:
ih,

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : OrderBot α
inst✝¹ : SemilatticeSup γ
inst✝ : OrderBot γ
s : Finset β
f : β → α
g : α → γ
g_sup : ∀ (x y : α), g (x ⊔ y) = g x ⊔ g y
bot : g ⊥ = ⊥
c : β
t : Finset β
hc : c ∉ t
ih : g (t.sup f) = t.sup (g ∘ f)
⊢ g (f c) ⊔ t.sup (g ∘ f) = (g ∘ f) c ⊔ t.sup (g ∘ f)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
x : Finset α
hxt : x ⊆ t
hxn : #x = n
hsx : s ⊆ x
⊢ #(x \ s) = n - #s

Tactic:
rw [card_sdiff_of_subset hsx, hxn]

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

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ a \ f b) = a \ s✝.sup f
⊢ (a \ f a✝ ⊓ s✝.inf fun b ↦ a \ f b) = a \ (f a✝ ⊔ s✝.sup f)

Tactic:
ih,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ a \ f b) = a \ s✝.sup f
⊢ a \ f a✝ ⊓ a \ s✝.sup f = a \ (f a✝ ⊔ s✝.sup f)
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ f b \ a) = s✝.inf f \ a
⊢ (f a✝ \ a ⊓ s✝.inf fun b ↦ f b \ a) = (f a✝ ⊓ s✝.inf f) \ a

Tactic:
ih,

Goal state after:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b ↦ f b \ a) = s✝.inf f \ a
⊢ f a✝ \ a ⊓ s✝.inf f \ a = (f a✝ ⊓ s✝.inf f) \ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_7
β : Type u_8
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
x : β
⊢ x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v

Tactic:
by
  induction s using Finset.cons_induction <;> simp [*]

Goal state after:
Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : ConditionallyCompletePartialOrderSup α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f g : β → α
hf : Monotone f
hg : Antitone g
h : f ≤ g
⊢ ⨆ n, f n ∈ ⋂ n, Icc (f n) (g n)

Tactic:
refine mem_iInter.2 fun n => ?_
  have : Nonempty β := ⟨n⟩
  have h₁ : ∀ m, f m ≤ g n := fun m => hf.forall_le_of_antitone hg h m n
  have h₂ : Directed (· ≤ ·) f := hf.directed_le
  exact ⟨h₂.le_ciSup ⟨g <| n, forall_mem_range.2 h₁⟩ _, h₂.ciSup_le h₁⟩

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simp only [Finset.mem_coe] at h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ ↑s, f i ∈ f '' ↑s
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ ↑s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s

Tactic:
simp only [Finset.mem_coe] at h

Goal state after:
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ⨅ i ∈ ↑s, f i ∈ f '' ↑s
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ici a = Ico ↑a ⊤

Tactic:
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]

Goal state after: