mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : f c < f a
⊢ f a = g a

Tactic:
hf.lt_iff_lt

Goal state after:
case inr.inr
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
hf : f ∈ {f | StrictMono f}
g : β → γ
hg : g ∈ {f | StrictMono f}
hfg : range f = range g
a✝ a : β
IH : ∀ (y : β), y < a → f y = g y
b : β
hb : g b = f a
h : a < b
c : β
hc : f c = g a
this : c < a
⊢ f a = g a
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
f : (i : { x // p x }) → β ↑i
g : (i : { x // ¬p x }) → β ↑i
i : α
⊢ (piEquivPiSubtypeProd p β).symm (f, g) i ∈ s i ↔ (∀ (b : p i), f ⟨i, b⟩ ∈ s i) ∧ ∀ (b : ¬p i), g ⟨i, b⟩ ∈ s i

Tactic:
by_cases hi : p i <;> simp [hi]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Ico a b ∪ {b} = Icc a b

Tactic:
Ico_union_right h

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)

Tactic:
by
  ext ⟨x, y⟩
  simp [and_assoc, and_left_comm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
a : α
inst✝ : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x✝ : α
⊢ x✝ ∈ upperBounds s

Tactic:
by rw [h, upperBounds_empty]; exact mem_univ _

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Semifield α
inst✝¹ : PartialOrder α
inst✝ : PosMulReflectLT α
a b : α
ha : 0 < a
h : a ≤ b
⊢ 1 / b ≤ 1 / a

Tactic:
by
  simpa using inv_anti₀ ha h

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

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
⊢ l.head! ∈ l

Tactic:
have h' : l.head! ∈ l.head! :: l.tail := mem_cons_self

Goal state after:
α : Type u
inst✝ : Inhabited α
l : List α
h : l ≠ []
h' : l.head! ∈ l.head! :: l.tail
⊢ l.head! ∈ l
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
ha : a ∈ l.dropLast
⊢ idxOf a l + 1 < l.length

Tactic:
have := idxOf_lt_length_of_mem ha
  grind [IsPrefix.idxOf_eq_of_mem]

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

Goal state before:
pp: M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L).prod * L[i] = (take (i + 1) L').prod
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
prod_take_succ L' i h₂,

Goal state after:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L).prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ map (fun a ↦ ↑a) (filter p l.attach) =
    map (fun a ↦ ↑a) (map (Subtype.map id ⋯) (filter (fun x ↦ decide (∃ h, p ⟨x, h⟩ = true)) l).attach)

Tactic:
simp [comp_def, map_filter _ Subtype.coe_injective]

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

Goal state before:
pp: q : ℚ
hq : q.num = 0
⊢ q = 0

Tactic:
by simpa [hq] using q.num_divInt_den.symm

Goal state after:
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.num = q.den

Tactic:
inv_def,

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ (divNat q.den q.num).num = q.den
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.den = q.num

Tactic:
inv_def,

Goal state after:
q : ℚ≥0
hq : q ≠ 0
⊢ (divNat q.den q.num).den = q.num
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a b c : α
hc : c ≠ 0
d : α
⊢ b * c = a * c * d ↔ b = a * d

Tactic:
rw [mul_right_comm, mul_left_inj' hc]

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

Goal state before:
pp: q₁ q₂ : ℚ
⊢ ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) ∣ q₁.num * q₂.num

Tactic:
← Int.dvd_natAbs

Goal state after:
q₁ q₂ : ℚ
⊢ ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den)) ∣ ↑(q₁.num * q₂.num).natAbs
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑a / ↑b

Tactic:
rw [← cast_natCast, ← cast_natCast b, ← cast_div]
  congr
  ext
  apply Rat.mkRat_eq_div

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

Goal state before:
pp: α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
inv_def,

Goal state after:
α : Type u_3
inst✝ : DivisionSemiring α
q : ℚ≥0
hq : ↑q.num ≠ 0
⊢ ↑(divNat q.den q.num) = (↑q)⁻¹
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
inv_def,

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
q : ℚ
hq : ↑q.num ≠ 0
⊢ ↑(↑q.den /. q.num) = (↑q)⁻¹
Module: Mathlib.Tactic.CancelDenoms.Core

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n e1 e2 t1 t2 : α
h1 : n * e1 = t1
h2 : n * e2 = t2
⊢ n * (e1 - e2) = t1 - t2

Tactic:
by simp [left_distrib, *, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Tactic.Linarith.Preprocessing

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
a b : M
h : 1 * a = b
⊢ a = b

Tactic:
rwa [one_mul] at h

Goal state after:
Module: Mathlib.Order.CompleteLattice.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ (⨆ a, ↑a).down = ⨆ a ∈ s, a.down

Tactic:
down_iSup,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝ : CompleteLattice α
s : Set (ULift α)
⊢ ⨆ i, (↑i).down = ⨆ a ∈ s, a.down
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ i, f ↑i

Tactic:
sSup_image'

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ ⨆ a, f ↑a = ⨆ i, f ↑i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i

Tactic:
iInf_iSup_eq,

Goal state after:
α : Type u
inst✝ : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ ⨆ i ∈ ⋂ j, s j, f i = ⨆ g, ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ a, f (g a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
s₁ s₂ : Set α
⊢ s₁ ⊆ s₂ ∪ s₁

Tactic:
apply subset_union_right

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s : Set α
⊢ (sInf s)ᶜ = ⨆ i ∈ s, iᶜ

Tactic:
simp only [sInf_eq_iInf, compl_iInf]

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Icc x y = Icc (e x) (e y)

Tactic:
by
  rw [← e.preimage_Icc, image_preimage_eq_inter_range, inter_eq_left.2 (he.out ⟨_, rfl⟩ ⟨_, rfl⟩)]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)

Tactic:
exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : S = ∅
⊢ IsLUB S ⟨a, ⋯⟩

pp: case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsLUB S ⟨sSup (Subtype.val '' S), ⋯⟩

Tactic:
· subst hS; simp only [isLUB_empty_iff, isBot_iff_eq_bot]; rfl

Goal state after:
case neg
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ IsLUB S ⟨sSup (Subtype.val '' S), ⋯⟩
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ ↑(⨆ i, f i) = ⨆ i, ↑(f i)

Tactic:
by
  rw [iSup, coe_sSup]; congr; ext; simp

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

Goal state before:
pp: n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n

Tactic:
exact Nat.mul_lt_mul_of_pos_left (by lia) (Nat.sub_pos_of_lt h)

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

Goal state before:
pp: case ofNat
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.ofNat n))⁻¹ = (↑(Int.ofNat n))⁻¹

pp: case negSucc
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹

Tactic:
· simp [cast_inv_nat]

Goal state after:
case negSucc
α : Type u_1
inst✝ : DivisionRing α
n : ℕ
⊢ ↑(↑(Int.negSucc n))⁻¹ = (↑(Int.negSucc n))⁻¹
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
y : ℤ
⊢ round (x + ↑y) = round x + y

Tactic:
rw [round, round, Int.fract_add_intCast, Int.floor_add_intCast, Int.ceil_add_intCast,
    ← apply_ite₂, ite_self]

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

Goal state before:
pp: case inr.refine_2
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑(m % n) / ↑n < 1

pp: case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)

Tactic:
· simpa only [div_lt_one hn', Nat.cast_lt] using m.mod_lt hn

Goal state after:
case inr.refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ ↑m / ↑n - ↑(m % n) / ↑n = ↑(↑m / ↑n)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌈a⌉ = ⌊a⌋ + 1

Tactic:
apply le_antisymm (Int.ceil_le_floor_add_one _)

Goal state after:
case refine_2
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : a ∉ range Int.cast
⊢ ⌊a⌋ + 1 ≤ ⌈a⌉
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ - 1 < ↑⌈(a - 1)⁻¹⌉ / a

Tactic:
sub_lt_comm,

Goal state after:
case inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha✝ : 1 ≤ a
ha : 1 < a
this : 0 < a - 1
⊢ ↑⌈(a - 1)⁻¹⌉ - ↑⌈(a - 1)⁻¹⌉ / a < 1
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
⊢ q⁻¹ = ↑q.den / ↑q.num

Tactic:
inv_def,

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
q_num_abs_eq_q_num : ↑q.num.natAbs = q.num
q_inv : ℚ := ↑q.den / ↑q.num
q_inv_def : q_inv = ↑q.den / ↑q.num
⊢ ↑q.den /. q.num = ↑q.den / ↑q.num
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
a b : k
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉ < b * a

Tactic:
calc
      ⌈a⌉ ≤ (⌈(b - 1)⁻¹⌉ : k) := by gcongr
      _ < b * a := by rwa [← div_lt_iff₀']; positivity

Goal state after:
Module: Mathlib.Data.List.Perm.Subperm

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

Tactic:
by_cases ha : a ∈ l₁

Goal state after:
case pos
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂

case neg
α : Type u_1
l₁ l₂ : List α
inst✝ : DecidableEq α
a : α
ha : ¬a ∈ l₁
⊢ a ∈ l₁ → count a l₁ ≤ count a l₂ ↔ count a l₁ ≤ count a l₂
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
Q : Type u_3
inst✝⁴ : Group G
inst✝³ : Torsor G P
inst✝² : SMul G Q
inst✝¹ : SDiv G Q
inst✝ : Nonempty Q
f : Q → P
hf : Injective f
smul : ∀ (c : G) (x : Q), f (c • x) = c • f x
sdiv : ∀ (x y : Q), x /ₛ y = f x /ₛ f y
c : G
x : Q
⊢ c • x /ₛ x = c

Tactic:
simp [sdiv, smul]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ (s + t).erase a = s.erase a + t

Tactic:
rw [Multiset.add_comm, erase_add_right_neg s h, Multiset.add_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : t ≤ s
⊢ a ::ₘ s - t = a ::ₘ (s - t)

Tactic:
rw [← singleton_add, ← singleton_add, Multiset.add_sub_assoc h]

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

Goal state before:
pp: α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) ↑l
⊢ b₁ ∈ replicate (↑l).card b₂

Tactic:
by rwa [map_const] at h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Multiset α
hst : Rel r s t
a✝ b✝ : α
as✝ bs✝ : Multiset α
hab : r a✝ b✝
_hst : Rel r as✝ bs✝
ih : map (Quot.mk r) as✝ = map (Quot.mk r) bs✝
⊢ map (Quot.mk r) (a✝ ::ₘ as✝) = map (Quot.mk r) (b✝ ::ₘ bs✝)

Tactic:
simp [ih, Quot.sound hab]

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

Goal state before:
pp: α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₁
⊢ l₁.bagInter (a :: l₂) = l₁.bagInter l₂

Tactic:
induction l₁ generalizing l₂ <;> grind

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ l₁
⊢ l₁.bagInter (l₂.erase a) = l₁.bagInter l₂

Tactic:
induction l₁ generalizing l₂ <;> grind

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
a : α
inst✝ : DecidableEq α
h : ¬a ∈ l₂
⊢ (l₁.erase a).bagInter l₂ = l₁.bagInter l₂

Tactic:
induction l₁ generalizing l₂ <;> grind

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t → u + s = u ∪ s

Tactic:
rintro rfl
      exact h0

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
⊢ (∃ a, a ∈ s ∧ true = true) ↔ s.Nonempty

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : a ∈ s
⊢ filter p (s.erase a) = (filter p s).erase a

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (s.erase a) = (filter p s).erase a

Tactic:
· rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
t✝ : Multiset α
a : α
t : Multiset α
IH : ∀ (s : Multiset α), filter p (s - t) = filter p s - filter p t
s : Multiset α
h : p a
m : ¬a ∈ s
⊢ filter p (s.erase a) = (filter p s).erase a
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a ∈ s, a ∈ t) ↔ (s ∩ t).Nonempty

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.attach.Nonempty ↔ s.Nonempty

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ Disjoint (filter p s) (filter q t)

Tactic:
simp_rw [disjoint_left, mem_filter]

Goal state after:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ s ⊆ map f.symm.toEmbedding t ↔ map f.toEmbedding s ⊆ t

Tactic:
constructor <;> intro h x hx

Goal state after:
case mp
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : s ⊆ map f.symm.toEmbedding t
x : β
hx : x ∈ map f.toEmbedding s
⊢ x ∈ t

case mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
h : map f.toEmbedding s ⊆ t
x : α
hx : x ∈ s
⊢ x ∈ map f.symm.toEmbedding t
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α → β
inst✝ : DecidableEq α
s : Multiset α
x✝ : β
⊢ x✝ ∈ image f s.toFinset ↔ x✝ ∈ (Multiset.map f s).toFinset

Tactic:
by simp only [mem_image, Multiset.mem_toFinset, Multiset.mem_map]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
y : β
⊢ {x ∈ s | f x = y}.Nonempty ↔ y ∈ image f s

Tactic:
simp [Finset.Nonempty]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
s : { s // ∀ a ∈ s, p a }
⊢ (fun s ↦ ⟨Finset.map { toFun := fun a ↦ ↑a, inj' := ⋯ } s, ⋯⟩)
      ((fun s ↦ Finset.map (Subtype.impEmbedding (Membership.mem ↑s) p ⋯) (↑s).attach) s) =
    s

Tactic:
ext a; constructor <;> intro h <;>
    simp only [Finset.mem_map, Finset.mem_attach, Subtype.exists, Embedding.coeFn_mk,
      Subtype.impEmbedding] at * <;>
    grind

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

Goal state before:
pp: case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n

Tactic:
rw [natCast_emod, Int.emod_eq_of_lt]

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) = ↑↑u - ↑↑v + ↑n

case isFalse.H1
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ 0 ≤ ↑(n - ↑v + ↑u)

case isFalse.H2
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) < ↑n
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑↑⟨(↑u + ↑v) % n, ⋯⟩ = ↑↑u + ↑↑v

Tactic:
rw [natCast_emod, Int.emod_eq_of_lt]

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) = ↑↑u + ↑↑v

case isTrue.H1
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ 0 ≤ ↑(↑u + ↑v)

case isTrue.H2
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) < ↑n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩) = ↑i

Tactic:
← val_castLE h

Goal state after:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ ↑(castLE h ((Equiv.ofInjective (castLE h) ⋯).symm ⟨i, hi⟩)) = ↑i
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n) * n - n + (n - (↑i % n + 1))) % n

Tactic:
Nat.sub_add_sub_cancel _ H₁,

Goal state after:
n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ (m * n - (↑i / n * n + ↑i % n + 1)) % n = ((m - ↑i / n) * n - (↑i % n + 1)) % n

n m : ℕ
i : Fin (m * n)
H₁ : ↑i % n + 1 ≤ n
H₂ : ↑i / n < m
⊢ n ≤ (m - ↑i / n) * n
Module: Mathlib.Data.Fin.SuccPred

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

Tactic:
rw [succAbove_of_castSucc_lt _ _ h]

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p
Module: Mathlib.Data.List.Duplicate

Goal state before:
pp: case cons_duplicate
α : Type u_1
l : List α
x y✝ : α
l✝ : List α
a✝ : x ∈+ l✝
hm : x ∈ l✝
⊢ x ∈ y✝ :: l✝

Tactic:
| cons_duplicate _ hm =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s

Tactic:
have (i : ℕ) : 0 < #(g i) := (hs₀.image _).card_pos

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α → α
s : Finset α
hs : Set.MapsTo f ↑s ↑s
hs₀ : s.Nonempty
g : ℕ → Finset α := fun i ↦ image f^[i] s
this : ∀ (i : ℕ), 0 < #(g i)
⊢ ∃ n < #s, ∀ (m : ℕ), n ≤ m → image f^[m] s = image f^[n] s
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case succ
n : ℕ
β : Sort u_2
a : β
q : Fin n → β
b : β
j : Fin (n + 1)
⊢ cons a (snoc q b) j.succ = snoc (cons a q) b j.succ

Tactic:
| succ j =>

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : Std.Total r
inst✝ : IsTrans α r
l l' : List α
h : Pairwise r l
h' : Pairwise r l'
a b c : α
h₁ : decide (r a b) = true
h₂ : decide (r b c) = true
⊢ r a ?m.42

Tactic:
simpa using h₁

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Tactic:
by
  simp only [Set.Infinite, finite_union, not_and_or]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
l : List α
⊢ (map (⇑e) l).SortedGE ↔ l.SortedGE

Tactic:
simp_rw [← sortedLE_reverse, ← map_reverse, sortedLE_listMap]

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

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

Tactic:
rotate'_rotate'

Goal state after:
α : Type u
l : List α
n m : ℕ
⊢ l.rotate' (n + m) = l.rotate' (n + m)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n) % l.length

Tactic:
rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]

Goal state after:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length