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

Goal state before:
pp: 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)))ᶜ

Tactic:
simpa using IsCompact.isClosed (isCompact_range (hσ i))

Goal state after:
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]
    exact i_ih

Goal state after:
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

Goal state after:
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
this : F = Equiv.functor eqv
⊢ LawfulFunctor t'
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
f : Filter α
F : f.Realizer
⊢ (¬∀ (a : F.σ), (F.F.f a).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b

Tactic:
not_forall

Goal state after:
α : Type u_1
f : Filter α
F : f.Realizer
⊢ (∃ x, ¬(F.F.f x).Nonempty) ↔ ∀ (b : Realizer.bot.σ), ∃ a, F.F.f a ⊆ Realizer.bot.F.f b
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Erased α), id <$> x = x

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (pure g✝ <*> x✝).out = (g✝ <$> x✝).out

Tactic:
simp [Seq.seq]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : α → β) (x : Erased α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
        let x ← f✝
        x <$> x✝).out =
    (f✝ <*> x✝).out

Tactic:
simp [Seq.seq]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : α) (f : α → Erased β), pure x >>= f = f x

Tactic:
intros; ext; simp

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (x : Erased α) (f : α → Erased β) (g : β → Erased γ), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
intros; ext; simp

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

Goal state before:
pp: α : Type u
α' : Type u'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
⊢ dlookup (f a) (map (Sigma.map f fun x ↦ id) l) = dlookup a l

Tactic:
have := dlookup_map (β' := fun _ => β) (f := f) (g := fun _ => id)

Goal state after:
α : Type u
α' : Type u'
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
this :
  ∀ (l : List ((_ : α) × β)),
    Function.Injective f → ∀ (a : α), dlookup (f a) (map (Sigma.map f fun x ↦ id) l) = Option.map id (dlookup a l)
⊢ dlookup (f a) (map (Sigma.map f fun x ↦ id) l) = dlookup a l
Module: Mathlib.Data.Finmap

Goal state before:
pp: α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries ~ b.entries → f a = f b
⊢ ⟦s⟧.liftOn f H = f s

Tactic:
by
  cases s
  rfl

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

Goal state before:
pp: case mp
α : 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✝
⊢ dlookup x✝ s₂.entries = some y✝ ∨ ¬x✝ ∈ s₂.entries.keys ∧ dlookup x✝ s₁.entries = some y✝

Tactic:
rcases h' with h' | h'
        · right
          refine ⟨?_, h'⟩
          apply h
          rw [keys, ← List.dlookup_isSome, h']
          exact rfl
        · left
          rw [h'.2]

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

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
head✝ : Sigma β
l : List (Sigma β)
⊢ (head✝ :: l).kunion [] = head✝ :: l

Tactic:
by rw [kunion, kerase_nil, kunion_nil]

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

Tactic:
convert! h0 using 1

Goal state after:
ι : 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 = ∅
⊢ f = fun x ↦ ∅
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
d : ℕ
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
x : Holor α [d]
y₁ y₂ : Holor α ds
hy₁ : y₁.CPRankMax1
hy₂ : CPRankMax n y₂
⊢ CPRankMax (n + 1) (x ⊗ (y₁ + y₂))

Tactic:
by
    rw [mul_left_distrib]
    rw [Nat.add_comm]
    apply cprankMax_add
    · exact cprankMax_1 (CPRankMax1.cons _ _ hy₁)
    · exact cprankMax_mul _ x y₂ hy₂

Goal state after:
Module: Mathlib.Data.Holor

Goal state before:
pp: α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
⊢ (∀ x_1 ∈ insert x s, CPRankMax n (f x_1)) → CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)

Tactic:
h_cprank

Goal state after:
α : Type
ds : List ℕ
inst✝ : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s✝ : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax ((insert x s).card * n) (∑ x ∈ insert x s, f x)
Module: Mathlib.Data.Int.CardIntervalMod

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

Tactic:
cast_mul,

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

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

Tactic:
cast_mul,

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

Goal state before:
pp: α : Type u_1
l : List α
⊢ (l ++ l.reverse).Palindrome

Tactic:
apply of_reverse_eq
  rw [reverse_append, reverse_reverse]

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

Goal state before:
pp: case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
⊢ (take n w ++ w)[j]? = w[j % p]?

Tactic:
have n_le_j : n ≤ j := le_of_not_gt j_lt_n

Goal state after:
case neg
α : Type u_1
p n : ℕ
w : List α
dvd : p ∣ n
len : n ≤ w.length
per : w.HasPeriod p
p_pos : p > 0
pos : n > 0
mod_w : ∀ i < w.length, w[i % p]? = w[i]?
i : ℕ
less_i : i < n + w.length
j : ℕ
less_j : j < n + w.length
j_lt_n : ¬j < n
j_minus : j - n < w.length
n_le_j : n ≤ j
⊢ (take n w ++ w)[j]? = w[j % p]?
Module: Mathlib.Data.Nat.Factorial.NatCast

Goal state before:
pp: A : Type u_1
inst✝³ : Semiring A
K : Type u_2
inst✝² : Semifield K
inst✝¹ : CharZero K
inst✝ : Algebra K A
n : ℕ
⊢ IsUnit ↑n !

Tactic:
by
  suffices IsUnit (n ! : K) by
    simpa using this.map (algebraMap K A)
  simp [isUnit_iff_ne_zero, n.factorial_ne_zero]

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

Goal state before:
pp: case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit ↑((n + 1) * n !) ↔ n + 1 < p

Tactic:
cast_mul,

Goal state after:
case succ
A : Type u_1
inst✝² : Ring A
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP A p
hp : Nat.Prime p
n : ℕ
ih : IsUnit ↑n ! ↔ n < p
⊢ IsUnit (↑(n + 1) * ↑n !) ↔ n + 1 < p
Module: Mathlib.Data.Nat.Choose.Lucas

Goal state before:
pp: n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) *
      ↑((∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) * (n / p ^ a % p).choose (k / p ^ a % p)) [ZMOD
    ↑p]

Tactic:
cast_mul,

Goal state after:
n k p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ a : ℕ
⊢ ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡
    ↑((n / p ^ a.succ).choose (k / p ^ a.succ)) *
      (↑(∏ x ∈ range a, (n / p ^ x % p).choose (k / p ^ x % p)) * ↑((n / p ^ a % p).choose (k / p ^ a % p))) [ZMOD
    ↑p]
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 ≡ 0 [ZMOD ↑p]
hm : n = p ^ multiplicity p n * m
⊢ p ^ (multiplicity p n + 1) ∣ n

pp: case hf
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
⊢ FiniteMultiplicity p n

Tactic:
· nth_rw 2 [hm]
    simpa [pow_add] using Nat.mul_dvd_mul_left _ (dvd_iff_mod_eq_zero.mpr (by exact_mod_cast h))

Goal state after:
case hf
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
⊢ FiniteMultiplicity p n
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Finite
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x

Tactic:
rcases exists_lt_card_finite_nth_eq hf h with ⟨n, hn, hx⟩

Goal state after:
case refine_1
p : ℕ → Prop
x : ℕ
h : p x
hf : (Set.ofPred p).Finite
n : ℕ
hn : n < #hf.toFinset
hx : nth p n = x
⊢ ∃ n, (∀ (hf : (Set.ofPred p).Finite), n < #hf.toFinset) ∧ nth p n = x
Module: Mathlib.Data.Ordering.Lemmas

Goal state before:
pp: α : Type u
lt : α → α → Prop
inst✝ : DecidableRel lt
a b : α
⊢ (cmpUsing lt a b = Ordering.lt) = lt a b

Tactic:
by
  simp only [cmpUsing, Ordering.ite_eq_lt_distrib, ite_self, if_false_right, and_true, reduceCtorEq]

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

Goal state before:
pp: case bit1
n : PosNum
⊢ (↑n + ↑n + 1).sqrt < ↑n + (1 + 1 + 1)

Tactic:
rw [Nat.sqrt_lt]

Goal state after:
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
Module: Mathlib.Data.Ordmap.Ordnode

Goal state before:
pp: case nil
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ Ordnode α

Tactic:
rcases id r with _ | ⟨rs, rl, rx, rr⟩
    · exact ι x
    · rcases id rr with _ | rrs
      · rcases rl with _ | ⟨_, _, rlx⟩
        · exact node 2 nil x r
        · exact node 3 (ι x) rlx ι rx
      · rcases id rl with _ | ⟨rls, rll, rlx, rlr⟩
        · exact node 3 (ι x) rx rr
        · 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.Ordmap.Ordset

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

Tactic:
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

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

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

Tactic:
map_eq_map,

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

Goal state before:
pp: case pos.succ.succ
α : 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
n✝¹ n✝ : ℕ
mm : n✝¹ + 1 + (n✝ + 1) ≤ 1
⊢ BalancedSz 1 (n✝¹ + 1) ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + (n✝¹ + 1) + 1) (n✝ + 1 + 1 + 1)

Tactic:
rw [Nat.succ_add] at mm

Goal state after:
case pos.succ.succ
α : 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
n✝¹ n✝ : ℕ
mm : (n✝¹ + (n✝ + 1)).succ ≤ 1
⊢ BalancedSz 1 (n✝¹ + 1) ∧ BalancedSz (n✝ + 1) 1 ∧ BalancedSz (1 + (n✝¹ + 1) + 1) (n✝ + 1 + 1 + 1)
Module: Mathlib.Data.Num.ZNum

Goal state before:
pp: a✝ b✝ : Num
⊢ ↑a✝ * ↑b✝ < 2 ^ (↑a✝).size * 2 ^ (↑b✝).size

Tactic:
exact mul_lt_mul'' (Nat.lt_size_self _) (Nat.lt_size_self _) (Nat.zero_le _) (Nat.zero_le _)

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

Goal state before:
pp: case mpr.succ.step.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
y : F.M
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
a✝¹ : y = M.mk ⟨a, y'⟩
x_a : F.A
x_f : F.B x_a → F.M
a✝ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) (y.approx (n✝ + 1 + 1))

Tactic:
induction y using PFunctor.M.casesOn' with

Goal state after:
case mpr.succ.step.f.f
F : PFunctor.{uA, uB}
n✝ : ℕ
n_ih : ∀ (x y : F.M), Agree' n✝ x y → Agree (x.approx n✝) (y.approx (n✝ + 1))
a : F.A
x' y' : F.B a → F.M
a✝² : ∀ (i : F.B a), Agree' n✝ (x' i) (y' i)
x_a : F.A
x_f : F.B x_a → F.M
a✝¹ : M.mk ⟨x_a, x_f⟩ = M.mk ⟨a, x'⟩
y_a : F.A
y_f : F.B y_a → F.M
a✝ : M.mk ⟨y_a, y_f⟩ = M.mk ⟨a, y'⟩
⊢ Agree ((M.mk ⟨x_a, x_f⟩).approx (n✝ + 1)) ((M.mk ⟨y_a, y_f⟩).approx (n✝ + 1 + 1))
Module: Mathlib.Data.PFunctor.Multivariate.M

Goal state before:
pp: n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
ff : P.B a' ⟹ α ::: P.M α
ef : splitFun f' f₁' = ff
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
a₁' : P.last.A
g₁' : P.last.B a₁' → P.last.M
e₁' : he₁' = ⟨a₁', g₁'⟩
e₁ : dest' P e₁' f₁ = ⟨a', ff⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩

Tactic:
cases e₁

Goal state after:
case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
a₁ : P.mp.A
f₁ : P.mp.B a₁ ⟹ α
a' : P.A
f' : (P.B a').drop ⟹ α
f₁' : (P.B a').last → P.M α
he₁' : ↑P.last P.last.M := PFunctor.M.dest a₁
g₁' : P.last.B a' → P.last.M
e₁' : he₁' = ⟨a', g₁'⟩
ef : splitFun f' f₁' = splitFun (pathDestLeft P e₁' f₁) fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
⊢ ∃ g₁',
    ∃ (e₁' : PFunctor.M.dest a₁ = ⟨a', g₁'⟩),
      f' = pathDestLeft P e₁' f₁ ∧ f₁' = fun x ↦ ⟨g₁' x, pathDestRight P e₁' f₁ x⟩
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: ⊢ factorMultiset 1 = 0

Tactic:
simp [factorMultiset, PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset]

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

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

Tactic:
size_balance' v.2 hr.2.2.2,

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : Preorder ι
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : ∀ (i : ι), DenselyOrdered (α i)
inst✝ : ∀ (i : ι), NoMinOrder (α i)
⊢ ∀ (a₁ a₂ : Σₗ' (i : ι), α i), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂

Tactic:
by
    rintro ⟨i, a⟩ ⟨j, b⟩ (⟨_, _, h⟩ | @⟨_, _, b, h⟩)
    · obtain ⟨c, hb⟩ := exists_lt b
      exact ⟨⟨j, c⟩, left _ _ h, right _ hb⟩
    · obtain ⟨c, ha, hb⟩ := exists_between h
      exact ⟨⟨i, c⟩, right _ ha, right _ hb⟩

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ l.balanceR x r = l.balance' x r

Tactic:
← dual_dual (balanceR l x r),

Goal state after:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l.size l' ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r' r.size ∧ BalancedSz l.size r'
⊢ (l.balanceR x r).dual.dual = l.balance' x r
Module: Mathlib.Data.Ordmap.Invariants

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

Tactic:
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this

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

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

Tactic:
ext u

Goal state after:
n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α : TypeVec.{u} n
a : (P F).A
f : (P F).B a ⟹ α
i✝ : Fin2 n
u : α i✝
⊢ u ∈ supp (abs ⟨a, f⟩) i✝ ↔ u ∈ f i✝ '' univ
Module: Mathlib.Data.QPF.Multivariate.Basic

Goal state before:
pp: n : ℕ
F : TypeVec.{u} n → Type u_1
q : MvQPF F
h : IsUniform
α β : TypeVec.{u} n
g : α ⟹ β
x : F α
i : Fin2 n
⊢ supp (g <$$> x) i = g i '' supp x i

Tactic:
rw [← abs_repr x]; obtain ⟨a, f⟩ := repr x; rw [← abs_map, MvPFunctor.map_eq]
  rw [supp_eq_of_isUniform h, supp_eq_of_isUniform h, ← image_comp]
  rfl

Goal state after:
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
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk ((TypeVec.id ::: _root_.id) <$$> x) = mk x

Tactic:
appendFun_id_id,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk (TypeVec.id <$$> x) = 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
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk (TypeVec.id <$$> x) = mk x

Tactic:
MvFunctor.id_map

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x✝ : Fix F α
x : F (α ::: Fix F α)
h : (TypeVec.id ::: mk ∘ rec (MvFunctor.map (TypeVec.id ::: mk))) <$$> x = (TypeVec.id ::: fun x ↦ x) <$$> x
⊢ mk x = mk x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (TypeVec.id ::: _root_.id) <$$> x = x

Tactic:
appendFun_id_id,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ TypeVec.id <$$> x = x
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ TypeVec.id <$$> x = x

Tactic:
MvFunctor.id_map

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ x = x
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: ⊢ (if 0 < 0 then -1 else if 0 < 0 then 1 else 0) = 0

Tactic:
if_neg (lt_irrefl _),

Goal state after:
⊢ (if 0 < 0 then 1 else 0) = 0
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this : LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) ((TypeVec.id ::: _root_.id) <$$> x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x

Tactic:
appendFun_id_id,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
ι : Type u
R : ι → ι → Prop
x : F (α ::: ι)
f : ι → ι
hh : ∀ (x : ι), R (f x) x
this : LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) (TypeVec.id <$$> x)
⊢ LiftR' (α.RelLast' R) ((TypeVec.id ::: f) <$$> x) x