mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
z : ℤ
⊢ ⌈a + ↑z⌉ = ⌈a⌉ + z

Tactic:
rw [← neg_inj, neg_add', ← floor_neg, ← floor_neg, neg_add', floor_sub_intCast]

Goal state after:
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = negOfNat ⌈↑n / ↑d⌉.toNat

Tactic:
@negOfNat_eq (toNat _),

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
n d : ℕ
inv : Invertible ↑d
⊢ ⌊↑(negOfNat n) / ↑d⌋ = -ofNat ⌈↑n / ↑d⌉.toNat
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case neg
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : 0 < y
q : ℕ
hq : x⁻¹ < y⁻¹ ^ q
⊢ ∃ n, y ^ n < x

Tactic:
exact ⟨q, by rwa [inv_pow, inv_lt_inv₀ hx (pow_pos y_pos _)] at hq⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
⊢ ∀ {m1 : Multiset α}, (∀ (a b : α), a ∈ m1 → b ∈ 0 → r a b) → m1.card = card 0 → Rel r m1 0

Tactic:
intro m _h hc

Goal state after:
case refine_1
α : Type u_1
m2 : Multiset α
r : α → α → Prop
m : Multiset α
_h : ∀ (a b : α), a ∈ m → b ∈ 0 → r a b
hc : m.card = card 0
⊢ Rel r m 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Tactic:
exact h

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

Goal state before:
pp: case nil
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₂ : List α
h : l₂.Nodup
⊢ ([] ∪ l₂).Nodup

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
⊢ ∀ (x y : { t // t ∈ b ∧ p t }), x = y

Tactic:
rintro ⟨x, px⟩ ⟨y, py⟩

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
inst✝ : DecidablePred p
l : Multiset α
a b : List α
p✝ : a ≈ b
hp : ∃! a, a ∈ ⟦b⟧ ∧ p a
x : α
px : x ∈ b ∧ p x
y : α
py : y ∈ b ∧ p y
⊢ ⟨x, px⟩ = ⟨y, py⟩
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Multiset α
l : List α
⊢ List.filterMap (Option.guard fun b ↦ decide (p b)) l = List.filter (fun b ↦ decide (p b)) l

Tactic:
rw [← List.filterMap_eq_filter]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
M N P Q : Multiset α
h : M + N = P + Q
⊢ N ∩ Q + (P - M) = N

Tactic:
ext x
  rw [Multiset.count_add, Multiset.count_inter, Multiset.count_sub]
  have h0 : M.count x + N.count x = P.count x + Q.count x := by
    rw [Multiset.ext] at h
    simp_all only [Multiset.count_add]
  omega

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ IsEmpty ↥s ↔ s = ∅

Tactic:
by
  simpa using @Set.isEmpty_coe_sort α s

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

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ (∃ s t, s ++ [x] ++ t = xs) ↔ ∃ s t, xs = s ++ x :: t

Tactic:
congr! 4

Goal state after:
α : Type u_1
x : α
xs x✝¹ x✝ : List α
⊢ x✝¹ ++ [x] ++ x✝ = xs ↔ xs = x✝¹ ++ x :: x✝
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∉ s
⊢ insert a s ⊆ insert a t ↔ s ⊆ t

Tactic:
by
  simp_rw [← coe_subset]; simp [ha]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s₁ s₂ : Finset α
x : α
h : x ∈ s₂
⊢ x ∈ s₂

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
f : α → β
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map (Subtype.restrict p f) univ.val = Multiset.map f (filter p univ).val

Tactic:
← univ_val_map_subtype_val,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
f : α → β
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : Fintype { a // p a }
⊢ Multiset.map (Subtype.restrict p f) univ.val = Multiset.map f (Multiset.map Subtype.val univ.val)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (map (Embedding.subtype fun x ↦ x ∈ s) s.attach).val = s.val

Tactic:
rw [map_val, attach_val]

Goal state after:
α : Type u_1
s : Finset α
⊢ Multiset.map (⇑(Embedding.subtype fun x ↦ x ∈ s)) s.val.attach = s.val
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : DecidableEq β
s : Finset α
β' : Type u_4
inst✝¹ : DecidableEq β'
inst✝ : DecidableEq γ
f : β → γ
g : α → β
f' : α → β'
g' : β' → γ
h_comm : ∀ (a : α), f (g a) = g' (f' a)
⊢ image f (image g s) = image g' (image f' s)

Tactic:
simp_rw [image_image, comp_def, h_comm]

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t

Tactic:
let : CanLift β s (f ∘ (↑)) fun y => y ∈ f '' s := ⟨fun y ⟨x, hxt, hy⟩ => ⟨⟨x, hxt⟩, hy⟩⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Set α
t : Finset β
f : α → β
h : ↑t ⊆ f '' s
this : CanLift β (↑s) (f ∘ Subtype.val) fun y ↦ y ∈ f '' s :=
  {
    prf := fun y x ↦
      match x with
      | Exists.intro x ⟨hxt, hy⟩ => Exists.intro ⟨x, hxt⟩ hy }
⊢ ∃ s', ↑s' ⊆ s ∧ image f s' = t
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case pos
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ ↑(a.castPred ⋯) ≤ ↑b - 1

Tactic:
exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)

Goal state after:
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case inr
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h : j ≤ i
⊢ i = j

Tactic:
obtain h | rfl := h.lt_or_eq

Goal state after:
case inr.inl
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h✝ : j ≤ i
h : j < i
⊢ i = j

case inr.inr
n : ℕ
j : Fin (n + 1)
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
hij : j.predAbove = j.predAbove
h : j ≤ j
⊢ j = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
k : Fin n
⊢ k ≠ 0 → 1 ≤ k

Tactic:
have : NeZero n := k.neZero
  intro hk
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
  cases n with
  | zero => simp only [Fin.isValue, Fin.zero_le]
  | succ n => rwa [Fin.le_iff_val_le_val, Fin.val_one, Nat.one_le_iff_ne_zero, val_ne_zero_iff]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ i ≤ ↑n

Tactic:
by
  rw [Fin.natCast_eq_last]
  exact Fin.le_last i

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b ≤ (a.pred ha).castSucc ↔ b < a

Tactic:
rw [castSucc_pred_eq_pred_castSucc, le_pred_castSucc_iff]

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

Goal state before:
pp: α : Type u
β : Type u_1
l : List α
f : α → β
⊢ (ofFn fun i ↦ f l[↑i]) = map f l

Tactic:
by
  rw [← Function.comp_def, ← map_ofFn, ofFn_getElem]

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
⊢ n ≤ #s ↔ ∃ t ⊆ s, #t = n

Tactic:
refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩

Goal state after:
α : Type u_1
s : Finset α
n : ℕ
h : n ≤ #s
⊢ ∃ t ⊆ s, #t = n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: case mp
α : Type u_1
s : Finset α
a b c d : α
hab : a ≠ b
hac : a ≠ c
had : a ≠ d
hbc : b ≠ c
hbd : b ≠ d
hcd : c ≠ d
hsub : {a, b, c, d} ⊆ s
⊢ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d

Tactic:
exact ⟨a, b, c, d, by simp_all [insert_subset_iff]⟩

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

Goal state before:
pp: case cons_mem
α : Type u_1
l : List α
x : α
h : x ∈ l
⊢ x ∈ l

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
⊢ ∀ (ix : ℕ), tl[ix]? = (drop (f 0 + 1) l')[f' ix]?

Tactic:
intro ix

Goal state after:
α : Type u_1
hd : α
tl : List α
IH : ∀ {l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), tl[ix]? = l'[f ix]?) → tl <+ l'
l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), (hd :: tl)[ix]? = l'[f ix]?
w : f 0 < l'.length
h : l'[f 0] = hd
f' : ℕ ↪o ℕ := OrderEmbedding.ofMapLEIff (fun i ↦ f (i + 1) - (f 0 + 1)) ⋯
ix : ℕ
⊢ tl[ix]? = (drop (f 0 + 1) l')[f' ix]?
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
i : ℕ
hi : i < l.length
h : f i < l'.length
⊢ f i < l'.length

Tactic:
exact h

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

Goal state before:
pp: case mp.refine_2
α : Type u_1
l l' : List α
f : ℕ ↪o ℕ
hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?
h : ∀ {i : ℕ}, i < l.length → f i < l'.length
⊢ ∀ (ix : Fin l.length), l.get ix = l'.get ((OrderEmbedding.ofMapLEIff (fun ix ↦ ⟨f ↑ix, ⋯⟩) ⋯) ix)

Tactic:
· intro i
      apply Option.some_injective
      simpa [getElem?_eq_getElem i.2, getElem?_eq_getElem (h i.2)] using hf i

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ insertionSort r l ~ l

Tactic:
by
  induction l <;> grind [List.Perm, perm_orderedInsert]

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

Goal state before:
pp: n : ℕ
α : Type u_3
f : Fin (n + 1) → α
⊢ (last n).removeNth f = init f

Tactic:
ext; simp [init, removeNth]

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

Goal state before:
pp: case mpr.refine_1
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ StrictMono fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length

pp: case mpr.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ ∀ (ix : ℕ),
    l[ix]? =
      l'[(OrderEmbedding.ofStrictMono (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ?mpr.refine_1)
          ix]?

Tactic:
· 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

Goal state after:
case mpr.refine_2
α : Type u_1
l l' : List α
f : Fin l.length ↪o Fin l'.length
hf : ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
⊢ ∀ (ix : ℕ),
    l[ix]? = l'[(OrderEmbedding.ofStrictMono (fun i ↦ if hi : i < l.length then ↑(f ⟨i, hi⟩) else i + l'.length) ⋯) ix]?
Module: Mathlib.Data.Finset.Fold

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
b : β
s✝ : Finset α
c : β
h : op c (op b c) = op b c
x : α
s : Finset α
hx : x ∉ s
IH : ∀ [hd : Decidable (s = ∅)], fold op b (fun x ↦ c) s = if s = ∅ then b else op b c
hd : Decidable (insert x s = ∅)
h✝ : ¬s = ∅
⊢ op c (op b c) = op b c

Tactic:
exact h

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

Tactic:
by
  have : ¬(k : ℕ) < j := not_lt.2 (le_of_eq h.symm)
  rw [contractNth, if_neg this, if_pos h]

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Symm R
hl : Pairwise R l
this : Std.Symm fun x y ↦ x ≠ y → R x y
a b : α
h : R a b
x✝ : a ≠ b
⊢ R a b

Tactic:
exact h

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

Goal state before:
pp: α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ R a b

Tactic:
apply h

Goal state after:
case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ∈ l

case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ b ∈ l

case a
α : Type u_1
R : α → α → Prop
l : List α
inst✝ : Std.Refl R
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → a ≠ b → R a b
a b : α
hab : [a, b] <+ l
heq : ¬a = b
⊢ a ≠ b
Module: Mathlib.Data.List.Range

Goal state before:
pp: a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
⊢ ∀ {a_1 b : List ℕ}, a_1.Disjoint b → (map (fun x ↦ a + x) a_1).Disjoint (map (fun x ↦ a + x) b)

Tactic:
intro u v

Goal state after:
a : ℕ
l : List ℕ
hl : Pairwise Disjoint l.ranges
u v : List ℕ
⊢ u.Disjoint v → (map (fun x ↦ a + x) u).Disjoint (map (fun x ↦ a + x) v)
Module: Mathlib.Data.List.Chain

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ R a b

Tactic:
apply h

Goal state after:
case cons_cons.a
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ head :: head' :: tail = ?cons_cons.l₁ ++ a :: b :: ?cons_cons.l₂

case cons_cons.l₁
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α

case cons_cons.l₂
α : Type u_1
R : α → α → Prop
head head' : α
tail : List α
a✝ : (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R tail
ih : ∀ (y : α), (∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, y :: tail = l₁ ++ a :: b :: l₂ → R a b) → IsChain R (y :: tail)
h : ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, head :: head' :: tail = l₁ ++ a :: b :: l₂ → R a b
a b : α
l₁ l₂ : List α
eq : head' :: tail = l₁ ++ a :: b :: l₂
⊢ List α
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n

Tactic:
by rw [rotate'_rotate', length_rotate', Nat.mod_add_div]

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

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
have : f = fun a ↦ ofList (f' a) := funext h'

Goal state after:
α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.rotate ↑⟨0, h⟩ = l

Tactic:
Fin.val_mk,

Goal state after:
α : Type u
l : List α
h : 0 < l.cyclicPermutations.length
⊢ l.rotate 0 = l
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
⊢ (n + 1).choose (k + 1) = 0

Tactic:
by
    have hnk : n < k := lt_of_succ_lt_succ hk
    have hnk1 : n < k + 1 := lt_of_succ_lt hk
    rw [choose_succ_succ, choose_eq_zero_of_lt hnk, choose_eq_zero_of_lt hnk1]

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

Goal state before:
pp: x✝ : ℕ
hk : x✝ ≤ 0
⊢ 0 < choose 0 x✝

Tactic:
rw [Nat.eq_zero_of_le_zero hk]; decide

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
⊢ List.count a l + List.count a l ≤ List.count a l * List.count a l

Tactic:
by
      rw [← Nat.two_mul]
      exact Nat.mul_le_mul_right _ h

Goal state after:
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝ : CommMonoid α
⊢ Function.RightInverse (Quotient.lift id ⋯) ConjClasses.mk

Tactic:
by
    rw [Function.RightInverse, Function.LeftInverse, forall_isConj]
    solve_by_elim

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

Goal state before:
pp: 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 : M
hx : x ∈ closure s
hy : y ∈ closure s
⊢ p x y hx hy

Tactic:
induction hx using closure_induction with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

Tactic:
← preimage_iUnion₂,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' ⋃ i ∈ s, {i} = f ⁻¹' s
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: case mem
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
z : M
hz : z ∈ s
⊢ motive x z hx ⋯

Tactic:
induction hx using closure_induction with

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
x : M
hx : x ∈ ↑(closure s)
⊢ x ∈ {1} ∪ ↑(Subsemigroup.closure s)

Tactic:
induction hx using closure_induction with

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

Goal state before:
pp: case mem
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
z : G
hz : z ∈ k
⊢ p x z hx ⋯

Tactic:
induction hx using closure_induction with

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

Goal state before:
pp: M : Type u_6
inst✝ : CommGroup M
S : Subgroup M
n : ℕ
⊢ (map (powMonoidHom n) S).subgroupOf S = (powMonoidHom n).range

Tactic:
ext : 1

Goal state after:
M : Type u_6
inst✝ : CommGroup M
S : Subgroup M
n : ℕ
x✝ : ↥S
⊢ x✝ ∈ (map (powMonoidHom n) S).subgroupOf S ↔ x✝ ∈ (powMonoidHom n).range
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
⊢ (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e

Tactic:
ext : 1

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
x✝ : M
⊢ ((↑e).comp (powMonoidHom n)) x✝ = ((powMonoidHom n).comp ↑e) x✝
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: case mp.left
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
x : M
hx : x ∈ ↑s
⊢ (inl M N) x ∈ u

Tactic:
apply h

Goal state after:
case mp.left
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
x : M
hx : x ∈ ↑s
⊢ (inl M N) x ∈ s.prod t
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
x : N
hx : x ∈ ↑t
⊢ (inr M N) x ∈ u

Tactic:
apply h

Goal state after:
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
x : N
hx : x ∈ ↑t
⊢ (inr M N) x ∈ s.prod t
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: n : ℕ
⊢ (n + 1).div2 = bif n.bodd then n.div2.succ else n.div2

Tactic:
cases n using bitCasesOn with
  | bit b n => cases b <;>
    simp [bit_val, div2_val, Nat.succ_div, Nat.add_assoc, Nat.dvd_add_right (Nat.dvd_mul_right _ _)]

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

Goal state before:
pp: case neg
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n

Tactic:
have hl : n - s * s - s ≤ s := Nat.sub_le_iff_le_add.2
      (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
    simp [s, pair, hl.not_gt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]

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

Goal state before:
pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
⊢ n.sqrt < n

Tactic:
have s0 : 0 < s := sqrt_pos.2 n1

Goal state after:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : s ≤ n - s * s
s0 : 0 < s
⊢ n.sqrt < n
Module: Mathlib.Data.Nat.Bits

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

Tactic:
ext b n

Goal state after:
motive : ℕ → Sort u
H₁ H₂ : (b : Bool) → (n : ℕ) → motive (bit b n)
h : (fun H n ↦ bitCasesOn n H) H₁ = (fun H n ↦ bitCasesOn n H) H₂
b : Bool
n : ℕ
⊢ H₁ b n = H₂ b n
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
H : Subgroup G
⊢ zpowers g ≤ H ↔ g ∈ H

Tactic:
rw [zpowers_eq_closure, closure_le, Set.singleton_subset_iff, SetLike.mem_coe]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ B' ⊓ (A ⊓ B))

Tactic:
inf_inf_inf_comm,

Goal state after:
G : Type u_1
inst✝ : Group G
A B' B : Subgroup G
hN : B ≤ normalizer ↑(B' ⊓ B)
⊢ A ⊓ B ≤ normalizer ↑(A ⊓ A ⊓ (B' ⊓ B))