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

Goal state before:
pp: case nil
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
⊢ foldl f a [] = foldr f a []

Tactic:
simp [*, foldl_assoc]

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

Goal state before:
pp: case cons
α : Type u_1
l : List α
a : α
f : α → α → α
inst✝ : Std.Associative f
ha : ∀ (x : α), f a x = f x a
head✝ : α
tail✝ : List α
tail_ih✝ : foldl f a tail✝ = foldr f a tail✝
⊢ foldl f a (head✝ :: tail✝) = foldr f a (head✝ :: tail✝)

Tactic:
simp [*, foldl_assoc]

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

Goal state before:
pp: α : Type u_1
p : α → Bool
l : List α
⊢ rtakeWhile p l <:+ l

Tactic:
rw [← reverse_prefix, rtakeWhile, reverse_reverse]
  exact takeWhile_prefix _

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

Goal state before:
pp: α : Type u_1
l : List α
p : l.Palindrome
⊢ l.reverse = l

Tactic:
induction p <;> try (exact rfl)
  simpa

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

Goal state before:
pp: case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
a : List α
len_a : a.length = n.succ
⊢ Acc (Shortlex r) a

Tactic:
obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a

Goal state after:
case ind
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α), a.length = m → Acc (Shortlex r) a
head : α
tail : List α
len_a : (head :: tail).length = n.succ
⊢ Acc (Shortlex r) (head :: tail)
Module: Mathlib.Data.Nat.ChineseRemainder

Goal state before:
pp: a b : ℕ
l : List ℕ
co : List.Pairwise Coprime l
⊢ a ≡ b [MOD l.prod] ↔ ∀ (i : Fin l.length), a ≡ b [MOD l.get i]

Tactic:
induction l with
  | nil => simp [modEq_one]
  | cons m l ih =>
    have : Coprime m l.prod := coprime_list_prod_right_iff.mpr (List.pairwise_cons.mp co).1
    simp only [List.prod_cons, ← modEq_and_modEq_iff_modEq_mul this, ih (List.Pairwise.of_cons co),
      List.length_cons]
    constructor
    · rintro ⟨h0, hs⟩ i
      cases i using Fin.cases <;> simp_all
    · 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:
by
  rw [Finset.mem_antidiagonal] at hk
  subst hk
  rw [eq_mul_inverse_iff_mul_eq, eq_mul_inverse_iff_mul_eq, ← Nat.cast_mul, ← Nat.cast_mul,
    add_comm, Nat.add_choose_mul_factorial_mul_factorial] <;>
    apply hm.natCast_factorial_of_le
  exacts [Nat.le_add_right k.1 k.2, Nat.le_add_left k.2 k.1]

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

Goal state before:
pp: case inr
p : ℕ → Prop
k a : ℕ
h : a < nth p (k + 1)
ha : p a
hf : (Set.ofPred p).Infinite
⊢ a ≤ nth p k

Tactic:
rcases subset_range_nth ha with ⟨n, rfl⟩

Goal state after:
case inr
p : ℕ → Prop
k : ℕ
hf : (Set.ofPred p).Infinite
n : ℕ
h : nth p n < nth p (k + 1)
ha : p (nth p n)
⊢ nth p n ≤ nth p k
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p (nth p b)
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p 0

Tactic:
hb0

Goal state after:
case neg
p : ℕ → Prop
a b : ℕ
hab : a ≤ b
h : p 0
h' : ∃ (h : (Set.ofPred p).Finite), #⋯.toFinset ≤ a
h'b : ∃ (hf : (Set.ofPred p).Finite), #hf.toFinset ≤ b
ha0 : nth p a = 0
hb0 : nth p b = 0
⊢ p 0
Module: Mathlib.Data.Num.ZNum

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

Tactic:
PosNum.cast_to_int

Goal state after:
α : Type u_1
inst✝ : AddGroupWithOne α
p : PosNum
⊢ ↑p = ↑p
Module: Mathlib.Data.Nat.Nth

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Infinite
n : ℕ
⊢ (n + if p (nth p n) then 1 else 0) = n + 1

Tactic:
if_pos (nth_mem_of_infinite hp _)

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
hp : (Set.ofPred p).Infinite
n : ℕ
⊢ n + 1 = n + 1
Module: Mathlib.Data.Num.ZNum

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

Tactic:
PosNum.cast_to_int

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

Goal state before:
pp: α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balance' x r).dual = r.dual.balance' x l.dual

Tactic:
simp [balance', add_comm]; split_ifs with h h_1 h_2 <;>
    simp [dual_rotateL, dual_rotateR, add_comm]
  cases delta_lt_false h_1 h_2

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

Goal state before:
pp: n d : PosNum
⊢ -↑(↑n.pred' / ↑(Num.pos d) + 1) = -(↑↑n.pred' + 1) / (↑↑d.pred' + 1)

Tactic:
change -[n.pred' / ↑d+1] = -[n.pred' / (d.pred' + 1)+1]

Goal state after:
n d : PosNum
⊢ -[↑n.pred' / ↑d+1] = -[↑n.pred' / (↑d.pred' + 1)+1]
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: u v : PrimeMultiset
⊢ (u + v).prod = u.prod * v.prod

Tactic:
change (coePNatMonoidHom (u + v)).prod = _

Goal state after:
u v : PrimeMultiset
⊢ (coePNatMonoidHom (u + v)).prod = u.prod * v.prod
Module: Mathlib.Data.PNat.Factors

Goal state before:
pp: v : PrimeMultiset
⊢ v.prod.factorMultiset = v

Tactic:
apply PrimeMultiset.coeNat_injective

Goal state after:
v : PrimeMultiset
⊢ v.prod.factorMultiset.toNatMultiset = v.toNatMultiset
Module: Mathlib.Data.PSigma.Order

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

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

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

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

Tactic:
· left
        apply lt_trans
        repeat' assumption

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

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

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
obtain rfl | ha := eq_top_or_lt_top a

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
b : α ⊤
⊢ ⟨⊤, b⟩ ≤ ⟨⊤, ⊤⟩

case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ' (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ m - n ≤ 1

Tactic:
tsub_le_iff_left

Goal state after:
n m : ℕ
H : Raised n m
H1 : n ≤ m
H2 : m ≤ n + 1
⊢ m ≤ n + 1
Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: k n m : ℕ
H : Raised n m
⊢ Raised (k + n) (k + m)

Tactic:
exact H.add_left _

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

Goal state before:
pp: case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcdD b ∣ a.gcd b

pp: case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcd b ∣ a.gcdD b

Tactic:
· apply dvd_gcd
    · exact Dvd.intro (gcdA' a b) (h₁.trans (mul_comm _ _)).symm
    · exact Dvd.intro (gcdB' a b) (h₂.trans (mul_comm _ _)).symm

Goal state after:
case a
a b : ℕ+
left✝² : a.gcdW b * a.gcdZ b = (a.gcdX b * a.gcdY b).succPNat
h₁ : a = a.gcdA' b * a.gcdD b
h₂ : b = a.gcdB' b * a.gcdD b
left✝¹ : a.gcdZ b * a.gcdA' b = (a.gcdX b * ↑(a.gcdB' b)).succPNat
left✝ : a.gcdW b * a.gcdB' b = (a.gcdY b * ↑(a.gcdA' b)).succPNat
h₅ : ↑(a.gcdZ b) * ↑a = a.gcdX b * ↑b + ↑(a.gcdD b)
right✝ : ↑(a.gcdW b) * ↑b = a.gcdY b * ↑a + ↑(a.gcdD b)
⊢ a.gcd b ∣ a.gcdD b
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case h.inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
r : Cofix F α → Cofix F α → Prop
h✝ : ∀ (x y : Cofix F α), r x y → (TypeVec.id ::: Quot.mk r) <$$> x.dest = (TypeVec.id ::: Quot.mk r) <$$> y.dest
r' : Cofix F α → Cofix F α → Prop := fun x y ↦ x = y ∨ r x y
x✝ y✝ : Cofix F α
rxy : r x✝ y✝
x y : Cofix F α
h : x = y
⊢ (TypeVec.id ::: Quot.mk r') <$$> x.dest = (TypeVec.id ::: Quot.mk r') <$$> y.dest

Tactic:
| inl h =>

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

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

Tactic:
· rw [sign_of_pos hp, sign_of_pos (inv_pos.mpr hp)]

Goal state after:
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 Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) a.dest b.dest

Tactic:
Ha,

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
X Y : Type u
x₀ : X
f : X → Y
g : Y → F (α ::: X)
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦ ∃ x, a = Cofix.corec (g ∘ f) x ∧ b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
a b : Cofix F α
x : X
Ha : a = Cofix.corec (g ∘ f) x
Hb : b = Cofix.corec (MvFunctor.map (TypeVec.id ::: f) ∘ g) (f x)
⊢ LiftR' (α.RelLast' R) (Cofix.corec (g ∘ f) x).dest b.dest
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R) a.dest b.dest

Tactic:
Ha,

Goal state after:
case inl
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
β : Type u
g : β → F (α ::: (Cofix F α ⊕ β))
x✝ : β
i : Cofix F α
R : Cofix F α → Cofix F α → Prop :=
  fun a b ↦
    ∃ x,
      a =
          corec
            (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
              Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
            (Sum.inl x) ∧
        b = x
a b x : Cofix F α
Ha :
  a =
    corec
      (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
        Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
      (Sum.inl x)
Hb : b = x
⊢ LiftR' (α.RelLast' R)
    (corec
        (MvFunctor.map (TypeVec.id ::: fun x ↦ x) ∘
          Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) fun val ↦ g val)
        (Sum.inl x)).dest
    b.dest
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case none
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
ht' : none ∈ s.destruct
ht2 : Option.rec nil Prod.snd none = t
td : some a ∈ Computation.pure none
⊢ ∃ a', some a' ∈ s.destruct

pp: case some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.2.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct

Tactic:
· have := mem_unique td (ret_mem _)
    contradiction

Goal state after:
case some
α : Type u
s : WSeq α
a : α × WSeq α
t : WSeq α
t' : α × WSeq α
td : some a ∈ t'.2.destruct
ht' : some t' ∈ s.destruct
ht2 : Option.rec nil Prod.snd (some t') = t
⊢ ∃ a', some a' ∈ s.destruct
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩

Tactic:
obtain rfl | ha := eq_top_or_lt_top a

Goal state after:
case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
b : α ⊤
⊢ ⟨⊤, b⟩ ≤ ⟨⊤, ⊤⟩

case inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderTop ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderTop (α ⊤)
x✝ : Σₗ (i : ι), α i
a : ι
b : α a
ha : a < ⊤
⊢ ⟨a, b⟩ ≤ ⟨⊤, ⊤⟩
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)
⊢ ∀ (a : Σₗ (i : ι), α i), ∃ b, b < a

Tactic:
by
    rintro ⟨i, a⟩
    obtain ⟨b, h⟩ := exists_lt a
    exact ⟨⟨i, b⟩, right _ _ h⟩

Goal state after:
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a (b :: t +-+ v) (Eq.recOn ⋯ (i.add k).fs) = Eq.recOn ⋯ (b :: t +-+ insert a v i)

Tactic:
← (Eq.recOn e' rfl :
      fs (Eq.recOn e' (i.add k) : Fin2 ((n + k) + 1)) =
        Eq.recOn (congr_arg (· + 1) e' : _ + 1 = _) (fs (i.add k)))

Goal state after:
case refine_2
α : Type u_1
m n : ℕ
a : α
t✝ : Vector3 α m
v : Vector3 α n
i : Fin2 (n + 1)
e : n + 1 + m = n + m + 1
k : ℕ
b : α
t : Vector3 α k
IH : ∀ (x : n + 1 + k = n + k + 1), insert a (t +-+ v) (Eq.recOn x (i.add k)) = Eq.recOn x (t +-+ insert a v i)
x✝ : n + 1 + (k + 1) = n + (k + 1) + 1
e' : n + 1 + k = n + k + 1
⊢ insert a (b :: t +-+ v) (Eq.recOn e' (i.add k)).fs = Eq.recOn ⋯ (b :: t +-+ insert a v i)
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f (?m.34 x✝ v fv :: ?m.35 x✝ v fv)

Tactic:
cons_head_tail v

Goal state after:
α : Type u_1
n : ℕ
f : Vector3 α n.succ → Prop
x✝ : Exists f
v : Vector3 α n.succ
fv : f v
⊢ f v
Module: Mathlib.Data.Vector3

Goal state before:
pp: α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p v ↔ ∀ (i : Fin2 n), p (v i)

Tactic:
refine v.recOn ?_ ?_

Goal state after:
case refine_1
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ VectorAllP p [] ↔ ∀ (i : Fin2 0), p []

case refine_2
α : Type u_1
n : ℕ
p : α → Prop
v : Vector3 α n
⊢ ∀ {n : ℕ} (a : α) (w : Vector3 α n),
    (VectorAllP p w ↔ ∀ (i : Fin2 n), p (w i)) → (VectorAllP p (a :: w) ↔ ∀ (i : Fin2 (n + 1)), p ((a :: w) i))
Module: Mathlib.Data.ZMod.Coprime

Goal state before:
pp: a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬a.gcd ↑p = 1

Tactic:
Int.gcd_comm,

Goal state after:
a : ℤ
p : ℕ
pp : Fact (Nat.Prime p)
⊢ ↑a = 0 ↔ ¬(↑p).gcd a = 1
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
⊢ stabilizer G s ≤ aestabilizer G μ s

Tactic:
intro g

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
g : G
⊢ g ∈ stabilizer G s → g ∈ aestabilizer G μ s
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: case inl
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
h : s =ᵐ[μ] ∅
⊢ g ∈ aestabilizer G μ s

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ (range fun x ↦ g ^ x) ⊆ ↑(MulAction.aestabilizer G μ s)

Tactic:
rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: case inl
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h✝ : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x ↦ g * x) ⁻¹' s = s
h : μ s = 0
⊢ False

Tactic:
| inl h =>

Goal state after:
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (#Finset.univ • min T (2 * T / (2 * ↑n)))

Tactic:
mul_div_mul_comm,

Goal state after:
case refine_4
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
hG_card : #Finset.univ = n
⊢ ENNReal.ofReal T ≤ ENNReal.ofReal (#Finset.univ • min T (2 / 2 * (T / ↑n)))
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
have h₁ := rnDeriv_add' (μ.singularPart ν) (ν.withDensity (μ.rnDeriv ν)) (ν + ν')

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropy T F = ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)

Tactic:
coverEntropy_eq_iSup_netEntropyEntourage T F

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U = ⨆ i, ⨆ (_ : p i), netEntropyEntourage T F (s i)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Nonempty (K ≃+* L)

Tactic:
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
    rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_eq mk_int) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_eq mk_int) hL)]
    exact Cardinal.lift_mk_eq'.2 hKL

Goal state after:
K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
⊢ Nonempty (K ≃+* L)
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
⊢ Sum.elim v xs ∘ relabelAux g m = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n)

Tactic:
ext x
  rcases x with x | x
  · simp only [BoundedFormula.relabelAux, Function.comp_apply, Sum.map_inl, Sum.elim_inl]
    rcases g x with l | r <;> simp
  · simp [BoundedFormula.relabelAux]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.zero.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
ts : Fin 0 → L[[α]].Term β
ih : ∀ (a : Fin 0), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions 0
⊢ (funMap val✝ fun i ↦ realize v (ts i)) = funMap (Sum.inl val✝) fun i ↦ realize v (ts i)

Tactic:
rw [withConstants_funMap_sumInl]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func.succ.inl
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
n✝ : ℕ
ts : Fin (n✝ + 1) → L[[α]].Term β
ih : ∀ (a : Fin (n✝ + 1)), realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a).constantsToVars = realize v (ts a)
val✝ : L.Functions (n✝ + 1)
⊢ (funMap val✝ fun i ↦ realize v (ts i)) = funMap (Sum.inl val✝) fun i ↦ realize v (ts i)

Tactic:
rw [withConstants_funMap_sumInl]

Goal state after: