mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
s₁ s₂ : List α
h : Shortlex r s₁ s₂
h2 : s₁.length = s₂.length ∧ Lex r s₁ s₂
⊢ Shortlex r s₁ (s₂ ++ [])

Tactic:
| nil =>

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

Goal state before:
pp: case inr.nil
α : Type u_1
r : α → α → Prop
t₁ t₂ : List α
h : Shortlex r t₁ t₂
h2 : t₁.length = t₂.length ∧ Lex r t₁ t₂
⊢ Shortlex r ([] ++ t₁) ([] ++ t₂)

Tactic:
| nil =>

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

Goal state before:
pp: case intro.intro.inr.nil
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
lt : Shortlex r [] (xa :: xb)
h2len : [].length = (xa :: xb).length
⊢ Acc (Shortlex r) []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
gs : List (List α)
⊢ splitBy.loop r [] a g gs = gs.reverse ++ splitBy.loop r [] a g []

Tactic:
| nil =>

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

Goal state before:
pp: case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = true
⊢ splitBy.loop r l b (a :: g) gs = gs.reverse ++ splitBy.loop r l b (a :: g) []

Tactic:
IH

Goal state after:
case h_1
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = true
⊢ gs.reverse ++ splitBy.loop r l b (a :: g) [] = gs.reverse ++ splitBy.loop r l b (a :: g) []
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 α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ splitBy.loop r l b [] ((a :: g).reverse :: gs) = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
IH

Goal state after:
case h_2
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
⊢ ((a :: g).reverse :: gs).reverse ++ splitBy.loop r l b [] [] = gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
| gs.reverse ++ splitBy.loop r l b [] [(a :: g).reverse]

Tactic:
IH

Goal state after:
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH : ∀ {a : α} {g : List α} (gs : List (List α)), splitBy.loop r l a g gs = gs.reverse ++ splitBy.loop r l a g []
a : α
g : List α
gs : List (List α)
x✝ : Bool
heq✝ : r a b = false
| gs.reverse ++ ([(a :: g).reverse].reverse ++ splitBy.loop r l b [] [])
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ (splitBy.loop r [] a g []).flatten = g.reverse ++ [a]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
a : α
g : List α
⊢ ¬[] ∈ splitBy.loop r [] a g []

Tactic:
| nil =>

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

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length + 1 = n.succ
⊢ Acc (Shortlex r) (head :: tail)

Tactic:
add_left_inj

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
⊢ Acc (Shortlex r) (head :: tail)
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
h : m ∈ splitBy.loop r [] a g []
⊢ IsChain (fun x y ↦ r x y = true) m

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
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
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy.loop r [] a g gs)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
⊢ IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (splitBy r [])

Tactic:
| nil =>

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

Goal state before:
pp: case nil.nil
α : Type u_1
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ [].head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r [] a g [] = (g.reverse ++ [a]) :: splitBy r []

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
g : List α
a : α
h : IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
ha : ∀ (x : α), x ∈ m.head? → r ([a].getLast ⋯) x = false
⊢ splitBy.loop r ([] ++ m) a g [] = (g.reverse ++ [a]) :: splitBy r m

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
hn : [] ≠ []
h : IsChain (fun x y ↦ r x y = true) []
⊢ splitBy r [] = [[]]

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
m : List α
r : α → α → Bool
hn : [] ≠ []
h : IsChain (fun x y ↦ r x y = true) []
ha : ∀ (x : α), x ∈ m.head? → r ([].getLast hn) x = false
⊢ splitBy r ([] ++ m) = [] :: splitBy r m

Tactic:
| nil =>

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

Goal state before:
pp: case nil
α : Type u_1
r : α → α → Bool
hn : ¬[] ∈ []
hc : ∀ (m : List α), m ∈ [] → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) []
⊢ splitBy r [].flatten = []

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(uIcc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, ((↑(count i t) - ↑(count i s)).natAbs + 1)

Tactic:
simp_rw [uIcc_eq, Finset.card_map, DFinsupp.card_uIcc, Nat.card_uIcc, Multiset.toDFinsupp_apply,
    toDFinsupp_support]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈r⌉₊ = ↑res

Tactic:
← hres,

Goal state after:
R : Type u_1
inst✝³ : Semifield R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : FloorSemiring R
r : R
n d : ℕ
h : IsNNRat r n d
res : ℕ
hres : ⌈↑n / ↑d⌉₊ = res
⊢ ⌈r⌉₊ = ↑⌈↑n / ↑d⌉₊
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
a b : ℕ
co : List.Pairwise Coprime []
⊢ a ≡ b [MOD [].prod] ↔ ∀ (i : Fin [].length), a ≡ b [MOD [].get i]

Tactic:
| nil =>

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

Goal state before:
pp: p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ (a + b).choose a

Tactic:
rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul,
    hp.dvd_factorial, hp.dvd_factorial] at h₁

Goal state after:
p a b : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ (a + b).choose a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ (a + b).choose a
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
ι : Type u_1
a b : ℕ
s : ι → ℕ
co : List.Pairwise (Coprime on s) []
⊢ a ≡ b [MOD (List.map s []).prod] ↔ ∀ i ∈ [], a ≡ b [MOD s i]

Tactic:
| nil =>

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

Goal state before:
pp: ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j hj

Goal state after:
ι : Type u_1
a b : ℕ
s : ι → ℕ
i : ι
l : List ι
ih : List.Pairwise (Coprime on s) l → (a ≡ b [MOD (List.map s l).prod] ↔ ∀ i ∈ l, a ≡ b [MOD s i])
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j hj

Goal state after:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
⊢ ∀ a_1 ∈ l, ↑k ≡ a a_1 [MOD s a_1]

Tactic:
intro j hj

Goal state after:
case property
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
this : (s i).Coprime (List.map s l).prod
ih : { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
k : { k // k ≡ a i [MOD s i] ∧ k ≡ ↑ih [MOD (List.map s l).prod] }
j : ι
hj : j ∈ l
⊢ ↑k ≡ a j [MOD s j]
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
ι : Type u_1
a s : ι → ℕ
co : List.Pairwise (Coprime on s) []
hs : ∀ i ∈ [], s i ≠ 0
⊢ ↑(chineseRemainderOfList a s [] co) < (List.map s []).prod

Tactic:
| nil =>

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j hj

Goal state after:
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
⊢ ∀ x ∈ l, ¬s x = 0

Tactic:
intro j hj

Goal state after:
case cons
ι : Type u_1
a s : ι → ℕ
i : ι
l : List ι
co : List.Pairwise (Coprime on s) (i :: l)
hs : ∀ i_1 ∈ i :: l, s i_1 ≠ 0
this : (s i).Coprime (List.map s l).prod
j : ι
hj : j ∈ l
⊢ ¬s j = 0
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: case nil
ι : Type u_1
a s : ι → ℕ
z : ℕ
co : List.Pairwise (Coprime on s) []
hz : ∀ i ∈ [], z ≡ a i [MOD s i]
⊢ z ≡ ↑(chineseRemainderOfList a s [] co) [MOD (List.map s []).prod]

Tactic:
| nil =>

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
⊢ ∀ a ∈ l, (s i).Coprime (s a)

Tactic:
intro j hj

Goal state after:
ι : Type u_1
a s : ι → ℕ
z : ℕ
i : ι
l : List ι
ih :
  ∀ (co : List.Pairwise (Coprime on s) l),
    (∀ i ∈ l, z ≡ a i [MOD s i]) → z ≡ ↑(chineseRemainderOfList a s l co) [MOD (List.map s l).prod]
co : List.Pairwise (Coprime on s) (i :: l)
hz : ∀ i_1 ∈ i :: l, z ≡ a i_1 [MOD s i_1]
j : ι
hj : j ∈ l
⊢ (s i).Coprime (s j)
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun a b ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib a + (map fib l).sum < fib a + fib (a - 1)

Tactic:
gcongr; exact sum_fib_lt hl.2 this

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

Goal state before:
pp: n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
⊢ IsPrimePow n

Tactic:
obtain ⟨q, hq, h⟩ := Nat.exists_prime_and_dvd hpn

Goal state after:
n : ℕ
hn : 1 < n
hpn : (Icc 1 (n - 1)).gcd n.choose ≠ 1
q : ℕ
hq : Nat.Prime q
h : q ∣ (Icc 1 (n - 1)).gcd n.choose
⊢ IsPrimePow n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
⊢ nth p n = sInf {x | p x ∧ ∀ k < n, nth p k < x}

Tactic:
by
  by_cases! hn : ∀ hf : (Set.ofPred p).Finite, n < #hf.toFinset
  · exact (isLeast_nth hn).csInf_eq.symm
  · rcases hn with ⟨hf, hn⟩
    rw [nth_of_card_le _ hn]
    refine ((congr_arg sInf <| Set.eq_empty_of_forall_notMem fun k hk => ?_).trans sInf_empty).symm
    rcases exists_lt_card_nth_eq hk.1 with ⟨k, hlt, rfl⟩
    exact (hk.2 _ ((hlt hf).trans_le hn)).false

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

Goal state before:
pp: p : ℕ → Prop
⊢ nth p 0 = sInf (Set.ofPred p)

Tactic:
by rw [nth_eq_sInf]; simp

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

Goal state before:
pp: case neg
n : PosNum
fuel : ℕ
ih : ∀ {k : PosNum}, (↑n).sqrt < fuel + ↑k.bit1 → ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
k : PosNum
h : (↑n).sqrt < fuel + 1 + ↑k.bit1
h✝¹ : ¬n < k.bit1 * k.bit1
h✝ : ¬k.bit1 ∣ n
⊢ ↑(n.minFacAux fuel k.succ) = (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
rw [ih] <;> [congr; convert! Nat.lt_succ_of_lt h using 1] <;>
      simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc,
        add_left_comm, ← one_add_one_eq_two]

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
a b c : ZNum
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑c → ↑a ≤ ↑c
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : ZNum
⊢ ↑a < ↑b ↔ ↑a ≤ ↑b ∧ ¬↑b ≤ ↑a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ a ≤ b → b ≤ a → a = b

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : ZNum
⊢ ↑a ≤ ↑b → ↑b ≤ ↑a → ↑a = ↑b
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ a ≤ b ∨ b ≤ a

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : ZNum
⊢ ↑a ≤ ↑b ∨ ↑b ≤ ↑a
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
⊢ ∀ (a b c : ZNum), a * (b + c) = a * b + a * c

Tactic:
transfer
      simp [mul_add]

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

Goal state before:
pp: α : Type u_1
a b c : ZNum
⊢ a ≤ b → a + c ≤ b + c

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b c : ZNum
⊢ ↑a ≤ ↑b → ↑a + ↑c ≤ ↑b + ↑c
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: α : Type u_1
a b : ZNum
⊢ 0 < a → 0 < b → 0 < a * b

Tactic:
transfer_rw

Goal state after:
α : Type u_1
a b : ZNum
⊢ 0 < ↑a → 0 < ↑b → 0 < ↑a * ↑b
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case inl
l r₁ r₂ : ℕ
h₁ : r₁ ≤ r₂
h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l
h : ¬l + r₂ ≤ 1
H : l + r₁ ≤ 1
⊢ l ≤ delta * r₂

Tactic:
cases r₂
    · cases h (le_trans (Nat.add_le_add_left (Nat.zero_le _) _) H)
    · exact le_trans (le_trans (Nat.le_add_right _ _) H) (Nat.le_add_left 1 _)

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

Goal state before:
pp: n d : PosNum
⊢ -↑↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)

Tactic:
Num.succ'_to_nat,

Goal state after:
n d : PosNum
⊢ -↑(↑(n.pred' / Num.pos d) + 1) = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: n d : PosNum
⊢ ↑↑(n.pred' / Num.pos d).succ' = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)

Tactic:
Num.succ'_to_nat,

Goal state after:
n d : PosNum
⊢ ↑(↑(n.pred' / Num.pos d) + 1) = -(↑↑n.pred' + 1) / -(↑↑d.pred' + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case nil
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
x : F.M
h : ¬IsPath [] x
⊢ iselect [] x = default.head

Tactic:
| nil =>

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

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

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x nil) o₂
⊢ Valid' o₁ (l.node' x nil).eraseMax ↑(findMax' x nil) ∧ (l.node' x nil).size = (l.node' x nil).eraseMax.size + 1

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
h : t.Valid
⊢ t.dual.eraseMin.Valid

Tactic:
exact eraseMin.valid h.dual

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

Goal state before:
pp: a b : ℕ+
⊢ Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a

Tactic:
rw [← card_Ioc, Fintype.card_ofFinset]

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝ : Preorder α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ nil o₂
hr : Valid' o₁ r o₂
sep : All (fun x ↦ All (fun y ↦ x < y) r) nil
⊢ Valid' o₁ (nil.merge r) o₂ ∧ (nil.merge r).size = nil.size + r.size

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.nil
α : Type u_1
inst✝ : Preorder α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
l_ih✝ :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ ll o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) ll → Valid' o₁ (ll.merge r) o₂ ∧ (ll.merge r).size = ll.size + r.size
IHlr :
  ∀ {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
    Valid' o₁ lr o₂ →
      Valid' o₁ r o₂ →
        All (fun x ↦ All (fun y ↦ x < y) r) lr → Valid' o₁ (lr.merge r) o₂ ∧ (lr.merge r).size = lr.size + r.size
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ nil o₂
sep : All (fun x ↦ All (fun y ↦ x < y) nil) (Ordnode.node ls ll lx lr)
⊢ Valid' o₁ ((Ordnode.node ls ll lx lr).merge nil) o₂ ∧
    ((Ordnode.node ls ll lx lr).merge nil).size = (Ordnode.node ls ll lx lr).size + nil.size

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ l.balanceR x r = l.balance' x r

Tactic:
by
  rw [← dual_dual (balanceR l x r), dual_balanceR,
    balanceL_eq_balance' hr.dual hl.dual sr.dual sl.dual (balance_sz_dual H), ← dual_balance',
    dual_dual]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
⊢ (∃ a f, abs (repr x) = abs ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a i), p i (f i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs (repr x)) i, p i u

Tactic:
obtain ⟨a, f⟩ := repr x

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
x : F α
p : (i : Fin2 n) → α i → Prop
a : (P F).A
f : (P F).B a ⟹ α
⊢ (∃ a_1 f_1, abs ⟨a, f⟩ = abs ⟨a_1, f_1⟩ ∧ ∀ (i : Fin2 n) (j : (P F).B a_1 i), p i (f_1 i j)) ↔
    ∀ (i : Fin2 n), ∀ u ∈ supp (abs ⟨a, f⟩) i, p i u
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> abs (repr x)) i = g i '' supp (abs (repr x)) i

Tactic:
obtain ⟨a, f⟩ := repr x

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
a : (P F).A
f : (P F).B a ⟹ α
⊢ supp (g <$$> abs ⟨a, f⟩) i = g i '' supp (abs ⟨a, f⟩) i
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' (Option.map f a₁) (map f nil) (Option.map f a₂) ∧ (map f nil).size = nil.size

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
⊢ Valid' a₁ (erase x nil) a₂ ∧ Raised (erase x nil).size nil.size

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ∀ {α β : TypeVec.{?u.11} n} (f : α ⟹ β) (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p

Tactic:
intro α

Goal state after:
n : ℕ
i : Fin2 n
α : TypeVec.{?u.11} n
⊢ ∀ {β : TypeVec.{?u.11} n} (f : α ⟹ β) (p : ↑(P i) α), abs i (f <$$> p) = f <$$> abs i p
Module: Mathlib.Data.QPF.Multivariate.Constructions.Quot

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u
q : MvQPF F
G : TypeVec.{u} n → Type u
inst✝ : MvFunctor G
FG_abs : {α : TypeVec.{u} n} → F α → G α
FG_repr : {α : TypeVec.{u} n} → G α → F α
FG_abs_repr : ∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x
FG_abs_map : ∀ {α β : TypeVec.{u} n} (f : α ⟹ β) (x : F α), FG_abs (f <$$> x) = f <$$> FG_abs x
α✝ β✝ : TypeVec.{u} n
f : α✝ ⟹ β✝
p : ↑(P F) α✝
⊢ FG_abs (abs (f <$$> p)) = f <$$> FG_abs (abs p)

Tactic:
by rw [abs_map, FG_abs_map]

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type v
q : QPF F
α : Type u
x : F α
⊢ id <$> abs (repr x) = abs (repr x)

Tactic:
obtain ⟨a, f⟩ := repr x

Goal state after:
F : Type u → Type v
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ id <$> abs ⟨a, f⟩ = abs ⟨a, f⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case nil
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ nil a₂
h_mem : x ∈ nil
⊢ (erase x nil).size = nil.size - 1

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
x : F (Fix F)
| (mk ∘ dest) <$> x = x

Tactic:
rhs
    rw [← id_map x]

Goal state after:
F : Type u → Type u
q : QPF F
x : F (Fix F)
| id <$> x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
⊢ ∀ {α : TypeVec.{u} n} (x : Fix F α), Quot.mk WEquiv (fixToW x) = x

Tactic:
intro α

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ α : TypeVec.{u} n
⊢ ∀ (x : Fix F α), Quot.mk WEquiv (fixToW x) = x