mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ (m * n).divisors = image (fun p ↦ p.1 * p.2) (image Subtype.val (m.divisors ×ˢ n.divisors).attach)

Tactic:
by
    rw [Finset.attach_image_val, ← Finset.mul_def, Nat.divisors_mul]

Goal state after:
Module: Mathlib.Data.Int.Fib.Lemmas

Goal state before:
pp: x a : ℤ
⊢ fib (x + a) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))

Tactic:
rw [add_comm x]

Goal state after:
x a : ℤ
⊢ fib (a + x) ^ 2 - fib x * fib (x + 2 * a) =
    (fib x * fib (a + 1) + fib (x - 1) * fib a) ^ 2 -
      fib x * (fib x * (fib (a + 1) ^ 2 + fib a ^ 2) + fib (x - 1) * (fib a * fib (a + 1) + fib (a - 1) * fib a))
Module: Mathlib.Data.Int.Order.Lemmas

Goal state before:
pp: a b : ℤ
hn : 0 ≤ b
⊢ |a| ≤ sqrt b ↔ a * a ≤ b

Tactic:
← abs_mul_abs_self,

Goal state after:
a b : ℤ
hn : 0 ≤ b
⊢ |a| ≤ sqrt b ↔ |a| * |a| ≤ b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
⊢ bitwise and m n = m.land n

Tactic:
rcases m with m | m <;> rcases n with n | n <;> try {rfl}
    <;> simp only [bitwise, natBitwise, Bool.not_false,
      cond_false, cond_true, Bool.and_true,
      Bool.and_false]

Goal state after:
case negSucc.ofNat
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x && y) m n) = -[m+1].land (ofNat n)

case negSucc.negSucc
m n : ℕ
⊢ -[Nat.bitwise (fun x y ↦ !(!x && !y)) m n+1] = -[m+1].land -[n+1]
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℕ
⊢ ↑m <<< ↑n = ↑(m <<< n)

Tactic:
unfold_projs; simp

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (if p x = true then rdropWhile p l else l ++ [x]) = l ++ [x]

Tactic:
if_neg h

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ l ++ [x] = l ++ [x]
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ (if p x = true then rtakeWhile p l ++ [x] else []) = []

Tactic:
if_neg h

Goal state after:
α : Type u_1
p : α → Bool
l : List α
x : α
h : ¬p x = true
⊢ [] = []
Module: Mathlib.Data.List.Map2

Goal state before:
pp: case cons
α : Type u
β : Type v
bs : List β
head✝ : α
atl : List α
⊢ zipWithLeft Prod.mk (head✝ :: atl) bs = (zipWithLeft' Prod.mk (head✝ :: atl) bs).fst

Tactic:
| cons _ atl =>

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

Goal state before:
pp: case intro.intro.inr.cons
α : 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
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xb.length + 1

Tactic:
← h2len

Goal state after:
case intro.intro.inr.cons
α : 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
xs : List α
lt : Shortlex r (xa :: xs) (xa :: xb)
h : Lex r xs xb
h2len : xs.length = xb.length
l : List α
hl : l.length < (xa :: xs).length
⊢ l.length < xs.length + 1
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.rel
α : 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
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xb.length + 1

Tactic:
← h2len

Goal state after:
case intro.intro.inr.rel
α : 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
x : α
xs : List α
lt : Shortlex r (x :: xs) (xa :: xb)
h : r x xa
h2len : xs.length = xb.length
l : List α
hl : l.length < (x :: xs).length
⊢ l.length < xs.length + 1
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: case mp
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
⊢ w[j]? = w[j + p]?

Tactic:
have i2 : j + p < w.length := by lia

Goal state after:
case mp
α : Type u_1
p : ℕ
w : List α
pref : w <+: take p w ++ w
j : ℕ
len : j < w.length - p
i1 : j < w.length
i2 : j + p < w.length
⊢ w[j]? = w[j + p]?
Module: Mathlib.LinearAlgebra.Matrix.Bilinear

Goal state before:
pp: 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✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
⊢ mulLeftLinearMap n R a = 0 ↔ a = 0

Tactic:
constructor <;> intro h

Goal state after:
case mp
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✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : mulLeftLinearMap n R a = 0
⊢ a = 0

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✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0
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✝¹ : SMulCommClass R A A
inst✝ : Nonempty n
a : Matrix l m A
h : a = 0
⊢ mulLeftLinearMap n R a = 0

Tactic:
· rw [h]
    exact mulLeftLinearMap_zero_eq_zero _ _

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

Goal state before:
pp: 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
⊢ mulRightLinearMap l R a = 0 ↔ a = 0

Tactic:
constructor <;> intro h

Goal state after:
case mp
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 : mulRightLinearMap l R a = 0
⊢ a = 0

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 a = 0
Module: Mathlib.Data.List.SplitBy

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

Tactic:
hy

Goal state after:
case cons
α : Type u_1
r : α → α → Bool
a : List α
l : List (List α)
IH :
  ¬[] ∈ l →
    (∀ (m : List α), m ∈ l → IsChain (fun x y ↦ r x y = true) m) →
      IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) l → splitBy r l.flatten = l
