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

Goal state before:
pp: case snd
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst✝¹ : CompletelyDistribLattice α
inst✝ : CompletelyDistribLattice β
ι✝ : Type (max u v)
κ✝ : ι✝ → Type (max u v)
f : (a : ι✝) → κ✝ a → α × β
⊢ (⨅ a, ⨆ b, f a b).2 = (⨆ g, ⨅ a, f a (g a)).2

Tactic:
simp [fst_iSup, fst_iInf, snd_iSup, snd_iInf, iInf_iSup_eq]

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
inst✝ : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ sSup (image2 (fun x1 x2 ↦ x1 ∆ x2) s t)

Tactic:
by
  rw [sSup_image2]
  calc
  _ ≤ ⨆ a ∈ s, a ∆ sSup t := by simpa [sSup_image] using sSup_symmDiff_le hs
  _ ≤ _ := iSup_mono fun a ↦ iSup_mono fun _ ↦ by simpa [sSup_image] using symmDiff_sSup_le ht

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

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : S ⊆ {⊤}
⊢ ⊤ ≤ a

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

Tactic:
· cases a
        · exact le_rfl
        cases h₁ haS

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective fun b ↦ Ι b a

Tactic:
rintro b c h

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : (fun b ↦ Ι b a) b = (fun b ↦ Ι b a) c
⊢ b = c
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ (if h : ∃ a, f a = x then g (Classical.choose h) else 1 x) = 1

Tactic:
dif_pos hf,

Goal state after:
case pos
ι : Type u_1
κ : Type u_2
N : Type u_4
inst✝ : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ∃ a, f a = x
⊢ g (Classical.choose hf) = 1
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : One M
inst✝ : One N
g : M → N
f : ι → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : ι
⊢ (g ∘ f) x = 1 ↔ f x = 1

Tactic:
by rw [Function.comp, hg (mem_range_self x)]

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

Goal state before:
pp: n k : ℕ
⊢ (n + 1).descFactorial (k.succ + 1) = (n + 1) * n.descFactorial k.succ

Tactic:
by
    rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ,
      Nat.mul_left_comm]

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

Goal state before:
pp: case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = n.descFactorial m

Tactic:
descFactorial_eq_zero_iff_lt.mpr (show n < m by lia)

Goal state after:
case neg
k m n : ℕ
hkm : k ≤ m
hmn : ¬m ≤ n
⊢ (n - k).descFactorial (m - k) * n.descFactorial k = 0
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.descFactorial (n + 1) ≤ m.descFactorial (n + 1)

Tactic:
| succ n ih =>

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

Goal state before:
pp: F : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : AddCommMonoid β
inst✝¹ : PartialOrder β
inst✝ : GroupNormClass F α β
f : F
x : α
⊢ x = 1 → f x = 0

Tactic:
rintro rfl
    exact map_one_eq_zero _

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

Goal state before:
pp: case succ.succ
p : ℕ+ → Sort u_1
a : ℕ+
hz : p 1
hi : (n : ℕ+) → ((m : ℕ+) → m ≤ n → p m) → p (n + 1)
k : ℕ
kprop : 0 < k + 1 + 1
hk : (m : ℕ+) → m < ⟨k + 1 + 1, kprop⟩ → p m
⊢ p ⟨k + 1 + 1, kprop⟩

Tactic:
exact hi ⟨k.succ, Nat.succ_pos _⟩ fun m hm => hk _ (Nat.lt_succ_iff.2 hm)

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a : α
ha : 1 < a
⊢ StrictMono fun n ↦ a ^ n

Tactic:
refine strictMono_int_of_lt_succ fun n ↦ ?_
  rw [zpow_add_one]
  exact lt_mul_of_one_lt_right' (a ^ n) ha

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

Goal state before:
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:
rw [sub_eq_iff_eq_add', ← mul_right_inj' hn'.ne', mul_div_cancel₀ _ hn'.ne', mul_add,
      mul_div_cancel₀ _ hn'.ne']

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 = ↑(m % n) + ↑n * ↑(↑m / ↑n)
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
m : ℤ
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
⊢ fract (↑m / ↑n) = ↑(m % ↑n) / ↑n

Tactic:
obtain ⟨m₀, rfl | rfl⟩ := m.eq_nat_or_neg

Goal state after:
case inr.inl
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑↑m₀ / ↑n) = ↑(↑m₀ % ↑n) / ↑n

case inr.inr
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
n : ℕ
hn : 0 < ↑n
this : ∀ {l : ℤ}, 0 ≤ l → fract (↑l / ↑n) = ↑(l % ↑n) / ↑n
m₀ : ℕ
⊢ fract (↑(-↑m₀) / ↑n) = ↑(-↑m₀ % ↑n) / ↑n
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
ha : 1 < a
b c : G
⊢ ∃! m, b / a ^ m ∈ Ico c (c * a)

Tactic:
simpa only [mem_Ico, le_div_iff_mul_le, one_mul, mul_comm c, div_lt_iff_lt_mul, mul_assoc] using
    existsUnique_zpow_near_of_one_lt' ha (b / c)

Goal state after:
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
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f x + n • b

Tactic:
← map_add_zsmul f x n,

Goal state after:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f (x + n • 1)
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: case h
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
x y : K
inst✝ : ExistsAddOfLE K
hx : 0 < x
hy : y < 1
y_pos : y ≤ 0
⊢ y < x

Tactic:
exact y_pos.trans_lt hx

Goal state after:
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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ l + a + n • a = l + (n + 1) • a

Tactic:
add_comm n,

Goal state after:
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)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn : n < 0
⊢ l + a + n • a = l + (1 + n) • a
Module: Mathlib.Algebra.Order.Archimedean.Basic

Goal state before:
pp: K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ Nat.find this < b * c
hn : Nat.find this ≠ 0
⊢ False

Tactic:
rw [(Nat.succ_pred_eq_of_ne_zero hn).symm, pow_succ, mul_lt_mul_iff_left₀ hc₀] at H

Goal state after:
K : Type u_4
inst✝⁴ : Semifield K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : Archimedean K
inst✝ : ExistsAddOfLE K
a b c : K
h : a < b * c
hb₀ : 0 < b
hb₁ : b ≤ 1
hc₀ : 0 < c
hc₁ : c < 1
this : ∃ n, c ^ n < b
H : c ^ (Nat.find this).pred < b
hn : Nat.find this ≠ 0
⊢ False
Module: Mathlib.Data.Rat.Floor

Goal state before:
pp: case right
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_inv_def : q_inv = ↑q.den / ↑q.num
q_inv_eq : q⁻¹ = q_inv
q_inv_num_denom_ineq : q⁻¹.num - ⌊q⁻¹⌋ * ↑q⁻¹.den < ↑q⁻¹.den
coprime_q_denom_q_num : (↑q.den).natAbs.Coprime q.num.natAbs
this : (↑q.den).natAbs = q.den
⊢ (↑q.den / ↑q.num).den = q.num.natAbs

Tactic:
· suffices (((q.den : ℚ) / q.num).den : ℤ) = q.num.natAbs by exact mod_cast this
      rw [q_num_abs_eq_q_num]
      exact mod_cast Rat.den_div_eq_of_coprime q_num_pos coprime_q_denom_q_num

Goal state after:
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ (g • p₁ /ₛ p₂) • p₂ = (g * (p₁ /ₛ p₂)) • p₂

Tactic:
sdiv_smul,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g : G
p₁ p₂ : P
⊢ g • p₁ = (g * (p₁ /ₛ p₂)) • p₂
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • (p₂ /ₛ p₃) • p₃ = (p₁ /ₛ p₃) • p₃

Tactic:
sdiv_smul,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • p₂ = (p₁ /ₛ p₃) • p₃
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • p₂ = (p₁ /ₛ p₃) • p₃

Tactic:
sdiv_smul,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p₃ : P
⊢ p₁ = (p₁ /ₛ p₃) • p₃
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ f ↑n ≤ f a ↔ ↑n ≤ a

Tactic:
hf.le_iff_le

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ ↑n ≤ a ↔ ↑n ≤ a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ f a ≤ f ↑n ↔ a ≤ ↑n

Tactic:
hf.le_iff_le

Goal state after:
F : Type u_1
R : Type u_2
S : Type u_3
inst✝⁷ : Ring R
inst✝⁶ : LinearOrder R
inst✝⁵ : Ring S
inst✝⁴ : LinearOrder S
inst✝³ : FloorRing R
inst✝² : FloorRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : StrictMono ⇑f
a : R
n : ℤ
⊢ a ≤ ↑n ↔ a ≤ ↑n
Module: Mathlib.Algebra.Torsor.Defs

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ * (p₁ /ₛ p₂) = v₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂

Tactic:
← mul_right_inj v₁⁻¹,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁⁻¹ * (v₁ * (p₁ /ₛ p₂)) = v₁⁻¹ * v₂ ↔ v₁⁻¹ * v₂ = p₁ /ₛ p₂
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ↑⌊a⌋.toNat = ⌊a⌋

Tactic:
Int.toNat_of_nonneg (Int.floor_nonneg.2 ha)

Goal state after:
R : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ ⌊a⌋ = ⌊a⌋
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ (p /ₛ p₂) • p₁ = (p /ₛ p₂) • p₂

Tactic:
sdiv_smul,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ p : P
h : p /ₛ p₁ = p /ₛ p₂
⊢ (p /ₛ p₂) • p₁ = p
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case pos
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

pp: case neg
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
· subst h
      simp_all

Goal state after:
case neg
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
eq : a ::ₘ as = b ::ₘ bs
h : ¬a = b
⊢ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
a b : α
as bs : Multiset α
⊢ a ::ₘ as = b ::ₘ bs ↔ a = b ∧ as = bs ∨ a ≠ b ∧ ∃ cs, as = b ::ₘ cs ∧ bs = a ::ₘ cs

Tactic:
have : DecidableEq α := Classical.decEq α
  constructor
  · intro eq
    by_cases h : a = b
    · subst h
      simp_all
    · have : a ∈ b ::ₘ bs := eq ▸ mem_cons_self _ _
      have : a ∈ bs := by simpa [h]
      rcases exists_cons_of_mem this with ⟨cs, hcs⟩
      simp only [h, hcs, false_and, ne_eq, not_false_eq_true, cons_inj_right, exists_eq_right',
        true_and, false_or]
      have : a ::ₘ as = b ::ₘ a ::ₘ cs := by simp [eq, hcs]
      have : a ::ₘ as = a ::ₘ b ::ₘ cs := by rwa [cons_swap]
      simpa using this
  · intro h
    rcases h with (⟨eq₁, eq₂⟩ | ⟨_, cs, eq₁, eq₂⟩)
    · simp [*]
    · simp [*, cons_swap a b]

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

Goal state before:
pp: α : Type u_1
l : List α
a : α
⊢ ↑l = {a} ↔ l = [a]

Tactic:
rw [← coe_singleton, coe_eq_coe, List.perm_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ range l.getI = insert default {x | x ∈ l}

Tactic:
unfold List.getI

Goal state after:
α : Type u_1
inst✝ : Inhabited α
l : List α
⊢ (range fun n ↦ l.getD n default) = insert default {x | x ∈ l}
Module: Mathlib.Data.Multiset.ZeroCons

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

Tactic:
· exact fun ⟨b, bs', hab, h, Eq⟩ => Eq.symm ▸ Rel.cons hab h

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

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ (t + s) = a ::ₘ (s + t)

Tactic:
Multiset.add_comm

Goal state after:
α : Type u_1
a : α
s t : Multiset α
⊢ a ::ₘ (s + t) = a ::ₘ (s + t)
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
Multiset.add_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : a ∈ t
⊢ s + t.erase a = s + t.erase a
Module: Mathlib.Data.Multiset.AddSub

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

Tactic:
Multiset.add_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
t : Multiset α
a : α
s : Multiset α
h : ¬a ∈ t
⊢ s.erase a + t = s.erase a + t
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ u + t ↔ s ≤ t + u

Tactic:
Multiset.add_comm

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s ≤ t + u ↔ s ≤ t + u
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
m1 m2 : Multiset α
r : α → α → Prop
h : ∀ (a b : α), a ∈ m1 → b ∈ m2 → r a b
hc : m1.card = m2.card
⊢ Rel r m1 m2

Tactic:
by
  revert m1
  refine @(m2.induction_on ?_ ?_)
  · intro m _h hc
    rw [rel_zero_right, ← card_eq_zero, hc, card_zero]
  · intro a t ih m h hc
    rw [card_cons] at hc
    obtain ⟨b, hb⟩ := card_pos_iff_exists_mem.1 (show 0 < card m from hc.symm ▸ Nat.succ_pos _)
    obtain ⟨m', rfl⟩ := exists_cons_of_mem hb
    refine rel_cons_right.mpr ⟨b, m', h _ _ hb (mem_cons_self _ _), ih ?_ ?_, rfl⟩
    · exact fun _ _ ha hb => h _ _ (mem_cons_of_mem ha) (mem_cons_of_mem hb)
    · simpa using hc

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

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ (List.insert a l).Nodup

Tactic:
insert_of_mem h'

Goal state after:
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ (l₁.erase a).diff l₂ = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁

Tactic:
(hl₁.erase _).sdiff_eq_filter,

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ : List α
a : α
l₂ : List α
hl₁ : l₁.Nodup
⊢ List.filter (fun x ↦ decide ¬x ∈ l₂) (l₁.erase a) = List.filter (fun x ↦ decide ¬x ∈ a :: l₂) l₁
Module: Mathlib.Data.Multiset.Dedup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s : Multiset α
⊢ (map f s.dedup).dedup = (map f s).dedup

Tactic:
by
  simp [dedup_ext]

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
IH : ∀ {t : Multiset α}, s ∩ t ≤ t
t : Multiset α
⊢ (a ::ₘ s) ∩ t ≤ t

Tactic:
by_cases h : a ∈ t
    · simpa [h] using cons_le_cons a (IH (t := t.erase a))
    · simp [h, IH]

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

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

Tactic:
Multiset.add_comm

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

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

Tactic:
Multiset.add_comm

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : List α
hs : s.Nodup
⊢ s.toFinset.toList.toFinset = s.toFinset

Tactic:
rw [toList_toFinset]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ count y (replicate n x ∩ s) = count y (replicate (min n (count x s)) x)

Tactic:
count_inter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α
s : Multiset α
y : α
⊢ min (count y (replicate n x)) (count y s) = count y (replicate (min n (count x s)) x)
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
a : α
s t : Multiset α
⊢ _root_.Disjoint s (a ::ₘ t) ↔ ¬a ∈ s ∧ _root_.Disjoint s t

Tactic:
by
  rw [_root_.disjoint_comm, disjoint_cons_left]; tauto

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), count a (s ∩ t) = count a 0

Tactic:
count_inter,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ (∀ (a : α), count a s + count a t = max (count a s) (count a t)) ↔ ∀ (a : α), min (count a s) (count a t) = count a 0
Module: Mathlib.Data.Finset.Insert

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
ha : a ∉ s
r : β → β → Prop
f : α → β
⊢ _root_.Pairwise (r on fun a_1 ↦ f ↑a_1) ↔ _root_.Pairwise (r on fun a ↦ f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)

Tactic:
by
  simp only [pairwise_subtype_iff_pairwise_finset', Finset.coe_cons, Set.pairwise_insert]
  grind

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ {a} ⊆ sᶜ ↔ a ∉ s

Tactic:
singleton_subset_iff,

Goal state after:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∈ sᶜ ↔ a ∉ s
Module: Mathlib.Data.Finset.Image

Goal state before:
pp: n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun i ↦ i + 1, inj' := ⋯ } (range n))

Tactic:
ext (⟨⟩ | ⟨n⟩) <;> simp [Nat.zero_lt_succ n]

Goal state after:
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)^[n + 1] s = image f^[n + 1] s

Tactic:
| succ n ih =>

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ⊤.succ = ⊤

Tactic:
rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']

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

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

Tactic:
natCast_emod,

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑(n - ↑v + ↑u) % ↑n = ↑↑u - ↑↑v
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:
natCast_emod,

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑(n - ↑v + ↑u) % ↑n = ↑↑u - ↑↑v + ↑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:
natCast_emod,

Goal state after:
case isTrue
n : ℕ
u v : Fin n
h✝ : ↑u + ↑v < n
⊢ ↑(↑u + ↑v) % ↑n = ↑↑u + ↑↑v
Module: Mathlib.Data.Fin.Basic

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

Tactic:
natCast_emod,

Goal state after:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬↑u + ↑v < n
⊢ ↑(↑u + ↑v) % ↑n = ↑↑u + ↑↑v - ↑n
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = 0 ↔ b = 0

Tactic:
by
  rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]

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

Goal state before:
pp: n : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ z, y.succAbove z = x

Tactic:
obtain hxy | hyx := Fin.lt_or_lt_of_ne h

Goal state after:
case inl
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hxy : x < y
⊢ ∃ z, y.succAbove z = x

case inr
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hyx : y < x
⊢ ∃ z, y.succAbove z = x
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (natAdd m i.castSucc) = f (natAdd m i)

Tactic:
natAdd_castSucc,

Goal state after:
case refine_2
n m : ℕ
α : Sort u_2
f : Fin (m + n) → α
a : α
i✝ : Fin (n + 1)
i : Fin n
⊢ snoc f a (natAdd m i).castSucc = f (natAdd m i)
Module: Mathlib.Data.List.Sort

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
⊢ Pairwise r l → insertionSort r l = l

Tactic:
by
  induction l <;> grind [cases List]

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 : α p
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f p x) = p.removeNth f

Tactic:
by ext i; simp [removeNth]

Goal state after: