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

Goal state before:
pp: case neg
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 h : IsEmpty (S' ⊗ ℕ∪{∞}) := isEmpty_prod.mpr <| Or.inl <| by simpa using hS'

Goal state after:
case neg
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
h : IsEmpty (↑S'.toTop ⊗ ↑ℕ∪{∞}.toTop)
⊢ ∃ g', (free R).map (lightProfiniteToLightCondSet.map (y' ▷ ℕ∪{∞})) ≫ f = g' ≫ p
Module: Mathlib.Data.List.Sigma

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys
⊢ (lookupAll a l).length ≤ 1

Tactic:
have := Nodup.sublist ((lookupAll_sublist a l).map _) h
  rw [map_map] at this
  rwa [← nodup_replicate, ← map_const]

Goal state after:
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s₁ s₂ : Finmap β
a₁ a₂ : AList β
⊢ insert a b (⟦a₁⟧ ∪ ⟦a₂⟧) = insert a b ⟦a₁⟧ ∪ ⟦a₂⟧

Tactic:
by simp [AList.insert_union]

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

Goal state before:
pp: α β : Type u
inst✝ : (P : Prop) → Decidable P
α✝ β✝ : Type u_1
s : Finset α✝
t : Finset β✝
⊢ s *> t = const α✝ id <$> s <*> t

Tactic:
by
      rw [seq_def, fmap_def, seqRight_def]
      obtain rfl | hs := s.eq_empty_or_nonempty
      · rw [if_pos rfl, image_empty, sup_empty, bot_eq_empty]
      · ext a
        rw [if_neg hs.ne_empty, mem_sup]
        refine ⟨fun ha => ⟨id, mem_image_const_self.2 hs, by rwa [image_id]⟩, ?_⟩
        rintro ⟨f, hf, ha⟩
        rw [mem_image] at hf ha
        obtain ⟨b, hb, rfl⟩ := ha
        obtain ⟨_, _, rfl⟩ := hf
        exact hb

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ List.Pairwise (Disjoint on Finsupp.support) l

Tactic:
← List.pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint hn

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid M
l : List (ι →₀ M)
hn : l.Nodup
hs : (↑l.toFinset).PairwiseDisjoint Finsupp.support
⊢ (↑l.toFinset).PairwiseDisjoint Finsupp.support
Module: Mathlib.Data.Int.Bitwise

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

Tactic:
rw [← bitwise_or, testBit_bitwise]

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

Goal state before:
pp: case pos
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : p hd = true
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

pp: case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : ¬p hd = true
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true

Tactic:
· simp only [h_p_hd, length_cons, Nat.zero_lt_succ, getElem_cons_zero, not_true_eq_false,
        imp_false, iff_false]
      intro h
      replace h := congrArg length h
      have := length_dropWhile_le p tl
      simp at h
      lia

Goal state after:
case neg
α : Type u_1
p : α → Bool
hd : α
tl : List α
h_p_hd : ¬p hd = true
⊢ (match p hd with
      | true => dropWhile p tl
      | false => hd :: tl) =
      hd :: tl ↔
    ∀ (hl : 0 < (hd :: tl).length), ¬p (hd :: tl)[0] = true
Module: Mathlib.Data.List.Intervals

Goal state before:
pp: n m l : ℕ
⊢ Ico n m ∩ Ico m l = []

Tactic:
by
  apply eq_nil_iff_forall_not_mem.2
  intro a
  simp only [and_imp, not_and, not_lt, List.mem_inter_iff, List.Ico.mem]
  intro _ h₂ h₃
  exfalso
  exact not_lt_of_ge h₃ h₂

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 l m) = Ico l m

Tactic:
filter_le_of_le_bot (le_refl l),

Goal state after:
case inl
n m l : ℕ
hnl : n ≤ l
hlm : l ≤ m
⊢ [] ++ Ico l m = Ico l m
Module: Mathlib.Data.List.Shortlex

Goal state before:
pp: case intro.intro.inr.nil
α : Type u_1
r : α → α → Prop
a xa : α
h✝¹ : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α},
        Acc (Shortlex r) b →
          (∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s) → Acc (Shortlex r) (y :: b)
b xb : List α
h✝ : ∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y
ihb :
  ∀ (y : List α),
    Shortlex r y xb → (∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s) → Acc (Shortlex r) (xa :: y)
ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s
lt : Shortlex r [] (xa :: xb)
h2len : [].length = (xa :: xb).length
⊢ Acc (Shortlex r) []

Tactic:
simp at h2len

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

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

Tactic:
simp_all [getElem_append_right, IsPrefix.getElem pref, min_eq_left_of_lt]

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

Goal state before:
pp: case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
⊢ w.HasPeriod p

Tactic:
rw [hasPeriod_iff_getElem?]

Goal state after:
case mpr
α : Type u_1
p : ℕ
w : List α
mod : ∀ i < w.length, w[i]? = w[i % p]?
⊢ ∀ i < w.length - p, w[i]? = w[i + p]?
Module: Mathlib.Data.List.SplitBy

Goal state before:
pp: case h_2.hgs
α : Type u_1
r : α → α → Bool
b : α
l : List α
IH :
  ∀ {a : α} {g : List α} {gs : List (List α)},
    ¬[] ∈ gs →
      IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) gs →
        (∀ (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) (splitBy.loop r l a g gs)
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
x✝ : Bool
heq✝ : r a b = false
⊢ IsChain (fun b a ↦ ∃ ha hb, r (a.getLast ha) (b.head hb) = false) ((g.reverse ++ [a]) :: gs)

Tactic:
apply isChain_cons.2 ⟨hga, hgs⟩

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

Goal state before:

Tactic:
w[q + i]? = w[i + q]? := congrArg (getElem? w) (add_comm q i)
     _ = w[i]? := (per_q i (by lia)).symm
     _ = w[i + (k + q)]? := per_plus i (by lia)
     _ = w[q + (i + k)]? := congr_arg (getElem? w) (by lia)

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✝² : Semiring R
inst✝¹ : Fintype m₁
inst✝ : Fintype m₂
B₁ : Matrix m₁ n R
B₂ : Matrix m₂ n R
v₁ : m₁ → R
v₂ : m₂ → R
x✝ : n
⊢ (Sum.elim v₁ v₂ ᵥ* B₁.fromRows B₂) x✝ = (v₁ ᵥ* B₁ + v₂ ᵥ* B₂) x✝

Tactic:
simp [Matrix.vecMul, fromRows, dotProduct]

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

Goal state before:
pp: R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝² : Semiring R
inst✝¹ : Fintype n₁
inst✝ : Fintype n₂
A₁ : Matrix m n₁ R
A₂ : Matrix m n₂ R
B₁ : Matrix n₁ n R
B₂ : Matrix n₂ n R
⊢ A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

Tactic:
by
  ext
  simp [mul_apply]

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

Goal state before:
pp: case refine_1
α : 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
⊢ Z₂ + (Z₁ - Y₂) ≠ ∅

Tactic:
simpa [-not_and, not_and_or] using .inl hZ₂

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

Goal state before:
pp: case cons.mpr
a b m : ℕ
l : List ℕ
ih : List.Pairwise Coprime l → (a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i])
co : List.Pairwise Coprime (m :: l)
this : m.Coprime l.prod
⊢ (∀ (i : Fin (l.length + 1)), a ≡ b [MOD (m :: l).get i]) → a ≡ b [MOD m] ∧ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
intro h; exact ⟨h 0, fun i => h i.succ⟩

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

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

Tactic:
Finset.mem_antidiagonal

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
m : ℕ
k : ℕ × ℕ
hm : IsUnit ↑m !
hk : k.1 + k.2 = m
⊢ ↑(m.choose k.1) = ↑m ! * (↑k.1!)⁻¹ʳ * (↑k.2!)⁻¹ʳ
Module: Mathlib.Data.Num.ZNum

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

Tactic:
· simpa using IH.2

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

Goal state before:
pp: case neg.inr.refine_4
α : 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 : 2 * l.size ≤ ml.size + mr.size + 1
⊢ r.size ≤ delta * mr.size

Tactic:
exact Valid'.node4L_lemma₃ mr₁ mm₁

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

Goal state before:
pp: n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (n ^ m).factorMultiset = m • n.factorMultiset

Tactic:
rw [this, ← PrimeMultiset.prod_smul]

Goal state after:
n : ℕ+
m : ℕ
u : PrimeMultiset := n.factorMultiset
this : n = u.prod
⊢ (m • u).prod.factorMultiset = m • u.prod.factorMultiset
Module: Mathlib.Data.PNat.Factors

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

Tactic:
let u := factorMultiset n
  have : n = u.prod := (prod_factorMultiset n).symm
  rw [this, ← PrimeMultiset.prod_smul]
  repeat' rw [PrimeMultiset.factorMultiset_prod]

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

Goal state before:
pp: case node.nil.node.nil.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
llx : α
llr : Ordnode α
hl : ((node lls nil llx llr).node' lx nil).Balanced
sl : (node ls (node lls nil llx llr) lx nil).Sized
this : nil.size = 0 ∧ llr.size = 0
⊢ node 3 (node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx llr).node' lx nil).node' x nil
    else ((node lls nil llx llr).node' lx nil).rotateR x nil

Tactic:
cases sl.2.1.2.2.size_eq_zero.1 this.2

Goal state after:
case node.nil.node.nil.refl.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
llx : α
hl : ((node lls nil llx nil).node' lx nil).Balanced
sl : (node ls (node lls nil llx nil) lx nil).Sized
this : nil.size = 0 ∧ nil.size = 0
⊢ node 3 (node lls nil llx nil) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx nil).node' lx nil).node' x nil
    else ((node lls nil llx nil).node' lx nil).rotateR x nil
Module: Mathlib.Data.PSigma.Order

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

Tactic:
obtain ⟨b, h⟩ := exists_lt a

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ b, b < ⟨i, a⟩
Module: Mathlib.Data.Pi.Interval

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → DecidableEq (α i)
inst✝¹ : (i : ι) → PartialOrder (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) → α i
⊢ #(Ioo a b) = ∏ i, #(Icc (a i) (b i)) - 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

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

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
⊢ ∀ (a : (P F).A) (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ

Tactic:
a

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
α : TypeVec.{u} n
x : F α
i : Fin2 n
u : α i
h : ∀ ⦃P : (i : Fin2 n) → α i → Prop⦄, LiftP P x → P i u
a : (P F).A
⊢ ∀ (f : (P F).B a ⟹ α), abs ⟨a, f⟩ = x → u ∈ f i '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
⊢ ∀ (a a' : (P F).A) (f : (P F).B a ⟹ α) (f' : (P F).B a' ⟹ α),
    abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ (i : Fin2 n), f i '' univ = f' i '' univ

Tactic:
a

Goal state after:
case mp
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : SuppPreservation
α : TypeVec.{u} n
a : (P F).A
⊢ ∀ (a' : (P F).A) (f : (P F).B a ⟹ α) (f' : (P F).B a' ⟹ α),
    abs ⟨a, f⟩ = abs ⟨a', f'⟩ → ∀ (i : Fin2 n), f i '' univ = f' i '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
⊢ rec g <$> x = h <$> x → rec g (mk x) = h (mk x)

Tactic:
hyp'

Goal state after:
F : Type u → Type u
q : QPF F
α : Type u
g : F α → α
h : Fix F → α
hyp : ∀ (x : F (Fix F)), h (mk x) = g (h <$> x)
x✝ : Fix F
x : F (Fix F)
hyp' : rec g <$> x = h <$> x
⊢ rec g (mk x) = h (mk x)
Module: Mathlib.Data.QPF.Multivariate.Constructions.Fix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
⊢ (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x → rec g (mk x) = h (mk x)

Tactic:
hyp'

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : F (α ::: β) → β
h : Fix F α → β
hyp : ∀ (x : F (α ::: Fix F α)), h (mk x) = g ((TypeVec.id ::: h) <$$> x)
x✝ : Fix F α
x : F (α ::: Fix F α)
hyp' : (TypeVec.id ::: rec g) <$$> x = (TypeVec.id ::: h) <$$> x
⊢ rec g (mk x) = h (mk x)
Module: Mathlib.Data.Rat.Star

Goal state before:
pp: case e'_2
n : ℕ
hn₀ : n ≠ 0
hn : Even n
this : ∀ (x : ℚ), ∃ y, ↑y ^ n = x ^ n
⊢ (range fun x ↦ x ^ n) = ⇑NNRat.coeHom '' range fun x ↦ x ^ n

Tactic:
simp [subset_antisymm_iff, range_subset_iff, this]

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

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
⊢ ∀ (a : (P F).A) (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ

Tactic:
a

Goal state after:
case mp
F : Type u → Type u
q : QPF F
α : Type u
x : F α
u : α
h : ∀ ⦃p : α → Prop⦄, Liftp p x → p u
a : (P F).A
⊢ ∀ (f : (P F).B a → α), abs ⟨a, f⟩ = x → u ∈ f '' univ
Module: Mathlib.Data.QPF.Univariate.Basic

Goal state before:
pp: case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
⊢ ∀ (a a' : (P F).A) (f : (P F).B a → α) (f' : (P F).B a' → α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ

Tactic:
a

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h : SuppPreservation
α : Type u
a : (P F).A
⊢ ∀ (a' : (P F).A) (f : (P F).B a → α) (f' : (P F).B a' → α), abs ⟨a, f⟩ = abs ⟨a', f'⟩ → f '' univ = f' '' univ
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
lem1 :
  ∀ (l : List (Computation α)) (S : WSeq (Computation α)),
    (∃ a, parallel.aux2 l = Sum.inl a) → (corec parallel.aux1 (l, S)).Terminates
l : List (Computation α)
S : WSeq (Computation α)
c : Computation α
m : c ∈ l
T : c.Terminates
⊢ (corec parallel.aux1 (l, S)).Terminates

Tactic:
revert l S

Goal state after:
α : 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
⊢ ∀ {l : List (Computation α)} {S : WSeq (Computation α)}, c ∈ l → (corec parallel.aux1 (l, S)).Terminates
Module: Mathlib.Data.Set.Enumerate

Goal state before:
pp: case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ enumerate sel s (n + 1) = some a → a ∈ s

Tactic:
simp only [enumerate, h]

Goal state after:
case some
α : Type u_1
sel : Set α → Option α
h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s
s : Set α
n : ℕ
a a' : α
h : sel s = some a'
⊢ (do
        let a ← some a'
        enumerate sel (s \ {a}) n) =
      some a →
    a ∈ s
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case some.none.mk.some
α : Type u
β : Type v
γ : Type w
R : α → α → Prop
inst✝ : IsTrans α R
s✝ t✝ u✝ : WSeq α
h1✝¹ : LiftRel R s✝ t✝
h2✝¹ : LiftRel R t✝ u✝
s u t : WSeq α
h1✝ : LiftRel R s t
h2✝ : LiftRel R t u
h1 : Computation.LiftRel (LiftRelO R (LiftRel R)) s.destruct t.destruct
h2 : Computation.LiftRel (LiftRelO R (LiftRel R)) t.destruct u.destruct
hc : none ∈ u.destruct
fst✝ : α
snd✝ : WSeq α
ha : some (fst✝, snd✝) ∈ s.destruct
b : α × WSeq α
hb : some b ∈ t.destruct
t2 : LiftRelO R (LiftRel R) (some b) none
t1 : LiftRelO R (LiftRel R) (some (fst✝, snd✝)) (some b)
⊢ LiftRelO R (fun s u ↦ ∃ t, LiftRel R s t ∧ LiftRel R t u) (some (fst✝, snd✝)) none

Tactic:
cases b
      cases t2

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

Goal state before:
pp: case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
⊢ ∃ a', some a' ∈ s.head

Tactic:
let ⟨a', h'⟩ := head_some_of_head_tail_some h

Goal state after:
case succ
α : Type u
s : WSeq α
n : ℕ
IH : ∀ {a : α}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
a : α
h : some a ∈ s.get? (n + 1)
a' : α
h' : some a' ∈ (s.drop n).head
⊢ ∃ a', some a' ∈ s.head
Module: Mathlib.Data.Set.FiniteExhaustion

Goal state before:
pp: α : Type u_1
s : Set α
x✝ : Nonempty s.FiniteExhaustion
K : s.FiniteExhaustion
⊢ (⋃ n, K n).Countable

Tactic:
exact countable_iUnion <| fun i ↦ (K.finite i).countable

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op

Tactic:
apply op_injective

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x : αᵒᵖ
x✝ : α
⊢ x✝ ∈ {x}.unop → x✝ ∈ {unop x}

Tactic:
apply op_injective

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mp
α : Type u_1
x x✝ : α
⊢ x✝ ∈ {op x}.unop → x✝ ∈ {x}

Tactic:
apply op_injective

Goal state after:
Module: Mathlib.Data.Set.Opposite

Goal state before:
pp: case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op

Tactic:
apply op_injective

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
h : a ∈ parallel S
l : List (Computation α)
⊢ α ⊕ List (Computation α) → Prop

Tactic:
a

Goal state after:
α : Type u
S : WSeq (Computation α)
a✝ : α
h : a✝ ∈ parallel S
l : List (Computation α)
a : α ⊕ List (Computation α)
⊢ Prop
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝¹ : Preorder ι
inst✝ : (i : ι) → Preorder (α i)
a b : Σₗ (i : ι), α i
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨b, a, hji⟩ | ⟨b, a, hba⟩) <;> obtain ⟨_, _, hij⟩ | ⟨_, _, hab⟩ := hab
        · exact hij.not_gt hji
        · exact lt_irrefl _ hji
        · exact lt_irrefl _ hij
        · exact hab.not_ge hba

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

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

Tactic:
obtain ⟨b, h⟩ := exists_lt a

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : Preorder ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
i : ι
a b : α i
h : b < a
⊢ ∃ b, b < ⟨i, a⟩
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
⊢ ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
a

Goal state after:
case ind
α : Type u
β : Type v
R : α → β → Prop
U : WSeq α → WSeq β → Prop
HU :
  ∀ (s1 : WSeq α) (s2 : WSeq β),
    (∃ s t S T, s1 = s.append S.join ∧ s2 = t.append T.join ∧ LiftRel R s t ∧ LiftRel (LiftRel R) S T) → U s1 s2
n : ℕ
IH :
  ∀ m < n,
    ∀ {S : WSeq (WSeq α)} {T : WSeq (WSeq β)},
      LiftRel (LiftRel R) S T →
        ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a m → ∃ b ∈ T.join.destruct, LiftRelO R U a b
S : WSeq (WSeq α)
T : WSeq (WSeq β)
ST : LiftRel (LiftRel R) S T
a : Option (α × WSeq α)
⊢ S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b
Module: Mathlib.Data.String.Basic

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

Tactic:
apply iff_of_true

Goal state after:
case nil.cons.ha
c₂ : Char
cs₂ : List Char
⊢ ltb { s := ofList [], i := 0 } { s := ofList (c₂ :: cs₂), i := 0 } = true

case nil.cons.hb
c₂ : Char
cs₂ : List Char
⊢ [] < c₂ :: cs₂
Module: Mathlib.Data.String.Basic

Goal state before:
pp: case cons.nil.ha
c₁ : Char
cs₁ : List Char
ih : ∀ (s₂ : List Char), ltb { s := ofList cs₁, i := 0 } { s := ofList s₂, i := 0 } = true ↔ cs₁ < s₂
⊢ ¬(if { s := ofList [], i := 0 }.hasNext = true then
        if { s := ofList (c₁ :: cs₁), i := 0 }.hasNext = true then
          if { s := ofList (c₁ :: cs₁), i := 0 }.curr = { s := ofList [], i := 0 }.curr then
            ltb { s := ofList (c₁ :: cs₁), i := 0 }.next { s := ofList [], i := 0 }.next
          else decide ({ s := ofList (c₁ :: cs₁), i := 0 }.curr < { s := ofList [], i := 0 }.curr)
        else true
      else false) =
      true

Tactic:
simp [Legacy.Iterator.hasNext]

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

Goal state before:
pp: α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
⊢ a ∈ parallel S

Tactic:
have := terminates_of_mem ac

Goal state after:
α : Type u
S : WSeq (Computation α)
a : α
H : ∀ s ∈ S, s ~> a
c : Computation α
cs : c ∈ S
ac : a ∈ c
this : c.Terminates
⊢ a ∈ parallel S