hn : ¬a = [] ∧ ¬[] ∈ l
hc : ∀ (m : List α), m ∈ a :: l → IsChain (fun x y ↦ r x y = true) m
hc' : IsChain (fun a b ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (a :: l)
y : α
hy : y ∈ l.flatten.head?
⊢ r (a.getLast ⋯) y = false
Module: Mathlib.Data.List.SplitBy

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

Tactic:
rw [mem_cons, not_or, eq_comm] at hn
    rw [flatten_cons, splitBy_append_of_isChain hn.1 (hc _ mem_cons_self),
      IH hn.2 (fun m hm ↦ hc _ (mem_cons_of_mem a hm)) hc'.tail]
    intro y hy
    rw [← head_of_mem_head? hy]
    rw [isChain_cons] at hc'
    obtain ⟨x, hx, _⟩ := flatten_ne_nil_iff.1 (ne_nil_of_mem (mem_of_mem_head? hy))
    obtain ⟨_, _, H⟩ := hc'.1 (l.head (ne_nil_of_mem hx)) (head_mem_head? _)
    rwa [head_flatten_eq_head_head]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
X₁ Y₁ Z₁ : Multiset α
hYZ₁ : ∀ (y : α), y ∈ Y₁ → ∃ z, z ∈ Z₁ ∧ y < z
X₂ Y₂ Z₂ : Multiset α
hZ₂ : Z₂ ≠ ∅
hXZXY : Z₁ + X₁ = Y₂ + X₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
y : α
hy : y ∈ Y₁
z : α
hz : z ∈ Z₁
hyz : y < z
z_in : ¬z ∈ Y₂
⊢ z ∈ Z₁ - Y₂

Tactic:
rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos]

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

Goal state before:
pp: a✝ : ℚ≥0
h : a✝ < 0
⊢ ⌊↑a✝⌋₊ = 0

Tactic:
by simpa using h.trans zero_lt_one

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

Goal state before:
pp: p q : ℚ
hp : 0 ≤ p
⊢ (p / q).toNNRat = p.toNNRat / q.toNNRat

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← toNNRat_inv, ← toNNRat_mul hp]

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

Goal state before:
pp: case cons
ι : 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)
this : (s i).Coprime (List.map s l).prod
⊢ a ≡ b [MOD (List.map s (i :: l)).prod] ↔ ∀ i_1 ∈ i :: l, a ≡ b [MOD s i_1]

Tactic:
simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]

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

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2 ↔ k % p = x₁ ∧ k / p = x₂

Tactic:
constructor <;> intro h

Goal state after:
case mp
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k = (x₁, x₂).1 + p * (x₁, x₂).2
⊢ k % p = x₁ ∧ k / p = x₂

case mpr
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
decompose : (X + 1) ^ n = (X + 1) ^ (n % p) * (X ^ p + 1) ^ (n / p)
x₁ x₂ : ℕ
hx : (x₁, x₂) ∈ range (n % p + 1) ×ˢ range (n / p + 1)
h : k % p = x₁ ∧ k / p = x₂
⊢ k = (x₁, x₂).1 + p * (x₁, x₂).2
Module: Mathlib.Data.Nat.Hyperoperation

Goal state before:
pp: n k : ℕ
⊢ hyperoperation (n + 3) 1 k = 1

Tactic:
induction n generalizing k with grind [cases Nat]

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

Goal state before:
pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ f (sInf {x | p (f x) ∧ ∀ k < n + 1, nth (fun i ↦ p (f i)) k < x}) =
    f (sInf {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i})

pp: p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty

Tactic:
· convert! rfl using 8 with k m' hm
      nth_rw 2 [← hf.lt_iff_lt]
      convert! Iff.rfl using 2
      exact ih m' (Nat.lt_add_one_iff.mp hm) fun hfi ↦ hm.trans (h hfi)

Goal state after:
p : ℕ → Prop
f : ℕ → ℕ
hf : StrictMono f
h0 : ∀ (k : ℕ), p k → k ∈ Set.range f
hs : ∀ {p' : ℕ → Prop}, (∀ (k : ℕ), p' k → k ∈ Set.range f) → f '' {i | p' (f i)} = Set.ofPred p'
n : ℕ
ih : ∀ m ≤ n, (∀ (hfi : (Set.ofPred p).Finite), m < #hfi.toFinset) → f (nth (fun i ↦ p (f i)) m) = nth p m
h : ∀ (hfi : (Set.ofPred p).Finite), n + 1 < #hfi.toFinset
h0' : ∀ (k' : ℕ), (p k' ∧ ∀ k < n + 1, nth p k < k') → k' ∈ Set.range f
⊢ {i | p (f i) ∧ ∀ k < n + 1, nth p k < f i}.Nonempty
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
⊢ (∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)) ↔ ∀ (i : P.B a), p (f i)

Tactic:
constructor <;> intro h

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)
⊢ ∀ (i : P.B a), p (f i)

case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
a : P.A
f : P.B a → α
h : ∀ (i : P.B a), p (f i)
⊢ ∃ a_1 f_1, ⟨a, f⟩ = ⟨a_1, f_1⟩ ∧ ∀ (i : P.B a_1), p (f_1 i)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: m : Num
p : PosNum
⊢ pos p = m ↔ ZNum.pos p = m.toZNum

Tactic:
cases m <;> constructor <;> intro h <;> try cases h <;> rfl

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

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

Tactic:
by
      rw [← PosNum.cast_to_int a, ← PosNum.cast_to_int b, ← Int.cast_neg, ← Int.cast_add (-a)]
      simp [add_comm]

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

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
⊢ (∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x) ↔ ∃ y, f y = x

Tactic:
constructor <;> intro h

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
⊢ ∃ y, f y = x

case mpr
P : PFunctor.{uA, uB}
α : Type u
a : P.A
f : P.B a → α
x : α
h : ∃ y, f y = x
⊢ ∀ ⦃p : α → Prop⦄, Liftp p ⟨a, f⟩ → p x
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.realSize + r.size + 1 = (node (l.realSize + r.size + 1) l x r).realSize

Tactic:
size_eq_realSize h₃

Goal state after:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
h₁ : s = l.size + r.size + 1
h₂ : l.Sized
h₃ : r.Sized
⊢ l.realSize + r.realSize + 1 = (node (l.realSize + r.realSize + 1) l x r).realSize
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (if l.size + r.size ≤ 1 then l.node' x r
      else
        if delta * l.size < r.size then l.rotateL x r
        else if delta * r.size < l.size then l.rotateR x r else l.node' x r).dual =
    if l.size + r.size ≤ 1 then r.dual.node' x l.dual
    else
      if delta * r.size < l.size then r.dual.rotateL x l.dual
      else if delta * l.size < r.size then r.dual.rotateR x l.dual else r.dual.node' x l.dual

Tactic:
split_ifs with h h_1 h_2 <;>
    simp [dual_rotateL, dual_rotateR, add_comm]

Goal state after:
case pos
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
h : ¬l.size + r.size ≤ 1
h_1 : delta * l.size < r.size
h_2 : delta * r.size < l.size
⊢ r.dual.rotateR x l.dual = r.dual.rotateL x l.dual
Module: Mathlib.Data.PFunctor.Multivariate.Basic

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
⊢ (∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x) ↔ ∃ y, f i y = x

Tactic:
constructor <;> intro h

Goal state after:
case mp
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
⊢ ∃ y, f i y = x

case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
a : P.A
f : P.B a ⟹ α
i : Fin2 n
x : α i
h : ∃ y, f i y = x
⊢ ∀ ⦃P_1 : (i : Fin2 n) → α i → Prop⦄, LiftP P_1 ⟨a, f⟩ → P_1 i x
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
⊢ Agree (x.approx n) (y.approx (n + 1)) ↔ Agree' n x y

Tactic:
constructor <;> intro h

Goal state after:
case mp
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree (x.approx n) (y.approx (n + 1))
⊢ Agree' n x y

case mpr
F : PFunctor.{uA, uB}
n : ℕ
x y : F.M
h : Agree' n x y
⊢ Agree (x.approx n) (y.approx (n + 1))
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
x : ↑F F.M
⊢ x.fst = (M.mk x).dest.fst

Tactic:
by rw [dest_mk]

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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ x.approx (i + 1) = y.approx (i + 1)

Tactic:
apply ext_aux x y x

Goal state after:
case succ.hx
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x x

case succ.hy
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ Agree' i x y

case succ.hrec
F : PFunctor.{uA, uB}
inst✝¹ : Inhabited F.M
inst✝ : DecidableEq F.A
x y : F.M
H : ∀ (ps : Path F), iselect ps x = iselect ps y
i : ℕ
i_ih : x.approx i = y.approx i
⊢ ∀ (ps : Path F), i = length ps → iselect ps x = iselect ps y
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ Valid' o₁ (l.node' x (rl.node' rx rr)).eraseMax ↑(findMax' x (rl.node' rx rr)) ∧
    (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1

Tactic:
refine ⟨Valid'.balanceL H.left h (Or.inr ⟨_, Or.inr e, H.3.1⟩), ?_⟩

Goal state after:
case node
α : Type u_1
inst✝ : Preorder α
s : ℕ
o₂ : WithTop α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
l_ih✝ :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rl) o₂ →
      Valid' o₁ (l.node' x rl).eraseMax ↑(findMax' x rl) ∧ (l.node' x rl).size = (l.node' x rl).eraseMax.size + 1
IHrr :
  ∀ {l : Ordnode α} {x : α} {o₁ : WithBot α},
    Valid' o₁ (l.node' x rr) o₂ →
      Valid' o₁ (l.node' x rr).eraseMax ↑(findMax' x rr) ∧ (l.node' x rr).size = (l.node' x rr).eraseMax.size + 1
l : Ordnode α
x : α
o₁ : WithBot α
H : Valid' o₁ (l.node' x (rl.node' rx rr)) o₂
this : Ordnode.node rs rl rx rr = rl.node' rx rr
h : Valid' (↑x) (rl.node' rx rr).eraseMax ↑(findMax' rx rr)
e : (rl.node' rx rr).size = (rl.node' rx rr).eraseMax.size + 1
⊢ (l.node' x (rl.node' rx rr)).size = (l.node' x (rl.node' rx rr)).eraseMax.size + 1
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
wp x y zp ap bp : ℕ
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y ↔
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
      ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
          { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

Tactic:
constructor <;> intro h

Goal state after:
case mp
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat

case mpr
u : XgcdType
wp x y zp ap bp : ℕ
h :
  { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.w *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.z =
    ({ wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y).succPNat
⊢ { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp +
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp +
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.wp *
        { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.zp =
    { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.x *
      { wp := wp, x := x, y := y, zp := zp, ap := ap, bp := bp }.y
Module: Mathlib.Data.PNat.Xgcd

Goal state before:
pp: u : XgcdType
⊢ u.bp = u.ap ↔ u.ap = u.bp

Tactic:
constructor <;> intro h

Goal state after:
case mp
u : XgcdType
h : u.bp = u.ap
⊢ u.ap = u.bp

case mpr
u : XgcdType
h : u.ap = u.bp
⊢ u.bp = u.ap