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

Goal state before:
pp: n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
⊢ β g

Tactic:
suffices g = nilFun by rwa [this]

Goal state after:
n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
⊢ g = nilFun
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec.{u_1} (n✝ + 1)
x y : α a✝.fs
⊢ ofRepeat (α.repeatEq a✝.fs (prod.mk a✝.fs x y)) ↔ x = y

Tactic:
rw [repeatEq]

Goal state after:
case fs
n n✝ : ℕ
a✝ : Fin2 n✝
i_ih : ∀ {α : TypeVec.{u_1} n✝} {x y : α a✝}, ofRepeat (α.repeatEq a✝ (prod.mk a✝ x y)) ↔ x = y
α : TypeVec.{u_1} (n✝ + 1)
x y : α a✝.fs
⊢ ofRepeat ((α.drop.repeatEq ::: uncurry Eq) a✝.fs (prod.mk a✝.fs x y)) ↔ x = y
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
F : Functor t'
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ LawfulFunctor t'

Tactic:
have : F = Equiv.functor eqv := by
    cases F
    dsimp [Equiv.functor]
    congr <;> ext <;> [rw [← h₀]; rw [← h₁]] <;> rfl
  subst this
  exact Equiv.lawfulFunctor eqv

Goal state after:
Module: Mathlib.Data.Analysis.Topology

Goal state before:
pp: α : Type u_1
τ : Type u_4
inst✝ : TopologicalSpace α
F : Realizer α
E : F.σ ≃ τ
s : τ
⊢ (F.ofEquiv E).F.f s = F.F.f (E.symm s)

Tactic:
delta ofEquiv; simp

Goal state after:
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
⊢ 1 ≤ prec

Tactic:
exact C.precPos

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b : β a
b' : β a'
s : AList β
h : a ≠ a'
⊢ (insert a' b' (insert a b s)).entries ~ (insert a b (insert a' b' s)).entries

Tactic:
by
  simp only [entries_insert]; rw [kerase_cons_ne, kerase_cons_ne, kerase_comm] <;>
    [apply Perm.swap; exact h; exact h.symm]

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

Goal state before:
pp: case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
refine ⟨?_, h'⟩

Goal state after:
case mp.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₁.entries = some y✝
⊢ ¬x✝ ∈ s₂.entries.keys
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝

Tactic:
refine ⟨?_, h'⟩

Goal state after:
case mpr.inl
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : dlookup x✝ s₂.entries = some y✝
⊢ ¬x✝ ∈ s₁.entries.keys
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys
h : ⟨a, b⟩ ∈ l
⊢ kreplace a b l = l

Tactic:
by
  refine (lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)
  · rintro ⟨a', b'⟩ h'
    dsimp [Option.guard]
    split_ifs
    · subst a'
      simp [nd.eq_of_mk_mem h h']
    · simp_all
    · simp_all
    · rfl
  · simp

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

Goal state before:
pp: case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

Tactic:
by_cases h₁ : a = ah

Goal state after:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : a = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
h : a ≠ a'
tl : List (Sigma β)
ih : dlookup a (kerase a' tl) = dlookup a tl
ah : α
bh : β ah
h₁ : ¬a = ah
⊢ dlookup a (kerase a' (⟨ah, bh⟩ :: tl)) = dlookup a (⟨ah, bh⟩ :: tl)
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
⊢ a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys

Tactic:
induction l₁ generalizing l₂ with

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

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

Tactic:
induction l₁ generalizing l₂ with

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₁

Tactic:
induction l₁ generalizing l₂ with

Goal state after:
Module: Mathlib.Data.Finset.PiInduction

Goal state before:
pp: case intro.a.inl
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
he : univ.sigma f = ∅
⊢ p f

pp: case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f

Tactic:
· convert! h0 using 1
    simpa [funext_iff] using he

Goal state after:
case intro.a.inr
ι : Type u_1
α : ι → Type u_2
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (α i)
r : (i : ι) → α i → Finset (α i) → Prop
H_ex : ∀ (i : ι) (s : Finset (α i)), s.Nonempty → ∃ x ∈ s, r i x (s.erase x)
p : ((i : ι) → Finset (α i)) → Prop
h0 : p fun x ↦ ∅
step : ∀ (g : (i : ι) → Finset (α i)) (i : ι) (x : α i), r i x (g i) → p g → p (update g i (insert x (g i)))
val✝ : Fintype ι
f : (i : ι) → Finset (α i)
ihs : ∀ t ⊂ univ.sigma f, ∀ (f : (i : ι) → Finset (α i)), univ.sigma f = t → p f
hne : (univ.sigma f).Nonempty
⊢ p f
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : ¬a ∈ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₂

Tactic:
induction l₁ generalizing l₂ with

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
⊢ b ∈ dlookup a (l₁.kunion l₂) ↔ b ∈ dlookup a l₁ ∨ ¬a ∈ l₁.keys ∧ b ∈ dlookup a l₂

Tactic:
induction l₁ generalizing l₂ with

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

Goal state before:
pp: case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ f.toAList.lookupFinsupp a = f a

Tactic:
suffices f.toAList.lookup a = none by simp [h, this]

Goal state after:
case pos
α : Type u_1
M : Type u_2
inst✝ : Zero M
f : α →₀ M
a : α
h : f a = 0
⊢ lookup a f.toAList = none
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
suffices CPRankMax (m + n + 1) (x₁ + (x₂ + y)) by
      simpa only [add_comm, add_assoc, add_left_comm] using this

Goal state after:
α : Type
ds : List ℕ
inst✝¹ : Mul α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n + 1) (x₁ + (x₂ + y))
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor]

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

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

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor]

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

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

Tactic:
simp only [bitwise, natBitwise, Bool.not_false, Bool.bne_eq_xor,
      cond_false, cond_true, negSucc.injEq, Bool.false_xor,
      Bool.true_xor, Bool.not_true,
      Int.xor, HXor.hXor, XorOp.xor, Nat.xor]

Goal state after:
case negSucc.negSucc
m n : ℕ
⊢ ↑(Nat.bitwise (fun x y ↦ !x ^^ !y) m n) = ↑(Nat.bitwise xor m n)
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: a : Bool
m : ℤ
b : Bool
n : ℤ
⊢ (bit a m).land (bit b n) = bit (a && b) (m.land n)

Tactic:
rw [← bitwise_and, bitwise_bit]

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

Goal state before:
pp: n m l : ℕ
⊢ filter (fun x ↦ decide (x < l)) (Ico n m) = Ico n (min m l)

Tactic:
rcases le_total m l with hml | hlm
  · rw [min_eq_left hml, filter_lt_of_top_le hml]
  · rw [min_eq_right hlm, filter_lt_of_ge hlm]

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

Goal state before:
pp: case intro
α : 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 : List α
acb : Acc (Shortlex r) b
ih : ∀ (s : List α), s.length < (xa :: b).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (xa :: b)

Tactic:
induction acb with

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

Goal state before:
pp: α : Type u_1
w : List α
p : ℕ
per : w.HasPeriod p
⊢ drop p w <+: w

Tactic:
by
  rw [← prefix_append_right_inj (take p w)]
  simp_all [HasPeriod, take_append_drop]

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

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

Tactic:
rw [h]
    exact mulRightLinearMap_zero_eq_zero _ _

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

Goal state before:
pp: k n m : ℕ
⊢ (k * n).dist (k * m) = k * n.dist m

Tactic:
mul_comm k n,

Goal state after:
k n m : ℕ
⊢ (n * k).dist (k * m) = k * n.dist m
Module: Mathlib.Data.Nat.Factorization.Root

Goal state before:
pp: a n : ℕ
⊢ ¬(n ≠ 0 ∧ a ≠ 0) ↔ n = 0 ∨ a = 0

Tactic:
by simp only [not_and_or, ne_eq, not_not]

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

Goal state before:
pp: n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑(m.choose 1) ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ False

Tactic:
choose_one_right

Goal state after:
n p : ℕ
hp : Fact (Nat.Prime p)
hn : 0 < n
hn₀ : n ≠ p ^ multiplicity p n
m : ℕ
h : ↑m ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ False
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
n : ℕ
h : nth p n ≠ 0
hf : (Set.ofPred p).Finite
⊢ n < #hf.toFinset

Tactic:
simp only [ne_eq, nth_eq_zero, not_or, not_exists, not_le] at h

Goal state after:
p : ℕ → Prop
n : ℕ
hf : (Set.ofPred p).Finite
h : ¬(p 0 ∧ n = 0) ∧ ∀ (x : (Set.ofPred p).Finite), n < #x.toFinset
⊢ n < #hf.toFinset
Module: Mathlib.Data.Num.Prime

Goal state before:
pp: n k : PosNum
h : ↑n < ↑k.bit1 * ↑k.bit1
⊢ ↑n = if ↑n < ↑k.bit1 * ↑k.bit1 then ↑n else if ↑k.bit1 ∣ ↑n then ↑k.bit1 else (↑n).minFacAux (↑k.bit1 + 2)

Tactic:
simp only [h, ite_true]

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

Goal state before:
pp: case nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
⊢ Ordnode α

Tactic:
rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
      · cases id rr
        · exact node 2 nil x r
        · exact node 3 (ι x) rx rr
      · rcases id rr with _ | rrs
        · exact node 3 (ι x) rlx ι rx
        · exact
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) nil x rl) rx rr
            else
              node (rs + 1) (node (size rll + 1) nil x rll) rlx
                (node (size rlr + rrs + 1) rlr rx rr)

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑(-↑p) = -↑p

Tactic:
Int.cast_neg,

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ -↑↑p = -↑p
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case pos
α : 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
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz l.size ml.size ∧ BalancedSz mr.size r.size ∧ BalancedSz (l.size + ml.size + 1) (mr.size + r.size + 1)

Tactic:
rw [l1, r1]

Goal state after:
case pos
α : 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
mm : ml.size + mr.size ≤ 1
r1 : r.size = 1
l1 : l.size = 1
⊢ BalancedSz 1 ml.size ∧ BalancedSz mr.size 1 ∧ BalancedSz (1 + ml.size + 1) (mr.size + 1 + 1)
Module: Mathlib.Data.PFunctor.Univariate.M

Goal state before:
pp: case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
⊢ ∀ (a'' : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))),
    a ≍ a'' → children' (CofixA.intro (head' (x.approx 1)) ch) a'' = ch a

Tactic:
intro _ hh

Goal state after:
case succ.intro
F : PFunctor.{uA, uB}
x : F.M
n : ℕ
a✝ : Approx.sMk x.dest n = x.approx n
hd : F.A
h' : hd = head' (x.approx 1)
ch : F.B (head' (x.approx 1)) → CofixA F n
h : x.approx n.succ = CofixA.intro (head' (x.approx 1)) ch
a : F.B (head' (x.approx 1))
a''✝ : F.B (head' (CofixA.intro (head' (x.approx 1)) ch))
hh : a ≍ a''✝
⊢ children' (CofixA.intro (head' (x.approx 1)) ch) a''✝ = ch a
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
r' : ℕ
H1 : BalancedSz l' r'
H2 : l.size.dist l' ≤ 1 ∧ r.size = r' ∨ r.size.dist r' ≤ 1 ∧ l.size = l'
⊢ r.size ≤ 3 * (l.size + 1)

Tactic:
rcases H2 with (⟨hl, rfl⟩ | ⟨hr, rfl⟩)

Goal state after:
case inl
α : Type u_2
l : Ordnode α
l' : ℕ
r : Ordnode α
hl : l.size.dist l' ≤ 1
H1 : BalancedSz l' r.size
⊢ r.size ≤ 3 * (l.size + 1)

case inr
α : Type u_2
l r : Ordnode α
r' : ℕ
hr : r.size.dist r' ≤ 1
H1 : BalancedSz l.size r'
⊢ r.size ≤ 3 * (l.size + 1)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Emem x_1 (node size✝ l x r) ∧ P x_1

Tactic:
simp only [Emem]

Goal state after:
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
t : Ordnode α
⊢ Emem x t ↔ x ∈ t.toList

Tactic:
by
  unfold Emem; induction t <;> simp [Any, *]

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

Goal state before:
pp: p q : ℕ+ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ { n // p n ∧ ∀ (m : ℕ+), m < n → ¬p m }

Tactic:
have : ∃ (n' : ℕ) (n : ℕ+) (_ : n' = n), p n := Exists.elim h fun n hn => ⟨n, n, rfl, hn⟩
  have n := Nat.findX this
  refine ⟨⟨n, ?_⟩, ?_, fun m hm pm => ?_⟩
  · obtain ⟨n', hn', -⟩ := n.prop.1
    rw [hn']
    exact n'.prop
  · obtain ⟨n', hn', pn'⟩ := n.prop.1
    simpa [hn', Subtype.coe_eta] using! pn'
  · exact n.prop.2 m hm ⟨m, rfl, pm⟩

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

Goal state before:
pp: case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ (m * n.divExact m).factorMultiset

Tactic:
factorMultiset_mul

Goal state after:
case mpr
m n : ℕ+
h : m ∣ n
⊢ m.factorMultiset ≤ m.factorMultiset + (n.divExact m).factorMultiset
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case neg
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : ¬rls < ratio * rrs
⊢ nil.node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
simp [node4L, node', sr.2.1.1]; abel

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

Goal state before:
pp: α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
this : delta * Nat.succ 0 < rs
⊢ delta ≤ rl.size + rr.size

Tactic:
sr.1,

Goal state after:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : delta * ls < rs
this : delta * Nat.succ 0 < rl.size + rr.size + 1
⊢ delta ≤ rl.size + rr.size
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rs ≤ 1
⊢ rl.size = 0 ∧ rr.size = 0

Tactic:
sr.1,

Goal state after:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
sr : (node rs rl rx rr).Sized
sl : nil.Sized
H1 : nil.size = 0 → (node rs rl rx rr).size ≤ 1
H2 : 1 ≤ nil.size → 1 ≤ (node rs rl rx rr).size → (node rs rl rx rr).size ≤ delta * nil.size
this : rl.size + rr.size + 1 ≤ 1
⊢ rl.size = 0 ∧ rr.size = 0
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: case ind
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x y : (P F).W α
a : (P F).A
f' : (P F).drop.B a ⟹ α
f₀ f₁ : (P F).last.B a → (P F).W α
_h : ∀ (x : (P F).last.B a), WEquiv (f₀ x) (f₁ x)
ih : ∀ (x : (P F).last.B a), WEquiv (f₁ x) (f₀ x)
⊢ WEquiv ((P F).wMk a f' f₁) ((P F).wMk a f' f₀)

Tactic:
exact WEquiv.ind _ _ _ _ ih

Goal state after:
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inl
z : ℤ
hn : z < 0
⊢ -1 = ↑(-1)

Tactic:
Int.cast_neg,

Goal state after:
case inl
z : ℤ
hn : z < 0
⊢ -1 = -↑1
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: case inr.inl
r : ℝ
hz : r.sign = 0
⊢ r.sign⁻¹ = r.sign

pp: case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign

Tactic:
· rw [hz]
    exact inv_zero

Goal state after:
case inr.inr
r : ℝ
hp : r.sign = 1
⊢ r.sign⁻¹ = r.sign
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
exact terminates_parallel.aux a T

Goal state after:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inl
α : Type u
S✝ : WSeq (Computation α)
c✝ : Computation α
h : c✝ ∈ S✝
T✝ : c✝.Terminates
n : ℕ
IH :
  ∀ (l : List (Computation α)) (S : Stream'.Seq (Option (Computation α))) (c : Computation α),
    c ∈ l ∨ some (some c) = S.get? n → c.Terminates → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : Stream'.Seq (Option (Computation α))
c : Computation α
T : c.Terminates
a : c ∈ l
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
exact terminates_parallel.aux a T

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

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → LE (α i)
a b : (i : ι) × α i
⊢ (∃ h, h ▸ a.snd ≤ b.snd) → a ≤ b

Tactic:
obtain ⟨i, a⟩ := a
    obtain ⟨j, b⟩ := b
    rintro ⟨rfl : i = j, h⟩
    exact LE.fiber _ _ _ h

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

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ ⟨i, a⟩ ≤ ⟨i, b⟩ ∧ ¬⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
mk_le_mk_iff,

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ a ≤ b ∧ ¬⟨i, b⟩ ≤ ⟨i, a⟩
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ a ≤ b ∧ ¬⟨i, b⟩ ≤ ⟨i, a⟩

Tactic:
mk_le_mk_iff,

Goal state after:
case mp
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
i : ι
a b : α i
hab : a < b
⊢ a ≤ b ∧ ¬b ≤ a
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil.hb
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬c₁ :: cs₁ < []

Tactic:
apply not_lt_of_gt; apply List.nil_lt_cons

Goal state after:
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case r
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ ∃ s S_1, map f S.join = s.append (map f S_1.join) ∧ (map (map f) S).join = s.append (map (map f) S_1).join

Tactic:
exact ⟨nil, S, by simp, by simp⟩

Goal state after: