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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
⊢ DirectedOn r (insert a s)

Tactic:
by
  rintro x (rfl | hx) y (rfl | hy)
  · exact ⟨y, Set.mem_insert _ _, refl _, refl _⟩
  · obtain ⟨w, hws, hwr⟩ := ha y hy
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
  · obtain ⟨w, hws, hwr⟩ := ha x hx
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩
  · obtain ⟨w, hws, hwr⟩ := hd x hx y hy
    exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Goal state after:
Module: Mathlib.Algebra.Group.Int.Units

Goal state before:
pp: u v : ℤ
⊢ u * v = 1 ↔ u = 1 ∧ v = 1 ∨ u = -1 ∧ v = -1

Tactic:
refine ⟨eq_one_or_neg_one_of_mul_eq_one', fun h ↦ Or.elim h (fun H ↦ ?_) fun H ↦ ?_⟩ <;>
    obtain ⟨rfl, rfl⟩ := H

Goal state after:
case refine_1
h : 1 = 1 ∧ 1 = 1 ∨ 1 = -1 ∧ 1 = -1
⊢ 1 * 1 = 1

case refine_2
h : -1 = 1 ∧ -1 = 1 ∨ -1 = -1 ∧ -1 = -1
⊢ -1 * -1 = 1
Module: Mathlib.Data.Set.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t : Set β
hf : Injective2 f
⊢ uncurry f '' (s ×ˢ t ∩ s' ×ˢ t) = uncurry f '' s ×ˢ t ∩ uncurry f '' s' ×ˢ t

Tactic:
image_inter hf.uncurry

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t t' : Set β
hf : Injective2 f
⊢ uncurry f '' (s ×ˢ t ∩ s ×ˢ t') = uncurry f '' s ×ˢ t ∩ uncurry f '' s ×ˢ t'

Tactic:
image_inter hf.uncurry

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : WellFoundedLT α
s : Set α
h : s.Nonempty
⊢ Minimal (fun x ↦ x ∈ s) (⋯.min s h)

Tactic:
by
  grind [Minimal, lt_iff_le_not_ge, WellFounded.min]

Goal state after:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : α → Type u_4
p : α → Prop
inst✝ : DecidablePred p
s : (i : α) → Set (β i)
⊢ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s = (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i

Tactic:
ext ⟨f, g⟩

Goal state after:
α : 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
⊢ (f, g) ∈ ⇑(piEquivPiSubtypeProd p β).symm ⁻¹' univ.pi s ↔ (f, g) ∈ (univ.pi fun i ↦ s ↑i) ×ˢ univ.pi fun i ↦ s ↑i
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DenselyOrdered α
x y : α
x✝ : ↑(Ioc x y)
a : α
ha : a ∈ Ioc x y
⊢ ∃ b, b < ⟨a, ha⟩

Tactic:
rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩
    exact ⟨⟨b, mem_Ioc.mpr ⟨hb₁, hb₂.le.trans ha.2⟩⟩, hb₂⟩

Goal state after:
Module: Mathlib.Tactic.Abel

Goal state before:
pp: α : Type u_1
inst✝ : AddCommMonoid α
x : α
⊢ x = term 1 x 0

Tactic:
by simp [term, one_nsmul]

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

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ l₁.eval * x₂ = l.eval

Tactic:
hx₂,

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval * l₂.eval = l.eval
⊢ l₁.eval * l₂.eval = l.eval
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval / x₂ = l.eval

Tactic:
hx₂,

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
l₁ l₂ l : NF M
x₁ x₂ : M
hx₁ : x₁ = l₁.eval
hx₂ : x₂ = l₂.eval
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval / l₂.eval = l.eval
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
l : NF M
r : ℤ
⊢ (l ^ r).eval = zpow' l.eval r

Tactic:
unfold NF.eval at ⊢
  simp only [zpow_apply, list_prod_zpow', map_map]
  congr! 2
  ext p
  simp [← zpow'_mul, mul_comm]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse f g
x : β
xs : List β
⊢ map f (map g (x :: xs)) = x :: xs

Tactic:
simp_rw [map_cons, h x, h.list_map xs]

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

Goal state before:
pp: L : List ℕ
h : ∀ (i : ℕ), i ∈ L → 1 ≤ i
⊢ L.length ≤ L.sum

Tactic:
induction L with

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

Goal state before:
pp: q r : ℚ
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)

Tactic:
have hqd : (q.den : ℤ) ≠ 0 := Int.natCast_ne_zero_iff_pos.2 q.den_pos

Goal state after:
q r : ℚ
hqd : ↑q.den ≠ 0
⊢ q + r = (q.num * ↑r.den + ↑q.den * r.num) /. (↑q.den * ↑r.den)
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b

Tactic:
have d0 : (d : α) ≠ 0 := by
    intro d0
    have dd := den_dvd a b
    rcases show (d : ℤ) ∣ b by rwa [e] at dd with ⟨k, ke⟩
    have : (b : α) = (d : α) * (k : α) := by rw [ke, Int.cast_mul, Int.cast_natCast]
    rw [d0, zero_mul] at this
    contradiction

Goal state after:
α : Type u_3
inst✝ : DivisionRing α
a b : ℤ
b0 : ↑b ≠ 0
b0' : b ≠ 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a /. b = { num := n, den := d, den_nz := h, reduced := c }
d0 : ↑d ≠ 0
⊢ ↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
Module: Mathlib.Data.Rat.Cast.Defs

Goal state before:
pp: α : Type u_3
inst✝ : DivisionRing α
a : ℤ
b : ℕ
hb : ↑b ≠ 0
⊢ ↑(mkRat a b) = ↑a / ↑b

Tactic:
by
  rw [Rat.mkRat_eq_divInt, cast_divInt_of_ne_zero, Int.cast_natCast]; rwa [Int.cast_natCast]

Goal state after:
Module: Mathlib.Tactic.Ring.Common

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a b₃ b₁ : R
b₂ : ℕ
⊢ a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)

Tactic:
rw [mul_left_comm]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (⇑e ⁻¹' s) ↔ BddAbove s

Tactic:
← e.bddAbove_image,

Goal state after:
α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (⇑e '' ⇑e ⁻¹' s) ↔ BddAbove s
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
hB : BddAbove s
⊢ BddAbove s

Tactic:
exact hB

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
Bs : BddAbove s
hB : BddAbove t
⊢ BddAbove t

Tactic:
exact hB

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
y : α
hy : y ∈ t
⊢ y ≤ sSup s

Tactic:
rcases ht y hy with ⟨x, xs, hyx⟩

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
s t : Set α
hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y
ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x
s_ne : s.Nonempty
t_ne : t.Nonempty
B : BddAbove s ∨ BddAbove t
Bs : BddAbove s
Bt : BddAbove t
y : α
hy : y ∈ t
x : α
xs : x ∈ s
hyx : y ≤ x
⊢ y ≤ sSup s
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a \ Ici b = Ico a b

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a ∩ (Ici b)ᶜ = Ico a b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a \ Ioi b = Icc a b

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a ∩ (Ioi b)ᶜ = Icc a b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ioi b = Ioc a b

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a ∩ (Ioi b)ᶜ = Ioc a b
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a \ Ici b = Ioo a b

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioi a ∩ (Ici b)ᶜ = Ioo a b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ BddBelow ((fun a ↦ ↑a) ⁻¹' S)

Tactic:
use ⊥

Goal state after:
case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ ⊥ ∈ lowerBounds ((fun a ↦ ↑a) ⁻¹' S)
Module: Mathlib.Order.Preorder.Chain

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

Tactic:
← e.toEquiv.eq_preimage_iff_image_eq,

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ c = ⇑e.toEquiv ⁻¹' t
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.toEquiv '' c = t

Tactic:
← e.toEquiv.eq_preimage_iff_image_eq,

Goal state after:
α : 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
⊢ c = ⇑e.toEquiv ⁻¹' t
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

Tactic:
simp_rw [← one_le_inv']; rw [leOnePart_def, ← maxDefault, ← sup_eq_maxDefault]; simp_rw [sup_comm]

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

Goal state before:
pp: n k : ℕ
h : 0 < n
⊢ n.pred ! * (n - succ 0 + succ 0).ascFactorial k = (n.pred + k)!

Tactic:
Nat.sub_one,

Goal state after:
n k : ℕ
h : 0 < n
⊢ n.pred ! * (n.pred + succ 0).ascFactorial k = (n.pred + k)!
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: n k j : ℕ
⊢ n.ascFactorial (j + 1) ≤ (j + 1)! * n ^ (j + 1)

Tactic:
rcases n.eq_zero_or_pos with rfl | hn
    · simp [zero_ascFactorial]
    rw [ascFactorial_succ, factorial_succ, pow_succ',
      Nat.mul_assoc (j + 1), Nat.mul_left_comm j !, ← Nat.mul_assoc (j + 1)]
    refine Nat.mul_le_mul ?_ (ascFactorial_le_factorial_mul_pow n j)
    rw [add_one_mul, Nat.add_comm, Nat.add_le_add_iff_right]
    exact Nat.le_mul_of_pos_right j hn

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 : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ |1 - fract x| = 1 - fract x

Tactic:
abs_one_sub_fract

Goal state after:
case inr
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
hx : 1 - fract x ≤ fract x
this : 0 < fract x
⊢ 1 - fract x = 1 - fract x
Module: Mathlib.Algebra.Order.Group.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
⊢ False

Tactic:
rcases exists_ne (1 : α) with ⟨b, hb⟩

Goal state after:
case inr.inl
α : Type u_1
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : DenselyOrdered α
inst✝ : Nontrivial α
h : IsCyclic α
ha : Surjective fun x ↦ 1 ^ x
b : α
hb : b ≠ 1
⊢ False
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: n d : ℕ
⊢ ⌊↑n / ↑d⌋ = ↑n / ↑d

Tactic:
exact floor_intCast_div_natCast n d

Goal state after:
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
n : ℕ
⊢ ⌈a + ↑n⌉ = ⌈a⌉ + ↑n

Tactic:
rw [← Int.cast_natCast, ceil_add_intCast]

Goal state after:
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 _)
    rw [add_one_le_iff, lt_ceil]
    exact lt_of_le_of_ne (Int.floor_le a) ((iff_false_right h).mp (floor_eq_self_iff_mem a))

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ g • x = h • x → g = h

Tactic:
smul_eq_iff_eq_inv_smul,

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ x = g⁻¹ • h • x → g = h
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
R : Type u_3
K✝ : Type u_4
K : Type u_5
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
⊢ Archimedean K

Tactic:
by
  rw [archimedean_iff_int_le]
  exact fun x => ⟨⌈x⌉, Int.le_ceil x⟩

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

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
m : ¬a ∈ s
t' : Multiset α
h : s ≤ t'
⊢ a ∈ t' → a ::ₘ s ≤ t'

Tactic:
revert m

Goal state after:
α : Type u_1
s t : Multiset α
a : α
t' : Multiset α
h : s ≤ t'
⊢ ¬a ∈ s → a ∈ t' → a ::ₘ s ≤ t'
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : l₁ <:+ l₂
hne : l₂ ≠ []
hl : l₂.head hne ∈ l₁
hnd : l₂.Nodup
⊢ l₁ = l₂

Tactic:
grind [List.IsSuffix]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ a ∈ l₁.bagInter l₂ ↔ a ∈ l₁ ∧ a ∈ l₂

Tactic:
by
  fun_induction List.bagInter with grind

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

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

Tactic:
by
  fun_induction List.bagInter with grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : List α
⊢ l₁.bagInter l₂ <+ l₁

Tactic:
by
  fun_induction List.bagInter with grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t : List α
h : l₁ ~ l₂
⊢ l₁.bagInter t ~ l₂.bagInter t

Tactic:
by
  induction h generalizing t with grind

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
⊢ List.drop n xs ~ ys ∩ List.drop n xs

Tactic:
let n' := xs.length - n

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ List.drop n xs ~ ys ∩ List.drop n xs
Module: Mathlib.Data.List.Perm.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ List.take n xs ++ List.drop (n + m) xs ~ ys ∩ List.take n xs ++ ys ∩ List.drop (n + m) xs

pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ (List.take n xs).Disjoint (List.drop (n + m) xs)

Tactic:
· exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ (List.take n xs).Disjoint (List.drop (n + m) xs)
Module: Mathlib.Data.Finset.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DecidableEq α
s t : Multiset α
⊢ IsWellFounded (Multiset β) fun x1 x2 ↦ x1 ⊂ x2

Tactic:
by
  classical
  exact Subrelation.isWellFounded (InvImage _ toFinset) toFinset_ssubset.2

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

Goal state before:
pp: α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = take (x.length + 1) y

Tactic:
← List.take_concat_get,

Goal state after:
α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ take x.length y ++ [y.get ⟨x.length, hl⟩] = (take x.length y).concat y[x.length]

α : Type u_1
x y : List α
h : x <+: y
hl : x.length < y.length
⊢ x.length < y.length
Module: Mathlib.Data.Multiset.FinsetOps

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
x✝ : s ≤ t ∧ a ∈ t
l : s ≤ t
m : a ∈ t
h : a ∈ s
⊢ ndinsert a s ≤ t

Tactic:
by simp [h, l]

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

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

Tactic:
simp [inits_eq_tails]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) i
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ ⊥

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ⊆ (fun x ↦ filter (fun x_1 ↦ f x_1 = x) t) (f x)
⊢ x ∈ ⊥
Module: Mathlib.Data.Finite.Defs

Goal state before:
pp: α : Type u
β : Type v
s : Set α
t : Set β
hst : ↑s ≃ ↑t
⊢ Finite ↑s ↔ Finite ↑t

Tactic:
hst.finite_iff

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev

Tactic:
succAbove_rev_left,

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.succAbove i.rev).rev.rev
Module: Mathlib.Data.Fin.Rev

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev

Tactic:
by rw [succAbove_rev_left, rev_rev]

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

Goal state before:
pp: n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev

Tactic:
succAbove_rev_left,

Goal state after:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = (p.succAbove i.rev.rev).rev
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
hb : b ≠ last n
hab : a ≤ b
⊢ a ≠ last n

Tactic:
intro rfl
  exact Nat.not_lt_of_le hab (lt_last_iff_ne_last.mpr hb)

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

Goal state before:
pp: m n : ℕ
a b : Fin n
h : b ≤ a
⊢ castAdd m a - castAdd m b = castAdd m (a - b)

Tactic:
by
  grind [Fin.sub_val_of_le]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), f a ha = b
hst : #s ≤ #t
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
⊢ a₁ = a₂

Tactic:
let f' : s → β := fun a ↦ f a a.2
  have hsurj' : Set.SurjOn f' s.attach t := fun x hx ↦ by simpa [f'] using hsurj x hx
  have hinj' := injOn_of_surjOn_of_card_le f' (fun x hx ↦ hf _ _) hsurj' (by simpa)
  exact congrArg Subtype.val (@hinj' ⟨a₁, ha₁⟩ (by simp) ⟨a₂, ha₂⟩ (by simp) ha₁a₂)

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

Goal state before:
pp: α : Type u_1
n : ℕ
x : α
b : Fin n → α
⊢ Set.range (cons x b) = insert x (Set.range b)

Tactic:
rw [range_fin_succ, cons_zero, tail_cons]

Goal state after:
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.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
n : ℕ
hn : #s ≤ n
⊢ ∃ t, s ⊆ t ∧ #t = n

Tactic:
induction n generalizing s with

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
i j : Fin (n + 1)
h : i < j
x : α i
p : (k : Fin n) → α (i.succAbove k)
⊢ i.insertNth x p j = ⋯ ▸ p (j.pred ⋯)

Tactic:
rw [insertNth, succAboveCases, dif_neg (Fin.ne_of_gt h), dif_neg (Fin.lt_asymm h)]

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
⊢ decide (r a c) = true

Tactic:
simpa using _root_.trans (by simpa using h₁) (by simpa using h₂)

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

Goal state before:
pp: α : Type u_1
L : List (List α)
x : List α
⊢ x ++ (map (fun x_1 ↦ x_1 ++ x) L).flatten = (map (fun x_1 ↦ x ++ x_1) L).flatten ++ x

Tactic:
induction L with

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

Goal state before:
pp: α : Type u_1
σ : α → Type u_3
head✝ : α
l : List α
⊢ ((head✝ :: l).sigma fun a ↦ []) = []

Tactic:
simp [sigma_cons, sigma_nil l]

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

Goal state before:
pp: case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain R (b :: l).reverse ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun a b ↦ R b a) (b :: l)

Tactic:
IH2,

Goal state after:
case cons_cons
α : Type u_1
R : α → α → Prop
a b : α
l : List α
IH : IsChain R l.reverse ↔ IsChain (fun a b ↦ R b a) l
IH2 : ∀ (y : α), IsChain R (y :: l).reverse ↔ IsChain (fun a b ↦ R b a) (y :: l)
⊢ IsChain (fun a b ↦ R b a) (b :: l) ∧ IsChain R [b, a] ↔ R b a ∧ IsChain (fun a b ↦ R b a) (b :: l)
Module: Mathlib.Algebra.BigOperators.Group.List.Lemmas

Goal state before:
pp: M : Type u_8
inst✝ : CommMonoid M
L : List M
h : IsUnit L.prod
⊢ ∀ (m : M), m ∈ L → IsUnit m

Tactic:
induction L with

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
n : ℕ
a : α
h : r a a
⊢ IsChain r (replicate n a)

Tactic:
by
  induction n using Nat.twoStepInduction <;> grind

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

Goal state before:
pp: α : Type u
l : List α
n : ℕ
x : α
⊢ [x] = l.rotate n ↔ [x] = l

Tactic:
by
  rw [eq_comm, rotate_eq_singleton_iff, eq_comm]

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

Goal state before:
pp: s : Multiset ℤ
n : ℤ
⊢ s.prod % n = (map (fun x ↦ x % n) s).prod % n

Tactic:
induction s using Multiset.induction <;> simp [Int.mul_emod, *]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
h : l₁ ~ l₂
⊢ l₁.offDiag ~ l₂.offDiag

Tactic:
by
  classical simp_all [perm_iff_count, count_offDiag_eq_mul_sub_ite]

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

Goal state before:
pp: m n : ℕ
hn : n ≠ 0
p : ℕ := n - 1
hp : n = p + 1
⊢ (m * (p + 1) + (p + 1)).choose (p + 1) * (m * (p + 1))! * (p + 1)! = (m * (p + 1) + (p + 1))!

Tactic:
by rw [add_choose_mul_factorial_mul_factorial]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
a : α
⊢ {a} ^ 0 = {a ^ 0}

Tactic:
simp [singleton_one]

Goal state after: