mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case pos
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' ℕ∪{∞})
hS' : Nonempty ↑S'.toTop
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p

Tactic:
have : Mono (LightProfinite.fibreIncl ∞ (π' ≫ snd _ _)) := by
      rw [CompHausLike.mono_iff_injective]
      exact Subtype.val_injective
    have : Nonempty (LightProfinite.fibre ∞ (π' ≫ snd _ _)) := by
      obtain ⟨x, hx⟩ := (.comp ((fun y ↦ ⟨(Nonempty.some inferInstance, y), rfl⟩))
        ((LightProfinite.epi_iff_surjective _).mp hπ') : ((snd S' ℕ∪{∞}) ∘ π').Surjective) ∞
      exact ⟨x, by simpa using hx⟩
    obtain ⟨r_inf, hr⟩ := Injective.factors (𝟙 _) (LightProfinite.fibreIncl ∞ (π' ≫ snd _ _))
    let hπ'' : RegularEpi <| lightProfiniteToLightCondSet.map π' :=
      regularEpiOfEpi _
    have : EffectiveEpi π' := by
      rw [LightProfinite.effectiveEpi_iff_surjective, ← LightProfinite.epi_iff_surjective]
      infer_instance
    let hπ' : RegularEpi <| lightProfiniteToLightCondSet.map π' :=
      regularEpiOfPreserves π' _ (pullback.cone _ _) (pullback.isLimit _ _)
    -- Use the effective epimorphism to descend the map from `T'` to `S' ⊗ ℕ∪{∞}`
    have hc := Limits.isColimitOfPreserves (free R) hπ'.isColimit
    refine ⟨hc.desc (cocone R π' ((lightProfiniteToLightCondSet ⋙ free R).map g' ≫ g)
      r_inf split.section_ hr), ?_⟩
    rw [← cancel_epi ((lightProfiniteToLightCondSet ⋙ free R).map π'),
      ← Functor.comp_map, ← map_comp_assoc]
    change _ = (((free R).mapCocone _).ι.app .one ≫
      hc.desc (cocone R π' _ r_inf split.section_ hr)) ≫ p
    -- Because the top in the square above is epic, proving that the lower
    -- triangle commutes is equivalent to proving that the upper triangle
    -- commutes, which is true by the universal property of the colimit.
    rw [hc.fac]
    -- simp? [← comm] says:
    simp only [Limits.parallelPair_obj_one, Functor.comp_map, Functor.map_comp,
      assoc, cocone_ι_app, eqToHom_refl, Preadditive.comp_add, Preadditive.comp_sub,
      id_comp, Preadditive.add_comp, Preadditive.sub_comp, ← comm]
    simp only [← Functor.map_comp, ← Functor.comp_map, ← assoc, ← comp]
    symm
    rw [sub_add, sub_eq_self, sub_eq_zero]
    simp only [Category.assoc]
    have : LightProfinite.fibreIncl ∞ (π' ≫ snd _ _) ≫ π' =
        LightProfinite.fibreIncl ∞ (π' ≫ snd _ _) ≫ π' ≫ fst _ _ ≫
          lift (𝟙 _) (const S' (∞ : ℕ∪{∞})) :=
      CartesianMonoidalCategory.hom_ext _ _ rfl (by ext a; exact a.prop)
    rw [reassoc_of% this, reassoc_of% split.id]

Goal state after:
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'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
· simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
      exact (lookupAll_sublist a l).cons _

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

Goal state before:
pp: case mp
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
a : γ✝
⊢ (∃ i ∈ u, ∃ a_1, (∃ i ∈ t, ∃ a ∈ s, i a = a_1) ∧ i a_1 = a) →
    ∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_2 ∈ s, i a_2 = a

Tactic:
rintro ⟨g, hg, b, ⟨f, hf, a, ha, rfl⟩, rfl⟩

Goal state after:
case mp
α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ γ✝ : Type u_1
s : Finset α✝
t : Finset (α✝ → β✝)
u : Finset (β✝ → γ✝)
g : β✝ → γ✝
hg : g ∈ u
f : α✝ → β✝
hf : f ∈ t
a : α✝
ha : a ∈ s
⊢ ∃ i, (∃ i_1, (∃ a ∈ u, comp a = i_1) ∧ ∃ a ∈ t, i_1 a = i) ∧ ∃ a_1 ∈ s, i a_1 = g (f a)
Module: Mathlib.Data.Finsupp.Sigma

Goal state before:
pp: κ : Type u_1
ι : κ → Type u_2
M : Type u_3
inst✝ : Zero M
k : κ
f : ι k →₀ M
⊢ f.embSigma.split k = f

Tactic:
ext i
  simp [split_apply]

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

Goal state before:
pp: i : ℕ
hn : ¬i + 1 = 0
⊢ fib (-↑(i + 1) + 1) * fib (-↑(i + 1) - 1) - fib (-↑(i + 1)) ^ 2 = (-1) ^ (-↑(i + 1)).natAbs

Tactic:
simp_rw [show -((i + 1 : ℕ) : ℤ) + 1 = -i by simp, sub_eq_add_neg, ← neg_add, fib_neg,
      natAbs_neg, natAbs_natCast, ← fib_natCast_succ_mul_fib_natCast_pred_sub_fib_natCast_sq]

Goal state after:
i : ℕ
hn : ¬i + 1 = 0
⊢ ((if Even ↑i then -fib ↑i else fib ↑i) * if Even (↑(i + 1) + 1) then -fib (↑(i + 1) + 1) else fib (↑(i + 1) + 1)) +
      -(if Even ↑(i + 1) then -fib ↑(i + 1) else fib ↑(i + 1)) ^ 2 =
    fib (↑(i + 1) + 1) * fib (↑(i + 1) - 1) - fib ↑(i + 1) ^ 2
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b ^ 2

Tactic:
sq

Goal state after:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ a * a = b * b
Module: Mathlib.Data.Int.Lemmas

Goal state before:
pp: a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b ^ 2

Tactic:
sq

Goal state after:
a b : ℤ
⊢ a.natAbs < b.natAbs ↔ a * a < b * b
Module: Mathlib.Data.Int.Lemmas

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

Tactic:
sq

Goal state after:
a b : ℤ
⊢ a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
Module: Mathlib.Data.Int.Bitwise

Goal state before:
pp: m n : ℤ
k : ℕ
⊢ (m.land n).testBit k = (m.testBit k && n.testBit k)

Tactic:
rw [← bitwise_and, testBit_bitwise]

Goal state after:
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:
rw [hlp]
          exact chineseRemainderOfList_lt_prod _ _ _ _
            (by simpa [List.Perm.mem_iff hl.symm] using hs)

Goal state after:
Module: Mathlib.Data.Nat.Fib.Zeckendorf

Goal state before:
pp: n : ℕ
⊢ (n + 1).zeckendorf.IsZeckendorfRep

Tactic:
by
    rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]
    refine (isZeckendorfRep_zeckendorf _).cons (fun a ha ↦ ?_)
    obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
    · simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
      subst ha
      exact le_greatestFib.2 le_add_self
    rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha
    subst a
    exact add_le_of_le_tsub_right_of_le (le_greatestFib.2 le_add_self)
      (greatestFib_sub_fib_greatestFib_le_greatestFib n.succ_ne_zero)

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

Goal state before:
pp: case zero
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}
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ f 0 ≤ nth p 0

Tactic:
Nat.nth_zero

Goal state after:
case zero
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}
hn : ∀ (hf : (Set.ofPred p).Finite), 0 < #hf.toFinset
⊢ f 0 ≤ sInf (Set.ofPred p)
Module: Mathlib.Data.Ordmap.Ordnode

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

Tactic:
· rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

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

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

Tactic:
rcases rl with _ | ⟨_, _, rlx⟩

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

case nil.node.nil.node
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
rs : ℕ
rx : α
rr : Ordnode α
size✝ : ℕ
l✝ : Ordnode α
rlx : α
r✝ : Ordnode α
⊢ Ordnode α
Module: Mathlib.Data.Ordmap.Ordnode

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

Tactic:
· rcases id lr with _ | ⟨lrs, lrl, lrx, lrr⟩
        · exact node 3 ll lx ι x
        · exact
            if lrs < ratio * lls then node (ls + 1) ll lx (node (lrs + 1) lr x nil)
            else
              node (ls + 1) (node (lls + size lrl + 1) ll lx lrl) lrx
                (node (size lrr + 1) lrr x nil)

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
⊢ count p (nth p 0) = 0

Tactic:
rw [count_eq_card_filter_range, card_eq_zero, filter_eq_empty_iff, nth_zero]
  exact fun n h₁ h₂ => (mem_range.1 h₁).not_ge (Nat.sInf_le h₂)

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

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ nth p n = 0

Tactic:
nth_of_card_le ((finite_toSet _).subset this)

Goal state after:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ 0 = 0

p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : Set.ofPred p ⊆ ↑(range n)
⊢ #⋯.toFinset ≤ n
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.inl
α : 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 : (Ordnode.node s ml z mr).size = 1
r0 : r.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 [hm.2.size_eq, Nat.succ_inj, add_eq_zero] at m1
    rw [l0, m1.1, m1.2]; revert r0; rcases size r with (_ | _ | _) <;>
      [decide; decide; (intro r0; unfold BalancedSz delta; lia)]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
a : ZNum
⊢ ↑(0 + a) = ↑0 + ↑a

Tactic:
by cases a <;> exact (_root_.zero_add _).symm

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

Goal state before:
pp: case succ
F : PFunctor.{uA, uB}
n : ℕ
n_ih : ∀ (x : CofixA F n) (y : CofixA F n.succ), Agree x y → truncate y = x
x : CofixA F (n + 1)
y : CofixA F (n + 1).succ
h : Agree x y
⊢ truncate y = x

Tactic:
cases h with

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

Goal state before:
pp: ⊢ ∀ (a b : Num), ↑(a.gcd b) = (↑a).gcd ↑b

Tactic:
have : ∀ a b : Num, (a * b).natSize ≤ a.natSize + b.natSize := by
    intros
    simp only [natSize_to_nat, cast_mul]
    rw [Nat.size_le, pow_add]
    exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)
  intros
  unfold gcd
  split_ifs with h
  · exact gcd_to_nat_aux h (this _ _)
  · rw [Nat.gcd_comm]
    exact gcd_to_nat_aux (le_of_not_ge h) (this _ _)

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

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun fx = dropFun fy
i : (P.B ax).last
h₁ : ((TypeVec.id ::: Quot.mk R) ⊚ fx) Fin2.fz i = ((TypeVec.id ::: Quot.mk R) ⊚ fy) Fin2.fz i
⊢ R (lastFun fx i) (lastFun fy i)

Tactic:
simp only [TypeVec.comp, appendFun, splitFun] at h₁

Goal state after:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
R : P.M α → P.M α → Prop
h₀ : Equivalence R
x y : P.M α
ax : P.A
fx fy : P.B ax ⟹ α ::: P.M α
Hdrop : dropFun fx = dropFun fy
i : (P.B ax).last
h₁ : Quot.mk R (fx Fin2.fz i) = Quot.mk R (fy Fin2.fz i)
⊢ R (lastFun fx i) (lastFun fy i)
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ l.toList ++ x :: foldr List.cons r r' = (node size✝ l x r).toList ++ r'

Tactic:
foldr_cons_eq_toList r,

Goal state after:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ l.toList ++ x :: (r.toList ++ r') = (node size✝ l x r).toList ++ r'
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node s l x r).toList = l.toList ++ x :: r.toList

Tactic:
rw [toList, foldr, foldr_cons_eq_toList]

Goal state after:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (match ll.splitMin' lx lr with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x✝ (node ls ll lx lr) x r).eraseMin)

Tactic:
splitMin_eq ls ll lx lr,

Goal state after:
α : Type u_1
x✝ ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
x : α
r : Ordnode α
⊢ (match (ll.findMin' lx, (node ls ll lx lr).eraseMin) with
    | (xm, l') => (xm, l'.balanceR x r)) =
    ((node ls ll lx lr).findMin' x, (node x✝ (node ls ll lx lr) x r).eraseMin)
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: n m : ℕ+
⊢ (n * m).factorMultiset = n.factorMultiset + m.factorMultiset

Tactic:
by
  let u := factorMultiset n
  let v := factorMultiset m
  have : n = u.prod := (prod_factorMultiset n).symm; rw [this]
  have : m = v.prod := (prod_factorMultiset m).symm; rw [this]
  rw [← PrimeMultiset.prod_add]
  repeat' rw [PrimeMultiset.factorMultiset_prod]

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

Goal state before:
pp: case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : m + 1 < PNat.find h₂ + 1
⊢ ¬p (m + 1)

Tactic:
simp only [add_lt_add_iff_right, lt_find_iff] at hm

Goal state after:
case succ
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h1 : ¬p 1
m : ℕ+
a✝ : m < PNat.find h₂ + 1 → ¬p m
hm : ∀ (m_1 : ℕ+), m_1 ≤ m → ¬p (m_1 + 1)
⊢ ¬p (m + 1)
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ : α a₁
a₂ : ι
b₂ : α a₂
hlt₁ : a₁ < a₂
hlt₂ : a₂ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩

pp: case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

Tactic:
· exact (lt_irrefl a₁ <| hlt₁.trans hlt₂).elim

Goal state after:
case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case left.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂ : α a₁
hlt₁ : a₁ < a₁
hlt₂ : b₂ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂⟩

pp: case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

pp: case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

Tactic:
· exact (lt_irrefl a₁ hlt₁).elim

Goal state after:
case right.left
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : a₁ < a₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩

case right.right
ι : Type u_1
α : ι → Type u_2
inst✝¹ : PartialOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a₁ : ι
b₁ b₂✝ : α a₁
hlt₁ : b₁ ≤ b₂✝
hlt₂ : b₂✝ ≤ b₁
⊢ ⟨a₁, b₁⟩ = ⟨a₁, b₂✝⟩
Module: Mathlib.Data.PSigma.Order

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Preorder ι
inst✝³ : DenselyOrdered ι
inst✝² : ∀ (i : ι), Nonempty (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), DenselyOrdered (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩

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

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMaxOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩

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

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : a < b
⊢ ∃ a_1, ⟨i, a⟩ < a_1 ∧ a_1 < ⟨i, b⟩

Tactic:
obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩

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

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

Tactic:
simp only [map, size_nil, and_true]; apply valid'_nil
    cases a₁; · trivial
    cases a₂; · trivial
    simp only [Option.map, Bounded]
    exact f_strict_mono h.ord

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

Goal state before:
pp: case mp
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ Liftr r x y → ∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)

pp: case mpr
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ (∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)) → Liftr r x y

Tactic:
· rintro ⟨u, xeq, yeq⟩
    rcases h : repr u with ⟨a, f⟩
    use a, fun i => (f i).val.fst, fun i => (f i).val.snd
    constructor
    · rw [← xeq, ← abs_repr u, h, ← abs_map]
      rfl
    constructor
    · rw [← yeq, ← abs_repr u, h, ← abs_map]
      rfl
    intro i
    exact (f i).property

Goal state after:
case mpr
F : Type u → Type v
q : QPF F
α : Type u
r : α → α → Prop
x y : F α
⊢ (∃ a f₀ f₁, x = abs ⟨a, f₀⟩ ∧ y = abs ⟨a, f₁⟩ ∧ ∀ (i : (P F).B a), r (f₀ i) (f₁ i)) → Liftr r x y
Module: Mathlib.Data.Ordmap.Ordset

Goal state before:
pp: case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ (t_l.balanceL t_x (erase x t_r)).size = (node size✝ t_l t_x t_r).size - 1

Tactic:
rw [size_balanceL h.left.bal t_r_valid.bal h.left.sz t_r_valid.sz
          (Or.inr (Exists.intro t_r.size (And.intro t_r_size h.bal.1)))]

Goal state after:
case node.gt
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLE α
x : α
size✝ : ℕ
t_l : Ordnode α
t_x : α
t_r : Ordnode α
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (node size✝ t_l t_x t_r) a₂
h_mem : mem x t_r = true
t_ih_r : (erase x t_r).size = t_r.size - 1
t_r_valid : Valid' (↑t_x) (erase x t_r) a₂
t_r_size : Raised (erase x t_r).size t_r.size
⊢ t_l.size + (erase x t_r).size + 1 = (node size✝ t_l t_x t_r).size - 1
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
rw [H2]

Goal state after:
case inr
α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
c : Computation α
T : c.Terminates
s : Computation α
IH : ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, s ∈ l → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
m : s.think ∈ l
H1 : ∀ (l' : List (Computation α)), parallel.aux2 l = Sum.inr l' → s ∈ l'
l' : List (Computation α)
h : parallel.aux2 l = Sum.inr l'
H2 :
  corec parallel.aux1 (l, S) =
    (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think
⊢ (corec parallel.aux1
        (match Seq.destruct S with
        | none => (l', Seq.nil)
        | some (none, S') => (l', S')
        | some (some c, S') => (c :: l', S'))).think.Terminates
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (a, s') ∈ t.head

Tactic:
dst.left

Goal state after:
case some.some
α : Type u
s t : WSeq α
h : s ~ʷ t
o : Option α
ho : o ∈ s.head
l : ∀ {a : Option (α × WSeq α)}, a ∈ s.destruct → ∃ b ∈ t.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
r : ∀ {b : Option (α × WSeq α)}, b ∈ t.destruct → ∃ a ∈ s.destruct, BisimO (fun x1 x2 ↦ x1 ~ʷ x2) a b
a : α
s' : WSeq α
dsm : some (a, s') ∈ s.destruct
dse : Prod.fst <$> some (a, s') = o
b : α
t' : WSeq α
dtm : some (b, t') ∈ t.destruct
dst : BisimO (fun x1 x2 ↦ x1 ~ʷ x2) (some (a, s')) (some (b, t'))
⊢ Prod.fst <$> some (b, s') ∈ t.head
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case h1
α : Type u
s : WSeq α
a : α
h : a ∈ s
⊢ ∀ (b : α) (s' : WSeq α), (a = b ∨ ∃ n, some a ∈ s'.get? n) → ∃ n, some a ∈ (cons b s').get? n

Tactic:
intro a' s' h
    rcases h with h | h
    · exists 0
      simp only [get?, drop, head_cons]
      rw [h]
      apply ret_mem
    · obtain ⟨n, h⟩ := h
      exists n + 1
      simpa [get?]

Goal state after: