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

Goal state before:
pp: case pos.mpr.inr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ y = b

Tactic:
symm

Goal state after:
case pos.mpr.inr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b = y
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
⊢ IsOpen (⋃ i, (Set.range (σ (Option.some i)))ᶜ ∩ Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
refine isOpen_iUnion fun i ↦ IsOpen.inter ?_ ?_

Goal state after:
case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Set.range (σ (Option.some i)))ᶜ

case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case neg
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
t : T
ht : t ∈ fibres π σ
t' : T
ht' : t' ∈ fibres π σ
property✝ : π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).1 = π_r π σ (⟨t, ht⟩, ⟨t', ht'⟩).2
h : ¬(π t).2 = none
n : X
hn : (π t).2 = Option.some n
⊢ ∃ a, coverToFun (fibreIncl π σ) (π_r π σ) a = ⟨(⟨t, ht⟩, ⟨t', ht'⟩), property✝⟩

Tactic:
exact ⟨Sum.inl ⟨σ n (π t).1, by grind⟩, by grind⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Zero (α i)
s✝ : Finset ι
f✝ : Π₀ (i : ι), α i
t✝ : (i : ι) → Finset (α i)
s : Finset ι
t : (i : ι) → Finset (α i)
f g : (a : ι) → a ∈ s → α a
h : (fun i ↦ f ↑i ⋯) = fun i ↦ g ↑i ⋯
i : ι
hi : i ∈ s
⊢ f i hi = g i hi

Tactic:
convert! congr_fun h ⟨i, hi⟩

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

Goal state before:
pp: case succ
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun x1 x2 ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin n
ihk : f k.castSucc < x
⊢ f k.succ < x

Tactic:
rw [range_subset_iff] at hbt
    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
obtain ⟨S', T', y', π', g', hπ', hy', comp, ⟨⟨split⟩⟩, epi⟩ := aux π

Goal state after:
R : Type
inst✝ : CommRing R
X Y : LightCondMod R
p : X ⟶ Y
hp : Epi p
S : LightProfinite
f : (free R).obj (S ⊗ ℕ∪{∞}).toCondensed ⟶ Y
T : LightProfinite
π : T ⟶ S ⊗ ℕ∪{∞}
g : (free R).obj T.toCondensed ⟶ X
hπ : Epi π
comm : (lightProfiniteToLightCondSet ⋙ free R).map π ≫ f = g ≫ p
S' T' : LightProfinite
y' : S' ⟶ S
π' : T' ⟶ S' ⊗ ℕ∪{∞}
g' : T' ⟶ T
hπ' : Epi π'
hy' : Epi y'
comp : π' ≫ y' ▷ ℕ∪{∞} = g' ≫ π
epi : Epi (cover π')
split : SplitEpi (LightProfinite.fibreIncl ∞ (π' ≫ snd S' ℕ∪{∞}) ≫ π' ≫ fst S' ℕ∪{∞})
⊢ ∃ S' π,
    ∃ (_ : Function.Surjective ⇑(ConcreteCategory.hom π)),
      ∃ g', (free R).map (lightProfiniteToLightCondSet.map (π ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ lookupAll a (⟨a', b⟩ :: l) = [] ↔ ∀ (b_1 : β a), ¬⟨a, b_1⟩ ∈ ⟨a', b⟩ :: l

Tactic:
simp [h, lookupAll_eq_nil]

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

Goal state before:
pp: 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 ⋯)
⊢ ((t i).sup (f i) ⊓ (s.pi t).sup fun g ↦ s.attach.inf fun i ↦ f (↑i) (g ↑i ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert ⟨i, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)

Tactic:
sup_inf_sup

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 ⋯)
⊢ ((t i ×ˢ s.pi t).sup fun i_1 ↦ f i i_1.1 ⊓ s.attach.inf fun i_2 ↦ f (↑i_2) (i_1.2 ↑i_2 ⋯)) =
    ((insert i s).pi t).sup fun g ↦ (insert ⟨i, ⋯⟩ (image (fun x ↦ ⟨↑x, ⋯⟩) s.attach)).inf fun i_1 ↦ f (↑i_1) (g ↑i_1 ⋯)
Module: Mathlib.Data.Finset.NatDivisors

Goal state before:
pp: m n : ℕ
hmn : m.Coprime n
⊢ (m * n).divisors = m.divisors * n.divisors

Tactic:
Nat.divisors_mul

Goal state after:
m n : ℕ
hmn : m.Coprime n
⊢ m.divisors * n.divisors = m.divisors * n.divisors
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ dlookup a (⟨a', b⟩ :: tail✝).dedupKeys = dlookup a (⟨a', b⟩ :: tail✝)

Tactic:
rw [dedupKeys_cons, dlookup_kinsert_ne h, l_ih, dlookup_cons_ne]

Goal state after:
case neg.a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
tail✝ : List (Sigma β)
l_ih : dlookup a tail✝.dedupKeys = dlookup a tail✝
a' : α
b : β a'
h : ¬a = a'
⊢ a ≠ ⟨a', b⟩.fst
Module: Mathlib.Data.Finsupp.AList

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : DecidableEq M
l : AList fun _x ↦ M
⊢ l.lookupFinsupp.support = (filter (fun x ↦ decide (x.snd ≠ 0)) l.entries).keys.toFinset

Tactic:
by
  dsimp only [lookupFinsupp]
  congr!

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (x + y)

Tactic:
match hx with
    | CPRankMax.zero => simp only [zero_add, hy]

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

Goal state before:
pp: case false
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0

Tactic:
decide

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

Goal state before:
pp: case H
b : Bool
n : ℤ
⊢ 2 ≠ 0

Tactic:
decide

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

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
⊢ ↑(count (fun x ↦ x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉

Tactic:
have hr' : 0 < (r : ℚ) := by positivity

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ ↑(count (fun x ↦ x ≡ v [MOD r]) b) = ⌈(↑b - ↑(v % r)) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈(0 - ↑(v % r)) / ↑r⌉

Tactic:
zero_sub

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
| ⌈(↑b - ↑(v % r)) / ↑r⌉ - ⌈-↑(v % r) / ↑r⌉
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: b r : ℕ
hr : 0 < r
v : ℕ
⊢ count (fun x ↦ x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0

Tactic:
have hr' : 0 < (r : ℚ) := by positivity

Goal state after:
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
⊢ count (fun x ↦ x ≡ v [MOD r]) b = b / r + if v % r < b % r then 1 else 0
Module: Mathlib.Data.Int.CardIntervalMod

Goal state before:
pp: case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 * ↑r < ↑(b % r) - ↑(v % r) ∧ ↑(b % r) - ↑(v % r) ≤ 0

Tactic:
tsub_nonpos,

Goal state after:
case neg
b r : ℕ
hr : 0 < r
v : ℕ
hr' : 0 < ↑r
h : ¬v % r < b % r
⊢ -1 * ↑r < ↑(b % r) - ↑(v % r) ∧ ↑(b % r) ≤ ↑(v % r)
Module: Mathlib.Data.List.DropRight

Goal state before:
pp: α : Type u_1
p : α → Bool
⊢ rdropWhile p [] = []

Tactic:
simp [rdropWhile]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rdropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true

Tactic:
simp [rdropWhile]

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

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

Tactic:
← append_consecutive hnl hlm,

Goal state after:
case inl
n m l : ℕ
hlm : l ≤ m
hnl : n ≤ l
⊢ filter (fun x ↦ decide (x < l)) (Ico n l ++ Ico l m) = Ico n l
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 m) = Ico l m

Tactic:
← append_consecutive hnl hlm,

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

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

Tactic:
cases s with
  | nil =>
    rw [List.nil_append, List.nil_append]
    exact h
  | cons head tail =>
    apply of_lex
    · simp only [List.cons_append, List.length_cons, List.length_append,
      add_left_inj, add_right_inj]
      exact h2.1
    exact List.Lex.append_left r h2.2 (head :: tail)

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

Goal state before:
pp: case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a.length = 0
⊢ Acc (Shortlex r) a

Tactic:
rw [List.length_eq_zero_iff] at len_a

Goal state after:
case zero
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) a
Module: Mathlib.Data.List.SplitBy

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

Tactic:
apply List.isChain_reverse.1

Goal state after:
case nil.inr
α : Type u_1
r : α → α → Bool
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
⊢ IsChain (fun b a ↦ r a b = true) (a :: g).reverse.reverse
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])

Tactic:
apply List.isChain_reverse.1

Goal state after:
case h_2.inl
α : Type u_1
r : α → α → Bool
b : α
l : List α
a : α
g : List α
hga : ∀ (b : α), b ∈ g.head? → r b a = true
hg : IsChain (fun y x ↦ r x y = true) g
x✝ : Bool
heq✝ : r a b = false
IH :
  ∀ {a_1 : α} {g_1 : List α},
    (∀ (b : α), b ∈ g_1.head? → r b a_1 = true) →
      IsChain (fun y x ↦ r x y = true) g_1 →
        g.reverse ++ [a] ∈ splitBy.loop r l a_1 g_1 [] → IsChain (fun x y ↦ r x y = true) (g.reverse ++ [a])
⊢ IsChain (fun b a ↦ r a b = true) (g.reverse ++ [a]).reverse
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) (gs.reverse ++ [(a :: g).reverse])

Tactic:
apply List.isChain_reverse.1

Goal state after:
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 b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) (gs.reverse ++ [(a :: g).reverse]).reverse
Module: Mathlib.Data.List.SplitBy

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

Tactic:
by
  cases l with
  | nil => contradiction
  | cons a l => rw [cons_append, splitBy, splitByLoop_append h ha]; simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
A : Matrix (m₁ ⊕ m₂) n R
⊢ A.toRows₁.fromRows A.toRows₂ = A

Tactic:
ext (i | i) j <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m : Type u_2
n₁ : Type u_6
n₂ : Type u_7
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
⊢ (A₁.fromCols A₂)ᵀ = A₁ᵀ.fromRows A₂ᵀ

Tactic:
ext (i | i) j <;> simp

Goal state after:
Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
⊢ -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

Tactic:
ext (i | i) j <;> simp

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 : X₁ + Z₁ = X₂ + Y₂
hYZ₂ : ∀ (y : α), y ∈ Y₂ → ∃ z, z ∈ Z₂ ∧ y < z
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)

Tactic:
rw [add_comm X₁, add_comm X₂] at hXZXY

Goal state after:
α : 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
⊢ (X₁ + Y₁).IsDershowitzMannaLT (X₂ + Z₂)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
l l' : List ι
hl : l.Perm l'
hs : ∀ i ∈ l, s i ≠ 0
co : List.Pairwise (Coprime on s) l
z : { k // ∀ i ∈ l', k ≡ a i [MOD s i] } := chineseRemainderOfList a s l' ⋯
hlp : (List.map s l).prod = (List.map s l').prod
⊢ ↑z < (List.map s l).prod

Tactic:
by rw [hlp]
          exact chineseRemainderOfList_lt_prod _ _ _ _
            (by simpa [List.Perm.mem_iff hl.symm] using hs)

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

Goal state before:
pp: ι : Type u_1
a s : ι → ℕ
m : Multiset ι
l l' : List ι
pp : l.Perm l'
nod' : l'.Nodup
nod : l.Nodup
hs' : ∀ i ∈ l', s i ≠ 0
⊢ ∀ i ∈ l, s i ≠ 0

Tactic:
simpa [List.Perm.mem_iff pp] using hs'

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1

Tactic:
have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)

Goal state after:
case zero
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
e : p.pred' = Num.zero
ep : p = Num.zero.succ'
⊢ -↑(Num.casesOn Num.zero 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1

Tactic:
have ep : p = _ := (succ'_pred' p).symm.trans (congr_arg Num.succ' e)

Goal state after:
case pos
α : Type u_1
inst✝ : AddGroupWithOne α
p a : PosNum
e : p.pred' = Num.pos a
ep : p = (Num.pos a).succ'
⊢ -↑(Num.casesOn (Num.pos a) 1 bit1) = -↑p + -↑p + 1
Module: Mathlib.Data.PFunctor.Univariate.Basic

Goal state before:
pp: case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : P.B a), p (f i)) → Liftp p x

Tactic:
rintro ⟨a, f, xeq, pf⟩

Goal state after:
case mpr
P : PFunctor.{uA, uB}
α : Type u
p : α → Prop
x : ↑P α
a : P.A
f : P.B a → α
xeq : x = ⟨a, f⟩
pf : ∀ (i : P.B a), p (f i)
⊢ Liftp p x
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inl.zero
α : 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 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ 0 ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 0 ∧ BalancedSz (0 + 0 + 1) (0 + 0 + 1)

Tactic:
decide

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

Goal state before:
pp: case node.inl.succ.zero
α : 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 : l.size = 0
m1 : ml.size = 0 ∧ mr.size = 0
⊢ 0 + 1 ≤ 1 → BalancedSz 0 0 ∧ BalancedSz 0 (0 + 1) ∧ BalancedSz (0 + 0 + 1) (0 + (0 + 1) + 1)

Tactic:
decide

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

Goal state before:
pp: a : PosNum
⊢ ofInt' ↑(neg a) = neg a

Tactic:
rw [cast_neg, ofInt'_neg, ← PosNum.cast_to_nat, ← Num.ofInt'_toZNum, PosNum.of_to_nat]; rfl

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

Goal state before:
pp: case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
⊢ (∃ a f, x = ⟨a, f⟩ ∧ ∀ (i : Fin2 n) (j : P.B a i), p (f i j)) → LiftP p x

Tactic:
rintro ⟨a, f, xeq, pf⟩

Goal state after:
case mpr
n : ℕ
P : MvPFunctor.{u} n
α : TypeVec.{u} n
p : ⦃i : Fin2 n⦄ → α i → Prop
x : ↑P α
a : P.A
f : P.B a ⟹ α
xeq : x = ⟨a, f⟩
pf : ∀ (i : Fin2 n) (j : P.B a i), p (f i j)
⊢ LiftP p x
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos.zero.zero
α : 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₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
mm : 0 + 0 ≤ 1
⊢ BalancedSz 1 0 ∧ BalancedSz 0 1 ∧ BalancedSz (1 + 0 + 1) (0 + 1 + 1)

Tactic:
decide

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

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 0 < delta

Tactic:
decide

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

Goal state before:
pp: a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 1 ≤ delta * delta

Tactic:
decide

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

Goal state before:
pp: case pos.zero.succ.refl
α : 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₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 0 ∧ BalancedSz (0 + 1) 1 ∧ BalancedSz (1 + 0 + 1) (0 + 1 + 1 + 1)

Tactic:
decide

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

Goal state before:
pp: α : Type u_1
n : ℕ
⊢ (Num.ofNat' (n + 1)).toZNum = (Num.ofNat' n).toZNum + 1

Tactic:
rw [Num.ofNat'_succ, Num.add_one, Num.toZNum_succ, ZNum.add_one]

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

Goal state before:
pp: case pos.succ.zero.refl
α : 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₁ : 2 * r.size ≤ ml.size + mr.size + 1
lr₁ : 3 * l.size ≤ ml.size + mr.size + (1 + 1)
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 (0 + 1) ∧ BalancedSz 0 1 ∧ BalancedSz (1 + (0 + 1) + 1) (0 + 1 + 1)

Tactic:
decide

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

Goal state before:
pp: α : Type u_1
⊢ 0 ≠ 1

Tactic:
decide

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

Goal state before:
pp: α : Type u_1
⊢ 0 ≤ 1

Tactic:
decide

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

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

Tactic:
by revert h; transfer_rw; intro h; gcongr

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

Goal state before:
pp: α : 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬0 + 0 ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size = 0
ml0 : ml.size = 0
⊢ 0 + 0 ≤ 1

Tactic:
decide

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

Goal state before:
pp: α : 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 ≤ ml.size + mr.size + 1
lr₁ : delta * l.size ≤ ml.size + mr.size + 1 + r.size
lr₂ : 3 * (ml.size + mr.size + 1 + r.size) ≤ 16 * l.size + 9
mr₂ : ml.size + mr.size + 1 ≤ delta * r.size
r0 : r.size > 0
mm : ¬ml.size + mr.size ≤ 1
mm₁ : ml.size ≤ delta * mr.size
mm₂ : mr.size ≤ delta * ml.size
ml0 : ml.size > 0
this✝ : delta * (ratio * l.size) ≤ ratio * (ml.size + mr.size + 1) + ratio * r.size
this : delta * (ratio * l.size) ≤ ratio.succ * (ml.size + mr.size + 1)
⊢ 0 < delta

Tactic:
decide

Goal state after: