mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b : α
hb : b < 0
⊢ a / b ≤ 1 ↔ b ≤ a

Tactic:
by rw [div_le_iff_of_neg hb, one_mul]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂

Tactic:
right

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
⊢ d ≤ c
Module: Mathlib.Data.List.Basic

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

Tactic:
simp only [reverseAux_eq, map_append, map_reverse]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ zpow' a (-n) = (zpow' a n)⁻¹

Tactic:
simp +contextual [zpow', apply_ite]

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
⊢ if a = 0 ∧ n = 0 then (a = 0 → ¬n = 0) → a ^ n = 0 else a = 0 → ¬n = 0
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * (xs.prod * (y * ys.prod))

Tactic:
right

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| xs.prod * (y * ys.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| y * (ys.prod * xs.prod)

Tactic:
right

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| ys.prod * xs.prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ ((map g ∘ map f) l)[i✝]? = some a✝ ↔ (map (g ∘ f) l)[i✝]? = some a✝

Tactic:
rw [comp_map, Function.comp_apply]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q✝ : ℚ≥0
n₁ n₂ d₁ d₂ : ℕ
C : ℚ≥0 → Sort u
q : ℚ≥0
H : (n d : ℕ) → d ≠ 0 → n.Coprime d → C (divNat n d)
⊢ C q

Tactic:
rw [← q.num_divNat_den]; exact H _ _ q.den_ne_zero q.coprime_num_den

Goal state after:
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
⊢ Injective NNRat.cast

Tactic:
rintro p q hpq

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
p q : ℚ≥0
hpq : ↑p = ↑q
⊢ p = q
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case a
q : ℚ
n : ℤ
⊢ q.den ∣ (q + ↑n).den

Tactic:
simpa using add_den_dvd (q + n) (-n)

Goal state after:
Module: Mathlib.Tactic.FieldSimp

Goal state before:
pp: «$v» : Level
«$M» : Type v
«$iM» : CommGroupWithZero «$M»
«$r» : ℤ
«$x» : «$M»
$snd✝ : ℕ
«$e» : «$M»
«$pf» : zpow' «$x» «$r» = «$e»
⊢ ((«$r», «$x») ::ᵣ []).eval = «$e»

Tactic:
by rw [NF.eval_cons]; exact Eq.trans (one_mul _) pf

Goal state after:
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: n✝¹ num✝ : ℤ
n✝ denom✝ : ℕ
inv✝ : Invertible ↑denom✝
h : ↑n✝¹ / ↑n✝ = ↑num✝ * ⅟↑denom✝
⊢ IsRat (mkRat ↑n✝¹ ↑n✝) num✝ denom✝

Tactic:
by rw [Rat.mkRat_eq_div]; exact ⟨_, h⟩

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

Goal state before:
pp: n : ℤ
⊢ ↑(n / n) = ↑n / ↑n

Tactic:
by
  by_cases hn : n = 0
  · subst hn
    simp
  · have : (n : ℚ) ≠ 0 := by rwa [← intCast_inj]  at hn
    simp only [Int.ediv_self hn, Int.cast_one, div_self this]

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

Goal state before:
pp: case nil
α : Type u
⊢ nil.numLeaves = nil.numNodes + 1

Tactic:
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

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

Goal state before:
pp: case node
α : Type u
value✝ : α
left✝ right✝ : BinaryTree α
left_ih✝ : left✝.numLeaves = left✝.numNodes + 1
right_ih✝ : right✝.numLeaves = right✝.numNodes + 1
⊢ (node value✝ left✝ right✝).numLeaves = (node value✝ left✝ right✝).numNodes + 1

Tactic:
simp [*, Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

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

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑((unionEqSigmaOfDisjoint h) x).snd = ↑x

Tactic:
right

Goal state after:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑x
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

Tactic:
suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x.2 = y.2
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective (Ι a)

Tactic:
by
  simpa only [uIoc_comm] using uIoc_injective_right a

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False

Tactic:
exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
  obtain ⟨c, rfl⟩ := hf c
  exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
by
    rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]
    exact hc.2 (ht.image _ fun _ _ ↦ e.symm.map_rel_iff.mp)
      ((e.toEquiv.subset_symm_image _ _).2 hf)

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
y : M
hy : y ≠ 1
⊢ mulSupport (update f x y) = insert x (mulSupport f)

Tactic:
by
  ext a; obtain rfl | hne := eq_or_ne a x <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : One M
inst✝ : DecidableEq ι
f : ι → M
x : ι
⊢ mulSupport (update f x 1) = mulSupport f \ {x}

Tactic:
by
  ext a; obtain rfl | hne := eq_or_ne a x <;> simp [*]

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

Goal state before:
pp: case succ
n m : ℕ
h : n ≤ m
k : ℕ
ih : n.ascFactorial k ≤ m.ascFactorial k
⊢ n.ascFactorial (k + 1) ≤ m.ascFactorial (k + 1)

Tactic:
exact Nat.mul_le_mul (by lia) ih

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

Goal state before:
pp: ⊢ ascFactorial = ascFactorialBinary

Tactic:
ext n k
  fun_induction ascFactorialBinary with
  | case1 => simp
  | case2 => simp [ascFactorial]
  | case3 n k ih₁ ih₂ => grind [ascFactorial_mul_ascFactorial]

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : ¬2 * fract x < 1
⊢ ⌊2 * fract x⌋ = 1

Tactic:
simpa [floor_eq_iff, ← two_mul, fract_lt_one] using h

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
a : α
⊢ round (a + 1) = round a + 1

Tactic:
by
  rw [← round_add_intCast a 1, cast_one]

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

Goal state before:
pp: m k : ℕ+
⊢ ↑(m.mod k) + ↑k * m.div k = ↑m

Tactic:
exact mod_add_div _ _

Goal state after:
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ fract x ≤ |x - ↑z| ∨ 1 - fract x ≤ |x - ↑z|

Tactic:
right

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
hx : x < ↑z
⊢ 1 - fract x ≤ |x - ↑z|
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
s : Set R
x : R
⊢ x ∈ fract ⁻¹' s ↔ x ∈ ⋃ m, (fun x ↦ x - ↑m) ⁻¹' (s ∩ Ico 0 1)

Tactic:
simp only [mem_preimage, mem_iUnion, mem_inter_iff]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
s : Set R
x : R
⊢ fract x ∈ s ↔ ∃ i, x - ↑i ∈ s ∧ x - ↑i ∈ Ico 0 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
⊢ q.num / ↑q.den = n / ↑d

Tactic:
obtain ⟨c, n_eq_c_mul_num, d_eq_c_mul_denom⟩ : ∃ c, n = c * q.num ∧ (d : ℤ) = c * q.den := by
    rw [q_eq]
    exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne')

Goal state after:
case inr
n : ℤ
d : ℕ
hd : 0 < d
q : ℚ := ↑n / ↑d
q_eq : q = ↑n / ↑d
c : ℤ
n_eq_c_mul_num : n = c * q.num
d_eq_c_mul_denom : ↑d = c * ↑q.den
⊢ q.num / ↑q.den = n / ↑d
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ fract a = 0 ∨ fract a = a + 1 - ↑⌈a⌉

Tactic:
right

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ fract a = a + 1 - ↑⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑⌈a⌉ = ↑(⌊a⌋ + 1)

Tactic:
refine congrArg Int.cast (ceil_eq_iff.mpr ⟨?_, _root_.le_of_lt <| by simp⟩)

Goal state after:
case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
ha : fract a ≠ 0
⊢ ↑(⌊a⌋ + 1) - 1 < a
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
x y : G
hxy : (fun x1 x2 ↦ x1 < x2) x y
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
this✝ : ∀ (x y : G), x < y → x ∈ Ico l (l + a) → R (f x) (f y)
hx : x ∉ Ico l (l + a)
m : ℤ
hm : x - m • a ∈ Ico l (l + a)
this : R (f (x - m • a)) (f (y - m • a))
⊢ R (f x) (f y)

Tactic:
by simpa using hR (m • b) this

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ ↑⌈(b - 1)⁻¹⌉ ≤ b * (↑⌈(b - 1)⁻¹⌉ / b)

Tactic:
mul_div_cancel₀

Goal state after:
case inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ ↑⌈(b - 1)⁻¹⌉ ≤ ↑⌈(b - 1)⁻¹⌉

case inl.hb
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b ≤ ↑⌈(b - 1)⁻¹⌉ / b
⊢ b ≠ 0
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ l <+~ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor
  · rw [subperm_iff]
    rintro ⟨s, hla, h⟩
    rwa [perm_singleton.mp hla, sublist_singleton] at h
  · rintro (rfl | rfl)
    exacts [nil_subperm, Subperm.refl _]

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

Goal state before:
pp: case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ head✝ :: tail✝.bagInter (l₂.erase head✝) <+ head✝ :: tail✝ ∩ l₂

Tactic:
cons_sublist_cons

Goal state after:
case cons.isTrue
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
ih : ∀ {l₂ : List α}, tail✝.bagInter l₂ <+ tail✝ ∩ l₂
l₂ : List α
h✝ : head✝ ∈ l₂
⊢ tail✝.bagInter (l₂.erase head✝) <+ tail✝ ∩ l₂
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝¹ : DecidablePred p
q : α → Prop
inst✝ : DecidablePred q
s✝ : Multiset α
a : α
s : Multiset α
IH : filter p s + filter q s = filter (fun a ↦ p a ∨ q a) s + filter (fun a ↦ p a ∧ q a) s
⊢ filter p (a ::ₘ s) + filter q (a ::ₘ s) = filter (fun a ↦ p a ∨ q a) (a ::ₘ s) + filter (fun a ↦ p a ∧ q a) (a ::ₘ s)

Tactic:
by by_cases p a <;> by_cases q a <;> simp [*]

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

Goal state before:
pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ∪ t + s ∩ t ≤ s + t

pp: case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t

Tactic:
· rw [union_add_distrib]
    refine union_le (Multiset.add_le_add_left inter_le_right) ?_
    rw [Multiset.add_comm]
    exact Multiset.add_le_add_right inter_le_left

Goal state after:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t ≤ s ∪ t + s ∩ t
Module: Mathlib.Data.Multiset.Filter

Goal state before:
pp: case cons.e_a
α : Type u_1
β : Type v
f : α → β
p : α → Prop
inst✝ : DecidablePred p
a : α
s : Multiset α
⊢ map (fun x ↦ f x) (if p a then {a} else 0) = (if p a then some {f a} else none).getD 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: α : Type u_3
motive : (s : Finset α) → s.Nonempty → Prop
singleton : ∀ (a : α), motive {a} ⋯
cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (hs : s.Nonempty), motive s hs → motive (Finset.cons a s h) ⋯
s : Finset α
hs : s.Nonempty
⊢ motive s hs

Tactic:
by
  induction s using Finset.cons_induction with
  | empty => exact (not_nonempty_empty hs).elim
  | cons a t ha h =>
    obtain rfl | ht := t.eq_empty_or_nonempty
    · exact singleton a
    · exact cons a t ha ht (h ht)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u

Tactic:
simp only [disjoint_left, mem_union, or_imp, forall_and]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⊆ (insert a s).erase a

Tactic:
← subset_insert

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s.erase a ⊆ s.erase a
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
p : α → Prop
s : Finset { x // p x }
x : { x // p x }
left✝ : x ∈ s
h : (Embedding.subtype fun x ↦ p x) x ∈ map (Embedding.subtype fun x ↦ p x) s
⊢ p ((Embedding.subtype fun x ↦ p x) x)

Tactic:
exact x.2

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

Goal state before:
pp: α : Sort u_1
k l k' l' : ℕ
h : k = l
h' : k' = l'
f : Fin k → Fin k' → α
g : Fin l → Fin l' → α
⊢ f ≍ g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩

Tactic:
subst h
  subst h'
  simp [funext_iff]

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

Goal state before:
pp: case h
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
⊢ ↑(e ⟨i, hi⟩) = i

Tactic:
refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)

Goal state after:
case h.refine_1
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < ↑(e ⟨i, hi⟩)
⊢ j < i

case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case neg
n : ℕ
h : 2 < n
this : NeZero n
i : ℕ
hi : i < n
j : ℕ
hj : j < n
h0 : ¬(0 ≠ i ∧ 0 ≠ j)
h1 : ¬(1 ≠ i ∧ 1 ≠ j)
⊢ ∃ k, ↑k ≠ i ∧ ↑k ≠ j

Tactic:
· refine ⟨⟨2, by lia⟩, ?_⟩
      dsimp only
      lia

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

Goal state before:
pp: n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ ↑(a + b) = ↑a + ↑b

Tactic:
val_add

Goal state after:
n : ℕ
a b : Fin n
huv : ↑a + ↑b < n
⊢ (↑a + ↑b) % n = ↑a + ↑b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
h : ¬last (n + 1) = 0
⊢ (last (n + 1)).pred h = last n

Tactic:
simp_rw [← succ_last, pred_succ]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi ≤ j ↔ i ≤ j.castSucc

Tactic:
by
  rw [← castSucc_le_castSucc_iff, castSucc_castPred]

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

Goal state before:
pp: n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j ≤ i.castPred hi ↔ j.castSucc ≤ i

Tactic:
by
  rw [← castSucc_le_castSucc_iff, castSucc_castPred]

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

Goal state before:
pp: case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p

Tactic:
exact Fin.ne_of_lt h

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

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ map (⇑σ) (finRange n) ~ finRange n

Tactic:
rw [perm_ext_iff_of_nodup ((nodup_finRange n).map σ.injective) <| nodup_finRange n]

Goal state after:
n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0

Tactic:
hi,

Goal state after:
case pos
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 0 = 0
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove i = last n

Tactic:
hi,

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove (last (n + 1)) = last n
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
one_lt_card

Goal state after:
α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
obtain h | h := Fin.le_or_gt (succ a) b
  · rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]
  · rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]

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

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
u : Fin m → α
v : Fin n → α
hu : m = 0
l : Fin m
⊢ append u v (castAdd n l) = (v ∘ Fin.cast ⋯) (castAdd n l)

Tactic:
exact (Fin.cast hu l).elim0

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

Goal state before:
pp: case refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append (append a b) c (castAdd p l) = append a (append b c) (Fin.cast ⋯ (castAdd p l))

Tactic:
rw [append_left]

Goal state after:
case refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
⊢ append a b l = append a (append b c) (Fin.cast ⋯ (castAdd p l))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_1.refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ append a b (castAdd n ll) = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))

Tactic:
rw [append_left]

Goal state after:
case refine_1.refine_1
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
l : Fin (m + n)
ll : Fin m
⊢ a ll = append a (append b c) (Fin.cast ⋯ (castAdd p (castAdd n ll)))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: m n : ℕ
α : Sort u_2
a : α
as : Fin n → α
bs : Fin m → α
⊢ append (cons a as) bs = cons a (append as bs) ∘ Fin.cast ⋯

Tactic:
by
  funext i
  rcases i with ⟨i, -⟩
  simp only [append, addCases, cons, castLT, comp_apply]
  rcases i with - | i
  · simp
  · split_ifs with h
    · have : i < n := Nat.lt_of_succ_lt_succ h
      simp [addCases, this]
    · have : ¬i < n := Nat.not_le_of_gt <| Nat.le_of_lt_succ <| Nat.gt_of_not_le h
      simp [addCases, this]

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

Goal state before:
pp: case mp.cons_cons
α : Type u_1
l l' l₁✝ l₂✝ : List α
a✝¹ : α
a✝ : l₁✝ <+ l₂✝
IH : ∃ f, ∀ (ix : ℕ), l₁✝[ix]? = l₂✝[f ix]?
⊢ ∃ f, ∀ (ix : ℕ), (a✝¹ :: l₁✝)[ix]? = (a✝¹ :: l₂✝)[f ix]?

Tactic:
| cons_cons _ _ IH =>

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
f : (i : Fin (n + 1)) → α i
⊢ removeNth 0 f = tail f

Tactic:
by
  ext; simp [tail, removeNth]

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
x y : α p
f : (i : Fin n) → α (p.succAbove i)
⊢ update (p.insertNth x f) p y = p.insertNth y f

Tactic:
simp [eq_insertNth_iff]

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

Goal state before:
pp: case neg
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
h : ∃ i, p i
h✝ : ¬p 0
⊢ Fin.find p h = (Fin.find (fun k ↦ p k.succ) ⋯).succ

Tactic:
grind [find_of_not_zero]

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : Std.Trichotomous r
a : α
l₁ : List α
b : α
l₂ : List α
hab : ¬Lex r (a :: l₁) (b :: l₂)
hba : ¬Lex r (b :: l₂) (a :: l₁)
⊢ a :: l₁ = b :: l₂

Tactic:
obtain rfl := Std.Trichotomous.trichotomous a b (mt rel hab) (mt rel hba)
      rw [aux l₁ l₂ (mt cons hab) (mt cons hba)]

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

Goal state before:
pp: case cons.intro
α : Type u_1
r : α → α → Prop
a✝ a : α
h✝ : ∀ (y : α), r y a → Acc r y
ih : ∀ (y : α), r y a → ∀ (l : List α) (hl : List.IsChain (flip r) (y :: l)), Acc (List.lex_chains r) ⟨y :: l, hl⟩
l : List α
hl : List.IsChain (flip r) (a :: l)
⊢ Acc (List.lex_chains r) ⟨a :: l, hl⟩

Tactic:
| intro a _ ih =>

Goal state after: