mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ s.card = 0 ↔ s = 0

Tactic:
Multiset.card_eq_zero

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → β
⊢ s = 0 ↔ s = 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l₁ l₂ : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
hl₁ : l₁.Nodup
⊢ a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ ¬a ∈ l₂

Tactic:
by
  rw [hl₁.sdiff_eq_filter, mem_filter, decide_eq_true_iff]

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun x1 x2 ↦ x1 = x2) (map f s) (map f t) ↔ Rel (fun x1 x2 ↦ x1 = x2) s t

Tactic:
rel_map

Goal state after:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b ↦ f a = f b) s t ↔ Rel (fun x1 x2 ↦ x1 = x2) s t
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t

Tactic:
rw [← rel_eq, ← rel_eq, rel_map]
  simp only [hf.eq_iff]

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ l.tails.length = l.length + 1

Tactic:
induction l with
  | nil => simp
  | cons x l IH => simpa using IH

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

Goal state before:
pp: n : ℕ
⊢ ↑(List.range n.succ) = n ::ₘ range n

Tactic:
List.range_succ,

Goal state after:
n : ℕ
⊢ ↑(List.range n ++ [n]) = n ::ₘ range n
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
h : a ∉ s
⊢ s ∩ {a} = ∅

Tactic:
rw [inter_comm, singleton_inter_of_notMem h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s ∆ t ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
symmDiff,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ⊔ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq γ
g : β → γ
⊢ image g ∘ image f = image (g ∘ f)

Tactic:
ext s

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq γ
g : β → γ
s : Finset α
a✝ : γ
⊢ a✝ ∈ (image g ∘ image f) s ↔ a✝ ∈ image (g ∘ f) s
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
⊢ ↑i.rev.modNat = ↑i.modNat.rev

Tactic:
have H₁ : i % n + 1 ≤ n := i.modNat.is_lt

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
⊢ ↑i.rev.modNat = ↑i.modNat.rev
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mpr
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t

Tactic:
rintro ⟨hst, h⟩
    obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)
    grind =>
      have : a ∈ t \ s
      have h : insert a s ⊆ t
      have := eq_of_subset_of_card_le h
      instantiate

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun i ↦ f l[↑i]) univ = (List.map f l).toFinset

Tactic:
simp only [univ_image_def, List.ofFn_getElem_eq_map]

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p : Fin n
⊢ Surjective p.predAbove

Tactic:
intro i
  by_cases hi : i ≤ p
  · exact ⟨i.castSucc, predAbove_castSucc_of_le p i hi⟩
  · rw [Fin.not_le] at hi
    exact ⟨i.succ, predAbove_succ_of_le p i (Fin.le_of_lt hi)⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ≃ β
⊢ card α = card β

Tactic:
rw [← ofEquiv_card f]; congr!

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (j.predAbove i).predAbove (i.succAbove j) = j

Tactic:
| inl h =>

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ #s = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
constructor
  · rw [card_eq_succ]
    grind [card_eq_three]
  · grind

Goal state after:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
| inl h =>

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

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : x i = x₀
⊢ False

Tactic:
← @snoc_last n (fun i ↦ α) x₀ x,

Goal state after:
case refine_2
n : ℕ
α : Type u_2
x₀ : α
x : Fin n → α
h : Injective (snoc x x₀)
i : Fin n
hi : x i = snoc x x₀ (last n)
⊢ False
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : (i.succAbove j).pred H₁ = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j

Tactic:
pred_succAbove _ _ (Fin.not_lt.1 hlt)

Goal state after:
case neg
n : ℕ
α : Fin (n + 1) → Sort u_1
i : Fin (n + 1)
x : α i
p : (j : Fin n) → α (i.succAbove j)
j : Fin n
hlt : ¬j.castSucc < i
H₀ : NeZero (n + 1)
H₁ : i.succAbove j ≠ 0
k : Fin n
hk : j = k
⊢ ∀ (H₂ : i.succAbove k = i.succAbove j), H₂ ▸ p k = p j
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
⊢ (f '' u).Finite

