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

Goal state before:
pp: case inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b

pp: case inr.inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

pp: case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b

Tactic:
· exact h.eq ha hb hab

Goal state after:
case inr.inl
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b

case inr.inr
α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
c : α
h : ↑a + 0 ≤ ↑a + c
hc : ↑b = ↑a + c
⊢ 0 ≤ c

Tactic:
exact le_of_add_le_add_left h

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

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

Tactic:
leOnePart_def,

Goal state after:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : Group α
inst✝ : MulLeftMono α
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)⁻¹

Tactic:
leOnePart_def,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ ⊔ 1 = (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⁻ᵐ ⊔ a⁻ᵐ = |a|ₘ

Tactic:
leOnePart_def,

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
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 ⊔ a⁻ᵐ = |a|ₘ

Tactic:
leOnePart_def,

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

Goal state before:
pp: m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (n + 1)!

Tactic:
intro k

Goal state after:
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
⊢ 0 < k → k ! < (k + 1)!
Module: Mathlib.Algebra.Order.Group.PosPart

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

Tactic:
leOnePart_def,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ max a⁻¹ 1 = if 1 ≤ a⁻¹ then a⁻¹ else 1
Module: Mathlib.Data.Nat.Factorial.Basic

Goal state before:
pp: case inr.inr
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m < n
⊢ n = m

Tactic:
h,

Goal state after:
case inr.inr
m n : ℕ
hn : 1 < m !
h : n ! = m !
hnm : m < n
⊢ n = m
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : ↑m % ↑k + ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ ↑m % ↑k + ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k

Tactic:
h,

Goal state after:
case pos
m k : ℕ+
h : ↑m % ↑k = 0
hm : 0 + ↑k * (↑m / ↑k) > 0
⊢ ↑k ≤ 0 + ↑k * (↑m / ↑k) ∧ ↑k ≤ ↑k
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ ↑m = ↑(k * ⟨n.succ, ⋯⟩)

Tactic:
h,

Goal state after:
case h
k m : ℕ+
n : ℕ
h : ↑m = ↑k * n.succ
⊢ ↑k * n.succ = ↑(k * ⟨n.succ, ⋯⟩)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case inr
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a b : R
h : ⌊a⌋ = ⌊b⌋
this : ∀ {a b : R}, ⌊a⌋ = ⌊b⌋ → b ≤ a → |a - b| < 1
h0 : ¬b ≤ a
⊢ |a - b| < 1

Tactic:
rw [abs_sub_comm]
    exact this h.symm (le_of_not_ge h0)

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 b : R
h : ⌊a⌋ = ⌊b⌋
h0 : b ≤ a
⊢ ↑⌊a⌋ + 1 - ↑⌊b⌋ = 1

Tactic:
h,

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

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

Tactic:
h,

Goal state after:
case refine_1
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsOrderedRing R
a : R
h : ⌈a⌉ = ⌊a⌋ + 1
ht : a ∈ range Int.cast
h0 : ↑⌊a⌋ = ↑(⌊a⌋ + 1)
⊢ False
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
g : G
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
by
  let s : Set ℤ := { n : ℤ | a ^ n ≤ g }
  obtain ⟨k, hk : g⁻¹ ≤ a ^ k⟩ := MulArchimedean.arch g⁻¹ ha
  have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩
  obtain ⟨k, hk⟩ := MulArchimedean.arch g ha
  have h_bdd : ∀ n ∈ s, n ≤ (k : ℤ) := by
    intro n hn
    apply (zpow_le_zpow_iff_right ha).mp
    rw [← zpow_natCast] at hk
    exact le_trans hn hk
  obtain ⟨m, hm, hm'⟩ := Int.exists_greatest_of_bdd ⟨k, h_bdd⟩ h_ne
  have hm'' : g < a ^ (m + 1) := by
    contrapose! hm'
    exact ⟨m + 1, hm', lt_add_one _⟩
  refine ⟨m, ⟨hm, hm''⟩, fun n hn => (hm' n hn.1).antisymm <| Int.le_of_lt_add_one ?_⟩
  rw [← zpow_lt_zpow_iff_right ha]
  exact lt_of_le_of_lt hm hn.2

Goal state after:
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 : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈(b - 1)⁻¹⌉ < b * a

Tactic:
← div_lt_iff₀'

Goal state after:
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)⁻¹
⊢ ↑⌈(b - 1)⁻¹⌉ / b < a

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)⁻¹
⊢ 0 < b
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₂ : G
p : P
h : g₁ • p = g₂ • p
⊢ g₁ • p /ₛ p = g₂

Tactic:
h,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
g₁ g₂ : G
p : P
h : g₁ • p = g₂ • p
⊢ g₂ • p /ₛ p = g₂
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
h : p₁ /ₛ p₂ = 1
⊢ (p₁ /ₛ p₂) • p₂ = p₂

Tactic:
h,

Goal state after:
G : Type u_1
P : Type u_2
inst✝ : Group G
T : Torsor G P
p₁ p₂ : P
h : p₁ /ₛ p₂ = 1
⊢ 1 • p₂ = p₂
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) = x✝

Tactic:
ext x; simp [Int.fract_eq_self.2 x.2, Int.floor_eq_zero_iff.2 x.2]

Goal state after:
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:
archimedean_iff_int_le

Goal state after:
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
⊢ ∀ (x : K), ∃ n, x ≤ ↑n
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mpr.inr
α : Type u_1
a b : α
as bs : Multiset α
this : DecidableEq α
left✝ : a ≠ b
cs : Multiset α
eq₁ : as = b ::ₘ cs
eq₂ : bs = a ::ₘ cs
⊢ a ::ₘ as = b ::ₘ bs

Tactic:
· simp [*, cons_swap a b]

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

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (a :: l.dropLast).Nodup ↔ l.Nodup

Tactic:
h,

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : l[0]? = l.getLast? → (l.dropLast.Nodup ↔ l.tail.Nodup)
hl : ¬l = []
h : a = l[l.length - 1]
⊢ (l[l.length - 1] :: l.dropLast).Nodup ↔ l.Nodup
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : 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₁

Tactic:
rel_add_left

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

Goal state before:
pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ (map ?f s).card = 1

pp: case f
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ α → ?m.41

pp: α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ Type ?u.34

Tactic:
h,

Goal state after:
α : Type u_1
β : Type v
f : α → β
s : Multiset α
b : β
h : map f s = {b}
⊢ {b}.card = 1
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ l.dedup.tail = l'

Tactic:
h,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
⊢ (a :: l').tail = l'
Module: Mathlib.Data.List.Dedup

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a l.dedup ≤ 1
⊢ False

Tactic:
h,

Goal state after:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
l : List α
a : α
l' : List α
h : l.dedup = a :: l'
ha : a ∈ l'
this✝ : 0 < count a l'
this : count a (a :: l') ≤ 1
⊢ False
Module: Mathlib.Data.List.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ l₃ : List α
h : l₂ <+ l₃
⊢ l₁ ∩ l₂ <+ l₁ ∩ l₃

Tactic:
grind [inter_def, monotone_filter_right]

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

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

Tactic:
exact ih.trans <| Sublist.inter_left (by grind [erase_sublist])

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
⊢ s + (t ∪ u) = s + t ∪ (s + u)

Tactic:
rw [Multiset.add_comm, union_add_distrib, s.add_comm, s.add_comm]

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

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

Tactic:
by
  apply List.perm_of_nodup_nodup_toFinset_eq (nodup_toList _) hs
  rw [toList_toFinset]

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

Goal state before:
pp: α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ l₁ = take l₁.length l₂

Tactic:
h,

Goal state after:
α : Type u_1
l₁ l₂ l₃ : List α
h✝ : l₁.length ≤ l₂.length
h : l₁ = take l₁.length (l₂ ++ l₃)
⊢ take l₁.length (l₂ ++ l₃) = take l₁.length l₂
Module: Mathlib.Data.Finset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
⊢ (s.erase a).Nonempty ↔ s.Nontrivial

Tactic:
by
  simp only [Finset.Nonempty, mem_erase, and_comm (b := _ ∈ _)]
  refine ⟨?_, fun hs ↦ hs.exists_ne a⟩
  rintro ⟨b, hb, hba⟩
  exact ⟨_, hb, _, ha, hba⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x : α
⊢ insert x {x}ᶜ = univ

Tactic:
rw [← compl_erase, erase_singleton, compl_empty]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Fintype ↑s
⊢ s.toFinset.Nonempty ↔ s.Nonempty

Tactic:
rw [← Finset.coe_nonempty, coe_toFinset]

Goal state after:
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ ↑s.toFinset = t

Tactic:
h,

Goal state after:
α : Type u_1
s t : Set α
inst✝¹ : Fintype ↑s
inst✝ : Fintype ↑t
h : s.toFinset = t.toFinset
⊢ ↑t.toFinset = t
Module: Mathlib.Data.Fintype.Sets

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
s : Set α
inst✝¹ : Fintype ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ {x | x ∈ s} = s.toFinset

Tactic:
ext
  rw [mem_filter_univ, mem_toFinset]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
⊢ Set.SurjOn f ↑s ↑t ↔ t ⊆ image f s

Tactic:
simp only [Set.SurjOn]
  norm_cast

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

Goal state before:
pp: case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = i.rev.rev.castPred ⋯

Tactic:
predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)),

Goal state after:
case inl
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ i.castPred ⋯ = i.rev.rev.castPred ⋯
Module: Mathlib.Order.Fin.Basic

Goal state before:
pp: case inr.inl
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
h✝ : j ≤ i
h : j < i
⊢ i = j

pp: case inr.inr
n : ℕ
j : Fin (n + 1)
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
hij : j.predAbove = j.predAbove
h : j ≤ j
⊢ j = j

Tactic:
· exact (this hij.symm h).symm

Goal state after:
case inr.inr
n : ℕ
j : Fin (n + 1)
this : ∀ ⦃i j : Fin (n + 1)⦄, i.predAbove = j.predAbove → i < j → i = j
hij : j.predAbove = j.predAbove
h : j ≤ j
⊢ j = j
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
k : Fin n
h : k ≤ 0
⊢ ↑k = ↑0

Tactic:
rw [Nat.eq_zero_of_le_zero h]; rfl

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

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

Tactic:
h,

Goal state after:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ j.castSucc.castPred ⋯ = j
Module: Mathlib.Data.Fin.Basic

Goal state before:
pp: case mpr
n : ℕ
α : Type u_1
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
⊢ (∀ (i : Fin n), r (f i.castSucc) (f i.succ)) → ((fun x1 x2 ↦ x1 < x2) ⇒ r) f f

Tactic:
· refine fun H i => Fin.induction (fun h ↦ ?_) ?_
    · simp at h
    · intro j ihj hij
      rw [← le_castSucc_iff] at hij
      obtain hij | hij := (le_def.1 hij).eq_or_lt
      · obtain rfl := Fin.ext hij
        exact H _
      · exact _root_.trans (ihj hij) (H j)

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

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

Tactic:
rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]

Goal state after:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc
Module: Mathlib.Data.Finset.Card

Goal state before:
pp: α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∀ k < #t, n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k

Tactic:
intro k

Goal state after:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
⊢ k < #t → n ≤ k → (∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ u, s ⊆ u ∧ u ⊆ t ∧ #u = k
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
⊢ P (f n)

Tactic:
have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2

Goal state after:
case h
α : Type u_4
P : α → Prop
r : α → α → Prop
this : Nonempty α
F : Finset α → α
hF : ∀ (s : Finset α), (∀ x ∈ s, P x) → P (F s) ∧ ∀ x ∈ s, r x (F s)
h' : ∀ (s : Finset α), ∃ y, (∀ x ∈ s, P x) → P y ∧ ∀ x ∈ s, r x y
f : ℕ → α := seqOfForallFinsetExistsAux P r h'
hf : f = seqOfForallFinsetExistsAux P r h'
n : ℕ
IH : ∀ m < n, P (f m)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (f n)
Module: Mathlib.Data.Fin.Tuple.Basic

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

Tactic:
rw [append_right]

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

Goal state before:
pp: 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))

Tactic:
rw [append_right]

Goal state after:
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
⊢ c r = append a (append b c) (Fin.cast ⋯ (natAdd (m + n) r))
Module: Mathlib.Data.Fintype.Card

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ Set.range Subtype.val

Tactic:
Subtype.range_coe_subtype

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : Fintype { a // p a }
x : α
hx : ¬p x
⊢ x ∉ {x | p x}
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
h : Fintype.card α ≤ Fintype.card β
⊢ Nonempty (α ↪ β)

Tactic:
classical exact (truncOfCardLE h).nonempty

Goal state after:
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ natEmbeddingAux α m = Classical.choose ⋯

Tactic:
h,

Goal state after:
α : Type u_4
inst✝ : Infinite α
this : DecidableEq α := Classical.decEq α
m n : ℕ
h : natEmbeddingAux α m = natEmbeddingAux α n
hmlen : m ≤ n
hmn✝ : ¬m = n
hmn : m < n
⊢ natEmbeddingAux α n = Classical.choose ⋯
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
β : Sort u_2
x : β
p : Fin (n + 1) → β
i : Fin (n + 1)
x✝ : Fin n
⊢ (cons x p ∘ i.succ.succAbove) x✝.succ = cons x (i.removeNth p) x✝.succ

Tactic:
by simp [removeNth]

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

Goal state before:
pp: α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ op a (fold op (op b₁ b₂) (s₁ + b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))

Tactic:
h,

Goal state after:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
b₁ b₂ : α
s₁ s₂ : Multiset α
a : α
b : Multiset α
h : fold op (op b₁ b₂) (s₁ + b) = op (fold op b₁ s₁) (fold op b₂ b)
⊢ op a (op (fold op b₁ s₁) (fold op b₂ b)) = op (fold op b₁ s₁) (op a (fold op b₂ b))
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (op (f a) (g a)) (fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b)) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))

Tactic:
h,

Goal state after:
α : Type u_1
β : Type u_2
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
f g : β → α
u₁ u₂ : α
s : Multiset β
a : β
b : Multiset β
h : fold op (op u₁ u₂) (map (fun x ↦ op (f x) (g x)) b) = op (fold op u₁ (map f b)) (fold op u₂ (map g b))
⊢ op (op (f a) (g a)) (op (fold op u₁ (map f b)) (fold op u₂ (map g b))) =
    op (fold op u₁ (map f (a ::ₘ b))) (fold op u₂ (map g (a ::ₘ b)))
Module: Mathlib.Data.Multiset.Fold

Goal state before:
pp: case neg
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : ¬a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

pp: case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
· simp [IH, h]

Goal state after:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)
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:
by simpa using _root_.trans (by simpa using h₁) (by simpa using h₂)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise rb (map (⇑e) l) ↔ List.Pairwise ra l

Tactic:
by
  simp [pairwise_map, e.map_rel_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ List.Pairwise (Function.swap rb) (map (⇑e) l) ↔ List.Pairwise (Function.swap ra) l

Tactic:
by
  simp [pairwise_map, e.map_rel_iff]

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

Goal state before:
pp: n : ℕ
p : Fin n → Bool
h : ∃ i, p i = true
⊢ (if h : ∃ i, p i = true then some (Fin.find (fun x ↦ p x = true) h) else none) =
    some (Fin.find (fun x ↦ p x = true) h)

Tactic:
h,

Goal state after:
n : ℕ
p : Fin n → Bool
h : ∃ i, p i = true
⊢ (if h_1 : True then some (Fin.find (fun x ↦ p x = true) ⋯) else none) = some (Fin.find (fun x ↦ p x = true) h)
Module: Mathlib.Data.List.Rotate

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (l.rotate' (n % l.length)).rotate' ((l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n

Tactic:
rotate'_rotate',

Goal state after:
α : Type u
l : List α
n : ℕ
⊢ l.rotate' (n % l.length + (l.rotate' (n % l.length)).length * (n / l.length)) = l.rotate' n