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

Goal state before:
pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)

pp: case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
·

Goal state after:
case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a₁✝¹ : α
l₁✝¹ : List α
hbc : Rₐ a₁✝¹ head✝
tbc : SublistForall₂ Rₐ l₁✝¹ tail✝
a₁✝ : α
l₁✝ : List α
hab : Rₐ a₁✝ a₁✝¹
tab : SublistForall₂ Rₐ l₁✝ l₁✝¹
⊢ SublistForall₂ Rₐ (a₁✝ :: l₁✝) (head✝ :: tail✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
·

Goal state after:
case cons.cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
atb : SublistForall₂ Rₐ a l₁✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
·

Goal state after:
case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
Module: Mathlib.Data.List.Perm.Basic

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

pp: α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
⊢ l₁.insertIdx n a ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
·

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₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂.insertIdx n a

pp: case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂

Tactic:
·

Goal state after:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂.insertIdx n a
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂

Tactic:
·

Goal state after:
case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂
Module: Mathlib.Data.List.Perm.Basic

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

pp: case mpr
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

pp: case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case swap
α : Type u_1
β : Type u_2
r : α → β → Prop
l u : List α
a₁ a₂ : α
h₂₃ : List α
v : List β
huv : Forall₂ r (a₁ :: a₂ :: h₂₃) v
⊢ (Forall₂ r ∘r Perm) (a₂ :: a₁ :: h₂₃) v

Tactic:
obtain - | ⟨h₁, hr₂₃⟩ := huv
    obtain - | ⟨h₂, h₁₂⟩ := hr₂₃
    exact ⟨_, Forall₂.cons h₂ (Forall₂.cons h₁ h₁₂), Perm.swap _ _ _⟩

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

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
a b : α
l : List α
h : a ∈ b :: l
hab : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l
Module: Mathlib.Data.List.Basic

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

pp: case mpr
α : Type u
⊢ Subsingleton α → Injective length

Tactic:
·

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

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

pp: case mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃

Tactic:
·

Goal state after:
case mp
α : 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 mpr
α : Type u
⊢ Subsingleton α → Injective length

Tactic:
·

Goal state after:
case mpr
α : Type u
⊢ Subsingleton α → Injective length
Module: Mathlib.Data.List.Perm.Basic

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

Tactic:
·

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

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

pp: case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

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

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

Tactic:
·

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

Goal state before:
pp: case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝

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

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

Tactic:
·

Goal state after:
case mpr.nil.cons
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
hl : [].length = (head✝ :: tail✝).length
⊢ [] = head✝ :: tail✝
Module: Mathlib.Data.List.Basic

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

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

Tactic:
·

Goal state after:
case mpr.cons.nil
α : Type u
hα : Subsingleton α
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ ⦃l2 : List α⦄, tail✝.length = l2.length → tail✝ = l2
hl : (head✝ :: tail✝).length = [].length
⊢ head✝ :: tail✝ = []
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
Module: Mathlib.Data.List.Basic

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

Tactic:
·

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

Goal state before:
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.some
α : Type u_1
b : α
p : none.toList ~ (some b).toList
⊢ none = some b
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
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 some.none
α : Type u_1
a : α
p : (some a).toList ~ none.toList
⊢ some a = none
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
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 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_head
α : 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
⊢ head✝¹ = head✝

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✝¹ = tail✝

Tactic:
·

Goal state after:
case e_head
α : 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
⊢ head✝¹ = head✝
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✝¹ = tail✝

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✝¹ = tail✝
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a

pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ l ⊆ [a, b] ↔ ∀ (c : α), c ∈ l → c = b ∨ c = a
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
l : List α
a b : α
m n : ℕ
h : a ≠ b
⊢ (∀ (c : α), c ∈ l → c = b ∨ c = a) ↔ ∀ (c : α), c ≠ b → c ≠ a → ¬c ∈ l
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length

pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length

Tactic:
·

Goal state after:
case nil
M : Type u_4
inst✝ : Monoid M
h : [].prod ≠ 1
⊢ 0 < [].length
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length

Tactic:
·

Goal state after:
case cons
M : Type u_4
inst✝ : Monoid M
head✝ : M
tail✝ : List M
h : (head✝ :: tail✝).prod ≠ 1
⊢ 0 < (head✝ :: tail✝).length
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : ¬n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : ¬n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
hn : ¬n = 0
⊢ (if m + n = 0 then 0 else 0 ^ (m + n)) = if n = 0 then 0 else if m = 0 then 0 else 0 ^ m * 0 ^ n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m + n) = zpow' a m * zpow' a n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case inl
α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = 0 ↔ a = 0

pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = 0 ↔ a = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
hn : n ≠ 0
⊢ zpow' a n = 0 ↔ a = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
h : ¬a = 0
⊢ (if a = 0 ∧ 0 = 0 then 0 else 1) = a / a
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
⊢ zpow' a 0 = a / a

Tactic:
by
  simp [zpow']
  by_cases h : a = 0
  · simp [h]
  · simp [h]

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : a = 0 ∧ n = 0
⊢ (a = 0 → ¬n = 0) → a ^ n = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℤ
h : ¬(a = 0 ∧ n = 0)
⊢ a = 0 → ¬n = 0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : a = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : n = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

pp: case neg
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : ¬m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : GroupWithZero α
a : α
m n : ℤ
ha : ¬a = 0
hn : ¬n = 0
hm : m = 0
⊢ zpow' a (m * n) = zpow' (zpow' a m) n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ^ ↑n = a ^ n

pp: case hn
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ ↑n ≠ 0

Tactic:
·

Goal state after:
α : Type u_1
inst✝ : GroupWithZero α
a : α
n : ℕ
hn : n ≠ 0
⊢ a ^ ↑n = a ^ n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

pp: case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : a = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

pp: case neg
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : ¬b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : CommGroupWithZero α
n : ℤ
a b : α
ha : ¬a = 0
hb : b = 0
⊢ zpow' (a * b) n = zpow' a n * zpow' b n
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case nil
α : Type u
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ ([] ++ t).head! = [].head!

pp: case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!

Tactic:
·

Goal state after:
case nil
α : Type u
inst✝ : Inhabited α
t : List α
h : [] ≠ []
⊢ ([] ++ t).head! = [].head!
Module: Mathlib.Data.List.Basic

Goal state before:
pp: case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!

Tactic:
·

Goal state after:
case cons
α : Type u
inst✝ : Inhabited α
t : List α
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ≠ [] → (tail✝ ++ t).head! = tail✝.head!
h : head✝ :: tail✝ ≠ []
⊢ (head✝ :: tail✝ ++ t).head! = (head✝ :: tail✝).head!