mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
L : List G
n : ℕ
a : G
⊢ (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Tactic:
refine (prod_set L n a).trans ?_
  split_ifs with hn
  · rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
  · simp (disch := grind) [take_of_length_le, drop_eq_nil_of_le]

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

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ Rat.divInt ↑n₁ ↑d₁ * Rat.divInt ↑n₂ ↑d₂ = Rat.divInt (↑n₁ * ↑n₂) (↑d₁ * ↑d₂)

Tactic:
exact Rat.divInt_mul_divInt _ _

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)

Tactic:
conv =>

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * (d * e)
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
H : IsRelPrime x y
H1 : x ∣ z
H2 : y ∣ z
hx : IsPrimal x
⊢ x * y ∣ z

Tactic:
by
  rw [mul_comm]; exact H.symm.mul_dvd_of_right_isPrimal H2 H1 hx

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

Goal state before:
pp: case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ d ∣ n.natAbs * b.natAbs

Tactic:
rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]

Goal state after:
case neg
a b : ℤ
b0 : ¬b = 0
n : ℤ
d : ℕ
h : d ≠ 0
c : n.natAbs.Coprime d
e : a * ↑d = n * b
⊢ ↑d ∣ a * ↑d
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
⊢ ⨆ x, f x = ⨆ y, g y

Tactic:
convert! h1.iSup_comp g

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
inst✝ : SupSet α
f : ι → α
g : ι' → α
h : ι → ι'
h1 : Surjective h
h2 : ∀ (x : ι), g (h x) = f x
x✝ : ι
⊢ f x✝ = g (h x✝)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ ⨆ a ∈ s, f a ≤ f (sSup s)

Tactic:
rw [sSup_eq_iSup]; exact hf.le_map_iSup₂ _

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
⊢ (⋂₀ S)ᶜ = ⋃₀ (compl '' S)

Tactic:
by
  rw [sUnion_eq_compl_sInter_compl, compl_compl_image]

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:
conv =>

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

Goal state before:
pp: α✝ : Type u
β✝ : Type v
ι : Sort w
κ : ι → Sort w'
inst✝ : CompleteLinearOrder α✝
α : Type u
β : α → Type u
g : (a : α) → β a → α✝
lhs : α✝ := ⨅ a, ⨆ b, g a b
rhs : α✝ := ⨆ h, ⨅ a, g a (h a)
⊢ lhs ≤ rhs

Tactic:
if h : ∃ x, rhs < x ∧ x < lhs then
      rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)
    else
      refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_
      replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
      have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
      choose f hf using this
      have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => this _

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
f : (i : ι) → κ i → α
a : α
⊢ (⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a

Tactic:
by
  simp only [iSup_inf_eq]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝² : Frame α
ι : Type u_1
inst✝¹ : Preorder ι
inst✝ : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
j : ι
h₁ : i.1 ≤ j
h₂ : i.2 ≤ j
⊢ ∃ i', f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'

Tactic:
exact ⟨j, inf_le_inf (hf h₁) (hg h₂)⟩

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : BddAbove s
hne : s.Nonempty
⊢ IsLUB s (sSup s)

Tactic:
· exact isLUB_csSup hne hs

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

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s t : Set α
h₁ : BddAbove t
h₂ : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
rcases eq_empty_or_nonempty s with rfl | h
  · rw [csSup_empty]
    exact bot_le
  · exact csSup_le_csSup h₁ h h₂

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

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ Icc b (a ⊔ b) = Icc b a

Tactic:
sup_eq_left.2 h

Goal state after:
α : Type u_1
inst✝ : Lattice α
a b : α
h : b ≤ a
⊢ Icc b a = Icc b a
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z

pp: case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)

Tactic:
· rcases hs with ⟨y, hy⟩
    refine fun H => ⟨f y, fun x hx => ?_⟩
    rcases eq_or_ne x y with (rfl | hne)
    · apply Std.Refl.refl
    · exact H hx hy hne

Goal state after:
case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
⊢ MonotoneOn f s ∨ AntitoneOn f s ↔ ∀ a ∈ s, ∀ b ∈ s, ∀ c ∈ s, c ∈ [[a, b]] → f c ∈ [[f a, f b]]

Tactic:
by
  simp [monotoneOn_iff_monotone, antitoneOn_iff_antitone, monotone_or_antitone_iff_uIcc,
    mem_uIcc]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ioo b (max a b) = Ioo b a

Tactic:
sup_eq_left.2 h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ Ioo b a = Ioo b a
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ p < q ↔ p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
by
  rw [lt_iff_le_not_ge, not_le_iff_exists]

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 '' Ioc x y = Ioc (e x) (e y)

Tactic:
← e.preimage_Ioc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' ⇑e ⁻¹' Ioc (e x) (e y) = Ioc (e x) (e y)
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x ∈ s, φ x = b
b' : β
hb' : ∃ x ∈ s, φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False

Tactic:
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
⊢ False
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ = a * (a⁻¹ ⊔ 1)

Tactic:
mul_sup,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
a : α
⊢ a⁺ᵐ = a * a⁻¹ ⊔ a * 1
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a * (a⁻¹ ⊔ 1) ⊔ (a⁻¹ ⊔ 1) = |a|ₘ

Tactic:
mul_sup,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a * a⁻¹ ⊔ a * 1 ⊔ (a⁻¹ ⊔ 1) = |a|ₘ
Module: Mathlib.Algebra.Order.Group.PosPart

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ * (a ⊔ 1) = |a|ₘ

Tactic:
mul_sup,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻ᵐ * a ⊔ a⁻ᵐ * 1 = |a|ₘ
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inl
m n : ℕ
hn : 1 < n
⊢ n ! = m ! ↔ n = m

Tactic:
exact factorial_inj hn

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

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

Tactic:
descFactorial_succ

Goal state after:
case succ
k m : ℕ
h : k ≤ m
n : ℕ
ih : k.descFactorial n ≤ m.descFactorial n
⊢ (k - n) * k.descFactorial n ≤ (m - n) * m.descFactorial n
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case pos.e_a
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
h : 2 * fract x < 1
⊢ fract x ∈ Ico 0 1

Tactic:
suffices fract x < 1 by simpa
      refine lt_of_le_of_lt ?_ h
      apply le_mul_of_one_le_left <;> simp

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

Goal state before:
pp: α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ |x - ↑(round x)| ≤ |x - ↑z|

Tactic:
abs_sub_round_eq_min,

Goal state after:
α : Type u_2
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
x : α
z : ℤ
⊢ min (fract x) (1 - fract x) ≤ |x - ↑z|
Module: Mathlib.Algebra.Order.Round

Goal state before:
pp: case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ |↑m / ↑n - ↑(round (↑m / ↑n))| = ↑(min (m % n) (n - m % n)) / ↑n

Tactic:
abs_sub_round_eq_min,

Goal state after:
case inr
α : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
m n : ℕ
hn : n > 0
hn' : 0 < ↑n
⊢ min (fract (↑m / ↑n)) (1 - fract (↑m / ↑n)) = ↑(min (m % n) (n - m % n)) / ↑n
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
m : ℤ
a : R
⊢ fract (↑m + a) = fract a

Tactic:
by
  rw [add_comm, fract_add_intCast]

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

Goal state before:
pp: k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ (fract (b / a) + ↑⌊b / a⌋) * a = b

Tactic:
fract_add_floor,

Goal state after:
k : Type u_4
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : FloorRing k
a b : k
ha : a ≠ 0
⊢ b / a * a = b
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 b : R
⊢ ⌈a⌉ + ⌈b⌉ ≤ ⌈a + b⌉ + 1

Tactic:
rw [← le_sub_iff_add_le, ceil_le, Int.cast_sub, Int.cast_add, Int.cast_one, le_sub_comm]

Goal state after:
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
⊢ ↑⌈b⌉ ≤ ↑⌈a + b⌉ + 1 - a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a b : k
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉ ≤ a
⊢ b * a < b * (↑⌊a⌋ + 1)

Tactic:
gcongr; apply lt_floor_add_one

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

Goal state before:
pp: q : ℚ
q_pos : 0 < q
⊢ (fract q⁻¹).num < q.num

Tactic:
have q_num_pos : 0 < q.num := Rat.num_pos.mpr q_pos

Goal state after:
q : ℚ
q_pos : 0 < q
q_num_pos : 0 < q.num
⊢ (fract q⁻¹).num < q.num
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case inl
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) ⟨j, hj⟩
hij : i < j
⊢ ⟨i, hi⟩ = ⟨j, hj⟩

Tactic:
exact (h i j hi hj hij hg).elim

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

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel r as (b ::ₘ bs) ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'

Tactic:
← rel_flip,

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
b : β
bs : Multiset β
⊢ Rel (flip r) (b ::ₘ bs) as ↔ ∃ a as', r a b ∧ Rel r as' bs ∧ as = a ::ₘ as'
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel r as (bs₀ + bs₁) ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
← rel_flip,

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ Rel (flip r) (bs₀ + bs₁) as ↔ ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l.concat a).Nodup

Tactic:
by
  rw [concat_eq_append]; exact h'.append (nodup_singleton _) (disjoint_singleton.2 h)

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

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel r s (map f t) ↔ Rel (fun a b ↦ r a (f b)) s t

Tactic:
← rel_flip,

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset α
t : Multiset γ
f : γ → β
⊢ Rel (flip r) (map f t) s ↔ Rel (fun a b ↦ r a (f b)) s t
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ f x :: (map f xs).dedup = map f (x :: xs.dedup)

Tactic:
ih,

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
hf : Function.Injective f
x : α
xs : List α
ih : (map f xs).dedup = map f xs.dedup
h : ¬x ∈ xs
⊢ f x :: map f xs.dedup = map f (x :: xs.dedup)
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₂

Goal state after:
case nil
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (a :: l₂) = [].bagInter l₂

case cons
α : Type u_1
l₁ : List α
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (l₂ : List α), ¬a ∈ tail✝ → tail✝.bagInter (a :: l₂) = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (head✝ :: tail✝).bagInter (a :: l₂) = (head✝ :: tail✝).bagInter l₂
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₂

Goal state after:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ []
⊢ [].bagInter (l₂.erase a) = [].bagInter l₂

case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬a ∈ tail✝ → tail✝.bagInter (l₂.erase a) = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ head✝ :: tail✝
⊢ (head✝ :: tail✝).bagInter (l₂.erase a) = (head✝ :: tail✝).bagInter l₂
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₂

Goal state after:
case nil
α : Type u_1
a : α
inst✝ : DecidableEq α
l₂ : List α
h : ¬a ∈ l₂
⊢ ([].erase a).bagInter l₂ = [].bagInter l₂

case cons
α : Type u_1
a : α
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {l₂ : List α}, ¬a ∈ l₂ → (tail✝.erase a).bagInter l₂ = tail✝.bagInter l₂
l₂ : List α
h : ¬a ∈ l₂
⊢ ((head✝ :: tail✝).erase a).bagInter l₂ = (head✝ :: tail✝).bagInter l₂
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
⊢ filter p (s.erase a) - filter p t = filter p s - filter p (a ::ₘ t)

Tactic:
rw [filter_cons_of_pos _ h, sub_cons]
    congr
    by_cases m : a ∈ s
    · rw [← cons_inj_right a, ← filter_cons_of_pos _ h, cons_erase (mem_filter_of_mem m h),
        cons_erase m]
    · rw [erase_of_notMem m, erase_of_notMem (mt mem_of_mem_filter m)]

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

Goal state before:
pp: a : ℕ
m : Multiset ℕ
⊢ _root_.Disjoint (range a) (map (fun x ↦ a + x) m)

Tactic:
by
  rw [disjoint_left]
  intro x hxa hxb
  rw [range, mem_coe, List.mem_range] at hxa
  obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
  exact (Nat.le_add_right _ _).not_gt hxa

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (∃ a, s = {a}) ↔ ∃! a, a ∈ s

Tactic:
simp only [eq_singleton_iff_unique_mem, ExistsUnique]

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

Goal state before:
pp: α : Type u_1
s t : Finset α
a : α
hs : a ∉ s
ht : a ∉ t
⊢ cons a s hs ⊆ cons a t ht ↔ s ⊆ t

Tactic:
by
  rwa [← coe_subset, coe_cons, coe_cons, Set.insert_subset_insert_iff, coe_subset]

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : Subsingleton α
⊢ s.Nonempty → s = univ

Tactic:
by
  rintro ⟨x, hx⟩
  exact eq_univ_of_forall fun y => by rwa [Subsingleton.elim y x]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ a ∈ s \ t ∨ a ∈ t \ s ↔ a ∈ s ∧ a ∉ t ∨ a ∈ t ∧ a ∉ s

Tactic:
mem_sdiff

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ x ∈ (replicate n a).toFinset ↔ x ∈ if n = 0 then ∅ else {a}

Tactic:
simp only [mem_toFinset, mem_replicate]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
a x : α
⊢ n ≠ 0 ∧ x = a ↔ x ∈ if n = 0 then ∅ else {a}
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image f ((image f)^[n] s) = image (f ∘ f^[n]) s

Tactic:
ih,

Goal state after:
case succ
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
f : α → α
n : ℕ
ih : (image f)^[n] s = image f^[n] s
⊢ image f (image f^[n] s) = image (f ∘ f^[n]) s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: α : Type u_1
t : Set α
s : Finset ↑t
⊢ ↑(map (Embedding.subtype fun x ↦ x ∈ t) s) ⊆ t

Tactic:
intro a ha
  rw [mem_coe] at ha
  convert! property_of_mem_map_subtype s ha

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

Goal state before:
pp: α : Type u_1
s : Finset α
n : ℕ
f : (i : ℕ) → i < n → α
hf : ∀ a ∈ s, ∃ i, ∃ (h : i < n), f i h = a
hf' : ∀ (i : ℕ) (h : i < n), f i h ∈ s
f_inj : ∀ (i j : ℕ) (hi : i < n) (hj : j < n), f i hi = f j hj → i = j
⊢ #s = n

Tactic:
have : s = (range n).attach.image fun i => f i.1 (mem_range.1 i.2) := by
    ext a
    suffices _ : a ∈ s ↔ ∃ (i : _) (hi : i ∈ range n), f i (mem_range.1 hi) = a by
      simpa only [mem_image, mem_attach, true_and, Subtype.exists]
    constructor
    · intro ha; obtain ⟨i, hi, rfl⟩ := hf a ha; use i, mem_range.2 hi
    · rintro ⟨i, hi, rfl⟩; apply hf'
  calc
    #s = #((range n).attach.image fun i => f i.1 (mem_range.1 i.2)) := by rw [this]
    _ = #(range n).attach := ?_
    _ = #(range n) := card_attach
    _ = n := card_range n
  apply card_image_of_injective
  intro ⟨i, hi⟩ ⟨j, hj⟩ eq
  exact Subtype.ext <| f_inj i j (mem_range.1 hi) (mem_range.1 hj) eq

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ ↑↑a = a.castSucc

Tactic:
ext
  exact val_cast_of_lt (Nat.lt_succ_of_lt a.is_lt)

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

Goal state before:
pp: case zero
α : Type u
n : ℕ
f : Fin (0 * n) → α
⊢ ofFn f = (ofFn fun i ↦ ofFn fun j ↦ f ⟨↑i * n + ↑j, ⋯⟩).flatten

Tactic:
simp [ofFn_zero, Nat.zero_mul, ofFn_zero]

Goal state after:
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 → α
i : Fin (m + n + p)
⊢ append (append a b) c i = append a (append b c) (Fin.cast ⋯ i)

Tactic:
refine Fin.addCases (fun l => ?_) (fun r => ?_) i

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 (append a b) c (castAdd p l) = append a (append b c) (Fin.cast ⋯ (castAdd p l))

case refine_2
m n : ℕ
α : Sort u_1
p : ℕ
a : Fin m → α
b : Fin n → α
c : Fin p → α
i : Fin (m + n + p)
r : Fin p
⊢ append (append a b) c (natAdd (m + n) r) = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: case h.inl
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hsing : Subsingleton α
⊢ P α

pp: case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α

Tactic:
· apply hbase

Goal state after:
case h.inr
P : (α : Type u_4) → [Fintype α] → Prop
hbase : ∀ (α : Type u_4) [inst : Fintype α] [Subsingleton α], P α
hstep :
  ∀ (α : Type u_4) [inst : Fintype α] [Nontrivial α],
    (∀ (β : Type u_4) [inst_2 : Fintype β], card β < card α → P β) → P α
n : ℕ
ih : ∀ m < n, ∀ (α : Type u_4) [inst : Fintype α], card α = m → P α
α : Type u_4
inst✝ : Fintype α
hn : card α = n
hnontriv : Nontrivial α
⊢ P α
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ init (snoc p x) i = p i

Tactic:
simp only [init, snoc, val_castSucc, is_lt, dite_true]

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
⊢ cast ⋯ (p (i.castSucc.castLT ⋯)) = p i
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
append_cast_right

Goal state after:
n m : ℕ
α : Sort u_2
xs : Fin n → α
x : α
ys : Fin m → α
⊢ (append xs (cons (cons x elim0 0) ys) ∘ Fin.cast ⋯) ∘ Fin.cast ⋯ = append xs (cons x ys) ∘ Fin.cast ⋯