mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inl
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : σ
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (inl val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inl val✝))

Tactic:
simp! [Sum.traverse, map_id, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Control.Traversable.Instances

Goal state before:
pp: case inr
σ : Type u
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
val✝ : α
⊢ Sum.traverse (Comp.mk ∘ (fun x ↦ f <$> x) ∘ g) (inr val✝) = Comp.mk (Sum.traverse f <$> Sum.traverse g (inr val✝))

Tactic:
simp! [Sum.traverse, map_id, functor_norm] <;> rfl

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: tail✝

Tactic:
rw [← ih]

Goal state after:
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
| head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
· simp only [Part.fix_def f h₀]
    constructor <;> intro hh
    · exact ⟨_, hh⟩
    have h₁ := Nat.find_spec h₀
    rw [dom_iff_mem] at h₁
    obtain ⟨y, h₁⟩ := h₁
    replace h₁ := approx_mono' f _ _ h₁
    suffices y = b by
      subst this
      exact h₁
    obtain ⟨i, hh⟩ := hh
    revert h₁; generalize succ (Nat.find h₀) = j; intro h₁
    wlog case : i ≤ j
    · rcases le_total i j with H | H <;> [skip; symm] <;> apply_assumption <;> assumption
    replace hh := approx_mono f case _ _ hh
    apply Part.mem_unique h₁ hh

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case some
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, Option.some x)

Tactic:
exact ⟨⟨σ x s, by simp⟩, Prod.ext (by grind) (by grind)⟩

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
⊢ dlookup a l₁ = dlookup a l₂

Tactic:
have nd₂ := (perm_nodupKeys p).mp nd₁

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys
⊢ dlookup a l₁ = dlookup a l₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
⊢ lookupAll a l₁ = lookupAll a l₂

Tactic:
have nd₂ := (perm_nodupKeys p).mp nd₁

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys
⊢ lookupAll a l₁ = lookupAll a l₂
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih : a ∈ tl.keys → ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a tl = l₁ ++ l₂
e : ¬a = hd.fst
h : a = hd.fst
⊢ ∃ b l₁ l₂, ¬a ∈ l₁.keys ∧ hd :: tl = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a (hd :: tl) = l₁ ++ l₂

Tactic:
exact absurd h e

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Pi

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
⊢ (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)

Tactic:
induction s using Finset.induction with

Goal state after:
case insert
α : Type u_1
ι : Type u_2
inst✝² : DistribLattice α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq ι
κ : ι → Type u_3
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → α
i : ι
s : Finset ι
hi : i ∉ s
ih : (s.inf fun i ↦ (t i).sup (f i)) = (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)
⊢ ((insert i s).inf fun i ↦ (t i).sup (f i)) =
    ((insert i s).pi t).sup fun g ↦ (insert i s).attach.inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s.sup ((fun f ↦ image f t) ∘ Prod.mk) = t.sup ((fun f ↦ image f s) ∘ fun b a ↦ (a, b))

Tactic:
sup_eq_biUnion

Goal state after:
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s.biUnion ((fun f ↦ image f t) ∘ Prod.mk) = t.biUnion ((fun f ↦ image f s) ∘ fun b a ↦ (a, b))
Module: Mathlib.Data.Finset.Functor

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ traverse pure s = pure s

Tactic:
rw [traverse, Multiset.id_traverse]
  exact s.val_toFinset

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

Goal state before:
pp: case cons.mk.right
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l' : List (Sigma β)
this : l'.NodupKeys
xs : List (Sigma β)
l_ih : (foldr (fun x ↦ kinsert x.fst x.snd) l' xs).NodupKeys
fst✝ : α
snd✝ : β fst✝
⊢ (kerase fst✝ (foldr (fun x ↦ kinsert x.fst x.snd) l' xs)).NodupKeys

Tactic:
exact l_ih.kerase _

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

Goal state before:
pp: m : ℕ
b : Bool
n : ℕ
⊢ (bit b ↑n).testBit m.succ = (↑n).testBit m

Tactic:
rw [bit_coe_nat]; apply Nat.testBit_bit_succ

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

Goal state before:
pp: a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Tactic:
rw [← abs_le_iff_mul_self_le, abs_eq_natAbs, abs_eq_natAbs]
  exact Int.ofNat_le.symm

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

Goal state before:
pp: case h_1
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x✝ : Bool
heq✝ : p head = true
⊢ (dropWhile p tail).length ≤ tail.length + 1

pp: case h_2
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x✝ : Bool
heq✝ : p head = false
⊢ (head :: tail).length ≤ tail.length + 1

Tactic:
· lia

Goal state after:
case h_2
α : Type u_1
p : α → Bool
head : α
tail : List α
ih : (dropWhile p tail).length ≤ tail.length
x✝ : Bool
heq✝ : p head = false
⊢ (head :: tail).length ≤ tail.length + 1
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: case e'_3
n m l : ℕ
hnm : n ≤ m
hml : m ≤ l
⊢ l - n = m - n + (l - m)

Tactic:
· lia

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

Goal state before:
pp: case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ filter (fun x ↦ decide (l ≤ x)) (Ico n l) ++ filter (fun x ↦ decide (l ≤ x)) (Ico l m) = Ico l m

Tactic:
filter_le_of_top_le (le_refl l),

Goal state after:
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ [] ++ filter (fun x ↦ decide (l ≤ x)) (Ico l m) = Ico l m
Module: Mathlib.Data.List.PeriodicityLemma

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ j + u.length + p - u.length < v.length

Tactic:
· lia

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

Goal state before:
pp: α : Type u_1
u v w : List α
p : ℕ
per : (u ++ v ++ w).HasPeriod p
j : ℕ
len : j < v.length - p
shift_position : (u ++ (v ++ w))[j + u.length]? = v[j]?
eq : j + u.length + p - u.length = j + p
⊢ u.length ≤ j + u.length + p

Tactic:
· lia

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

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A B : Matrix n n (DualNumber R)
⊢ (of fun i j ↦ fst ((A * B) i j), of fun i j ↦ snd ((A * B) i j)) =
    (of fun i j ↦ fst (A i j), of fun i j ↦ snd (A i j)) * (of fun i j ↦ fst (B i j), of fun i j ↦ snd (B i j))

Tactic:
ext
    · dsimp [mul_apply]
      simp_rw [fst_sum]
      rfl
    · simp_rw [snd_mul, smul_eq_mul, op_smul_eq_mul]
      simp only [mul_apply, snd_sum, DualNumber.snd_mul, snd_mk, of_apply, fst_mk, add_apply]
      rw [← Finset.sum_add_distrib]

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

Goal state before:
pp: R n : Type
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
r : R
⊢ (of fun i j ↦ fst ((algebraMap R (Matrix n n (DualNumber R))) r i j),
      of fun i j ↦ snd ((algebraMap R (Matrix n n (DualNumber R))) r i j)) =
    (algebraMap R (DualNumber (Matrix n n R))) r

Tactic:
by
    simp_rw [algebraMap_eq_inl', algebraMap_eq_diagonal, Pi.algebraMap_def,
      Algebra.algebraMap_self_apply, algebraMap_eq_inl, ← diagonal_map (inl_zero R), map_apply,
      fst_inl, snd_inl]
    rfl

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

Goal state before:
pp: case refine_4.refine_2
α : 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₁
⊢ ∃ z, (z ∈ Z₂ ∨ z ∈ Z₁ - Y₂) ∧ y < z

Tactic:
obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
    exact ⟨z, .inl hz, hyz⟩

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ - 1 < ↑x ∧ ↑x ≤ ↑↑⌈x⌉₊

Tactic:
sub_lt_iff_lt_add

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
x : ℚ≥0
⊢ ↑↑⌈x⌉₊ < ↑x + 1 ∧ ↑x ≤ ↑↑⌈x⌉₊
Module: Mathlib.Data.Nat.ChineseRemainder

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

Tactic:
induction l with
  | nil => simp [modEq_one]
  | cons i l ih =>
    have : Coprime (s i) (l.map s).prod := by
      simp only [coprime_list_prod_right_iff, List.mem_map, forall_exists_index, and_imp,
        forall_apply_eq_imp_iff₂]
      intro j hj
      exact (List.pairwise_cons.mp co).1 j hj
    simp [← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co)]

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ ↑((k.1 + k.2).choose k.1) = ↑(k.1 + k.2)! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ

Tactic:
rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul,
    add_comm, Nat.add_choose_mul_factorial_mul_factorial]

Goal state after:
case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ IsUnit ↑k.1!

case h
A : Type u_1
inst✝ : CommSemiring A
k : ℕ × ℕ
hm : IsUnit ↑(k.1 + k.2)!
⊢ IsUnit ↑k.2!
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image ((fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) ∘ Subtype.val) (Finset.Iic n.factorization).attach

Tactic:
rw [← Finset.image_image, Finset.attach_image_val]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n.divisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iic n.factorization)
Module: Mathlib.Data.Nat.Factorization.Divisors

Goal state before:
pp: n : ℕ
⊢ n.properDivisors =
    Finset.image ((fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) ∘ Subtype.val) (Finset.Iio n.factorization).attach

Tactic:
rw [← Finset.image_image, Finset.attach_image_val]

Goal state after:
n : ℕ
⊢ n.properDivisors = Finset.image (fun x ↦ x.prod fun x1 x2 ↦ x1 ^ x2) (Finset.Iio n.factorization)
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n p : ℕ
inst✝ : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
⊢ n = p ^ multiplicity p n

Tactic:
rename_i hp

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
h : ∀ i ∈ Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]
⊢ n = p ^ multiplicity p n
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n : ℕ
h : IsPrimePow n
⊢ n.minFac ∣ (Icc 1 (n - 1)).gcd n.choose

Tactic:
obtain ⟨k, _, _, hn₁⟩ := (isPrimePow_nat_iff_bounded_log_minFac _).mp h
  exact dvd_gcd_iff.mpr fun i hi => by
    nth_rw 2 [hn₁]
    exact Prime.dvd_choose_pow (minFac_prime_iff.mpr h.ne_one) (by grind) (by grind)

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

Goal state before:
pp: case pos.h
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 : ℕ
ih : ∀ m < n, (∀ (hf : (Set.ofPred p).Finite), m < #hf.toFinset) → nth p m ≤ f m
hn : ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset
⊢ nth p n ≤ f n

Tactic:
rw [nth_eq_sInf]
    refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩
    have : f k < f n := by apply hmono <;> grind
    grind

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

Goal state before:
pp: case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n + 1 ≤ m

Tactic:
rw [Nat.succ_le_iff]

Goal state after:
case succ.refine_2
p : ℕ → Prop
f : ℕ → ℕ
hsurj : Set.SurjOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset} (Set.ofPred p)
hmono : MonotoneOn f {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
n : ℕ
ih : (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) → f n ≤ nth p n
hn : ∀ (hf : (Set.ofPred p).Finite), n + 1 < #hf.toFinset
m : ℕ
hm : m ∈ {n | ∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset}
hb : p (f m)
h : ∀ k < n + 1, nth p k < f m
⊢ n < m
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil.node.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
⊢ Ordnode α

Tactic:
exact node 2 l x nil

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

Goal state before:
pp: case node.nil.nil.nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
⊢ Ordnode α

Tactic:
exact node 2 l x nil

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
rw [size_dual, size_dual]

Goal state after:
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x✝ : α
r : Ordnode α
lo✝ : WithBot α
hi✝ : WithTop α
ol : l.Bounded lo✝ ↑x✝
Or : r.Bounded (↑x✝) hi✝
sl : l.Sized
sr : r.Sized
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
ol' : l.dual.Bounded (↑x✝) lo✝
sl' : l.dual.Sized
bl' : l.dual.Balanced
or' : r.dual.Bounded hi✝ ↑x✝
sr' : r.dual.Sized
br' : r.dual.Balanced
⊢ BalancedSz r.size l.size
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t.dual.dual o₂
⊢ Valid' o₁ t o₂

Tactic:
dual_dual,

Goal state after:
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Valid' o₂ t.dual o₁
this : Valid' o₁ t o₂
⊢ Valid' o₁ t o₂
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node
α : 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
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ Valid' o₁ (l.node4L x (Ordnode.node s ml z mr) y r) o₂

Tactic:
suffices
    BalancedSz (size l) (size ml) ∧
      BalancedSz (size mr) (size r) ∧ BalancedSz (size l + size ml + 1) (size mr + size r + 1) from
    Valid'.node' (hl.node' hm.left this.1) (hm.right.node' hr this.2.1) this.2.2

Goal state after:
case node
α : 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
H :
  l.size = 0 ∧ (Ordnode.node s ml z mr).size = 1 ∧ r.size ≤ 1 ∨
    0 < l.size ∧
      ratio * r.size ≤ (Ordnode.node s ml z mr).size ∧
        delta * l.size ≤ (Ordnode.node s ml z mr).size + r.size ∧
          3 * ((Ordnode.node s ml z mr).size + r.size) ≤ 16 * l.size + 9 ∧
            (Ordnode.node s ml z mr).size ≤ delta * r.size
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ P.map Subtype.val ⟨a, f⟩ = ⟨a, fun i ↦ ↑(f i)⟩

Tactic:
PFunctor.map_eq

Goal state after:
case mp
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
y : ↑P (Subtype p)
hy : Subtype.val <$> y = x
a : P.A
f : P.B a → Subtype p
h : y = ⟨a, f⟩
⊢ ⟨a, Subtype.val ∘ f⟩ = ⟨a, fun i ↦ ↑(f i)⟩
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
| inr H =>

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

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.dual.size l.dual.size

Tactic:
rw [size_dual, size_dual]

Goal state after:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x✝ : α
r : Ordnode α
b : BalancedSz l.size r.size
bl : l.Balanced
br : r.Balanced
⊢ BalancedSz r.size l.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = (l.dual.dual.rotateR x r.dual.dual).dual

Tactic:
dual_dual,

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = (l.rotateR x r.dual.dual).dual
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case bit1.h₂
d n : PosNum
q r : Num
IH : ↑r + ↑d * ↑q = ↑n ∧ ↑r < ↑d
⊢ 2 * ↑r + 1 < 2 * ↑d

Tactic:
· lia

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

Goal state before:
pp: F : PFunctor.{uA, uB}
x : ↑F F.M
n : ℕ
i : F.B x.fst
⊢ Agree ((x.snd i).approx n) ((x.snd i).approx (n + 1))

Tactic:
apply (x.2 i).consistent

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

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i)

Tactic:
simp only [isubtree, dif_pos, isubtree, M.casesOn_mk']

Goal state after:
F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree ps (f (cast ⋯ i)) = isubtree ps (f i)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: F : PFunctor.{uA, uB}
inst✝¹ : DecidableEq F.A
inst✝ : Inhabited F.M
ps : Path F
a : F.A
f : F.B a → F.M
i : F.B a
⊢ isubtree (⟨a, i⟩ :: ps) (M.mk ⟨a, f⟩) = isubtree ps (f i)

Tactic:
simp only [isubtree, dif_pos, isubtree, M.casesOn_mk']; rfl

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (l.dual.dual.balanceR x r.dual.dual).dual

Tactic:
dual_dual,

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceR x r).dual = (l.balanceR x r.dual.dual).dual
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ P.map f ⟨a, f'⟩ = ⟨a, f ∘ f'⟩

Tactic:
PFunctor.map_eq

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
⊢ ⟨a, f ∘ f'⟩ = ⟨a, f ∘ f'⟩
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ P.map (M.corec g) ⟨a, f'⟩ = ⟨a, M.corec g ∘ f'⟩

Tactic:
PFunctor.map_eq

Goal state after:
P : PFunctor.{uA, uB}
α : Type u_2
g : α → ↑P α
f : α → P.M
hyp : ∀ (x : α), (f x).dest = P.map f (g x)
x : α
a✝ : True
a : P.A
f' : P.B a → α
gxeq : g x = ⟨a, f'⟩
h₀ : (f x).dest = ⟨a, f ∘ f'⟩
⊢ ⟨a, M.corec g ∘ f'⟩ = ⟨a, M.corec g ∘ f'⟩
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
H : rl.size + rr.size ≤ 1
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

pp: case inr
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs

Tactic:
· lia

Goal state after:
case inr
α : Type u_1
inst✝ : Preorder α
o₁ : WithBot α
o₂ : WithTop α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr t : Ordnode α
hl : Valid' o₁ (Ordnode.node ls ll lx lr) o₂
hr : Valid' o₁ (Ordnode.node rs rl rx rr) o₂
h : 3 * (ll.size + lr.size + 1) < rl.size + rr.size + 1
v : Valid' o₁ t ↑rx
e : t.size = ll.size + lr.size + 1 + rl.size
hr₁ : rl.size ≤ delta * rr.size
hr₂ : rr.size ≤ delta * rl.size
⊢ Valid' o₁ (t.balanceL rx rr) o₂ ∧ (t.balanceL rx rr).size = ls + rs