mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ (∃ u, (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y) ↔
    ∃ u, (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y

Tactic:
apply exists_iff_exists_of_mono F (f' rr _ _) (g' rr _ _)

Goal state after:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ f' rr n α ⊚ g' rr n α = TypeVec.id

case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ (fun i t ↦ (↑t).1) = fun i x ↦ (↑(f' rr n α i x)).1

Tactic:
ext i ⟨x, _⟩

Goal state after:
case h₁.e_a.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α i ⟨x, property✝⟩)).1
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_b.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ (fun i t ↦ (↑t).2) = fun i x ↦ (↑(f' rr n α i x)).2

Tactic:
ext i ⟨x, _⟩

Goal state after:
case h₁.e_b.e_a.e_a
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x✝ y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α i ⟨x, property✝⟩)).2
Module: Mathlib.Data.TypeVec

Goal state before:
pp: ⊢ ∀ {n : ℕ} {α β : TypeVec.{u} n}, (id ⊗' id) = id

Tactic:
intros
  ext i a
  induction i with
  | fz => cases a; rfl
  | fs _ i_ih => apply i_ih

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ toMultiset f < toMultiset g ↔ f < g

Tactic:
← Multiset.toDFinsupp_lt_toDFinsupp,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ Multiset.toDFinsupp (toMultiset f) < Multiset.toDFinsupp (toMultiset g) ↔ f < g
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
C : AList β → Sort u_1
H0 : C ∅
IH : (a : α) → (b : β a) → (l : AList β) → ¬a ∈ l → C l → C (insert a b l)
c : Sigma β
l : List (Sigma β)
h : (c :: l).NodupKeys
⊢ ¬c.fst ∈ { entries := l, nodupKeys := ⋯ }

Tactic:
exact notMem_keys_of_nodupKeys_cons h

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
x✝ : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), ((s, f).2 i).isSome = true ↔ i ∈ (s, f).1
⊢ (fun s ↦ ⟨(s.keys, fun i ↦ lookup i s), ⋯⟩)
      ((fun f ↦ { entries := ((↑f).1.sigma fun i ↦ ((↑f).2 i).toFinset).val, nodupKeys := ⋯ }) ⟨(s, f), hf⟩) =
    ⟨(s, f), hf⟩

Tactic:
dsimp only at hf
    ext
    · simp [keys, Multiset.keys, ← hf, Option.isSome_iff_exists]
    · simp +contextual [lookup_eq_some_iff, ← hf]

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case none
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
⊢ none.getD 0 = x ↔ x ∈ none

Tactic:
simp [hx.symm]

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: case some
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x ↦ M
a : α
x : M
hx : x ≠ 0
m : M
⊢ (some m).getD 0 = x ↔ x ∈ some m

Tactic:
simp [hx.symm]

Goal state after:
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ (singleton a m).lookupFinsupp = Finsupp.single a m

Tactic:
simp [← AList.insert_empty]

Goal state after:
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case ofNat.negSucc
m n : ℕ
⊢ bitwise or (ofNat m) -[n+1] = (ofNat m).lor -[n+1]

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Goal state after:
case ofNat.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(x || !y)) m n = Nat.bitwise (fun a b ↦ a && !b) n m
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.ofNat
m n : ℕ
⊢ bitwise or -[m+1] (ofNat n) = -[m+1].lor (ofNat n)

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || y)) m n = Nat.bitwise (fun a b ↦ a && !b) m n
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: case negSucc.negSucc
m n : ℕ
⊢ bitwise or -[m+1] -[n+1] = -[m+1].lor -[n+1]

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.or_true, cond_true, lor, Nat.ldiff,
      negSucc.injEq, Bool.true_or]

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ Nat.bitwise (fun x y ↦ !(!x || !y)) m n = m &&& n
Module: Mathlib.Data.LawfulXor.Basic

Goal state before:
pp: α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = a ^^^ a ↔ b = 0

Tactic:
xor_self a

Goal state after:
α : Type u_1
inst✝² : XorOp α
inst✝¹ : Zero α
inst✝ : LawfulXor α
a b : α
⊢ b = 0 ↔ b = 0
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ ¬p (dropWhile p tl)[0] = true

Tactic:
apply IH

Goal state after:
case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
hl : 0 < (dropWhile p (hd :: tl)).length
hp✝ : p hd = true
IH : ∀ (hl : 0 < (dropWhile p tl).length), ¬p (dropWhile p tl)[0] = true
hp : p hd = true
⊢ 0 < (dropWhile p tl).length
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case cons
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx : x ∈ takeWhile p (hd :: tl)
⊢ p x = true

Tactic:
simp [takeWhile] at hx

Goal state after:
case cons
α : Type u_1
p : α → Bool
l : List α
x hd : α
tl : List α
IH : x ∈ takeWhile p tl → p x = true
hx :
  x ∈
    match p hd with
    | true => hd :: takeWhile p tl
    | false => []
⊢ p x = true
Module: Mathlib.Data.List.TakeWhile

Goal state before:
pp: case nil
α : Type u_1
p : α → Bool
l : List α
x : α
hx : x ∈ takeWhile p []
⊢ p x = true

Tactic:
simp [takeWhile] at hx

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

Goal state before:
pp: n : ℕ
⊢ range' n (n + 1 - n) = [n]

Tactic:
simp [Nat.add_sub_cancel_left]

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

Goal state before:
pp: α : Type u_1
f : α → α
a : α
tl : List α
r : Array α
⊢ go f (tl ++ [a]) r = r.toListAppend (go f (tl ++ [a]) #[])

Tactic:
cases tl with

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

Goal state before:
pp: case cons
α : Type u_1
f : α → α
l₁ : List α
hd : α
tl : List α
x✝ : hd :: tl ≠ []
⊢ modifyLast f (l₁ ++ hd :: tl) = l₁ ++ modifyLast f (hd :: tl)

Tactic:
cases tl with

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_4
f : α → σ → σ × β
a : α
as : List α
s : σ
⊢ mapAccumr f (a :: as) s =
    foldr
      (fun a s ↦
        let r := f a s.1;
        (r.1, r.2 :: s.2))
      (s, []) (a :: as)

Tactic:
simp only [mapAccumr, foldr, mapAccumr_eq_foldr f as]

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

Goal state before:
pp: α : Type u_1
head : ℕ
tail : List ℕ
ih : ∀ (l : List α), l.length ≤ tail.sum → (tail.splitLengths l).flatten = l
l : List α
h : l.length ≤ (head :: tail).sum
⊢ ((head :: tail).splitLengths l).flatten = l

Tactic:
simp only [splitLengths_cons, flatten_cons]
    rw [ih, take_append_drop]
    simpa [add_comm] using h

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

Goal state before:
pp: case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l b [] ((a :: g).reverse :: gs))

Tactic:
apply IH

Goal state after:
case h_2.hgs'
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ ¬[] ∈ (a :: g).reverse :: gs

case h_2.hgs
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) ((a :: g).reverse :: gs)

case h_2.hga
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
          IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r l a g gs)
a : α
g : List α
gs : List (List α)
hgs' : ¬[] ∈ gs
hgs : IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs
hga : ∀ (m : List α), m ∈ gs.head? → ∃ ha hb, r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false
x✝ : Bool
heq✝ : r a b = false
⊢ ∀ (m : List α), m ∈ ((a :: g).reverse :: gs).head? → ∃ ha hb, r (m.getLast ha) (([].reverse ++ [b]).head hb) = false
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: case mpr
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : Semiring R
inst✝³ : Semiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
a : Matrix m n A
inst✝ : Nonempty l
h : a = 0
⊢ mulRightLinearMap l R 0 = 0

Tactic:
exact mulRightLinearMap_zero_eq_zero _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ mulRightLinearMap l R a ^ n * mulRightLinearMap l R a = mulRightLinearMap l R (a ^ (n + 1))

Tactic:
pow_succ',

Goal state after:
l : Type u_1
m : Type u_2
R : Type u_5
A : Type u_6
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
a : Matrix m m A
k n : ℕ
⊢ mulRightLinearMap l R a ^ n * mulRightLinearMap l R a = mulRightLinearMap l R (a * a ^ n)
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n = m
⊢ n.dist m = 0

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
h : n ≤ m
⊢ n.dist m = m - n

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ m ≤ n.dist m + n

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ m ≤ n + n.dist m

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n ≤ n.dist m + m

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n m : ℕ
⊢ n ≤ m + n.dist m

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n : ℕ
⊢ n.dist 0 = n

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: n : ℕ
⊢ dist 0 n = n

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
⊢ i.succ.dist j.succ = i.dist j

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Dist

Goal state before:
pp: i j : ℕ
h : i ≠ j
⊢ 0 < i.dist j

Tactic:
by unfold Nat.dist; lia

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌊/⌋ n

Tactic:
obtain rfl | rfl := h

Goal state after:
case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌊/⌋ 0

case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌊/⌋ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: case pos
n a : ℕ
h : n = 0 ∨ a = 0
⊢ factorization 0 = a.factorization ⌈/⌉ n

Tactic:
obtain rfl | rfl := h

Goal state after:
case pos.inl
a : ℕ
⊢ factorization 0 = a.factorization ⌈/⌉ 0

case pos.inr
n : ℕ
⊢ factorization 0 = factorization 0 ⌈/⌉ n
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: n a : ℕ
⊢ (n.ceilRoot a).factorization = a.factorization ⌈/⌉ n

Tactic:
rw [ceilRoot_def]
  split_ifs with h
  · obtain rfl | rfl := h <;> simp
  refine prod_pow_factorization_eq_self fun p hp ↦ ?_
  have : p.Prime ∧ p ∣ a ∧ ¬a = 0 := by simpa using support_ceilDiv_subset hp
  exact this.1

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ↑(n.choose k) ≡ ↑((n % p).choose (k % p) * (n / p).choose (k / p)) [ZMOD ↑p]

Tactic:
exact_mod_cast choose_modEq_choose_mod_mul_choose_div

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

Goal state before:
pp: o₁ o₂ : Ordering
⊢ (o₁.dthen fun x ↦ o₂) = o₁.then o₂

Tactic:
cases o₁

Goal state after:
case lt
o₂ : Ordering
⊢ (lt.dthen fun x ↦ o₂) = lt.then o₂

case eq
o₂ : Ordering
⊢ (eq.dthen fun x ↦ o₂) = eq.then o₂

case gt
o₂ : Ordering
⊢ (gt.dthen fun x ↦ o₂) = gt.then o₂
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.lt) = lt a b

Tactic:
simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right, and_true, reduceCtorEq]

Goal state after:
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
⊢ nth p n ≤ f n

Tactic:
by_cases! hn : (∀ hf : Set.Finite (Set.ofPred p), n < hf.toFinset.card)

Goal state after:
case pos
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n

case neg
p : ℕ → Prop
f : ℕ → ℕ
hmaps : Set.MapsTo f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : StrictMonoOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
hn : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ n
⊢ nth p n ≤ f n
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1

Tactic:
have : ((-1 + n + n : ℤ) : α) = (n + n + -1 : ℤ) := by simp [add_comm]

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
n : ZNum
this : ↑(-1 + ↑n + ↑n) = ↑(↑n + ↑n + -1)
⊢ -(↑(-n) + ↑(-n) + 1) = ↑n + ↑n - 1
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * r.size
r0 : r.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rw [r0] at mr₂

Goal state after:
case node.inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * 0
r0 : r.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x y : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑y) r o₂
s : ℕ
ml : Ordnode α
z : α
mr : Ordnode α
hm : Valid' (↑x) (Ordnode.node s ml z mr) ↑y
Hm : 0 < (Ordnode.node s ml z mr).size
l0 : 0 < l.size
mr₁ : ratio * r.size ≤ (Ordnode.node s ml z mr).size
lr₁ : delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size
lr₂ : 3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9
mr₂ : (Ordnode.node s ml z mr).size ≤ delta * 0
r0 : r.size = 0
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
cases not_le_of_gt Hm mr₂

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑a.pred' = ↑a - ↑1

Tactic:
← Num.cast_to_nat,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a : PosNum
⊢ ↑↑a.pred' = ↑a - ↑1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑b.pred' = ↑b - ↑1

Tactic:
← Num.cast_to_nat,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
b : PosNum
⊢ ↑↑b.pred' = ↑b - ↑1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑↑a + ↑↑b = ↑↑b + ↑↑a

Tactic:
← Int.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + ↑b) = ↑↑b + ↑↑a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + ↑b) = ↑↑b + ↑↑a

Tactic:
← Int.cast_add,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
a b : PosNum
⊢ ↑(↑a + ↑b) = ↑(↑b + ↑a)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case node
α : Type u_1
C : Ordnode α → Prop
H0 : C nil
H1 : ∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l : l✝.Sized → C l✝
t_ih_r : r✝.Sized → C r✝
hl : (node size✝ l✝ x✝ r✝).Sized
⊢ C (l✝.node' x✝ r✝)

Tactic:
exact H1 _ _ _ (t_ih_l hl.2.1) (t_ih_r hl.2.2)

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : ↑F F.M
n : ℕ
⊢ Agree (Approx.sMk x n.succ) (Approx.sMk x n.succ.succ)

Tactic:
constructor
    introv
    apply (x.2 i).consistent

Goal state after:
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x : F.M
⊢ Agree' n x x

Tactic:
induction n generalizing x with | zero => ?_ | succ _ n_ih => ?_ <;>
  induction x using PFunctor.M.casesOn' <;> constructor <;> try rfl
  intro; apply n_ih

Goal state after:
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n : PosNum
d : ZNum
⊢ ↑(↑d).natAbs - ↑(↑n.pred' % (↑d).natAbs + 1) = -↑n % ↑d

Tactic:
← Int.subNatNat_eq_coe,

Goal state after:
n : PosNum
d : ZNum
⊢ subNatNat (↑d).natAbs (↑n.pred' % (↑d).natAbs + 1) = -↑n % ↑d
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case f.f.cons
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
a' : F.A
i : F.B a'
hh : IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ iselect (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩) ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a', i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a', i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)

Tactic:
obtain rfl : a = a' := by rcases hh with hh | hh <;> cases isPath_cons hh <;> rfl

Goal state after:
case f.f.cons
F : PFunctor.{uA, uB}
R : F.M → F.M → Prop
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
bisim : IsBisimulation R
ps : List F.Idx
ps_ih :
  ∀ (a : F.A) (f f' : F.B a → F.M),
    R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩) →
      IsPath ps (M.mk ⟨a, f⟩) ∨ IsPath ps (M.mk ⟨a, f'⟩) →
        iselect ps (M.mk ⟨a, f⟩) = iselect ps (M.mk ⟨a, f'⟩) ∧
          ∃ a_1 f_1 f'_1,
            isubtree ps (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
              isubtree ps (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)
a : F.A
f f' : F.B a → F.M
h₀ : R (M.mk ⟨a, f⟩) (M.mk ⟨a, f'⟩)
i : F.B a
hh : IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) ∨ IsPath (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩)
⊢ iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = iselect (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) ∧
    ∃ a_1 f_1 f'_1,
      isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = M.mk ⟨a_1, f_1⟩ ∧
        isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f'⟩) = M.mk ⟨a_1, f'_1⟩ ∧ ∀ (i : F.B a_1), R (f_1 i) (f'_1 i)