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

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : DecidableRel r
inst✝ : DecidableRel s
f : α → β
l : List α
hl : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → (r a b ↔ s (f a) (f b))
⊢ map f (insertionSort r l) = insertionSort s (map f l)

Tactic:
induction l with
  | nil => simp
  | cons x xs ih =>
    simp_rw [List.forall_mem_cons, forall_and] at hl
    simp_rw [List.map, insertionSort_cons]
    rw [List.map_orderedInsert _ s, ih hl.2.2]
    · simpa only [mem_insertionSort] using hl.2.1
    · simpa only [mem_insertionSort] using hl.1.2

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

Goal state before:
pp: m n : ℕ
α✝ : Fin (n + 1) → Sort u_1
β : Sort u_2
α : Fin (n + 1) → Type u
p : Fin (n + 1)
f : α p × ((i : Fin n) → α (p.succAbove i))
⊢ (fun f ↦ (f p, p.removeNth f)) ((fun f ↦ p.insertNth f.1 f.2) f) = f

Tactic:
by ext <;> simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : Std.Antisymm r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l c : List α
hs : Pairwise r c
hc : c <+~ l
⊢ c <+ insertionSort r l

Tactic:
obtain ⟨d, hc, hd⟩ := hc
  induction l generalizing c d with
  | nil         => grind [nil_perm]
  | cons a _ ih =>
    cases hd with
    | cons  _ h => exact ih hs _ hc h |>.trans (sublist_orderedInsert ..)
    | cons_cons _ h =>
      specialize ih (hs.erase _) _ (erase_cons_head a ‹List _› ▸ hc.erase a) h
      have hm := hc.mem_iff.mp <| mem_cons_self ..
      have he := orderedInsert_erase _ _ hm hs
      exact he ▸ Sublist.orderedInsert_sublist _ ih (pairwise_insertionSort ..)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Infinite α
f : α → β
hi : Injective f
⊢ (range f).Infinite

Tactic:
rw [← image_univ, infinite_image_iff hi.injOn]
  exact infinite_univ

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ ↑⋯.toFinset ⊆ s

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ InjOn f ↑⋯.toFinset

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_3
R : α → α → Prop
l : List α
v : α
hl : IsChain R l
hv : ∀ (lne : l ≠ []), R v (l.head lne)
⊢ IsChain R (v :: l)

Tactic:
cases l <;> grind

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

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
⊢ ∀ (l : List M), op l.prod = (map op l).reverse.prod

Tactic:
intro l; induction l with
  | nil => rfl
  | cons x xs ih =>
    rw [List.prod_cons, List.map_cons, List.reverse_cons', List.prod_concat, op_mul, ih]

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

Goal state before:
pp: M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
h : ∀ (a' : M), a' ≠ a → a' ∈ s → a' = 1
⊢ s.prod = a ^ count a s

Tactic:
induction s using Quotient.inductionOn

Goal state after:
case h
M : Type u_5
inst✝¹ : CommMonoid M
s : Multiset M
inst✝ : DecidableEq M
a : M
a✝ : List M
h : ∀ (a' : M), a' ≠ a → a' ∈ ⟦a✝⟧ → a' = 1
⊢ prod ⟦a✝⟧ = a ^ count a ⟦a✝⟧
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
h : ∀ (x : M), x ∈ s → x = 1
⊢ s.prod = 1

Tactic:
induction s using Quotient.inductionOn

Goal state after:
case h
M : Type u_5
inst✝ : CommMonoid M
s : Multiset M
a✝ : List M
h : ∀ (x : M), x ∈ ⟦a✝⟧ → x = 1
⊢ prod ⟦a✝⟧ = 1
Module: Mathlib.Data.Finset.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
x' : β
hx : x' ∈ ↑t
y' : β
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ f a = x' → ¬(a ∈ s ∧ f a = y')

Tactic:
rintro i ⟨_, rfl⟩ ⟨_, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
i : α
left✝¹ : i ∈ s
hx : f i ∈ ↑t
left✝ : i ∈ s
hy : f i ∈ ↑t
hne : f i ≠ f i
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Goal state before:
pp: ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
s : Multiset ι
hs : s ≠ 0
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) s).prod = f (map f₁ s).prod (map f₂ s).prod

Tactic:
induction s using Quotient.inductionOn

Goal state after:
case h
ι : Type u_2
M : Type u_5
N : Type u_6
O : Type u_7
inst✝² : CommMonoid M
inst✝¹ : CommMonoid N
inst✝ : CommMonoid O
f : M → N → O
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) ⟦a✝⟧).prod = f (map f₁ ⟦a✝⟧).prod (map f₂ ⟦a✝⟧).prod
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
l : List α
this✝ : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
this : 1 + List.count a l < List.count a l * List.count a l
⊢ ¬(List.count a l * List.count a l - if a = a then List.count a l else 0) ≤ 1

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
l : List α
this : DecidableEq α := Classical.decEq α
a : α
h : 1 < List.count a l
⊢ 1 + List.count a l < List.count a l + List.count a l

Tactic:
by simpa

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

Goal state before:
pp: ι : Type u_2
π : ι → Type u_3
s t : Finset ι
inst✝ : DecidablePred fun x ↦ x ∈ s
hst : s ⊆ t
u : (i : ↥s) → Set (π ↑i)
⊢ restrict₂ hst ⁻¹' Set.univ.pi u = Set.univ.pi fun j ↦ if h : ↑j ∈ s then u ⟨↑j, h⟩ else Set.univ

Tactic:
by
  grind [restrict₂]

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

Goal state before:
pp: case mem.mem
M : Type u_1
inst✝ : Mul M
s : Set M
p : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    p z x hz hx → p z y hz hy → p z (x * y) hz ⋯
x y z : M
hz : z ∈ s
x✝ : M
h : x✝ ∈ s
⊢ p z x✝ ⋯ ⋯

Tactic:
exact mem _ _ hz h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsLeftCancelMul α
s t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
c : α
hc : c ∈ s
⊢ c * a ≠ c * b

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Mul α
inst✝ : IsRightCancelMul α
s t : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
c : α
hc : c ∈ t
⊢ a * c ≠ b * c

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : CancelMonoid α
s : Set α
hs : s.Nontrivial
x✝ : 1 ≠ 0
⊢ (s ^ 1).Nontrivial

Tactic:
by simpa

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 ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔ ((fun x ↦ x⁻¹ * a) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty

Tactic:
mul_inv_rev,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun a_1 ↦ a_1⁻¹ * a⁻¹⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ x⁻¹ * a) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty
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 ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔ ((fun x ↦ a * x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty

Tactic:
mul_inv_rev,

Goal state after:
α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
a : α
⊢ ((fun a_1 ↦ a⁻¹⁻¹ * a_1⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty ↔
    ((fun x ↦ a * x⁻¹) '' s ∩ (fun x ↦ x⁻¹) '' t).Nonempty
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set (β → γ)
t : Set (α → β)
u : Set α
⊢ image2 (fun f a ↦ f a) s (image2 (fun f a ↦ f a) t u) = image2 (fun f a ↦ f a) (image2 (fun x1 x2 ↦ x1 ∘ x2) s t) u

Tactic:
exact .symm <| image2_assoc fun _ _ _ ↦ rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
s t : Set α
ht : 1 ∈ t
⊢ 1 ∈ t⁻¹

Tactic:
by simpa

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

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
A : Type u_3
inst✝³ : Monoid M✝
inst✝² : Monoid N✝
s✝ : Set M✝
M : Type ?u.13
N : Type ?u.15
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Set M
f : M → N
hs : closure s = ⊤
h1 : f 1 = 1
hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y
x y : M
⊢ ∀ (x : M), f (x * 1) = f x * f 1

Tactic:
by simp [h1]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ g ∈ normalizer S ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S

Tactic:
← inv_mem_iff,

Goal state after:
G : Type u_1
inst✝ : Group G
S : Set G
g : G
⊢ g⁻¹ ∈ normalizer S ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ map f (H ⊓ K) = map f H ⊓ map f K

Tactic:
← SetLike.coe_set_eq

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H K : Subgroup G
f : G →* N
hf : Injective ⇑f
⊢ ↑(map f (H ⊓ K)) = ↑(map f H ⊓ map f K)
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
x : G
⊢ x ∈ f.toHomUnits.ker ↔ x ∈ f.ker

Tactic:
simp [mem_ker, Units.ext_iff]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

Tactic:
by_cases h : p

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h

case neg
G : Type u_1
inst✝ : Group G
p : Prop
K : p → Subgroup G
x : G
h : ¬p
⊢ x ∈ ⨆ (h : p), K h ↔ x = 1 ∨ ∃ (h : p), x ∈ K h
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n)) (f (Directed.sequence f hf (n + 1)))

Tactic:
dsimp [Directed.sequence]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Inhabited α
r : β → β → Prop
f : α → β
hf : Directed r f
n : ℕ
⊢ r (f (Directed.sequence f hf n))
    (f
      (match decode n with
      | none => Classical.choose ⋯
      | some a => Classical.choose ⋯))
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ normalizer s
⊢ g ∈ normalizer ↑(closure s)

Tactic:
mem_normalizer_iff_conj_image_eq

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : ⇑(MulAut.conj g) '' s = s
⊢ g ∈ normalizer ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
⊢ closure s ≤ normalClosure s

Tactic:
simp only [subset_normalClosure, closure_le]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → f i ≤ g i
⊢ Forall₂ (fun x1 x2 ↦ x1 ≤ x2) (map f l) (map g l)

Tactic:
by simpa

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

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝² : AddZeroClass M
inst✝¹ : Zero N
inst✝ : LinearOrder N
f : M → N
h0 : f 0 ≤ 0
hadd : ∀ (x y : M), f (x + y) ≤ max (f x) (f y)
l : List M
⊢ f l.sum ≤ foldr max 0 (map f l)

Tactic:
induction l with
  | nil => simpa using h0
  | cons hd tl IH =>
    simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
    exact (hadd _ _).trans (max_le_max le_rfl IH)

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

Tactic:
by_cases h : p

Goal state after:
case pos
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h

case neg
M : Type u_1
inst✝ : MulOneClass M
p : Prop
S : p → Submonoid M
x : M
h : ¬p
⊢ x ∈ ⨆ (h : p), S h ↔ x = 1 ∨ ∃ (h : p), x ∈ S h
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type ?u.8
β : Type ?u.9
x✝ : (f : α ↪ β) × ↑(range ⇑f)ᶜ
f : α ↪ β
y : β
hy : y ∈ (range ⇑f)ᶜ
⊢ (fun f ↦ ⟨Embedding.some.trans f, ⟨f none, ⋯⟩⟩) ((fun f ↦ f.fst.optionElim ↑f.snd ⋯) ⟨f, ⟨y, hy⟩⟩) = ⟨f, ⟨y, hy⟩⟩

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ (subtypeOrLeftEmbedding p q) ((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x) = Sum.inr x

Tactic:
rw [subtypeOrLeftEmbedding_apply_right]

Goal state after:
case inr
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ Sum.inr ⟨↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x), ⋯⟩ = Sum.inr x

case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
this : ¬p ↑x
⊢ ¬p ↑((Subtype.impEmbedding q (fun x ↦ p x ∨ q x) ⋯) x)

Tactic:
by simpa

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x : M
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
⊢ motive x

Tactic:
refine closure_induction (fun x hx => ?_) one (fun _ _ _ _ ↦ mul _ _) hx

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
motive : M → Prop
x✝ : M
hx✝ : x✝ ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
hx : x ∈ ⋃ i, ↑(S i)
⊢ motive x
Module: Mathlib.Data.Finset.Sum

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

Tactic:
simp [subset_iff]

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

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

Tactic:
simp [subset_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
ha : inl a ∉ u
⊢ a ∉ u.toLeft

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
s₁ s₂ : Finset α
t₁ t₂ : Finset β
a✝ : α
b✝ : β
x : α ⊕ β
u v : Finset (α ⊕ β)
a : α
b : β
hb : inr b ∉ u
⊢ b ∉ u.toRight

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = (image (⇑ofDual) s).min

Tactic:
rw [min_eq_inf_withTop, inf_image]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithBot.map (⇑ofDual) s.max = s.inf (WithTop.some ∘ ⇑ofDual)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = (image (⇑toDual) s).min

Tactic:
rw [min_eq_inf_withTop, inf_image]

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
⊢ WithBot.map (⇑toDual) s.max = s.inf (WithTop.some ∘ ⇑toDual)
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
y : α
hy : y ∈ s ∧ x < y
⊢ y ∈ s ∧ x < y

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
h : ∃ y ∈ s, x < y
Hne : {x_1 ∈ s | x < x_1}.Nonempty
aux : {x_1 ∈ s | x < x_1}.min' Hne ∈ s ∧ x < {x_1 ∈ s | x < x_1}.min' Hne
z : α
hzs : z ∈ s
hz : x < z
⊢ x < z

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
hxy : x < y
a : α
hat : a ∈ t
hxa : x < a
hay : a < y
⊢ x < a

Tactic:
by simpa

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

Goal state before:
pp: case H.inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DecidableEq α
motive : Finset α → Prop
empty : motive ∅
insert : ∀ (a : α) (s : Finset α), (∀ x ∈ s, x < a) → motive s → motive (Insert.insert a s)
s : Finset α
ih : ∀ s_1 ∈ s, motive (s.erase s_1)
hne : s.Nonempty
H : s.max' hne ∈ s
⊢ motive (Insert.insert (s.max' hne) (s.erase (s.max' hne)))

Tactic:
exact insert _ _ (fun x ↦ s.lt_max'_of_mem_erase_max' hne) (ih _ H)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
h : s.Nonempty
⊢ ∅ ⊆ s ∧ ∅ ≠ s

Tactic:
exact ⟨empty_subset s, h.ne_empty.symm⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
i : ℕ
⊢ Multiset.map val (powersetCard i s).val = Multiset.powersetCard i s.val

Tactic:
simp [Finset.powersetCard, map_pmap, pmap_eq_map, map_id']

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
hn : 0 < n
⊢ powersetCard (#s + n) s = ∅

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ #(s.erase none) = #s

Tactic:
erase_eq_of_notMem h

Goal state after:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ #s = #s
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
⊢ (∃ i, x ∈ s ↑i ∩ t) → x ∈ t

Tactic:
rintro ⟨i, -, H⟩

Goal state after:
case mpr
α : Type u
ι : Type u_1
s : ι → Set α
t : Set α
tfin : t.Finite
h : t ⊆ ⋃ i, s i
I : Set ι
Ifin : I.Finite
hI : t ⊆ ⋃ i ∈ I, s i
x : α
i : ↑{i | i ∈ I}
H : x ∈ t
⊢ x ∈ t
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b

Tactic:
by
  rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]

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

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ t, ⨆ i ∈ t, s i.down

Tactic:
← iSup_eq_iSup_finset,

Goal state after:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ i, s i.down
Module: Mathlib.Order.Cover

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

Tactic:
mem_Ico,

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_3
α : ι → Type u_4
inst✝ : (i : ι) → Preorder (α i)
a b : (i : ι) → α i
h : a ⩿ b
i : ι
ci : α i
h₁ : a i < ci
h₂ : ci < b i
hcb : Function.update a i ci ≤ b
⊢ a < Function.update a i ci

Tactic:
by simpa

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

Goal state before:
pp: α : Type u
β : Type v
s : Finset β
f : α → β
hf : InjOn f (f ⁻¹' ↑s)
inst✝ : DecidablePred fun x ↦ x ∈ Set.range f
⊢ InjOn f ↑(s.preimage f hf)

Tactic:
by simpa

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 ↦ Q x ∧ P x) x ↔ Q x ∧ Minimal P x

Tactic:
by
  simp_rw [iff_comm, and_comm, minimal_and_iff_right_of_imp hPQ, and_comm]

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P : α → Prop
x y : α
inst✝ : PartialOrder α
hy : P y
hP : ∀ ⦃x : α⦄, P x → y ≤ x
⊢ x = y → Minimal P x

Tactic:
rintro rfl; exact ⟨hy, fun z hz _ ↦ hP hz⟩

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy : Q y
⊢ Q x

Tactic:
((h'.le_of_le (hPQ hy)) hyx).antisymm hyx

Goal state after:
case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
y : α
hyx : y ≤ x
hy : Q y
⊢ Q y
Module: Mathlib.Order.Minimal

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
P : α → Prop
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
y : α
hy : P y
h : f y ∈ {x | Minimal (fun x ↦ ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ f y ∈ f '' {x | Minimal P x}

Tactic:
exact mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := Set.ofPred P) hy hf).1 h

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α →o β
hf : Function.Injective ⇑f
hg : Function.Injective ⇑g
h : Set.range ⇑f = Set.range ⇑g
x✝ : α
⊢ Set.range ⇑(OrderEmbedding.ofStrictMono ⇑f ⋯) = Set.range ⇑(OrderEmbedding.ofStrictMono ⇑g ⋯)

Tactic:
by simpa

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
h : 0 < a
x : ℕ
⊢ x ∈ Ico (a - 1) a ↔ x ∈ {a - 1}

Tactic:
mem_Ico,

Goal state after:
a : ℕ
h : 0 < a
x : ℕ
⊢ a - 1 ≤ x ∧ x < a ↔ x ∈ {a - 1}
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Ico (f a) (f b) ↔ a ≤ x ∧ x < b

Tactic:
mem_Ico,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f a ≤ f x ∧ f x < f b ↔ a ≤ x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ a ≤ x ∧ x ≤ b

Tactic:
le_def,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b x : α × β
⊢ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x.1 ≤ b.1 ∧ x.2 ≤ b.2 ↔ (a.1 ≤ x.1 ∧ a.2 ≤ x.2) ∧ x ≤ b