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

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

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

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

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
γ : Type x
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ t
h : t ⊆ s
⊢ Fintype ↑(s ∩ t)

Tactic:
apply Set.fintypeInterOfLeft

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
op : (j : Fin (n + 1)) → α j → α j → α j
i : Fin (n + 1)
x y : α i
p q : (j : Fin n) → α (i.succAbove j)
⊢ op i x y = op i (i.insertNth x p i) (i.insertNth y q i) ∧
    (fun j ↦ op (i.succAbove j) (p j) (q j)) = i.removeNth fun j ↦ op j (i.insertNth x p j) (i.insertNth y q j)

Tactic:
by unfold removeNth; simp

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

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ i ≤ Fin.find p h ↔ ∀ (m : Fin n), m < i → ¬p m

Tactic:
← not_lt,

Goal state after:
n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
h : ∃ k, p k
i : Fin n
⊢ ¬Fin.find p h < i ↔ ∀ (m : Fin n), m < i → ¬p m
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List α
⊢ (map (⇑OrderDual.toDual) l).SortedLT ↔ l.SortedGT

Tactic:
by
  grind [OrderDual.toDual_lt_toDual]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : List αᵒᵈ
⊢ (map (⇑OrderDual.toDual) l).SortedGT ↔ l.SortedLT

Tactic:
by
  grind [OrderDual.toDual_lt_toDual]

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

Goal state before:
pp: n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
⊢ j.contractNth op g k = g (j.succAbove k)

Tactic:
rcases lt_trichotomy (k : ℕ) j with (h | h | h)

Goal state after:
case inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k < ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

case inr.inl
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑k = ↑j
⊢ j.contractNth op g k = g (j.succAbove k)

case inr.inr
n : ℕ
α : Sort u_1
j : Fin (n + 1)
op : α → α → α
g : Fin (n + 1) → α
k : Fin n
hjk : ↑j ≠ ↑k
h : ↑j < ↑k
⊢ j.contractNth op g k = g (j.succAbove k)
Module: Mathlib.Data.List.Range

Goal state before:
pp: r : ℕ → ℕ → Prop
n : ℕ
⊢ IsChain r (range n) ↔ ∀ (m : ℕ), m < n - 1 → r m m.succ

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    simp only [range_succ, Nat.add_one_sub_one, Nat.lt_sub_iff_add_lt] at hn ⊢
    cases n with
    | zero => simp
    | succ n =>
      simp only [range_succ, Nat.add_lt_add_iff_right, succ_eq_add_one, append_assoc, cons_append,
        nil_append, isChain_append_cons_cons, IsChain.singleton, and_true] at hn ⊢
      rw [hn, forall_lt_succ_right]

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

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

Tactic:
apply nil

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
⊢ (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b) → IsChain R l

Tactic:
induction l using twoStepInduction with
  | nil => grind
  | singleton => grind
  | cons_cons head head' tail _ ih =>
    refine fun h ↦ isChain_cons_cons.mpr ⟨h (nil_append _).symm, ih _ fun ⦃a b l₁ l₂⦄ eq => ?_⟩
    apply h
    rw [eq, cons_append]

Goal state after:
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; aesop (add simp List.prod_hom₂_nonempty)

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

Goal state before:
pp: case some
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
f : α → Option β
g : β → Multiset γ
a : α
ham : a ∈ m
b : β
⊢ ((Option.map singleton (some b)).getD 0).bind g = (Option.map g (some b)).getD 0

Tactic:
| some b =>

Goal state after:
Module: Mathlib.Logic.Function.DependsOn

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ DependsOn f s ↔ FactorsThrough f s.domRestrict

Tactic:
rw [DependsOn, FactorsThrough]

Goal state after:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
f : ((i : ι) → α i) → β
s : Set ι
⊢ (∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y) ↔
    ∀ ⦃a b : (i : ι) → α i⦄, s.domRestrict a = s.domRestrict b → f a = f b
Module: Mathlib.Data.Finset.Pi

Goal state before:
pp: case e_f
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
⊢ (fun b ↦ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val)) = fun b ↦
    (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup

Tactic:
funext b

Goal state after:
case e_f
α : Type u_1
β : α → Type u
inst✝¹ : DecidableEq α
inst✝ : (a : α) → DecidableEq (β a)
s : Finset α
t : (a : α) → Finset (β a)
a : α
ha : a ∉ s
b : β a
⊢ Multiset.map (Multiset.Pi.cons s.val a b) (s.val.pi fun a ↦ (t a).val) =
    (Multiset.map (fun f a' h' ↦ Multiset.Pi.cons s.val a b f a' ⋯) (s.val.pi fun a ↦ (t a).val)).dedup
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)

Tactic:
have hp : n = p + 1 := (succ_pred_eq_of_ne_zero hn).symm

Goal state after:
m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * n + n).choose n * ((m * n)! * n !) = (m + 1) * (m * n + n - 1).choose p * ((m * n)! * n !)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (p * n + 1 * n).choose n = (p + 1) * (p * n + 1 * n - 1).choose (n - 1)

Tactic:
Nat.one_mul,

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (p * n + n).choose n = (p + 1) * (p * n + n - 1).choose (n - 1)
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n : ℕ
⊢ n.multichoose 1 = n

Tactic:
induction n with
  | zero => simp
  | succ n IH => simp [multichoose_succ_succ n 0, IH]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
m : Multiset α
t : (a : α) → Multiset (β a)
f : (a : α) → a ∈ m → β a
⊢ f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a

Tactic:
induction m using Multiset.induction_on with
  | empty =>
    have : f = Pi.empty β := funext (fun _ => funext fun h => (notMem_zero _ h).elim)
    simp only [this, pi_zero, mem_singleton, true_iff]
    intro _ h; exact (notMem_zero _ h).elim
  | cons a m ih => ?_

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
β : α → Type u_2
t : (a : α) → Multiset (β a)
a : α
m : Multiset α
ih : ∀ (f : (a : α) → a ∈ m → β a), f ∈ m.pi t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a
f : (a_1 : α) → a_1 ∈ a ::ₘ m → β a_1
⊢ f ∈ (a ::ₘ m).pi t ↔ ∀ (a_1 : α) (h : a_1 ∈ a ::ₘ m), f a_1 h ∈ t a_1
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

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

Tactic:
ext; simp [Prod.ext_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
C : Set (Set α)
t : Set β
⊢ ⋃₀ C ×ˢ t = ⋃₀ ((fun s ↦ s ×ˢ t) '' C)

Tactic:
simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
T : Set (Set β)
hT : T.Nonempty
s : Set α
⊢ ⋂ r ∈ {s} ×ˢ T, r.1 ×ˢ r.2 = ⋂ t ∈ T, s ×ˢ t

Tactic:
simp_rw [singleton_prod, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right]

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : MulOneClass M
s : Set M
motive : (x y : M) → x ∈ closure s → y ∈ closure s → Prop
mem : ∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯
one_left : ∀ (x : M) (hx : x ∈ closure s), motive 1 x ⋯ hx
one_right : ∀ (x : M) (hx : x ∈ closure s), motive x 1 hx ⋯
mul_left :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : M) (hx : x ∈ closure s) (hy : y ∈ closure s) (hz : z ∈ closure s),
    motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯
x y : M
hx : x ∈ closure s
x✝ y✝ : M
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : motive x x✝ hx hx✝
h₂ : motive x y✝ hx hy✝
⊢ motive x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ hx h₁ h₂

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : MulOneClass M
motive : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, motive x
one : motive 1
mul : ∀ (x y : M), motive x → motive y → motive (x * y)
x : M
⊢ motive 1

Tactic:
exact one

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

Goal state before:
pp: case one
M : Type u_1
N : Type u_2
A : Type u_3
inst✝¹ : MulOneClass M
s✝ : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
p : M → Prop
s : Set M
closure : Submonoid.closure s = ⊤
mem : ∀ x ∈ s, p x
one : p 1
mul : ∀ (x y : M), p x → p y → p (x * y)
⊢ p 1

Tactic:
exact one

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

Goal state before:
pp: case mul
G : Type u_1
inst✝ : Group G
k : Set G
p : (x y : G) → x ∈ closure k → y ∈ closure k → Prop
mem : ∀ (x y : G) (hx : x ∈ k) (hy : y ∈ k), p x y ⋯ ⋯
one_left : ∀ (x : G) (hx : x ∈ closure k), p 1 x ⋯ hx
one_right : ∀ (x : G) (hx : x ∈ closure k), p x 1 hx ⋯
mul_left :
  ∀ (x y z : G) (hx : x ∈ closure k) (hy : y ∈ closure k) (hz : z ∈ closure k),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (y z x : G) (hy : y ∈ closure k) (hz : z ∈ closure k) (hx : x ∈ closure k),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
inv_left : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x⁻¹ y ⋯ hy
inv_right : ∀ (x y : G) (hx : x ∈ closure k) (hy : y ∈ closure k), p x y hx hy → p x y⁻¹ hx ⋯
x y : G
hx : x ∈ closure k
x✝ y✝ : G
hx✝ : x✝ ∈ closure k
hy✝ : y✝ ∈ closure k
h₁ : p x x✝ hx hx✝
h₂ : p x y✝ hx hy✝
⊢ p x (x✝ * y✝) hx ⋯

Tactic:
exact mul_right _ _ _ _ _ hx h₁ h₂

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

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1

pp: case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

pp: case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

pp: case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
· intro y hy
    rw [eq_of_mem_singleton hy]
    exact ⟨1, zpow_one x⟩

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
Module: Mathlib.Algebra.Group.Subgroup.Map

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁶ : Group G
inst✝⁵ : Group G'
inst✝⁴ : Group G''
A : Type u_4
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N✝ : Type u_5
inst✝² : Group N✝
P : Type u_6
inst✝¹ : Group P
N : Type u_7
inst✝ : Group N
f : G →* N
H : Subgroup N
a : G
ha : a ∈ ⇑f ⁻¹' ↑H
⊢ f a⁻¹ ∈ H

Tactic:
rw [f.map_inv]; exact H.inv_mem ha

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

Goal state before:
pp: case refine_1.inr
C : Type u_2
inst✝ : CommGroup C
s t : Subgroup C
x : C
h✝ : x ∈ closure (↑s ∪ ↑t)
y : C
h : y ∈ ↑t
⊢ ∃ y_1 ∈ s, ∃ z ∈ t, y_1 * z = y

Tactic:
exact ⟨1, s.one_mem, y, h, by simp⟩

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

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

Tactic:
exact mul_mem_sup hy hz

Goal state after:
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
y : G
hy : y ∈ s
z : G
hz : z ∈ t
⊢ y * z ∈ s ⊔ t

Tactic:
exact mul_mem_sup hy hz

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) ⊔ mrange (inr M N) = ⊤

Tactic:
by
  simp only [mrange_inl, mrange_inr, prod_bot_sup_bot_prod, top_prod_top]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ a ∈ H

Tactic:
rw [← mul_one a, ← inv_one, ← one_mul a]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a : G
h : a ∈ H.normalCore
⊢ 1 * a * 1⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ a • s / b • t = (a / b) • (s / t)

Tactic:
by
  simp_rw [← image_smul, smul_eq_mul, ← singleton_mul, mul_div_mul_comm _ s,
    singleton_div_singleton]

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

Goal state before:
pp: case nil
α : 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)
hpl : ∀ (a : α), a ∈ [] → p a
⊢ f [].prod ≤ (map f []).prod

Tactic:
simp [h_one]

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

Goal state before:
pp: case nil
α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : AddMonoid β
inst✝¹ : Preorder β
inst✝ : AddLeftMono β
l : List α
f : α → β
h_one : f 1 ≤ 0
h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b
⊢ f [].prod ≤ (map f []).sum

Tactic:
simp [h_one]

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

Goal state before:
pp: case one
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
h : (FreeMonoid.lift Subtype.val) 1 ∈ closure s
⊢ motive ((FreeMonoid.lift Subtype.val) 1) h

Tactic:
exact one

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

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

Tactic:
exact one

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

Goal state before:
pp: case one
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)
⊢ motive 1

Tactic:
exact one

Goal state after:
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:
rw [mem_disjSum, or_iff_right]

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ (∃ b_1, b_1 ∈ t ∧ inr b_1 = inr b) ↔ b ∈ t

α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
b : β
⊢ ¬∃ a, a ∈ s ∧ inl a = inr b
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
t : Finset β
u : Finset (α ⊕ β)
⊢ u ⊆ map Embedding.inr t ↔ u.toLeft = ∅ ∧ u.toRight ⊆ t

Tactic:
simp [← empty_disjSum, subset_disjSum]

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

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s : Finset α
h : s.max = ⊥
H : s.Nonempty
a : α
ha : ⊥ = ↑a
⊢ s = ∅

Tactic:
cases ha

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:
by
  rw [powersetCardAux, sublistsLenAux_eq, append_nil]

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

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
⊢ i' ∈ t → ∀ i_2 ∈ t, Disjoint (f (i, i')) (f (j, i_2))

Tactic:
hi'

Goal state after:
case refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
⊢ ∀ i_1 ∈ t, Disjoint (f (i, i')) (f (j, i_1))
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons none (map Embedding.some s) ⋯ ⊆ cons none (map Embedding.some t) ⋯ ↔ s ⊆ t

Tactic:
rw [cons_subset_cons, map_subset_map]

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
⊢ i' ∈ s → ∀ i_2 ∈ s, Disjoint (f (i', i)) (f (i_2, j))

Tactic:
hi'

Goal state after:
case refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : Frame α
s : Set ι
t : Set ι'
f : ι × ι' → α
h : (s ×ˢ t).PairwiseDisjoint f
i : ι'
hi : i ∈ t
j : ι'
hj : j ∈ t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
⊢ ∀ i_1 ∈ s, Disjoint (f (i', i)) (f (i_1, j))
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: P : (α : Type u) → [Fintype α] → Prop
of_equiv : ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β), P α → P β
h_empty : P PEmpty.{u + 1}
h_option : ∀ (α : Type u) [inst : Fintype α], P α → P (Option α)
α✝ : Type u
h_fintype : Fintype α✝
f_empty : ∀ (i : Fintype PEmpty.{u + 1}), P PEmpty.{u + 1} := fun i ↦ ?m.44
α : Type u
hα : Fintype α
Pα : ∀ (h : Fintype α), P α
hα' : Fintype (Option α)
⊢ P (Option α)

Tactic:
convert! h_option α (Pα _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ⨆ c, f (b, c) ≤ c

Tactic:
rw [ciSup_le_iff (h₂ b)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
h₂ : ∀ (b : β), BddAbove (range fun c ↦ f (b, c))
c : α
b : β
| ∀ (i : γ), f (b, i) ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case mp
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
this : OrderBot α
⊢ (∃ i, f i = ⨅ i, f i) ∧ ∀ (i : ι), ⨅ i, f i ≤ f i

Tactic:
exact ⟨ciInf_mem f, ciInf_le (OrderBot.bddBelow ..)⟩

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
⊢ MapsTo f ↑(s.preimage f hf) ↑({x ∈ s | x ∈ Set.range f})

Tactic:
by simp [Set.MapsTo]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
⊢ s.Infinite

Tactic:
have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
s : Set α
inst✝ : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : ℕ → α := fun n ↦ Nat.recOn n ⋯.choose fun x a ↦ ⋯.choose
hf : ∀ (n : ℕ), f n ∈ s
⊢ s.Infinite
Module: Mathlib.Order.Interval.Multiset

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

Tactic:
rw [Ioc, Finset.Ioc_self, Finset.empty_val]

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

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = Iic n

Tactic:
rw [range_succ_eq_Icc_zero]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
⊢ cons ⊤ (Finset.map Embedding.coeWithTop s) ⋯ ⊆ cons ⊤ (Finset.map Embedding.coeWithTop t) ⋯ ↔ s ⊆ t

Tactic:
rw [cons_subset_cons, map_subset_map]

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

Goal state before:
pp: case e'_2
n a : ℕ
⊢ ∀ x ∈ (Finset.Ico n (n + a)).val, ∀ y ∈ (Finset.Ico n (n + a)).val, x % a = y % a → x = y

Tactic:
exact mod_injOn_Ico _ _

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
⊢ WellQuasiOrdered s

Tactic:
intro seq

Goal state after:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
h : WellQuasiOrdered r
f : r →r s
hf : Function.Surjective ⇑f
seq : ℕ → β
⊢ ∃ m n, m < n ∧ s (seq m) (seq n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
by
  rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = insert a (Ioi a)

Tactic:
Ioi_insert

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ Ici a = Ici a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ≠ b ∧ a✝ ≤ b ↔ a✝ ∈ Iio b

Tactic:
mem_Iio,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ≠ b ∧ a✝ ≤ b ↔ a✝ < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ = b ∨ a✝ ∈ Iio b ↔ a✝ ≤ b

Tactic:
mem_Iio,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ = b ∨ a✝ < b ↔ a✝ ≤ b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Group α
inst✝ : MulDistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (submonoid M α).carrier
x✝ : M
⊢ x✝ • x✝¹⁻¹ = x✝¹⁻¹

Tactic:
smul_inv',

Goal state after:
M : Type u
α : Type v
inst✝² : Monoid M
inst✝¹ : Group α
inst✝ : MulDistribMulAction M α
x✝¹ : α
ha : x✝¹ ∈ (submonoid M α).carrier
x✝ : M
⊢ (x✝ • x✝¹)⁻¹ = x✝¹⁻¹