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

Goal state before:
pp: α : 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)) ⋯
ix : ℕ
⊢ tl[ix]? = l'[f 0 + 1 + f' ix]?

Tactic:
OrderEmbedding.coe_ofMapLEIff,

Goal state after:
α : 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)) ⋯
ix : ℕ
⊢ tl[ix]? = l'[f 0 + 1 + (f (ix + 1) - (f 0 + 1))]?
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
⊢ ∀ (hts : Insert.insert a s ⊆ s✝), motive (Insert.insert a s) ⋯

Tactic:
haS

Goal state after:
α : Type u
motive : (s : Set α) → s.Finite → Prop
s✝ : Set α
hs : s✝.Finite
empty : motive ∅ ⋯
insert : ∀ {a : α} {t : Set α}, a ∈ s✝ → ∀ (hts : t ⊆ s✝), a ∉ t → motive t ⋯ → motive (Insert.insert a t) ⋯
a : α
s : Set α
has : a ∉ s
hs✝ : s.Finite
hCs : ∀ (hts : s ⊆ s✝), motive s ⋯
haS : Insert.insert a s ⊆ s✝
⊢ motive (Insert.insert a s) ⋯
Module: Mathlib.Data.List.Sort

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

Tactic:
by simpa using Std.Total.total a b

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Infinite ↔ Infinite α

Tactic:
simpa using (finite_range_iff hf).not

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₁ b₂) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
hc.comm,

Goal state after:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ Multiset.fold op (op b₂ b₁) (Multiset.map f s₁.val + Multiset.map f s₂.val) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
Module: Mathlib.Data.List.Pairwise

Goal state before:
pp: case H₁
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
⊢ ∀ (x : α), x ∈ l → x ≠ x → R x x

Tactic:
exact fun _ _ ↦ absurd rfl

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

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

Tactic:
by
  rw [isChain_cons_split, isChain_cons_cons]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
h : ¬IsChain R l
⊢ ∃ n h, ¬R l[n] l[n + 1]

Tactic:
simp_all [isChain_iff_getElem]

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

Goal state before:
pp: α : Type u
l : List α
hl : l.Nodup
i j : ℕ
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
rcases eq_or_ne l [] with rfl | hn
  · simp
  · simp only [hn, or_false]
    refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩
    rw [← rotate_mod, h, rotate_mod]

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

Goal state before:
pp: α : Type u
l l' : List α
⊢ l.reverse ~r l' ↔ l ~r l'.reverse

Tactic:
constructor <;>
    · intro h
      simpa using h.reverse

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
T : Multiset M
⊢ a ∈ S → T ⊆ S → (map g1 T).prod ∣ (map g2 T).prod → (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod

Tactic:
haS

Goal state after:
case h₂
M : Type u_5
N : Type u_6
inst✝ : CommMonoid N
S : Multiset M
g1 g2 : M → N
h : ∀ (a : M), a ∈ S → g1 a ∣ g2 a
a : M
T : Multiset M
haS : a ∈ S
⊢ T ⊆ S → (map g1 T).prod ∣ (map g2 T).prod → (map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod
Module: Mathlib.Data.Nat.Choose.Basic

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

Tactic:
simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

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.choose k.succ * k.succ ! * (n - k.succ)!)

Tactic:
simp [factorial_succ, Nat.mul_comm, Nat.mul_left_comm, Nat.mul_assoc]

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

Goal state before:
pp: case inl
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)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + 1 * n ! + (n - k) * n ! = (n + 1)!

Tactic:
Nat.mul_sub_right_distrib,

Goal state after:
case inl
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)!
h₂ : n.choose k.succ * k.succ ! * ((n - k) * (n - k.succ)!) = (n - k) * n !
h₃ : k * n ! ≤ n * n !
⊢ k * n ! + 1 * n ! + (n * n ! - k * n !) = (n + 1)!
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)
this : Fintype (PLift α)
⊢ Finite ((a : α) → β a)

Tactic:
have := fun a => Fintype.ofFinite (PLift (β a))

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

Goal state before:
pp: ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x ↦ x i) '' ⋂ k, (fun x ↦ x k) ⁻¹' v k = v i

Tactic:
apply Subset.antisymm
    · simp [iInter_subset]
    · intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h✝ : IsEmpty ι
⊢ f '' ⋂ i, s i = ⋂ i, f '' s i

Tactic:
simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : InvolutiveInv α
s : Set α
inst✝ : InvolutiveInv β
f g : α → β
H : ∀ (x : α), x ∈ s → f x⁻¹ = (g x)⁻¹
⊢ f '' s⁻¹ = (g '' s)⁻¹

Tactic:
conv_rhs => rw [← image_inv_eq_inv, image_image, ← image_inv_of_apply_inv_eq H]

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

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : SemilatticeSup α
s : α → Set β
t : α → Set γ
hs : Monotone s
ht : Monotone t
z : β
w : γ
x : α
hz : z ∈ s x
hw : w ∈ t x
⊢ (∃ i, z ∈ s i) ∧ ∃ i, w ∈ t i

Tactic:
exact ⟨⟨x, hz⟩, x, hw⟩

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

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

Tactic:
refine ⟨fun h => ?_, ?_⟩
  · have hst : (s * t).Nonempty := h.symm.subst one_nonempty
    obtain ⟨a, ha⟩ := hst.of_image2_left
    obtain ⟨b, hb⟩ := hst.of_image2_right
    have H : ∀ {a b}, a ∈ s → b ∈ t → a * b = (1 : α) := fun {a b} ha hb =>
      h.subset <| mem_image2_of_mem ha hb
    refine ⟨a, b, ?_, ?_, H ha hb⟩ <;> refine eq_singleton_iff_unique_mem.2 ⟨‹_›, fun x hx => ?_⟩
    · exact (eq_inv_of_mul_eq_one_left <| H hx hb).trans (inv_eq_of_mul_eq_one_left <| H ha hb)
    · exact (eq_inv_of_mul_eq_one_right <| H ha hx).trans (inv_eq_of_mul_eq_one_right <| H ha hb)
  · rintro ⟨b, c, rfl, rfl, h⟩
    rw [singleton_mul_singleton, h, singleton_one]

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:
by
    rintro ⟨y, hy, z, hz, rfl⟩; exact mul_mem_sup hy hz

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H K : Subgroup G
⊢ map f H ≤ map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker

Tactic:
simp only [map_le_map_iff, sup_le_iff, le_sup_right, and_true]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker 1 = ⊤

Tactic:
by
  ext
  simp [mem_mker]

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

Goal state before:
pp: motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n

Tactic:
simpa only [bitCasesOn_bit] using congr_fun h (bit b n)

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

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

Tactic:
simp at h₁

Goal state after:
case neg
a₁ a₂ b : ℕ
h : a₁ < a₂
h₁ : b ≤ a₁
⊢ 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 neg
a b₁ b₂ : ℕ
h : b₁ < b₂
h₁ : ¬a < b₁
⊢ a * a + (a + b₁) < if a < b₂ then b₂ * b₂ + a else a * a + (a + b₂)

Tactic:
by_cases h₂ : a < b₂

Goal state after:
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₂)

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₂)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Characteristic
⊢ (⨆ i ∈ s, H i).Characteristic

Tactic:
simp [← iSup_subtype'', characteristic_iSup, h]

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

Goal state before:
pp: case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective f
head : β
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
⊢ ∃ a, (map f) a = of head * tail

Tactic:
specialize fs head

Goal state after:
case mpr.of_mul
α : Type u_1
β : Type u_2
f : α → β
head : β
fs : ∃ a, f a = head
tail : FreeMonoid β
ih : ∃ a, (map f) a = tail
⊢ ∃ a, (map f) a = of head * tail
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map f l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
apply List.prod_le_prod'

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → f i ≤ max (f i) (g i)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ (map g l).prod ≤ (map (fun i ↦ max (f i) (g i)) l).prod

Tactic:
apply List.prod_le_prod'

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
l : List α
f g : α → M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
⊢ ∀ (i : α), i ∈ l → g i ≤ max (f i) (g i)
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map f l).prod

Tactic:
apply List.prod_le_prod'

Goal state after:
case left
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ f i
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ (map (fun i ↦ min (f i) (g i)) l).prod ≤ (map g l).prod

Tactic:
apply List.prod_le_prod'

Goal state after:
case right
α : Type u_2
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
l : List α
f g : α → M
⊢ ∀ (i : α), i ∈ l → min (f i) (g i) ≤ g i
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case nil
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
x : M
h₁ : x ∈ []
⊢ x ≤ [].prod

Tactic:
simp at h₁

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

Goal state before:
pp: A : Type u_2
inst✝ : AddMonoid A
x : A
⊢ ⇑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (Multiplicative.ofAdd x))

Tactic:
symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_powers_eq_multiples_ofMul

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

Goal state before:
pp: case append_singleton.none
α : 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 ∈ Option.casesOn (foldl (argAux r) o tl) (some a) fun c ↦ if r a c then some a else some c
hf : foldl (argAux r) o tl = none
⊢ ¬r b m

Tactic:
rw [hf] at ho
    rw [foldl_argAux_eq_none] at hf
    simp_all [hf.1, hf.2, hr₀.irrefl _]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ s.card + (map inr t).card = s.card + t.card

Tactic:
card_map

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ s.card + t.card = s.card + t.card
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
⊢ m ∈ argmax f l

Tactic:
rcases harg : argmax f l with - | n

Goal state after:
case none
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
harg : argmax f l = none
⊢ m ∈ none

case some
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
l : List α
m : α
inst✝ : DecidableEq α
hml : m ∈ l
ham : ∀ (a : α), a ∈ l → f a ≤ f m
hma : ∀ (a : α), a ∈ l → f m ≤ f a → idxOf m l ≤ idxOf a l
n : α
harg : argmax f l = some n
⊢ m ∈ some n
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case mpr
α : Type u
hd : α
tl : List α
ih : ∀ {init tail : List α}, (init, tail) ∈ tl.inits.zip tl.tails ↔ init ++ tail = tl
init tail : List α
⊢ init ++ tail = hd :: tl →
    (init, tail) = ([], hd :: tl) ∨
      ∃ a b, (a, b) ∈ tl.inits.zip tl.tails ∧ Prod.map (fun t ↦ hd :: t) id (a, b) = (init, tail)

Tactic:
rcases init with - | ⟨hd', tl'⟩
      · simp
      · intro h
        right
        use tl', tail
        simp_all

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

Goal state before:
pp: α : Type u_1
s : Multiset α
powerset : s.powerset = {0}
⊢ s = 0

Tactic:
simpa using congr(card $powerset)

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

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
⊢ powersetCardAux n l = List.map ofList (sublistsLen n l)

Tactic:
powersetCardAux,

Goal state after:
α : Type u_1
n : ℕ
l : List α
⊢ sublistsLenAux n l ofList [] = List.map ofList (sublistsLen n l)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x ∈ s, t x)

Tactic:
biUnion_eq_iUnion

Goal state after:
α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x, t ↑x)
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
inst✝ : Finite ↑s
t : ι → Set α
H : ∀ i ∈ s, Finite ↑(t i)
⊢ Finite ↑(⋃ x ∈ s, t x)

Tactic:
by
  rw [biUnion_eq_iUnion]
  have : ∀ i : s, Finite (t i) := fun i => H i i.property
  infer_instance

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

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
biUnion_eq_iUnion

Goal state after:
α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
this : Finite ↑s
⊢ (⋃ x, t ↑x ⋯).Finite
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ i ∈ a, s i).Infinite

Tactic:
biUnion_eq_iUnion

Goal state after:
α : Type u
ι : Type u_1
s : ι → Set α
a : Set ι
ha : a.Infinite
hs : InjOn s a
⊢ (⋃ x, s ↑x).Infinite
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x ∈ {c}
⊢ a = c ∧ a ⋖ b

Tactic:
mem_singleton_iff

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : ∀ (x : α), a ≤ x ∧ x < b ↔ x = c
⊢ a = c ∧ a ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), a < x ∧ x < b ↔ x ∈ {c}
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
mem_singleton_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), a < x ∧ x < b ↔ x = c
⊢ a ⋖ c ∧ c ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ∀ (x : α), a < x ↔ x ∈ {b}
⊢ IsTop b ∧ a ⋖ b

Tactic:
mem_singleton_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ∀ (x : α), a < x ↔ x = b
⊢ IsTop b ∧ a ⋖ b
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
⊢ (TransGen fun x1 x2 ↦ x1 ⩿ x2) = ReflTransGen fun x1 x2 ↦ x1 ⋖ x2

Tactic:
rw [wcovBy_eq_reflGen_covBy, transGen_reflGen]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac : a < c
hcb : c < b
⊢ a i < c i

Tactic:
obtain ⟨hac, j, hj⟩ := Pi.lt_def.1 hac

Goal state after:
ι : Type u_3
α : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
inst✝ : Nonempty ι
i : ι
hab : a i ⩿ b i
h : ∀ (j : ι), j ≠ i → AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) (a j) (b j)
c : (i : ι) → α i
hac✝ : a < c
hcb : c < b
hac : a ≤ c
j : ι
hj : a j < c j
⊢ a i < c i
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b

Tactic:
Ioc,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ (Finset.Ioc a b).val ↔ a < x ∧ x ≤ b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc a b = 0 ↔ ¬a < b

Tactic:
Ioc,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ (Finset.Ioc a b).val = 0 ↔ ¬a < b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ Ioc a a = 0

Tactic:
Ioc,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ (Finset.Ioc a a).val = 0
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ filter (fun x ↦ x < c) (Finset.Ico a b).val = ∅

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hca : c ≤ a
⊢ {x ∈ Finset.Ico a b | x < c}.val = ∅
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hbc : b ≤ c
⊢ filter (fun x ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a b).val

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hbc : b ≤ c
⊢ {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a b).val
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ filter (fun x ↦ x < c) (Finset.Ico a b).val = Ico a c

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ x < c
hcb : c ≤ b
⊢ {x ∈ Finset.Ico a b | x < c}.val = Ico a c
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hca : c ≤ a
⊢ filter (fun x ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico a b).val

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hca : c ≤ a
⊢ {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico a b).val
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ filter (fun x ↦ b ≤ x) (Finset.Ico a b).val = ∅

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ b ≤ x
⊢ {x ∈ Finset.Ico a b | b ≤ x}.val = ∅
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ filter (fun x ↦ c ≤ x) (Finset.Ico a b).val = Ico c b

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x ↦ c ≤ x
hac : a ≤ c
⊢ {x ∈ Finset.Ico a b | c ≤ x}.val = Ico c b
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ filter (fun x ↦ x ≤ a) (Finset.Ico a b).val = {a}

Tactic:
← Finset.filter_val,

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x ↦ x ≤ a
hab : a < b
⊢ {x ∈ Finset.Ico a b | x ≤ a}.val = {a}