mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₁) / 2 < (a₁ + a₂) / 2

Tactic:
by gcongr; exact zero_lt_two

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x

Tactic:
;

Goal state after:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α : Type v
x : F (G α)
⊢ mk (mk x) = mk x
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b c d e : α
m n : ℤ
inst✝ : IsStrictOrderedRing α
a₁ a₂ : α
h : a₁ < a₂
⊢ (a₁ + a₂) / 2 < (a₂ + a₂) / 2

Tactic:
by gcongr; exact zero_lt_two

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝
Module: Mathlib.Algebra.BigOperators.Group.List.Defs

Goal state before:
pp: case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ (a :: replicate n a).prod = a ^ (n + 1)

Tactic:
prod_cons,

Goal state after:
case succ
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
ih : (replicate n a).prod = a ^ n
⊢ a * (replicate n a).prod = a ^ (n + 1)
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ (na.mul ↑db).add (-(nb * ↑da)) = (↑k).mul nc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Semiring α
na nb nc da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (is.length + 1), ts.length)
    (ts.length + 1 + is.length, ts.length + 1)

Tactic:
;

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (ts.length + (is.length + 1), ts.length)
    (ts.length + 1 + is.length, ts.length + 1)
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length, is.length) (ts.length + 1 + is.length, ts.length + 1)

Tactic:
;

Goal state after:
α : Type u_1
t : α
ts is : List α
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (is.length, is.length) (ts.length + 1 + is.length, ts.length + 1)
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ↑da * ↑db * ⅟↑da * ⅟↑db * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑k * ↑nc * ⅟↑da * ⅟↑db = ↑nc * ⅟↑dc
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: «$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$na» «$nb» : ℕ
⊢ AddMonoidWithOne «$α»

Tactic:
;

Goal state after:
«$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$na» «$nb» : ℕ
⊢ AddMonoidWithOne «$α»
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: «$u» : Level
«$α» : Type u
«$a» «$b» : «$α»
«$inst» : Semiring «$α»
«$mα'» : AddMonoidWithOne «$α»
«$na» : ℕ
«$pa» : IsNat «$a» «$na»
«$mα» : AddMonoidWithOne «$α»
«$nb» : ℕ
«$pb» : IsNat «$b» «$nb»
⊢ AddMonoidWithOne «$α»

Tactic:
by clear! mα mα'; apply AddCommMonoidWithOne.toAddMonoidWithOne

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case e_a.e_5
α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝

Tactic:
;

Goal state after:
case e_a.e_5
α : Type u
inst✝ : Semiring α
num✝ denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: case e_a.e_5
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝

Tactic:
;

Goal state after:
case e_a.e_5
α : Type u
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
inv✝¹ inv✝ : Invertible ↑denom✝
⊢ inv✝¹ = inv✝
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
;

Goal state after:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI l₁.length (l₁ ++ l₂) = l₁

Tactic:
;

Goal state after:
α : Type u
inst✝ : Inhabited α
l₁ l₂ : List α
n : ℕ
h : l₁.length = n
⊢ takeI l₁.length (l₁ ++ l₂) = l₁
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD l₁.length (l₁ ++ l₂) a = l₁

Tactic:
;

Goal state after:
α : Type u
l₁ l₂ : List α
n : ℕ
a : α
h : l₁.length = n
⊢ takeD l₁.length (l₁ ++ l₂) a = l₁
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b = (a = b)

Tactic:
;

Goal state after:
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b = (a = b)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []

Tactic:
;

Goal state after:
case nil
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ [] = []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
⊢ Forall₂ R [] []
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
R : α → β → Prop
a : α
l₁ : List α
IH : ∀ {l₂ : List β}, l₁.length = l₂.length → (∀ {a : α} {b : β}, (a, b) ∈ l₁.zip l₂ → R a b) → Forall₂ R l₁ l₂
b : β
l₂ : List β
h₂ : ∀ {a_1 : α} {b_1 : β}, (a_1, b_1) ∈ (a :: l₁).zip (b :: l₂) → R a_1 b_1
h₁ : l₁.length = l₂.length
a✝ : α
b✝ : β
h : (a✝, b✝) ∈ l₁.zip l₂
⊢ a✝ = a ∧ b✝ = b ∨ (a✝, b✝) ∈ zipWith Prod.mk l₁ l₂
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c

Tactic:
;

Goal state after:
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n✝ : ℕ
a : α
as : List α
h✝ : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
h : p a ∧ ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ (pmap f (a :: as) h✝).eraseIdx (n + 1) = pmap f ((a :: as).eraseIdx (n + 1)) ⋯

Tactic:
;

