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

Goal state before:
pp: case pos
α : Type u
inst✝ : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x✝¹ : ι × ι
i j : ι
x✝ : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
hij : i = j
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i

Tactic:
exact le_iSup₂_of_le i ⟨his, hij ▸ hjs⟩ inf_le_left

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

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

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ico (e x) (e y) = Ico x y

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ioc (e x) (e y) = Ioc x y

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ioo (e x) (e y) = Ioo x y

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
S : Set ↑(Icc a b)
hS : ¬S = ∅
⊢ sSup (Subtype.val '' S) ∈ Icc a b

Tactic:
by
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS
    refine ⟨?_, csSup_le (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.2)⟩
    obtain ⟨c, hc⟩ := hS
    exact c.2.1.trans (le_csSup ⟨b, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.2⟩ ⟨c, hc, rfl⟩)

Goal state after:
Module: Mathlib.Algebra.Notation.Support

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : One M
f : ι → M
s : Set ι
⊢ mulSupport f = s ↔ (∀ (x : ι), x ∈ s → f x ≠ 1) ∧ ∀ (x : ι), ¬x ∈ s → f x = 1

Tactic:
by
  simp +contextual only [Set.ext_iff, mem_mulSupport, ne_eq, iff_def,
    not_imp_comm, and_comm, forall_and]

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

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

Tactic:
descFactorial_one,

Goal state after:
n : ℕ
⊢ n + 1 = (n + 1) * 1
Module: Mathlib.Algebra.Order.Hom.Basic

Goal state before:
pp: F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹ * y) = f (x * y⁻¹)

Tactic:
← map_inv_eq_map,

Goal state after:
F : Type u_2
β : Type u_4
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
f : F
α : Type u_7
inst✝² : FunLike F α β
inst✝¹ : CommGroup α
inst✝ : GroupSeminormClass F α β
x y : α
⊢ f (x⁻¹ * y)⁻¹ = f (x * y⁻¹)
Module: Mathlib.Data.Nat.Factorial.Basic

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

Tactic:
show n - m = (n - k) - (m - k) by lia,

Goal state after:
case pos
k m n : ℕ
hkm : k ≤ m
hmn : m ≤ n
⊢ (n - k - (m - k))! * ((n - k).descFactorial (m - k) * n.descFactorial k) = n !
Module: Mathlib.Data.PNat.Basic

Goal state before:
pp: n : ℕ+
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
⊢ (n + 1).recOn one succ = succ n (n.recOn one succ)

Tactic:
obtain ⟨n, h⟩ := n

Goal state after:
p : ℕ+ → Sort u_1
one : p 1
succ : (n : ℕ+) → p n → p (n + 1)
n : ℕ
h : 0 < n
⊢ (⟨n, h⟩ + 1).recOn one succ = succ ⟨n, h⟩ (recOn ⟨n, h⟩ one succ)
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
⊢ (0 ≤ b ∧ b < 1 ∧ ∃ z, a - b = ↑z) → fract a = b

Tactic:
rintro ⟨h₀, h₁, z, hz⟩
    rw [← self_sub_floor, eq_comm, eq_sub_iff_add_eq, add_comm, ← eq_sub_iff_add_eq, hz]
    refine congrArg Int.cast ?_
    rw [floor_eq_iff, ← hz]
    constructor <;> simpa [sub_eq_add_neg, add_assoc]

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

Goal state before:
pp: n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.Coprime n
⊢ (↑n % ↑d).natAbs.Coprime d

Tactic:
Nat.Coprime,

Goal state after:
n d : ℕ
n_coprime_d : n.Coprime d
this✝ : ↑n % ↑d = ↑n - ↑d * ⌊↑n / ↑d⌋
this : d.gcd n = 1
⊢ (↑n % ↑d).natAbs.Coprime d
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:
by rwa [← div_lt_iff₀']; positivity

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

Goal state before:
pp: case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ ↑⌈a⌉₊ < a + 1

Tactic:
ceil_eq_zero.mpr h.le,

Goal state after:
case neg
R : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : FloorRing R
inst✝ : IsStrictOrderedRing R
a : R
ha : -1 < a
h : a < 0
⊢ ↑0 < a + 1
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: G : Type u_1
M : Type u_2
A : Type u_3
B : Type u_4
α : Type u_5
β : Type u_6
inst✝⁴ : Monoid M
inst✝³ : Monoid A
inst✝² : MulDistribMulAction M A
inst✝¹ : Monoid B
inst✝ : SMul M B
f : B →* A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
x y : B
⊢ f (c • (x * y)) = f (c • x * c • y)

Tactic:
simp only [smul, f.map_mul, smul_mul']

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

Goal state before:
pp: case mk.mk.mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
c✝ : Multiset α
l₃ : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₂) →
    Multiset.Le (Quot.mk (⇑(isSetoid α)) l₂) (Quot.mk (⇑(isSetoid α)) l₃) →
      Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₃)

Tactic:
exact @Subperm.trans _ _ _ _

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

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

Tactic:
simp only [ih, cons_add, rel_cons_left]
      constructor
      · intro h
        rcases h with ⟨b, bs', hab, h, rfl⟩
        rcases h with ⟨bs₀, bs₁, h₀, h₁, rfl⟩
        exact ⟨b ::ₘ bs₀, bs₁, ⟨b, bs₀, hab, h₀, rfl⟩, h₁, by simp⟩
      · intro h
        rcases h with ⟨bs₀, bs₁, h, h₁, rfl⟩
        rcases h with ⟨b, bs, hab, h₀, rfl⟩
        exact ⟨b, bs + bs₁, hab, ⟨bs, bs₁, h₀, h₁, rfl⟩, by simp⟩

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ ↑s.attach = Set.univ

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
h : xs ⊆ ys
⊢ (xs ++ ys).dedup = ys.dedup

Tactic:
rw [List.dedup_append, Subset.union_eq_right (List.Subset.trans h <| subset_dedup _)]

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

Goal state before:
pp: case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ (a : α), a ∈ s' → P a
⊢ False

Tactic:
have card := card_le_card (monotone_filter_left P hs') |>.trans H

Goal state after:
case mp
α : Type u_1
s : Multiset α
P : α → Prop
inst✝ : DecidablePred P
n : ℕ
H : (filter P s).card ≤ n
s' : Multiset α
hs' : s' ≤ s
s'_card : n < s'.card
rid : ∀ (a : α), a ∈ s' → P a
card : (filter P s').card ≤ n
⊢ False
Module: Mathlib.Data.Multiset.UnionInter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : List α
⊢ ↑s ∩ ↑t = ↑(s.bagInter t)

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
d : s.Nodup
⊢ (s ∩ t).Nodup

Tactic:
rw [← ndinter_eq_inter d]
  exact d.filter _

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

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ True
s : Finset α
⊢ filter (fun x ↦ True) s = s

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
h : DecidablePred fun x ↦ False
s : Finset α
⊢ filter (fun x ↦ False) s = ∅

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
⊢ ↑univ = Set.univ

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
this : b ∈ s.erase a
⊢ ∃ t a, ∃ (ha : a ∉ t), ∃ b, ∃ (hb : b ∉ t) (hab : ¬a = b), cons a (cons b t hb) ⋯ = s

Tactic:
refine ⟨(s.erase a).erase b, a, ?_, b, ?_, ?_, ?_⟩ <;> simp [insert_erase ha, *]

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

Goal state before:
pp: m n : ℕ
⊢ range m ∩ range n = range (min m n)

Tactic:
by ext; simp

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

Goal state before:
pp: m n : ℕ
⊢ range m ∪ range n = range (max m n)

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α ↪ β
a : α
s : Finset α
⊢ map f (insert a s) = insert (f a) (map f s)

Tactic:
simp only [insert_eq, map_union, map_singleton]

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

Goal state before:
pp: n : ℕ
h : n = n
⊢ castOrderIso h = OrderIso.refl (Fin n)

Tactic:
by ext; simp

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

Goal state before:
pp: case h.refine_2
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), ↑(e ⟨m_1, hi⟩) = m_1
hi : i < n
j : ℕ
hj : j < i
⊢ j < ↑(e ⟨i, hi⟩)

Tactic:
rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ ↑n = 0

Tactic:
by ext; simp

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

Goal state before:
pp: n : ℕ
⊢ ↑n = last n

Tactic:
by ext; simp

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

Goal state before:
pp: n : ℕ
h : n = n
⊢ finCongr h = Equiv.refl (Fin n)

Tactic:
by ext; simp

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

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < b ↔ a ≤ b

Tactic:
pred_lt_iff,

Goal state after:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc < b.succ ↔ a ≤ b
Module: Mathlib.Data.Fin.SuccPred

Goal state before:
pp: n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b ≤ (a.pred ha).castSucc ↔ b < a

Tactic:
by
  rw [castSucc_pred_eq_pred_castSucc, le_pred_castSucc_iff]

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

Goal state before:
pp: n : ℕ
j : Fin n
this : succAbove 1 j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
zero_succAbove

Goal state after:
n : ℕ
j : Fin n
this : succAbove 1 j.succ = j.succ.succ
⊢ succAbove 1 j.succ = j.succ.succ
Module: Mathlib.Data.List.FinRange

Goal state before:
pp: n : ℕ
σ : Perm (Fin n)
⊢ ∀ (a : Fin n), a ∈ map (⇑σ) (finRange n) ↔ a ∈ finRange n

Tactic:
simpa [mem_map, mem_finRange] using! σ.surjective

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
⊢ cons x (update p i y) = update (cons x p) i.succ y

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
y : α i.succ
j : Fin (n + 1)
⊢ cons x (update p i y) j = update (cons x p) i.succ y j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z = cons z p

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
⊢ cons (q 0) (tail q) = q

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ cons (q 0) (tail q) j = q j
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)
IH' : ∀ (x : Fin n), P (f ↑x)
⊢ P (seqOfForallFinsetExistsAux P r h' n)

Tactic:
seqOfForallFinsetExistsAux

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 (Classical.choose ⋯)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: case refine_2
n : ℕ
α : Type u_1
x₀ : α
x : Fin n → α
h : Injective (cons x₀ x)
⊢ Injective x

Tactic:
· simpa [Function.comp] using! h.comp (Fin.succ_injective _)

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
⊢ tail (update q 0 z) = tail q

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
z : α 0
j : Fin n
⊢ tail (update q 0 z) j = tail q j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
⊢ tail (update q i.succ y) = update (tail q) i y

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.succ
j : Fin n
⊢ tail (update q i.succ y) j = update (tail q) i y j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
⊢ g ∘ cons y q = cons (g y) (g ∘ q)

Tactic:
ext j

Goal state after:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
y : α
q : Fin n → α
j : Fin (n + 1)
⊢ (g ∘ cons y q) j = cons (g y) (g ∘ q) j
Module: Mathlib.Data.Fintype.Basic

Goal state before:
pp: α : 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'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (seqOfForallFinsetExistsAux P r h' n)

Tactic:
seqOfForallFinsetExistsAux

Goal state after:
α : 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'
A : ∀ (n : ℕ), P (f n)
m n : ℕ
hmn : m < n
⊢ r (f m) (Classical.choose ⋯)
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
⊢ g ∘ tail q = tail (g ∘ q)

Tactic:
ext j

Goal state after:
n : ℕ
α : Sort u_1
β : Sort u_2
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ tail q) j = tail (g ∘ q) j
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
y : α i.castSucc
⊢ snoc (update p i y) x = update (snoc p x) i.castSucc y

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (i : Fin n) → α i.castSucc
i : Fin n
y : α i.castSucc
j : Fin (n + 1)
⊢ snoc (update p i y) x j = update (snoc p x) i.castSucc y j
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
z : α (last n)
⊢ update (snoc p x) (last n) z = snoc p z

Tactic:
ext j

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

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

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
j : Fin (n + 1)
⊢ snoc (init q) (q (last n)) j = q j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
⊢ init (update q (last n) z) = init q

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
z : α (last n)
j : Fin n
⊢ init (update q (last n) z) j = init q j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
⊢ init (update q i.castSucc y) = update (init q) i y

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
q : (i : Fin (n + 1)) → α i
i : Fin n
y : α i.castSucc
j : Fin n
⊢ init (update q i.castSucc y) j = update (init q) i y j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
⊢ g ∘ snoc q y = snoc (g ∘ q) (g y)

Tactic:
ext j

Goal state after:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n → α
y : α
j : Fin (n + 1)
⊢ (g ∘ snoc q y) j = snoc (g ∘ q) (g y) j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
⊢ g ∘ init q = init (g ∘ q)

Tactic:
ext j

Goal state after:
n : ℕ
α : Sort u_2
β : Sort u_3
g : α → β
q : Fin n.succ → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j
Module: Mathlib.Data.Fintype.EquivFin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
n : ℕ
i : Infinite ι
s : Finset ι
w : n + 1 ≤ n
c : #s = n + 1
⊢ False

Tactic:
exact Nat.not_succ_le_self n w

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
⊢ p = removeNth 0 (cons x fun j ↦ cast ⋯ (p j))

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α 0
p : (j : Fin n) → α (succAbove 0 j)
j : Fin n
⊢ p j = removeNth 0 (cons x fun j ↦ cast ⋯ (p j)) j
Module: Mathlib.Data.List.NodupEquivFin

Goal state before:
pp: α : Type u_1
l : List α
x : α
⊢ replicate 2 x <+ l ↔ ∃ n m x_1, x = l.get n ∧ x = l.get m

Tactic:
sublist_iff_exists_fin_orderEmbedding_get_eq

Goal state after:
α : Type u_1
l : List α
x : α
⊢ (∃ f, ∀ (ix : Fin (replicate 2 x).length), (replicate 2 x).get ix = l.get (f ix)) ↔
    ∃ n m x_1, x = l.get n ∧ x = l.get m
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
⊢ p = (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x)

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
x : α (last n)
p : (j : Fin n) → α ((last n).succAbove j)
j : Fin n
⊢ p j = (last n).removeNth (snoc (fun j ↦ cast ⋯ (p j)) x) j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
⊢ i.succ.insertNth x (cons a p) = cons a (i.insertNth x p)

Tactic:
ext j

Goal state after:
n : ℕ
α : Sort u_3
i : Fin (n + 1)
x a : α
p : Fin n → α
j : Fin (n + 1 + 1)
⊢ i.succ.insertNth x (cons a p) j = cons a (i.insertNth x p) j
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ (range f).Finite ↔ Finite α

Tactic:
by
  simpa [finite_univ_iff] using finite_image_iff (s := univ) hf.injOn

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
⊢ p.removeNth (update f (p.succAbove i) x) = update (p.removeNth f) i x

Tactic:
ext j

Goal state after:
n : ℕ
α : Fin (n + 1) → Sort u_1
p : Fin (n + 1)
i : Fin n
x : α (p.succAbove i)
f : (j : Fin (n + 1)) → α j
j : Fin n
⊢ p.removeNth (update f (p.succAbove i) x) j = update (p.removeNth f) i x j
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
α : Type u_3
⊢ insertNthEquiv (fun x ↦ α) (last n) = snocEquiv fun x ↦ α

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
g : α → β
H : ∀ x ∈ s, f x = g x
⊢ fold op b f s = fold op b g s

Tactic:
rw [fold, fold, map_congr rfl H]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ fold op' (m b) (fun x ↦ m (f x)) s = m (fold op b f s)

Tactic:
rw [fold, fold, ← Multiset.fold_hom op hm, Multiset.map_map]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s : Finset α
op' : γ → γ → γ
inst✝¹ : Std.Commutative op'
inst✝ : Std.Associative op'
m : β → γ
hm : ∀ (x y : β), m (op x y) = op' (m x) (m y)
⊢ Multiset.fold op' (m b) (Multiset.map (fun x ↦ m (f x)) s.val) = Multiset.fold op' (m b) (Multiset.map (m ∘ f) s.val)
Module: Mathlib.Data.Set.Finite.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq β
f : α → β
s : Set α
t : Finset β
hfs : SurjOn f s ↑t
u : Set α
hus : u ⊆ s
hf : InjOn f u
himg : f '' u = ↑t
⊢ image f ⋯.toFinset = t

Tactic:
simpa [← Finset.coe_inj]

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

Goal state before:
pp: case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
⊢ fold op b (fun i ↦ if p i then f i else g i) (insert x s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))

Tactic:
simp only [Finset.fold_insert hx]

Goal state after:
case insert
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
s✝ : Finset α
g : α → β
hb : op b b = b
p : α → Prop
inst✝ : DecidablePred p
x : α
s : Finset α
hx : x ∉ s
IH : fold op b (fun i ↦ if p i then f i else g i) s = op (fold op b f (filter p s)) (fold op b g ({i ∈ s | ¬p i}))
⊢ op (if p x then f x else g x) (fold op b (fun i ↦ if p i then f i else g i) s) =
    op (fold op b f (filter p (insert x s))) (fold op b g ({i ∈ insert x s | ¬p i}))
Module: Mathlib.Data.Fin.Tuple.Basic

Goal state before:
pp: n : ℕ
p : Fin n → Prop
inst✝ : DecidablePred p
⊢ (find? fun x ↦ decide (p x)) = if h : ∃ i, p i then some (Fin.find p h) else none

Tactic:
simp_rw [find?_eq_dite, decide_eq_true_eq]

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

Goal state before:
pp: r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 ∧ IsChain r (0 :: map succ (range n)) ↔ r a 0 ∧ ∀ (m : ℕ), m < n → r m m.succ

Tactic:
and_congr_right_iff,

Goal state after:
r : ℕ → ℕ → Prop
n a : ℕ
⊢ r a 0 → (IsChain r (0 :: map succ (range n)) ↔ ∀ (m : ℕ), m < n → r m m.succ)