Tactic:
by simp [himg]

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
h : ↑j < ↑k
⊢ j.contractNth op g k = g k.succ

Tactic:
by
  rw [contractNth, if_neg (not_lt_of_gt h), if_neg (Ne.symm <| ne_of_lt h)]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: case refine_1
α : Type u_1
a : α
s : Multiset α
ha : a ∈ 0 • s
⊢ False

Tactic:
simp [zero_nsmul] at ha

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

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ a / (l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-1 * (-1) ^ l₁.length)

Tactic:
Int.neg_mul,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l₁ l₂ : List G
⊢ a / (l₁.alternatingProd * l₂.alternatingProd ^ (-1) ^ l₁.length) =
    a / l₁.alternatingProd * l₂.alternatingProd ^ (-(1 * (-1) ^ l₁.length))
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-1 * (-1) ^ l.length) * a ^ (-1) ^ l.length =
    (a / l.alternatingProd) ^ (-1 * (-1 * (-1) ^ l.length))

Tactic:
Int.neg_mul,

Goal state after:
G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ l.alternatingProd ^ (-(1 * (-1) ^ l.length)) * a ^ (-1) ^ l.length =
    (a / l.alternatingProd) ^ (-(1 * -(1 * (-1) ^ l.length)))
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
a : G
l : List G
⊢ (a :: l).reverse.alternatingProd = (a :: l).alternatingProd ^ (-1) ^ ((a :: l).length + 1)

Tactic:
simp_rw [reverse_cons, alternatingProd_append, alternatingProd_reverse,
      alternatingProd_singleton, alternatingProd_cons, length_reverse, length, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, inv_inv]
    rw [mul_comm, ← div_eq_mul_inv, div_zpow]

Goal state after:
Module: Mathlib.Algebra.Order.Group.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
⊢ f = g

Tactic:
ext s

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : AddZeroClass β
f g : Multiset α →+ β
h : ∀ (x : α), f {x} = g {x}
s : Multiset α
⊢ f s = g s
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l)[n] = (replicate (a :: l).length a)[n]

Tactic:
getElem_replicate,

Goal state after:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l)[n] = a
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

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

Tactic:
simp [List.prod_eq_pow_single a h]

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 M
inst✝² : CommMonoid N
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
a✝ : List M
hs : Quot.mk (⇑(List.isSetoid M)) a✝ ≠ 0
⊢ (map (⇑f) (Quot.mk (⇑(List.isSetoid M)) a✝)).prod = f (prod (Quot.mk (⇑(List.isSetoid M)) a✝))

Tactic:
aesop (add simp List.prod_hom_nonempty)

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)

Tactic:
rel_map

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b ↦ Rel p (f a) (g b)) s t
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ count x (s.dedup.bind f).dedup = count x (s.bind f).dedup

Tactic:
count_dedup

Goal state after:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (if x ∈ s.dedup.bind f then 1 else 0) = if x ∈ s.bind f then 1 else 0
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
hd : α
tl : List α
h : hd :: tl ≠ []
⊢ (hd :: tl).cyclicPermutations = (zipWith (fun x1 x2 ↦ x1 ++ x2) (hd :: tl).tails (hd :: tl).inits).dropLast

Tactic:
exact cyclicPermutations_cons _ _

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

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

Tactic:
by
  ext
  simp_all

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

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

Tactic:
have hp : m = p + 1 := (succ_pred_eq_of_ne_zero hm).symm

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
p : ℕ := m - 1
hp : m = p + 1
⊢ (m * n).choose n = m * (m * n - 1).choose (n - 1)
Module: Mathlib.Algebra.Group.Subsemigroup.Defs

Goal state before:
pp: case mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s : Set M
q : Subsemigroup M
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier = q.carrier
⊢ { carrier := carrier✝, mul_mem' := mul_mem'✝ } = q

Tactic:
cases q

Goal state after:
case mk.mk
M : Type u_1
N : Type u_2
inst✝ : Mul M
s carrier✝¹ : Set M
mul_mem'✝¹ : ∀ {a b : M}, a ∈ carrier✝¹ → b ∈ carrier✝¹ → a * b ∈ carrier✝¹
carrier✝ : Set M
mul_mem'✝ : ∀ {a b : M}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
h : { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ }.carrier = { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
⊢ { carrier := carrier✝¹, mul_mem' := mul_mem'✝¹ } = { carrier := carrier✝, mul_mem' := mul_mem'✝ }
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1

Tactic:
rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]

Goal state after:
case h₂
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
    ∀ (i : ι), Bijective ((U i).restrictPreimage f)

Tactic:
simp [Bijective, forall_and]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ i, s i)

Tactic:
intro x hx y hy hxy

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
⊢ x = y
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_7
inst✝ : Group N
f : G →* N
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
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
x : G
hx : x ∈ comap f (map f H)
⊢ x ∈ H ⊔ f.ker

Tactic:
simp only [mem_map, mem_comap] at 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_1 ∈ H, f x_1 = f x
⊢ x ∈ H ⊔ f.ker
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: case mp.refine_4
G : Type u_1
inst✝ : Group G
s t : Subgroup G
ht : t.Normal
x : G
hx : x ∈ closure (↑s ∪ ↑t)
⊢ ∀ x ∈ closure (↑s ∪ ↑t), (∃ y ∈ s, ∃ z ∈ t, y * z = x) → ∃ y ∈ s, ∃ z ∈ t, y * z = x⁻¹

Tactic:
· rintro _ _ ⟨y, hy, z, hz, rfl⟩
      exact ⟨y⁻¹, s.inv_mem hy,
            y * z⁻¹ * y⁻¹, ht.conj_mem z⁻¹ (t.inv_mem hz) y, by simp [mul_assoc]⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))

Tactic:
rw [codisjoint_iff, ← subgroupOf_sup, subgroupOf_self]

Goal state after:
case hA
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ H ≤ H ⊔ K

case hA'
G : Type u_1
inst✝ : Group G
H K : Subgroup G
⊢ K ≤ H ⊔ K
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ Set.range ⇑f = ↑⊤ ↔ Set.range ⇑f = Set.univ

Tactic:
coe_top

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
F : Type u_4
inst✝ : FunLike F M N
mc : MonoidHomClass F M N
f : F
⊢ Set.range ⇑f = Set.univ ↔ Set.range ⇑f = Set.univ
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: x✝² x✝¹ x✝ : ℕ
hk : x✝ ≤ x✝¹
⊢ x✝² <<< (x✝¹ - x✝) = x✝² <<< x✝¹ >>> x✝

Tactic:
simp only [← shiftLeft'_false, shiftLeft'_sub false _ hk]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
⊢ DecidableEq ↑(Set.range Encodable.encode)

Tactic:
exact Encodable.decidableEqOfEncodable _

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

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

Tactic:
intro g

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s → g ∈ normalizer ↑(closure s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ (Subgroup.map f H).Normal

Tactic:
rw [← normalizer_eq_top_iff, ← top_le_iff, ← f.range_eq_top_of_surjective hf, f.range_eq_map,
    ← H.normalizer_eq_top]

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
H : Subgroup G
h : H.Normal
f : G →* N
hf : Surjective ⇑f
⊢ Subgroup.map f (normalizer ↑H) ≤ normalizer ↑(Subgroup.map f H)
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (of (f head) * (map f) a✝¹).length = (of d).length
⊢ f head = d

Tactic:
simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H

Goal state after:
case h
α : Type u_1
β : Type u_2
f : α → β
fs : Function.Surjective ⇑(map f)
d : β
head : α
a✝¹ : FreeMonoid α
a✝ : (map f) a✝¹ = of d → ∃ a, f a = d
hb : of (f head) * (map f) a✝¹ = of d
H : (map f) a✝¹ = 1
⊢ f head = d
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ ∀ n ∈ iInf a, ∀ (g : G), g * n * g⁻¹ ∈ iInf a

Tactic:
intro g

Goal state after:
G : Type u_1
inst✝ : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
⊢ g ∈ iInf a → ∀ (g_1 : G), g_1 * g * g_1⁻¹ ∈ iInf a
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
hd : M
tl : List M
ih : (∀ (x : M), x ∈ tl → 1 ≤ x) → ∀ (x : M), x ∈ tl → x ≤ tl.prod
hl₁ : 1 ≤ hd ∧ ∀ (x : M), x ∈ tl → 1 ≤ x
⊢ ∀ (x : M), x ∈ tl → x ≤ hd * tl.prod

Tactic:
exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ ∃ b_1, toLex (a, b) < b_1

Tactic:
use toLex (a, c)

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
a : α
b c : β
h : b < c
⊢ toLex (a, b) < toLex (a, c)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case append_singleton
α : 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
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m

Tactic:
| append_singleton tl a ih =>

Goal state after:
case append_singleton
α : 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
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m
Module: Mathlib.Data.Finset.Sum

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

Tactic:
by simp [← h, toLeft_disjSum_toRight]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a ∆ b) = f a ∆ f b

Tactic:
symmDiff,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b ⊔ b \ a) = f a ∆ f b
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b ⊔ b \ a) = f a ∆ f b

Tactic:
symmDiff,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : BooleanAlgebra α
inst✝² : BooleanAlgebra β
inst✝¹ : FunLike F α β
inst✝ : BoundedLatticeHomClass F α β
f : F
a b : α
⊢ f (a \ b ⊔ b \ a) = f a \ f b ⊔ f b \ f a
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 ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
⊢ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y

Tactic:
intro x hx y hy hxy

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → (∀ z ∈ s, z ∉ Set.Ioo x y) → ∃ z ∈ t, x < z ∧ z < y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∈ t, x < z ∧ z < y
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
⊢ StrictMonoOn f ↑s

Tactic:
intro x hx y hy hxy

Goal state after:
α : 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
⊢ f x < f y
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l' : List α
h : l' <+ l
⊢ l' ∈ sublistsLen l'.length l

Tactic:
by
  induction h with
  | slnil => simp
  | @cons l₁ l₂ a s IH =>
    rcases l₁ with - | ⟨b, l₁⟩
    · simp
    · rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH
  | cons_cons a s IH =>
    rw [length, sublistsLen_succ_cons]
    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

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

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
f : α → β
n : ℕ
⊢ powersetCard n (map f 0) = map (map f) (powersetCard n 0)

Tactic:
cases n <;> simp [powersetCard_zero_left]

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
f : α → β
t : α
s : Multiset α
ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)
n : ℕ
⊢ powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))

Tactic:
cases n <;> simp [ih]

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
sublist : l₁ <+ l₂
⊢ l₁.sublists' <+ l₂.sublists'

Tactic:
induction sublist with

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

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
List.range_succ,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length ++ [tl.length]) ~ tl.sublists'
Module: Mathlib.Data.Set.Finite.Powerset

Goal state before:
pp: α : Type u
a : Set α
h : a.Finite
⊢ {b | b ⊆ a} = ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)

Tactic:
ext s

Goal state after:
α : Type u
a : Set α
h : a.Finite
s : Set α
⊢ s ∈ {b | b ⊆ a} ↔ s ∈ ↑(Finset.map Finset.coeEmb.toEmbedding h.toFinset.powerset)
Module: Mathlib.Data.Finset.Powerset

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
ht : t ∈ s.powerset
h : a ∉ s
⊢ a ∉ t

Tactic:
by
  apply mt _ h
  apply mem_powerset.1 ht

Goal state after: