mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
a : α
⊢ Sum.inl a ∈ sumEquiv.symm s → Sum.elim f g (Sum.inl a) ∈ t

pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
b : β
⊢ Sum.inr b ∈ sumEquiv.symm s → Sum.elim f g (Sum.inr b) ∈ t

Tactic:
<;>

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
a : α
⊢ Sum.inl a ∈ sumEquiv.symm s → Sum.elim f g (Sum.inl a) ∈ t

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
t : Set γ
hf : MapsTo f s.1 t
hg : MapsTo g s.2 t
b : β
⊢ Sum.inr b ∈ sumEquiv.symm s → Sum.elim f g (Sum.inr b) ∈ t
Module: Mathlib.Order.Hom.Set

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

pp: case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

pp: case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inl a₁ = Sum.inl a₂

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
a₁ : α
h₁ : Sum.inl a₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inl a₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inl a₁ = Sum.inr b₂

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
a₂ : α
h₂ : Sum.inl a₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inl a₂)
⊢ Sum.inr b₁ = Sum.inl a₂

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → γ
g : β → γ
s : Set α × Set β
hf : InjOn f s.1
hg : InjOn g s.2
hfg : ∀ (a : α), a ∈ s.1 → ∀ (b : β), b ∈ s.2 → f a ≠ g b
b₁ : β
h₁ : Sum.inr b₁ ∈ sumEquiv.symm s
b₂ : β
h₂ : Sum.inr b₂ ∈ sumEquiv.symm s
heq : Sum.elim f g (Sum.inr b₁) = Sum.elim f g (Sum.inr b₂)
⊢ Sum.inr b₁ = Sum.inr b₂
Module: Mathlib.Order.Bounds.Basic

Goal state before:
pp: case inl
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : a ≤ b
⊢ min a b ∈ s ∪ t

pp: case inr
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : b ≤ a
⊢ min a b ∈ s ∪ t

Tactic:
<;>

Goal state after:
case inl
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : a ≤ b
⊢ min a b ∈ s ∪ t

case inr
γ : Type u_3
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsLeast s a
hb : IsLeast t b
h : b ≤ a
⊢ min a b ∈ s ∪ t
Module: Mathlib.Control.Functor

Goal state before:
pp: case map_const
γ : Type u_1
⊢ ∀ {α β : Type u_2}, mapConst = map ∘ Function.const β

pp: case id_map
γ : Type u_1
⊢ ∀ {α : Type u_2} (x : Const γ α), id <$> x = x

pp: case comp_map
γ : Type u_1
⊢ ∀ {α β γ_1 : Type u_2} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x

Tactic:
<;>

Goal state after:
case map_const
γ : Type u_1
⊢ ∀ {α β : Type u_2}, mapConst = map ∘ Function.const β

case id_map
γ : Type u_1
⊢ ∀ {α : Type u_2} (x : Const γ α), id <$> x = x

case comp_map
γ : Type u_1
⊢ ∀ {α β γ_1 : Type u_2} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x
Module: Mathlib.Control.Functor

Goal state before:
pp: case map_const
γ : Type u_1
α✝ β✝ : Type u_2
⊢ mapConst = map ∘ Function.const β✝

pp: case id_map
γ : Type u_1
α✝ : Type u_2
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝

pp: case comp_map
γ : Type u_1
α✝ β✝ γ✝ : Type u_2
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝

Tactic:
<;>

Goal state after:
case map_const
γ : Type u_1
α✝ β✝ : Type u_2
⊢ mapConst = map ∘ Function.const β✝

case id_map
γ : Type u_1
α✝ : Type u_2
x✝ : Const γ α✝
⊢ id <$> x✝ = x✝

case comp_map
γ : Type u_1
α✝ β✝ γ✝ : Type u_2
g✝ : α✝ → β✝
h✝ : β✝ → γ✝
x✝ : Const γ α✝
⊢ (h✝ ∘ g✝) <$> x✝ = h✝ <$> g✝ <$> x✝
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n

pp: case refine_2
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ n

case refine_2
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ 0 < a ^ m
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ n

pp: case refine_2
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ m

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ n

case refine_2
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ 0 < a ^ m
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

pp: case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ m)⁻¹ = 1 / a ^ m

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 ≤ a
m n : ℕ
mn : m ≤ n
⊢ (a ^ m)⁻¹ = 1 / a ^ m
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

pp: case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ m)⁻¹ = 1 / a ^ m

Tactic:
<;>

Goal state after:
case e'_3
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ n)⁻¹ = 1 / a ^ n

case e'_4
α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a : α
inst✝ : IsStrictOrderedRing α
a1 : 1 < a
m n : ℕ
mn : m < n
⊢ (a ^ m)⁻¹ = 1 / a ^ m
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Semifield α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
a b : α
inst✝ : IsStrictOrderedRing α
s : Set α
ha : 0 ≤ a
hs : IsGLB s b
⊢ IsGLB ((fun b ↦ a * b) '' s) (a * b)

Tactic:
by
  rcases lt_or_eq_of_le ha with (ha | rfl)
  · exact (OrderIso.mulLeft₀ _ ha).isGLB_image'.2 hs
  · simp_rw [zero_mul]
    rw [hs.nonempty.image_const]
    exact isGLB_singleton

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

Goal state before:
pp: case zero
α : Type u_1
f : α → α
a : α
l : List α
⊢ iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0

pp: case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α) (l : List α), iterateTR.loop f a n✝ l = l.reverse ++ iterate f a n✝
a : α
l : List α
⊢ iterateTR.loop f a (n✝ + 1) l = l.reverse ++ iterate f a (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
f : α → α
a : α
l : List α
⊢ iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0

case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α) (l : List α), iterateTR.loop f a n✝ l = l.reverse ++ iterate f a n✝
a : α
l : List α
⊢ iterateTR.loop f a (n✝ + 1) l = l.reverse ++ iterate f a (n✝ + 1)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case succ.nil
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
⊢ tail^[n + 1] [] = drop (n + 1) []

pp: case succ.cons
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
head✝ : α
tail✝ : List α
⊢ tail^[n + 1] (head✝ :: tail✝) = drop (n + 1) (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case succ.nil
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
⊢ tail^[n + 1] [] = drop (n + 1) []

case succ.cons
α : Type u
n : ℕ
ih : ∀ (l : List α), tail^[n] l = drop n l
head✝ : α
tail✝ : List α
⊢ tail^[n + 1] (head✝ :: tail✝) = drop (n + 1) (head✝ :: tail✝)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case false
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = false
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

pp: case true
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = true
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

Tactic:
<;>

Goal state after:
case false
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = false
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))

case true
α : Type u
p : α → Bool
a : α
l l₂ : List α
hp : p a = true
⊢ loop p (a :: l) l₂ = (l₂.reverse ++ takeWhile p (a :: l), dropWhile p (a :: l))
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []

pp: case cons
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S (a✝² :: l₁✝) (b✝ :: l₂✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []

case cons
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S (a✝² :: l₁✝) (b✝ :: l₂✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝

pp: case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝

Tactic:
<;>

Goal state after:
case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝

case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case zero
α : Type u
a : α
l : List α
hn : 0 ≠ l.length
⊢ (l.eraseIdx 0).insertIdx 0 a = l.set 0 a

pp: case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
l : List α
hn : n✝ + 1 ≠ l.length
⊢ (l.eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = l.set (n✝ + 1) a

Tactic:
<;>

Goal state after:
case zero
α : Type u
a : α
l : List α
hn : 0 ≠ l.length
⊢ (l.eraseIdx 0).insertIdx 0 a = l.set 0 a

case succ
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
l : List α
hn : n✝ + 1 ≠ l.length
⊢ (l.eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = l.set (n✝ + 1) a
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case zero.nil
α : Type u
a : α
hn : 0 ≠ [].length
⊢ ([].eraseIdx 0).insertIdx 0 a = [].set 0 a

pp: case zero.cons
α : Type u
a head✝ : α
tail✝ : List α
hn : 0 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx 0).insertIdx 0 a = (head✝ :: tail✝).set 0 a

pp: case succ.nil
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
hn : n✝ + 1 ≠ [].length
⊢ ([].eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = [].set (n✝ + 1) a

pp: case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
head✝ : α
tail✝ : List α
hn : n✝ + 1 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = (head✝ :: tail✝).set (n✝ + 1) a

Tactic:
<;>

Goal state after:
case zero.nil
α : Type u
a : α
hn : 0 ≠ [].length
⊢ ([].eraseIdx 0).insertIdx 0 a = [].set 0 a

case zero.cons
α : Type u
a head✝ : α
tail✝ : List α
hn : 0 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx 0).insertIdx 0 a = (head✝ :: tail✝).set 0 a

case succ.nil
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
hn : n✝ + 1 ≠ [].length
⊢ ([].eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = [].set (n✝ + 1) a

case succ.cons
α : Type u
a : α
n✝ : ℕ
a✝ : ∀ {l : List α}, n✝ ≠ l.length → (l.eraseIdx n✝).insertIdx n✝ a = l.set n✝ a
head✝ : α
tail✝ : List α
hn : n✝ + 1 ≠ (head✝ :: tail✝).length
⊢ ((head✝ :: tail✝).eraseIdx (n✝ + 1)).insertIdx (n✝ + 1) a = (head✝ :: tail✝).set (n✝ + 1) a
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case zero.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx 0 (f a ha) = pmap f ([].insertIdx 0 a) ⋯

pp: case zero.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx 0 (f a ha) = pmap f ((head✝ :: tail✝).insertIdx 0 a) ⋯

Tactic:
<;>

Goal state after:
case zero.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx 0 (f a ha) = pmap f ([].insertIdx 0 a) ⋯

case zero.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx 0 (f a ha) = pmap f ((head✝ :: tail✝).insertIdx 0 a) ⋯
Module: Mathlib.Data.List.InsertIdx

Goal state before:
pp: case succ.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx (n + 1) (f a ha) = pmap f ([].insertIdx (n + 1) a) ⋯

pp: case succ.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx (n + 1) (f a ha) = pmap f ((head✝ :: tail✝).insertIdx (n + 1) a) ⋯

Tactic:
<;>

Goal state after:
case succ.nil
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
hl : ∀ (x : α), x ∈ [] → p x
⊢ (pmap f [] hl).insertIdx (n + 1) (f a ha) = pmap f ([].insertIdx (n + 1) a) ⋯

case succ.cons
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
a : α
ha : p a
n : ℕ
ihn : ∀ {l : List α} (hl : ∀ (x : α), x ∈ l → p x), (pmap f l hl).insertIdx n (f a ha) = pmap f (l.insertIdx n a) ⋯
head✝ : α
tail✝ : List α
hl : ∀ (x : α), x ∈ head✝ :: tail✝ → p x
⊢ (pmap f (head✝ :: tail✝) hl).insertIdx (n + 1) (f a ha) = pmap f ((head✝ :: tail✝).insertIdx (n + 1) a) ⋯
Module: Mathlib.Data.List.Forall2

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

pp: case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ → ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inr
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m ≥ l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
rw [getElem?_eq_none hm, eq_comm, getElem?_eq_none_iff] at h
    rw [eraseIdx_of_length_le h, eraseIdx_of_length_le hm]

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

Goal state before:
pp: case mpr.nil
α : Type u
hα : Subsingleton α
l2 : List α
hl : [].length = l2.length
⊢ [] = l2

pp: case mpr.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
l2 : List α
hl : (head✝ :: tail✝).length = l2.length
⊢ head✝ :: tail✝ = l2

Tactic:
<;>

Goal state after:
case mpr.nil
α : Type u
hα : Subsingleton α
l2 : List α
hl : [].length = l2.length
⊢ [] = l2

case mpr.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
l2 : List α
hl : (head✝ :: tail✝).length = l2.length
⊢ head✝ :: tail✝ = l2
Module: Mathlib.Data.List.Perm.Basic

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

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

Tactic:
<;>

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

case some
α : Type u_1
o₂ : Option α
a : α
p : (some a).toList ~ o₂.toList
⊢ some a = o₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
hl : [x] ≠ []
⊢ (map ⇑f [x]).prod = f [x].prod

pp: case cons
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
head✝ : M
tail✝ : List M
tail_ih✝ : ∀ (x : M), x :: tail✝ ≠ [] → (map (⇑f) (x :: tail✝)).prod = f (x :: tail✝).prod
x : M
hl : x :: head✝ :: tail✝ ≠ []
⊢ (map (⇑f) (x :: head✝ :: tail✝)).prod = f (x :: head✝ :: tail✝).prod

Tactic:
<;>

Goal state after:
case nil
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
x : M
hl : [x] ≠ []
⊢ (map ⇑f [x]).prod = f [x].prod

case cons
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
l : List M
F : Type u_8
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
hl✝ : l ≠ []
head✝ : M
tail✝ : List M
tail_ih✝ : ∀ (x : M), x :: tail✝ ≠ [] → (map (⇑f) (x :: tail✝)).prod = f (x :: tail✝).prod
x : M
hl : x :: head✝ :: tail✝ ≠ []
⊢ (map (⇑f) (x :: head✝ :: tail✝)).prod = f (x :: head✝ :: tail✝).prod
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
hl : [x] ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) [x]).prod = f (map f₁ [x]).prod (map f₂ [x]).prod

pp: case cons
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
head✝ : ι
tail✝ : List ι
tail_ih✝ :
  ∀ (x : ι),
    x :: tail✝ ≠ [] →
      (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: tail✝)).prod = f (map f₁ (x :: tail✝)).prod (map f₂ (x :: tail✝)).prod
x : ι
hl : x :: head✝ :: tail✝ ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: head✝ :: tail✝)).prod =
    f (map f₁ (x :: head✝ :: tail✝)).prod (map f₂ (x :: head✝ :: tail✝)).prod

Tactic:
<;>

Goal state after:
case nil
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
hl : [x] ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) [x]).prod = f (map f₁ [x]).prod (map f₂ [x]).prod

case cons
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
head✝ : ι
tail✝ : List ι
tail_ih✝ :
  ∀ (x : ι),
    x :: tail✝ ≠ [] →
      (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: tail✝)).prod = f (map f₁ (x :: tail✝)).prod (map f₂ (x :: tail✝)).prod
x : ι
hl : x :: head✝ :: tail✝ ≠ []
⊢ (map (fun i ↦ f (f₁ i) (f₂ i)) (x :: head✝ :: tail✝)).prod =
    f (map f₁ (x :: head✝ :: tail✝)).prod (map f₂ (x :: head✝ :: tail✝)).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ []).flatten.head? = [].head?

pp: case cons
α : Type u
n : ℕ
h : n.succ ≠ 0
head✝ : α
tail✝ : List α
tail_ih✝ : (replicate n.succ tail✝).flatten.head? = tail✝.head?
⊢ (replicate n.succ (head✝ :: tail✝)).flatten.head? = (head✝ :: tail✝).head?

Tactic:
<;>

Goal state after:
case nil
α : Type u
n : ℕ
h : n.succ ≠ 0
⊢ (replicate n.succ []).flatten.head? = [].head?

case cons
α : Type u
n : ℕ
h : n.succ ≠ 0
head✝ : α
tail✝ : List α
tail_ih✝ : (replicate n.succ tail✝).flatten.head? = tail✝.head?
⊢ (replicate n.succ (head✝ :: tail✝)).flatten.head? = (head✝ :: tail✝).head?