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

Goal state before:
pp: case node
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
f_strict_mono : StrictMono f
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
t_ih_l :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ l✝ a₂ → Valid' (Option.map f a₁) (map f l✝) (Option.map f a₂) ∧ (map f l✝).size = l✝.size
t_ih_r :
  ∀ {a₁ : WithBot α} {a₂ : WithTop α},
    Valid' a₁ r✝ a₂ → Valid' (Option.map f a₁) (map f r✝) (Option.map f a₂) ∧ (map f r✝).size = r✝.size
a₁ : WithBot α
a₂ : WithTop α
h : Valid' a₁ (Ordnode.node size✝ l✝ x✝ r✝) a₂
⊢ Valid' (Option.map f a₁) (map f (Ordnode.node size✝ l✝ x✝ r✝)) (Option.map f a₂) ∧
    (map f (Ordnode.node size✝ l✝ x✝ r✝)).size = (Ordnode.node size✝ l✝ x✝ r✝).size

Tactic:
have t_ih_l' := t_ih_l h.left
    have t_ih_r' := t_ih_r h.right
    clear t_ih_l t_ih_r
    obtain ⟨t_l_valid, t_l_size⟩ := t_ih_l'
    obtain ⟨t_r_valid, t_r_size⟩ := t_ih_r'
    simp only [map, size_node, and_true]
    constructor
    · exact And.intro t_l_valid.ord t_r_valid.ord
    · constructor
      · rw [t_l_size, t_r_size]; exact h.sz.1
      · constructor
        · exact t_l_valid.sz
        · exact t_r_valid.sz
    · constructor
      · rw [t_l_size, t_r_size]; exact h.bal.1
      · constructor
        · exact t_l_valid.bal
        · exact t_r_valid.bal

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Prj

Goal state before:
pp: n : ℕ
i : Fin2 n
⊢ ∀ {α : TypeVec.{?u.11} n} (x : Prj i α), abs i (repr i x) = x

Tactic:
intros

Goal state after:
n : ℕ
i : Fin2 n
α✝ : TypeVec.{?u.11} n
x✝ : Prj i α✝
⊢ abs i (repr i 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
r : Cofix F α → Cofix F α → Prop
h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest
⊢ ∀ (x y : Cofix F α), r x y → LiftR (α.RelLast r) x.dest y.dest

Tactic:
intros

Goal state after:
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 → LiftR' (α.RelLast' r) x.dest y.dest
x✝ y✝ : Cofix F α
a✝ : r x✝ y✝
⊢ LiftR (α.RelLast r) x✝.dest y✝.dest
Module: Mathlib.Data.Real.Sign

Goal state before:
pp: r : ℝ
⊢ (-r).sign = -r.sign

Tactic:
obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
  · rw [sign_zero, neg_zero, sign_zero]
  · rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

Goal state after:
Module: Mathlib.Data.QPF.Multivariate.Constructions.Cofix

Goal state before:
pp: case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := ⋯
a✝ : (P F).M α
⊢ ∀ (x : (P F).M α),
    R
      (((Quot.mk Mcongr ∘
            M.corec (P F)
              (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
          Quot.mk Mcongr)
        x)
      (Quot.mk Mcongr x)

Tactic:
intros

Goal state after:
case mk
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
R : Cofix F α → Cofix F α → Prop := fun x y ↦ abs y.repr = x
a✝ x✝ : (P F).M α
⊢ R
    (((Quot.mk Mcongr ∘
          M.corec (P F)
            (MvQPF.repr ∘ Quot.lift (fun x ↦ (TypeVec.id ::: Quot.mk Mcongr) <$$> MvQPF.abs (M.dest (P F) x)) ⋯)) ∘
        Quot.mk Mcongr)
      x✝)
    (Quot.mk Mcongr x✝)
Module: Mathlib.Data.QPF.Univariate.Basic

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

Tactic:
PFunctor.liftp_iff'

Goal state after:
case mp
F : Type u → Type u
q : QPF F
h :
  ∀ ⦃α : Type u⦄ (x : ↑(P F) α), {y | ∀ ⦃p : α → Prop⦄, Liftp p (abs x) → p y} = {y | ∀ ⦃p : α → Prop⦄, Liftp p x → p y}
α : Type u
p : α → Prop
a : (P F).A
f : (P F).B a → α
h' : IsUniform
⊢ (∀ u ∈ f '' univ, p u) ↔ ∀ (i : (P F).B a), p (f i)
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
⊢ ∀ (x : Cofix F α),
    R
      (corec
        (fun x ↦
          (TypeVec.id ::: fun x ↦ x) <$$>
            Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x)
        (Sum.inl x))
      x

Tactic:
intros

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
x✝ : Cofix F α
⊢ R
    (corec
      (fun x ↦
        (TypeVec.id ::: fun x ↦ x) <$$> Sum.rec (fun val ↦ (TypeVec.id ::: Sum.inl) <$$> val.dest) (fun val ↦ g val) x)
      (Sum.inl 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} (f : α ⟹ β) (p : ↑(P F).mp α), Quot.mk Mcongr (f <$$> p) = f <$$> Quot.mk Mcongr p

Tactic:
intros

Goal state after:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α✝ β✝ : TypeVec.{u} n
f✝ : α✝ ⟹ β✝
p✝ : ↑(P F).mp α✝
⊢ Quot.mk Mcongr (f✝ <$$> p✝) = f✝ <$$> Quot.mk Mcongr p✝
Module: Mathlib.Data.Set.Opposite

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

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

Tactic:
· apply unop_injective

Goal state after:
case mpr
α : Type u_1
x : α
x✝ : αᵒᵖ
⊢ x✝ ∈ {op x} → x✝ ∈ {x}.op
Module: Mathlib.Data.Set.Opposite

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

Tactic:
· apply unop_injective

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

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

Tactic:
· apply unop_injective

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

Goal state before:
pp: α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
⊢ ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')

Tactic:
apply Computation.memRecOn h <;> [skip; intro c IH] <;> intro s m <;>
    induction s using WSeq.recOn

Goal state after:
case h1.nil
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
m : nil.destruct = Computation.pure (some (a', s'))
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

case h1.cons
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = Computation.pure (some (a', s'))
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

case h1.think
α : Type u
a a' : α
s' : WSeq α
c : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c
s✝ : WSeq α
m : s✝.think.destruct = Computation.pure (some (a', s'))
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'

case h2.nil
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
m : nil.destruct = c.think
⊢ a ∈ nil ↔ a = a' ∨ a ∈ s'

case h2.cons
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
x✝ : α
s✝ : WSeq α
m : (cons x✝ s✝).destruct = c.think
⊢ a ∈ cons x✝ s✝ ↔ a = a' ∨ a ∈ s'

case h2.think
α : Type u
a a' : α
s' : WSeq α
c✝ : Computation (Option (α × WSeq α))
h : some (a', s') ∈ c✝
c : Computation (Option (α × WSeq α))
IH : ∀ {s : WSeq α}, s.destruct = c → (a ∈ s ↔ a = a' ∨ a ∈ s')
s✝ : WSeq α
m : s✝.think.destruct = c.think
⊢ a ∈ s✝.think ↔ a = a' ∨ a ∈ s'
Module: Mathlib.Data.Set.Opposite

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

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

Tactic:
· apply unop_injective

Goal state after:
case mpr
α : Type u_1
x x✝ : αᵒᵖ
⊢ x✝ ∈ {x} → x✝ ∈ {unop x}.op
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
⊢ ((↑s).drop n).tail = ↑(s.drop n).tail

Tactic:
rw [dropn_ofSeq s n, tail_ofSeq]

Goal state after:
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 β)},
    LiftRel (LiftRel R) S T →
      ∀ {a : Option (α × WSeq α)}, S.join.destruct.Results a n → ∃ b ∈ T.join.destruct, LiftRelO R U a b

Tactic:
intro S

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 β)},
    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 case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c }.next { s := ofList (c :: s₂.s.toList), i := s₂.i + c }.next =
    ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c }

Tactic:
simp only [Legacy.Iterator.next, Pos.Raw.next, get_cons_addChar, ofList_toList]

Goal state after:
case case1
c : Char
s₁ s₂ : Legacy.Iterator
h₁ : s₂.hasNext = true
h₂ : s₁.hasNext = true
h : s₁.curr = s₂.curr
ih :
  ltb { s := ofList (c :: s₁.next.s.toList), i := s₁.next.i + c }
      { s := ofList (c :: s₂.next.s.toList), i := s₂.next.i + c } =
    ltb s₁.next s₂.next
⊢ ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + c + Pos.Raw.get s₁.s s₁.i }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + c + Pos.Raw.get s₂.s s₂.i } =
    ltb { s := ofList (c :: s₁.s.toList), i := s₁.i + Pos.Raw.get s₁.s s₁.i + c }
      { s := ofList (c :: s₂.s.toList), i := s₂.i + Pos.Raw.get s₂.s s₂.i + c }
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₂
⊢ ¬ltb { s := ofList (c₁ :: cs₁), i := 0 } { s := ofList [], i := 0 } = true

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

Tactic:
· unfold ltb
      simp [Legacy.Iterator.hasNext]

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

Goal state before:
pp: case nil.nil
α : Type u
S T✝ : WSeq (WSeq α)
s1 s2 : WSeq α
h : ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join)
T : WSeq (WSeq α)
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ ∃ s S T, s1 = s.append (S.append T).join ∧ s2 = s.append (S.join.append T.join))
    (fun c1 c2 ↦ ∃ s S T, c1 = (s.append (S.append T).join).destruct ∧ c2 = (s.append (S.join.append T.join)).destruct)
    T.join.destruct.destruct T.join.destruct.destruct

Tactic:
induction T using WSeq.recOn with
      | nil => simp
      | cons s T =>
        simp only [join_cons, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
      | think T =>
        simp only [join_think, destruct_think, Computation.destruct_think, liftRelAux_inr_inr]
        refine ⟨nil, nil, T, ?_, ?_⟩ <;> simp

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

Goal state before:
pp: α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ S = WSeq.map ((map fun c ↦ c.1) ∘ fun c ↦ map (fun a ↦ (a, c)) c) S

Tactic:
refine (WSeq.map_id _).symm.trans (congr_arg (fun f => WSeq.map f S) ?_)

Goal state after:
α : Type u
β : Type v
S : WSeq (Computation α)
C : α → Sort v
H : (s : Computation α) → s ∈ S → (a : α) → a ∈ s → C a
a : α
h : a ∈ parallel S
T : WSeq (Computation (α × Computation α)) := WSeq.map (fun c ↦ map (fun a ↦ (a, c)) c) S
⊢ id = (map fun c ↦ c.1) ∘ fun c ↦ map (fun a ↦ (a, c)) c
Module: Mathlib.Data.Vector.Mem

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a ∈ (a' ::ᵥ v').toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList

Tactic:
Vector.mem_cons_iff,

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
a' : α
v' : Vector α n
h : v = a' ::ᵥ v'
⊢ a = a' ∨ a ∈ v'.toList ↔ a = (a' ::ᵥ v').head ∨ a ∈ (a' ::ᵥ v').tail.toList
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
⊢ (mapAccumr f xs s).2 = map f' xs

Tactic:
rw [mapAccumr_eq_map Set.univ (Set.mem_univ _) (fun _ _ _ => Set.mem_univ _)
    (fun a s s' _ _ => by rw [h, h])]

Goal state after:
α : Type u_1
β : Type u_2
σ : Type u_5
n : ℕ
xs : Vector α n
f : α → σ → σ × β
f' : α → β
s : σ
h : ∀ (a : α) (s : σ), (f a s).2 = f' a
⊢ map (fun x ↦ (f x s).2) xs = map f' xs
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz

Tactic:
intros

Goal state after:
case refine_1
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ insert a v fz fz = (a :: v) fz
Module: Mathlib.Data.Vector3

Goal state before:
pp: case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
⊢ ∀ (n_1 : Fin2 n), insert a v fz n_1.fs = (a :: v) n_1.fs

Tactic:
intros

Goal state after:
case refine_2
α : Type u_1
n : ℕ
a : α
v : Vector3 α n
j : Fin2 (n + 1)
n✝ : Fin2 n
⊢ insert a v fz n✝.fs = (a :: v) n✝.fs
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ |f (g 0) - (f 0 + g 0)| < 1

Tactic:
abs_lt,

Goal state after:
f g : CircleDeg1Lift
⊢ -1 < f (g 0) - (f 0 + g 0) ∧ f (g 0) - (f 0 + g 0) < 1
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f g : CircleDeg1Lift
⊢ -1 < f (g 0) - (f 0 + g 0) ∧ f (g 0) - (f 0 + g 0) < 1

Tactic:
lt_sub_iff_add_lt',

Goal state after:
f g : CircleDeg1Lift
⊢ f 0 + g 0 + -1 < f (g 0) ∧ f (g 0) - (f 0 + g 0) < 1
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ T

Tactic:
by linarith [hT.out]

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case neg
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
simp [hg, cond g hg]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
inst✝ : V.IsSymm
n : ℕ
⊢ coverMincard S F (map φ φ ⁻¹' (V ○ V)) n ≤ coverMincard T (φ '' F) V n

Tactic:
by
  rcases eq_top_or_lt_top (coverMincard T (φ '' F) V n) with h' | h'
  · exact h' ▸ le_top
  obtain ⟨t, t_cover, t_card⟩ := (coverMincard_finite_iff T (φ '' F) V n).1 h'
  obtain ⟨s, s_cover, s_card⟩ := t_cover.preimage h
  rw [← t_card]
  exact s_cover.coverMincard_le_card.trans (WithTop.coe_le_coe.2 s_card)

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m : ℕ
F_nonempty : F.Nonempty
⊢ coverMincard T F (U ○ U) (m * 0) ≤ coverMincard T F U m ^ 0

case inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
m n : ℕ
F_nonempty : F.Nonempty
hn : n ≠ 0
⊢ coverMincard T F (U ○ U) (m * n) ≤ coverMincard T F U m ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
⊢ coverEntropyEntourage T ∅ U = ⊥

Tactic:
simp only [coverEntropyEntourage, coverMincard_empty]
  rw [ENat.toENNReal_zero, ← Pi.zero_def, expGrowthSup_zero]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ netEntropyEntourage T F U ≤ coverEntropy T F

Tactic:
apply (netEntropyEntourage_antitone T F SetRel.symmetrize_subset_self).trans

Goal state after:
case a
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ (fun U ↦ netEntropyEntourage T F U) (SetRel.symmetrize U) ≤ coverEntropy T F
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) x) =ᵐ[map f ν] 0

Tactic:
refine Measure.rnDeriv_eq_zero_of_mutuallySingular ?_ Measure.AbsolutelyContinuous.rfl

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ map f (μ.singularPart ν) ⟂ₘ map f ν
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), (⇑hnp ∘ ⇑hmn) (funMap f x) = funMap f ((⇑hnp ∘ ⇑hmn) ∘ x)

Tactic:
intros

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap f✝ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r ((⇑hnp ∘ ⇑hmn) ∘ x) ↔ RelMap r x

Tactic:
intros

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ x✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
⊢ ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), (⇑hnp ∘ ⇑hmn) (funMap f x) = funMap f ((⇑hnp ∘ ⇑hmn) ∘ x)

Tactic:
intros

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
f✝ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap f✝ x✝) = funMap f✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝)
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
⊢ ∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M), RelMap r ((⇑hnp ∘ ⇑hmn) ∘ x) ↔ RelMap r x

Tactic:
intros

Goal state after:
L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ≃[L] P
hmn : M ≃[L] N
n✝ : ℕ
r✝ : L.Relations n✝
x✝ : Fin n✝ → M
⊢ RelMap r✝ ((⇑hnp ∘ ⇑hmn) ∘ x✝) ↔ RelMap r✝ x✝
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
hfg : (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g
⊢ f = g

Tactic:
convert! (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg) <;>
    rw [comp_assoc, self_comp_symm, comp_refl]

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.Basic

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
⊢ ∀ (a a_1 : R), funMap addFunc (Fin.cons a (Fin.cons a_1 finZeroElim)) = a + Fin.cons a (Fin.cons a_1 finZeroElim) 1

Tactic:
intros

Goal state after:
α : Type u_1
R : Type u_2
inst✝ : ring.Structure R
a✝¹ a✝ : R
⊢ funMap addFunc (Fin.cons a✝¹ (Fin.cons a✝ finZeroElim)) = a✝¹ + Fin.cons a✝¹ (Fin.cons a✝ finZeroElim) 1