mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = k ! * n.choose k

Tactic:
rw [Nat.mul_comm]

Goal state after:
case inr
n k : ℕ
h : n ≥ k
⊢ n.descFactorial k = n.choose k * k !
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
⊢ ∀ ⦃x : G⦄, x ∈ S ^ (n + 1) → x * a * a⁻¹ ∈ S ^ (n + 1)

Tactic:
intro x hx

Goal state after:
case inr
G : Type u_5
inst✝² : Group G
inst✝¹ : Fintype G
S : Set G
inst✝ : (k : ℕ) → DecidablePred fun x ↦ x ∈ S ^ k
hG : 0 < Fintype.card G
a : G
ha : a ∈ S
key :
  ∀ (a : G) (s t : Set G) [inst : Fintype ↑s] [inst_1 : Fintype ↑t],
    (∀ b ∈ s, b * a ∈ t) → Fintype.card ↑s ≤ Fintype.card ↑t
mono : Monotone fun n ↦ Fintype.card ↑(S ^ n)
x✝ n : ℕ
h : Fintype.card ↑(S ^ n) = Fintype.card ↑(S ^ (n + 1))
h₂ : S ^ n * {a} = S ^ (n + 1)
x : G
hx : x ∈ S ^ (n + 1)
⊢ x * a * a⁻¹ ∈ S ^ (n + 1)
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f (↑c * a) = f b * f ↑c

Tactic:
hc.eq,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
a b : α
c : αˣ
hc : SemiconjBy (↑c) a b
⊢ f (b * ↑c) = f b * f ↑c
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (range f)⁻¹ = range fun i ↦ (f i)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Goal state after:
α : Type u_2
inst✝ : InvolutiveInv α
ι : Sort u_5
f : ι → α
⊢ (fun x ↦ x⁻¹) '' range f = range fun i ↦ (f i)⁻¹
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ b ∈ t, (fun a ↦ (a, b)) '' s

Tactic:
by
  rw [iUnion_image_right, image2_mk_eq_prod]

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

Goal state before:
pp: case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
⊢ ↑(closure s) ⊆ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
intro x hx

Goal state after:
case a
M : Type u_1
inst✝ : MulOneClass M
s : Set M
x : M
hx : x ∈ ↑(closure s)
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → Inv (α i)
s : Set ι
t : (i : ι) → Set (α i)
⊢ (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹

Tactic:
by ext x; simp

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup G
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup (Additive G)
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : AddSubgroup A
⊢ (fun S ↦
        let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
        { toAddSubmonoid := __src, neg_mem' := ⋯ })
      ((fun S ↦
          let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
          { toSubmonoid := __src, inv_mem' := ⋯ })
        x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
x : Subgroup (Multiplicative A)
⊢ (fun S ↦
        let __src := AddSubmonoid.toSubmonoid S.toAddSubmonoid;
        { toSubmonoid := __src, inv_mem' := ⋯ })
      ((fun S ↦
          let __src := Submonoid.toAddSubmonoid S.toSubmonoid;
          { toAddSubmonoid := __src, neg_mem' := ⋯ })
        x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
h : Surjective ⇑f
⊢ map f ⊤ = ⊤

Tactic:
rw [eq_top_iff]
  intro x _
  obtain ⟨y, hy⟩ := h x
  exact ⟨y, trivial, hy⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H.subgroupOf K = ⊤ ↔ K ≤ H

Tactic:
rw [← top_subgroupOf, subgroupOf_inj, top_inf_eq, inf_eq_right]

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 : Subgroup G
⊢ comap f (map f H) ≤ H ⊔ f.ker

Tactic:
intro x hx

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup G
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
P : C → Prop
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
by
  simp [mem_sup]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S x : Submonoid M
⊢ (fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
S : Submonoid M
x : AddSubmonoid (Additive M)
⊢ (fun S ↦ { carrier := ⇑Additive.toMul ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Additive.ofMul ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
x : AddSubmonoid A
⊢ (fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ }) x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type u_4
inst✝ : AddZeroClass A
x : Submonoid (Multiplicative A)
⊢ (fun S ↦ { carrier := ⇑Multiplicative.toAdd ⁻¹' ↑S, mul_mem' := ⋯, one_mem' := ⋯ })
      ((fun S ↦ { carrier := ⇑Multiplicative.ofAdd ⁻¹' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }) x) =
    x

Tactic:
cases x; rfl

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

Goal state before:
pp: case mp.right
N : Type u_2
inst✝¹ : MulOneClass N
M : Type u_5
inst✝ : MulOneClass M
s : Submonoid M
t : Submonoid N
u : Submonoid (M × N)
h : s.prod t ≤ u
⊢ map (inr M N) t ≤ u

Tactic:
· rintro _ ⟨x, hx, rfl⟩
      apply h
      exact ⟨Submonoid.one_mem _, hx⟩

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
⊢ mrange (inl M N) = ⊤.prod ⊥

Tactic:
simpa only [mrange_eq_map] using map_inl ⊤

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : N →* G
x : N
h : ∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H
n : N
⊢ f n ∈ H ↔ f (x * n * x⁻¹) ∈ H

Tactic:
simp [h (f n)]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
⊢ map f (normalizer ↑H) ≤ normalizer ↑(map f H)

Tactic:
intro x hx

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
N : Type u_5
inst✝ : Group N
f : G →* N
x : N
hx : x ∈ map f (normalizer ↑H)
⊢ x ∈ normalizer ↑(map f H)
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
hp_prod : p s.prod
⊢ f (a * s.prod) ≤ (map f (a :: s)).prod

Tactic:
map_cons,

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) ≤ (f a :: map f s).prod
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ f (a * l.prod) ≤ (map f (a :: l)).prod

Tactic:
map_cons,

Goal state after:
case cons
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
l : List α
ih : l ≠ [] → (∀ (a : α), a ∈ l → p a) → f l.prod ≤ (map f l).prod
hl_nonempty : a :: l ≠ []
hl : ∀ (a_1 : α), a_1 ∈ a :: l → p a_1
⊢ f (a * l.prod) ≤ (f a :: map f l).prod
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
a b : Lex (α × β)
⊢ compare a b = compareOfLessAndEq a b

Tactic:
have : DecidableLT (α ×ₗ β) := Prod.Lex.decidable _ _
    have : Std.LawfulBEqOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_eq]⟩
    have : Std.LawfulLTOrd (α ×ₗ β) := ⟨by
      simp [compare_def, compareLex, compareOn, Ordering.then_eq_lt, toLex_lt_toLex,
        compare_lt_iff_lt]⟩
    convert! Std.LawfulLTCmp.eq_compareOfLessAndEq (cmp := compare) a b

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

Goal state before:
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
w✝¹ : x ∈ ⨆ i, S i
Cx : motive x w✝¹
w✝ : y ∈ ⨆ i, S i
Cy : motive y w✝
⊢ ∃ (hm : x * y ∈ ⨆ i, S i), motive (x * y) hm

Tactic:
exact ⟨_, mul _ _ _ _ Cx Cy⟩

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
α : Type u_4
f : α → M
⊢ mrange (FreeMonoid.lift f) = closure (Set.range f)

Tactic:
rw [mrange_eq_map, ← FreeMonoid.closure_range_of, map_mclosure, ← Set.range_comp,
    FreeMonoid.lift_comp_of]

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

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
y : N
z : α
⊢ (x • x' • y) • z = x • x' • y • z

Tactic:
hs x hx,

Goal state after:
case refine_2
M : Type u_1
N : Type u_4
α : Type u_5
inst✝³ : Monoid M
inst✝² : MulAction M N
inst✝¹ : SMul N α
inst✝ : MulAction M α
s : Set M
htop : Submonoid.closure s = ⊤
hs : ∀ x ∈ s, ∀ (y : N) (z : α), (x • y) • z = x • y • z
x : M
hx : x ∈ s
x' : M
hx' : ∀ (y : N) (z : α), (x' • y) • z = x' • y • z
y : N
z : α
⊢ x • (x' • y) • z = x • x' • y • z
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: N : Type u_4
inst✝ : CommMonoid N
P : N → Prop
s t : Submonoid N
⊢ (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)

Tactic:
by
  simp [mem_sup]

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

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

Tactic:
by ext x; simp

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

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

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toLeft = u.toLeft ∩ v.toLeft

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∩ v).toRight = u.toRight ∩ v.toRight

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toRight = u.toRight ∪ v.toRight

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toLeft = u.toLeft \ v.toLeft

Tactic:
by ext x; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u \ v).toRight = u.toRight \ v.toRight

Tactic:
by ext x; simp

Goal state after:
Module: Mathlib.Order.Hom.Bounded

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ f a = f ⊤ ↔ a = ⊤

Tactic:
(EquivLike.injective f).eq_iff

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : EquivLike F α β
inst✝⁴ : LE α
inst✝³ : OrderTop α
inst✝² : PartialOrder β
inst✝¹ : OrderTop β
inst✝ : OrderIsoClass F α β
f : F
a : α
⊢ a = ⊤ ↔ a = ⊤
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min = ↑a

Tactic:
rw [← insert_empty_eq]
  exact min_insert

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

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

Tactic:
map_cons,

Goal state after:
α : Type u
β : Type v
f : α → β
a : α
l : List α
⊢ (f a :: map f l).sublists = map (map f) (a :: l).sublists
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inl
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ (l₂' ++ [a]) ~ l' ++ [a]

Tactic:
rw [← append_assoc]

Goal state after:
case append_singleton.inl
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁ l₂' : List α
h : (l₁, l₂') ∈ l'.sublists.zip l'.sublists.reverse
⊢ id l₁ ++ l₂' ++ [a] ~ l' ++ [a]
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ (id l₂ ++ [a]) ~ l' ++ [a]

Tactic:
rw [← append_assoc]

Goal state after:
case append_singleton.inr
α : Type u
l' : List α
a : α
ih : ∀ (l₁ l₂ : List α), (l₁, l₂) ∈ l'.sublists.zip l'.sublists.reverse → l₁ ++ l₂ ~ l'
l₁' l₂ : List α
h : (l₁', l₂) ∈ l'.sublists.zip l'.sublists.reverse
⊢ l₁' ++ id l₂ ++ [a] ~ l' ++ [a]
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ (insert a r).sup id ≤ z

Tactic:
sup_insert,

Goal state after:
case right
α : Type u_7
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Set α
hs : s.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
r : Finset α
a✝ : a ∉ r
ih : (∀ x ∈ r, ∃ y ∈ s, x ≤ y) → ∃ x ∈ s, r.sup id ≤ x
h : ∀ x ∈ insert a r, ∃ y ∈ s, x ≤ y
incs : ↑r ⊆ ↑(insert a r)
x : α
hxs : x ∈ s
hsx_sup : r.sup id ≤ x
y : α
hys : y ∈ s
hay : a ≤ y
z : α
hzs : z ∈ s
hxz : x ≤ z
hyz : y ≤ z
⊢ id a ⊔ r.sup id ≤ z
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
n : ℕ
s : Finset α
⊢ powersetCard n s = {x ∈ s.powerset | #x = n}

Tactic:
by
  ext
  simp [mem_powersetCard]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
⊢ ∀ ⦃x : α⦄, x ∈ u → x ∈ (powersetCard n.succ u).biUnion id

Tactic:
intro x hx

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
u : Finset α
n : ℕ
hn : n < #u
x : α
hx : x ∈ u
⊢ x ∈ (powersetCard n.succ u).biUnion id
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
⊢ ∃ a, f i ≤ if a ∈ s then f a else sSup ∅

Tactic:
refine ⟨i, ?_⟩

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
s : Finset ι
h : ∃ x ∈ s, sSup ∅ ≤ f x
h' : (image f s).Nonempty
i : ι
hi : i ∈ s
⊢ f i ≤ if i ∈ s then f i else sSup ∅
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
h✝ : IsEmpty (κ i)
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅

pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅

Tactic:
· exact iSup_of_empty' (f i) ▸ le_sup_right

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
κ : ι → Sort u_5
f : (i : ι) → κ i → α
H : BddAbove (⋃ i, range (f i))
a : α
h : a ∈ upperBounds (⋃ i, range (f i))
x : α
x✝ : x ∈ range fun i ↦ ⨆ j, f i j
i : ι
hx : (fun i ↦ ⨆ j, f i j) i = x
h✝ : Nonempty (κ i)
⊢ (fun i ↦ ⨆ j, f i j) i ≤ a ⊔ sSup ∅
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: case h_empty
α : Type u
ι✝ : Sort v
κ✝ : ι✝ → Sort w
inst✝² : Order.Frame α
inst✝¹ : Finite ι✝
f✝ : (a : ι✝) → κ✝ a → α
ι : Type v
inst✝ : Finite ι
κ : PEmpty.{v + 1} → Type w
f : (a : PEmpty.{v + 1}) → κ a → α
⊢ ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)

Tactic:
simp [iInf_of_empty, iSup_const]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : Ioo a b = {c}
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
simp_rw [Set.ext_iff, mem_Ioo, mem_singleton_iff] at h
    have ⟨hac, hcb⟩ := (h c).mpr rfl
    exact ⟨⟨hac, fun d had hdc ↦ hdc.ne ((h d).mp ⟨had, hdc.trans hcb⟩)⟩,
      ⟨hcb, fun d hcd hdb ↦ hcd.ne ((h d).mp ⟨hac.trans hcd, hdb⟩).symm⟩⟩

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: case top
α : Type u_1
inst✝¹ : LinearOrder α
a : α
inst✝ : OrderTop α
x✝ : IsTop ⊤ ∧ a ⋖ ⊤
hab : a ⋖ ⊤
⊢ Ioi a = {⊤}

Tactic:
rwa [← Ioc_top, Ioc_eq_singleton_right_iff]

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: ⊢ ∀ {a b : Bool}, a ⩿ b ↔ a ≤ b

Tactic:
by unfold WCovBy; decide

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ x, ↑(f x) = ⊤ ↔ IsEmpty ι

Tactic:
simp [isEmpty_iff]

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

Goal state before:
pp: α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
⊢ SurjOn Subtype.val (Subtype.val ⁻¹' ↑t) ↑t

Tactic:
intro x hx

Goal state after:
α : Type u
inst✝¹ : Lattice α
inst✝ : OrderBot α
P : α → Prop
Psup : ∀ ⦃s t : α⦄, P s → P t → P (s ⊔ t)
Pbot : P ⊥
t : Finset α
ht : ∀ x ∈ t, P x
this : OrderBot (Subtype P) := Subtype.orderBot Pbot
x : α
hx : x ∈ ↑t
⊢ x ∈ Subtype.val '' Subtype.val ⁻¹' ↑t
Module: Mathlib.Order.Interval.Multiset

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

Tactic:
by rw [Icc, ← Finset.mem_def, Finset.mem_Icc]

Goal state after:
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) (Ico a b) = Ico a c

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
  rfl

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

Goal state before:
pp: case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

Tactic:
obtain hi | hi := lt_or_ge i (n % a)

Goal state after:
case inr.mpr.inl
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i

case inr.mpr.inr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : n % a ≤ i
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ (Icc a b).Nonempty ↔ a ≤ b

Tactic:
rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]

Goal state after: