mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n m : ℕ
i : Fin n
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨↑i + 1, ⋯⟩

Tactic:
split_ifs with h

Goal state after:
case pos
n m : ℕ
i : Fin n
h : i.succ = last n
⊢ (castAdd m i).succ = natAdd n 0

case neg
n m : ℕ
i : Fin n
h : ¬i.succ = last n
⊢ (castAdd m i).succ = castAdd (m + 1) ⟨↑i + 1, ⋯⟩
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ p.succAbove (i.castPred ⋯) = i

Tactic:
by
  rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]

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:
by
  refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩
  exact exists_subset_card_eq h

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

Goal state before:
pp: α : Type u_4
P : α → Prop
r : α → α → Prop
h : ∀ (s : Finset α), (∀ x ∈ s, P x) → ∃ y, P y ∧ ∀ x ∈ s, r x y
this : Nonempty α
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)

Tactic:
choose! F hF using h

Goal state after:
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
⊢ ∃ f, (∀ (n : ℕ), P (f n)) ∧ ∀ (m n : ℕ), m < n → r (f m) (f n)
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
p i : Fin n
⊢ ∃ a, p.predAbove a = i

Tactic:
by_cases hi : i ≤ p

Goal state after:
case pos
n : ℕ
p i : Fin n
hi : i ≤ p
⊢ ∃ a, p.predAbove a = i

case neg
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ a, p.predAbove a = i
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
⊢ append (append a b) c = append a (append b c) ∘ Fin.cast ⋯

Tactic:
ext i
  rw [Function.comp_apply]
  refine Fin.addCases (fun l => ?_) (fun r => ?_) i
  · rw [append_left]
    refine Fin.addCases (fun ll => ?_) (fun lr => ?_) l
    · rw [append_left]
      simp [castAdd_castAdd]
    · rw [append_right]
      simp [castAdd_natAdd]
  · rw [append_right]
    simp [← natAdd_natAdd]

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

Goal state before:
pp: case inr
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs✝ : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
⊢ p t ht

Tactic:
have := card_lt_card hts

Goal state after:
case inr
α : Type u_1
p : (s : Finset α) → s.Nonempty → Prop
h₀ : ∀ (a : α), p {a} ⋯
h₁ : ∀ ⦃s : Finset α⦄ (hs : s.Nontrivial), (∀ (t : Finset α) (ht : t.Nonempty), t ⊂ s → p t ht) → p s ⋯
s : Finset α
hs✝ : s.Nonempty
hs : s.Nontrivial
t : Finset α
ht : t.Nonempty
hts : t ⊂ s
this : #t < #s
⊢ p t ht
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n m : ℕ
α : Sort u_2
xs : Fin n → α
y : α
ys : Fin m → α
⊢ append xs (cons y ys) = append (snoc xs y) ys ∘ Fin.cast ⋯

Tactic:
by
  rw [append_left_snoc]; rfl

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

Goal state before:
pp: case succ
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
⊢ (if h : i + 1 < n + 1 then cases a as ⟨i + 1, ⋯⟩ else ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯)) =
    cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

Tactic:
split_ifs with h

Goal state after:
case pos
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : i + 1 < n + 1
⊢ cases a as ⟨i + 1, ⋯⟩ = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)

case neg
m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
i : ℕ
isLt✝ : i + 1 < n + 1 + m
h : ¬i + 1 < n + 1
⊢ ⋯ ▸ bs (subNat (n + 1) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩) ⋯) = cases a (addCases as bs) (Fin.cast ⋯ ⟨i + 1, isLt✝⟩)
Module: Mathlib.Data.List.NodupEquivFin

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

Tactic:
rintro ⟨f, hf⟩
    exact sublist_of_orderEmbedding_getElem?_eq f hf

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

Goal state before:
pp: α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑t

Tactic:
← sep_eq_of_subset h

Goal state after:
α : Type u
s t : Set α
inst✝ : Finite ↑s
h : t ⊆ s
⊢ Finite ↑{x | x ∈ s ∧ x ∈ t}
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
⊢ univ.Infinite ↔ Infinite α

Tactic:
Set.Infinite,

Goal state after:
α : Type u
⊢ ¬univ.Finite ↔ Infinite α
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
h_inf : s.Infinite
h_fin : (f '' s).Finite
this✝ : Finite ↑(f '' s)
this : Infinite ↑s
h : InjOn f s
⊢ Injective (codRestrict (s.domRestrict f) (f '' s) ⋯)

Tactic:
rwa [injective_codRestrict, ← injOn_iff_injective]

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

Goal state before:
pp: α : Type u_1
l : List α
inst✝ : Preorder α
⊢ l.SortedGE ↔ Pairwise (fun x1 x2 ↦ x1 ≥ x2) l

Tactic:
simp only [sortedGE_iff_antitone_get, antitone_iff_forall_lt, Fin.forall_iff]
  grind [pairwise_iff_getElem]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
⊢ op (if p x then f x else g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : p x
⊢ op (f x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

case neg
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
h : ¬p x
⊢ op (g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Module: Mathlib.Data.List.Chain

Goal state before:
pp: α : Type u_1
R : α → α → Prop
a : α
l : List α
⊢ IsChain R ([a] ++ l) ↔ IsChain R [a] ∧ IsChain R l ∧ ∀ (x : α), x ∈ [a].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
by simp [isChain_cons, and_comm]

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

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

Tactic:
by rw [rotate'_length, rotate'_length_mul l n]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ IsChain (fun x1 x2 ↦ x1 > x2) (a :: b :: bs)

Tactic:
apply hm.cons_cons

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
a : α
as : List α
ha : IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
b : α
bs : List α
hm : IsChain (fun x1 x2 ↦ x1 > x2) (b :: bs)
hmas : b :: bs ≤ as
⊢ a > b
Module: Mathlib.Algebra.BigOperators.Group.Multiset.Basic

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

Tactic:
by
  induction s using Quotient.inductionOn; simp [List.prod_eq_pow_single a h]

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

Goal state before:
pp: case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ (l.rotate k).cyclicPermutations

Tactic:
rw [cyclicPermutations_rotate, mem_rotate]

Goal state after:
case mpr
α : Type u
l : List α
k : ℕ
⊢ l ∈ l.cyclicPermutations
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l l' : List α
h : l ~r l'
⊢ l.cyclicPermutations ~r l'.cyclicPermutations

Tactic:
obtain ⟨k, rfl⟩ := h
  exact ⟨k, by simp⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : z = x
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = count y l

case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
x y z : α
h : ¬z = x
⊢ count (x, y) (map (fun x ↦ (z, x)) l) = 0
Module: Mathlib.Data.List.OffDiag

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = if z = y then count x l else 0

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = count x l

case neg
α : Type u_1
inst✝ : DecidableEq α
a b c : α
l : List α
ihl : count (a, b) l.offDiag = count a l * count b l - if a = b then count a l else 0
H₁ : ∀ {x y z : α}, count (x, y) (map (fun x ↦ (z, x)) l) = if z = x then count y l else 0
x y z : α
h : ¬z = y
⊢ count (x, y) (map (fun x ↦ (x, z)) l) = 0
Module: Mathlib.Data.Nat.Choose.Basic

Goal state before:
pp: i j : ℕ
⊢ i ! * (i + j - i)! ∣ (i + j)!

Tactic:
exact factorial_mul_factorial_dvd_factorial (Nat.le_add_right _ _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
⊢ {a} ×ˢ {b} = {(a, b)}

Tactic:
by
  simp only [product_singleton, Function.Embedding.coeFn_mk, map_singleton]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s' : Finset α
t t' : Finset β
⊢ Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'

Tactic:
simp_rw [← disjoint_coe, coe_product, Set.disjoint_prod]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
Set.Infinite,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬s.Finite ∧ t.Nonempty ∨ ¬t.Finite ∧ s.Nonempty
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: 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
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ b ∈ s, b * a ∈ t
⊢ Function.Injective fun x ↦
    match x with
    | ⟨b, hb⟩ => ⟨b * a, ⋯⟩

Tactic:
rintro ⟨b, hb⟩ ⟨c, hc⟩ hbc

Goal state after:
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
a : G
s t : Set G
x✝¹ : Fintype ↑s
x✝ : Fintype ↑t
h : ∀ b ∈ s, b * a ∈ t
b : G
hb : b ∈ s
c : G
hc : c ∈ s
hbc :
  (fun x ↦
        match x with
        | ⟨b, hb⟩ => ⟨b * a, ⋯⟩)
      ⟨b, hb⟩ =
    (fun x ↦
        match x with
        | ⟨b, hb⟩ => ⟨b * a, ⋯⟩)
      ⟨c, hc⟩
⊢ ⟨b, hb⟩ = ⟨c, hc⟩
Module: Mathlib.Algebra.Group.Conj

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
⊢ Function.Surjective (map f)

Tactic:
intro b
  obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b
  obtain ⟨a, rfl⟩ := hf b
  exact ⟨ConjClasses.mk a, rfl⟩

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

Goal state before:
pp: δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
⊢ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 = (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x

Tactic:
ext ⟨_, _⟩

Goal state after:
δ : Type u_4
α : Type u_9
β : Type u_10
γ : Type u_11
s : Set α
t : Set β
f : α → Set γ
g : β → Set δ
fst✝ : γ
snd✝ : δ
⊢ (fst✝, snd✝) ∈ ⋃ x ∈ s ×ˢ t, f x.1 ×ˢ g x.2 ↔ (fst✝, snd✝) ∈ (⋃ x ∈ s, f x) ×ˢ ⋃ x ∈ t, g x
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
T : Set (Set β)
⊢ image2 f s (⋂₀ T) ⊆ ⋂ t ∈ T, image2 f s t

Tactic:
by
  rw [sInter_eq_biInter]
  exact image2_iInter₂_subset_right ..

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (Prod.mk '' s).seq t = ((fun b a ↦ (a, b)) '' t).seq s

Tactic:
← prod_eq_seq,

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ((fun b a ↦ (a, b)) '' t).seq s
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y⁻¹ * x ∈ ⊥
⊢ x = y

Tactic:
mem_bot,

Goal state after:
G : Type u_1
inst✝¹ : Group G
M : Type u_7
inst✝ : MulOneClass M
f : G →* M
h : f.ker = ⊥
x y : G
hxy : y⁻¹ * x = 1
⊢ x = y
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
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K < comap f L ↔ K < L

Tactic:
simp_rw [lt_iff_le_not_ge, comap_le_comap_of_surjective hf]

Goal state after:
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 : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ ((↑e).comp (powMonoidHom n)).range = (powMonoidHom n).range

Tactic:
H,

Goal state after:
M : Type u_5
N : Type u_6
inst✝¹ : CommGroup M
inst✝ : CommGroup N
e : M ≃* N
n : ℕ
H : (↑e).comp (powMonoidHom n) = (powMonoidHom n).comp ↑e
⊢ ((powMonoidHom n).comp ↑e).range = (powMonoidHom n).range
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
⊢ pair
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).1
      (if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt)
        else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)).2 =
    n

Tactic:
split_ifs with h

Goal state after:
case pos
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : n - n.sqrt * n.sqrt < n.sqrt
⊢ pair (n - n.sqrt * n.sqrt, n.sqrt).1 (n - n.sqrt * n.sqrt, n.sqrt).2 = n

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
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)

Goal state after:
case neg
n : ℕ
s : ℕ := n.sqrt
sm : s * s + (n - s * s) = n
h : ¬n - n.sqrt * n.sqrt < n.sqrt
hl : n - s * s - s ≤ s
⊢ pair (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).1 (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt).2 = n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: a b : ℕ
⊢ unpair (if a < b then b * b + a else a * a + a + b) = (a, b)

Tactic:
split_ifs with h

Goal state after:
case pos
a b : ℕ
h : a < b
⊢ unpair (b * b + a) = (a, b)

case neg
a b : ℕ
h : ¬a < b
⊢ unpair (a * a + a + b) = (a, b)
Module: Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
⊢ zpowers g = closure {g}

Tactic:
by
  ext
  exact mem_closure_singleton.symm

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

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
inst✝¹ : H.Characteristic
inst✝ : K.Characteristic
⊢ (H ⊓ K).Characteristic

Tactic:
by
  simp_all [characteristic_iff_comap_eq, comap_inf]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
α₁ : Type u_6
g : α₁ → α
x : FreeMonoid α₁
⊢ { toFun := fun l ↦ ofList (List.map f (toList l)), map_one' := ⋯, map_mul' := ⋯ }
      ({ toFun := fun l ↦ ofList (List.map g (toList l)), map_one' := ⋯, map_mul' := ⋯ } x) =
    { toFun := fun l ↦ ofList (List.map (f ∘ g) (toList l)), map_one' := ⋯, map_mul' := ⋯ } x

Tactic:
simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

Goal state after:
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 : (map f) a✝¹ = 1
⊢ f head = d

Tactic:
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) * 1 = of d
H : (map f) a✝¹ = 1
⊢ f head = d
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case mpr.inr
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
b : (i : ι) × α i
a : α b.fst
h : s b.fst (⋯ ▸ a) b.snd
⊢ Lex r s ⟨b.fst, a⟩ b

Tactic:
· exact Lex.right _ _ h

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

Goal state before:
pp: case mp.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : s i✝ a b
⊢ Lex r (fun i ↦ Function.swap (s i)) ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
· exact Lex.right _ _ h

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

Goal state before:
pp: case mpr.right
ι : Type u_1
α : ι → Type u_2
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
i✝ : ι
a b : α i✝
h : Function.swap (s i✝) a b
⊢ Lex (Function.swap r) s ⟨i✝, b⟩ ⟨i✝, a⟩

Tactic:
· exact Lex.right _ _ h

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ closure s = mrange (FreeMonoid.lift Subtype.val)

Tactic:
FreeMonoid.mrange_lift,

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ closure s = closure (Set.range Subtype.val)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : M
⊢ powers n = closure {n}

Tactic:
by
  ext
  exact mem_closure_singleton.symm

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

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

Tactic:
by simp [h, toLeft_disjSum_toRight]

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

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : z ∈ l ∧ ∀ (b : α), b ∈ l → b ≤ z
this : Std.Antisymm fun x1 x2 ↦ x1 ≤ x2
⊢ (some z).getD d = y

Tactic:
· rw [Option.getD_some]
        exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left)

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ foldr max b (y :: l)

Tactic:
simp only [List.foldr]

Goal state after:
case cons
α : Type u_1
inst✝ : LinearOrder α
a x b : α
h : a ≤ x
y : α
l : List α
IH : x ∈ l → a ≤ foldr max b l
hx : x ∈ y :: l
⊢ a ≤ max y (foldr max b l)
Module: Mathlib.Order.Hom.BoundedLattice

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁸ : FunLike F α β
inst✝⁷ : Max α
inst✝⁶ : Bot α
inst✝⁵ : Max β
inst✝⁴ : Bot β
inst✝³ : Max γ
inst✝² : Bot γ
inst✝¹ : Max δ
inst✝ : Bot δ
f g : SupBotHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f
    obtain ⟨⟨_, _⟩, _⟩ := g
    congr

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Max α
inst✝⁴ : Bot α
inst✝³ : Max β
inst✝² : Bot β
inst✝¹ : Max γ
inst✝ : Bot γ
g : SupBotHom β γ
f₁ f₂ : SupBotHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
by rw [← comp_apply, h, comp_apply]

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

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists' ↔ s <+ t

Tactic:
by
  induction t generalizing s with
  | nil =>
    simp only [sublists'_nil, mem_singleton]
    exact ⟨fun h => by rw [h], eq_nil_of_sublist_nil⟩
  | cons a t IH => ?_
  simp only [sublists'_cons, mem_append, IH, mem_map]
  constructor <;> intro h
  · rcases h with (h | ⟨s, h, rfl⟩)
    · exact sublist_cons_of_sublist _ h
    · exact h.cons_cons _
  · obtain - | ⟨-, h⟩ | ⟨-, h⟩ := h
    · exact Or.inl h
    · exact Or.inr ⟨_, h, rfl⟩

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ powersetAux l ~ powersetAux' l

Tactic:
rw [powersetAux_eq_map_coe]

Goal state after:
α : Type u_1
l : List α
⊢ List.map ofList l.sublists ~ powersetAux' l
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r → ∀ (n : κ), (f n).Pairwise r

Tactic:
intro H n
    exact Pairwise.mono (subset_iUnion _ _) H

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ s.sup f ≤ a ↔ ∀ b ∈ s, f b ≤ a

Tactic:
apply Iff.trans Multiset.sup_le

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ≤ a) ↔ ∀ b ∈ s, f b ≤ a
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
obtain rfl | ha' := eq_or_ne a ⊥

Goal state after:
case inl
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
ha : ⊥ ∈ s
⊢ id ⊥ ≤ (s.erase ⊥).sup id

case inr
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id