Goal state after:
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
l : List α
hl : ∀ (a : α), a ∈ l → p a
n✝ : ℕ
a : α
as : List α
h✝ : ∀ (a_1 : α), a_1 ∈ a :: as → p a_1
h : p a ∧ ∀ (x : α), x ∈ as → p x
n : ℕ
⊢ (pmap f (a :: as) h✝).eraseIdx (n + 1) = pmap f ((a :: as).eraseIdx (n + 1)) ⋯
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ l₁✝
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)

Tactic:
;

Goal state after:
case mpr.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝ l₂✝ : List β
a✝¹ : β
a✝ : l₁✝ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝ → SublistForall₂ R l₁ l₂✝
l₁ : List α
hl1 : Forall₂ R l₁ l₁✝
⊢ SublistForall₂ R l₁ (a✝¹ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr.cons_cons.cons
α : Type u_1
β : Type u_2
R : α → β → Prop
l₂ l l₁✝¹ l₂✝ : List β
a✝² : β
a✝¹ : l₁✝¹ <+ l₂✝
ih : ∀ {l₁ : List α}, Forall₂ R l₁ l₁✝¹ → SublistForall₂ R l₁ l₂✝
a✝ : α
l₁✝ : List α
hr : R a✝ a✝²
hl : Forall₂ R l₁✝ l₁✝¹
⊢ SublistForall₂ R (a✝ :: l₁✝) (a✝² :: l₂✝)

Tactic:
exact SublistForall₂.cons hr (ih hl)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
by
  constructor <;> intro h
  · induction h with
    | nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
    | @cons a b l1 l2 rab _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
    | cons_right _ ih =>
      obtain ⟨l, hl1, hl2⟩ := ih
      exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
  · obtain ⟨l, hl1, hl2⟩ := h
    revert l₁
    induction hl2 with
    | slnil =>
      intro l₁ hl1
      rw [forall₂_nil_right_iff.1 hl1]
      exact SublistForall₂.nil
    | cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
    | cons_cons _ _ ih =>
      intro l₁ hl1
      obtain - | ⟨hr, hl⟩ := hl1
      exact SublistForall₂.cons hr (ih hl)

Goal state after:
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case ha
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 0 ≤ ε⁻¹

Tactic:
;

Goal state after:
case ha
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b ε : α
hε : 0 < ε
h : 2 * (ε * a) * b ≤ (ε * a) ^ 2 + b ^ 2
⊢ 0 ≤ ε⁻¹
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
wlog hle : length l₁ ≤ length l₂ generalizing l₁ l₂

Goal state after:
case inr
α : Type u_1
l₁ l₂ : List α
n : ℕ
a : α
this : ∀ {l₁ l₂ : List α}, l₁.length ≤ l₂.length → (l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂)
hle : ¬l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)

Tactic:
;

Goal state after:
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c = (a ~ c)
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case nil.nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []

Tactic:
;

Goal state after:
case nil.nil
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
⊢ (Forall₂ r ∘r Perm) [] []
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l

Tactic:
;

Goal state after:
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ = (Perm ∘r Forall₂ r) l₁ l₃
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
h : Injective length
⊢ Subsingleton α

Tactic:
;

Goal state after:
case mp
α : Type u
h : Injective length
⊢ Subsingleton α
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
h : Injective length
x y : α
⊢ x = y

Tactic:
;

Goal state after:
case mp
α : Type u
h : Injective length
x y : α
⊢ x = y
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]

Tactic:
;

Goal state after:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x] = [y]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case mp
α : Type u
h : Injective length
x y : α
⊢ [x].length = [y].length

Tactic:
;

Goal state after:
case mp
α : Type u
h : Injective length
x y : α
⊢ [x].length = [y].length
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f y✝ (f x✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))

Tactic:
;

Goal state after:
case swap'
α : Type u_1
β : Type u_2
f : α → β → β
l₁ l₂ : List α
lcomm : LeftCommutative f
x✝ y✝ : α
l₁✝ l₂✝ : List α
h✝ : l₁✝ ~ l₂✝
r : ∀ (b : β), foldr f b l₁✝ = foldr f b l₂✝
b : β
⊢ f y✝ (f x✝ (foldr f b l₁✝)) = f x✝ (f y✝ (foldr f b l₂✝))
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

pp: case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

pp: case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

pp: case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b

Tactic:
;

Goal state after:
case none.none
α : Type u_1
p : none.toList ~ none.toList
⊢ none = none

case none.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b

case some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none

case some.some
α : Type u_1
a b : α
p : (some a).toList ~ (some b).toList
⊢ some a = some b
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹.length = tail✝.length

Tactic:
;

Goal state after:
case e_tail
α : Type u
hα : Subsingleton α
head✝¹ : α
tail✝¹ : List α
ih : ∀ ⦃l2 : List α⦄, tail✝¹.length = l2.length → tail✝¹ = l2
head✝ : α
tail✝ : List α
hl : (head✝¹ :: tail✝¹).length = (head✝ :: tail✝).length
⊢ tail✝¹.length = tail✝.length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
h : l ≠ []
⊢ (∃ a b, l = [a, b]) ↔ l = [l.head h, l.getLast h]

Tactic:
;

Goal state after:
α : Type u
l : List α
h : l ≠ []
⊢ (∃ a b, l = [a, b]) ↔ l = [l.head h, l.getLast h]
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l l' : List α
f : α → β
hf : Function.Injective f
⊢ Relation.Comp (fun x1 x2 ↦ x1 = map f x2) (fun x1 x2 ↦ x1 ~ x2) (map f l) l' ↔ l ~ l'

Tactic:
by simp [Relation.Comp, map_inj_right hf]

Goal state after:
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ Forall₂ (fun c b ↦ f c ~ g b) l l

Tactic:
List.forall₂_same

Goal state after:
α : Type u_1
β : Type u_2
l : List α
f g : α → List β
h : ∀ (a : α), a ∈ l → f a ~ g a
⊢ ∀ (x : α), x ∈ l → f x ~ g x
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂

Tactic:
;

Goal state after:
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case refl
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂

Tactic:
;

Goal state after:
case refl
α : Type u
β : Type v
l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (map reverse (replicate n l)).reverse.flatten.head? = l.reverse.head?

Tactic:
List.map_replicate,

Goal state after:
α : Type u
n : ℕ
h : n ≠ 0
l : List α
⊢ (replicate n l.reverse).reverse.flatten.head? = l.reverse.head?
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse

Tactic:
;

Goal state after:
α : Type u
l : List α
a : α
⊢ [a].reverse ++ l.reverse = a :: l.reverse
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ l₂.getLast h₁ = l₂.getLast h₂

Tactic:
;

Goal state after:
α : Type u
l₂ : List α
h₂ h₁ : l₂ ≠ []
⊢ l₂.getLast h₁ = l₂.getLast h₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n)).prod * [f n].prod = (map f (range n)).prod * f n

Tactic:
prod_cons,

Goal state after:
M : Type u_4
inst✝ : Monoid M
f : ℕ → M
n : ℕ
⊢ (map f (range n)).prod * (f n * [].prod) = (map f (range n)).prod * f n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l✝ l₁ l₂ l : List α
i : ℕ
h : i < l.length - 1
⊢ i + 1 < l.length
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf b (b :: l) = 0
Module: Mathlib.Data.List.Basic

Goal state before:
pp: ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
h : [].length - 1 < [].length
⊢ False

Tactic:
;

Goal state after:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l l₁ l₂ : List α
h : [].length - 1 < [].length
⊢ False
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ : List α
n✝ : ℕ
a✝ : n✝ < max l₁.length l₁.length
⊢ l₁[n✝]? = l₁[n✝]?

Tactic:
;

Goal state after:
α : Type u
l₁ : List α
n✝ : ℕ
a✝ : n✝ < max l₁.length l₁.length
⊢ l₁[n✝]? = l₁[n✝]?
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod)

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * (xs.prod * (y * ys.prod))

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * (xs.prod * (y * ys.prod))
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| xs.prod * (y * ys.prod)

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| xs.prod * (y * ys.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| y * (ys.prod * xs.prod)

Tactic:
;

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| y * (ys.prod * xs.prod)
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : Group G
x : G
xs : List G
⊢ (x :: xs).prod⁻¹ = (map (fun x ↦ x⁻¹) (x :: xs)).reverse.prod

Tactic:
by simp [prod_append, prod_inv_reverse xs]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ ((map g ∘ map f) l)[i✝]? = some a✝ ↔ (map (g ∘ f) l)[i✝]? = some a✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
g : β → γ
f : α → β
l : List α
i✝ : ℕ
a✝ : γ
⊢ ((map g ∘ map f) l)[i✝]? = some a✝ ↔ (map (g ∘ f) l)[i✝]? = some a✝
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
x✝ : ℕ
⊢ ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) x✝ = f x✝ / f (x✝ + 1)

Tactic:
;

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
x✝ : ℕ
⊢ ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) x✝ = f x✝ / f (x✝ + 1)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂

Tactic:
;

Goal state after:
α : Type u
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ replicate l.length b₂
⊢ b₁ = b₂