mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)

pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Tactic:
·

Goal state after:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ IsPeriodicPt f (minimalPeriod f x) (f^[n] x)
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f

Tactic:
·

Goal state after:
α : Type u_1
f : α → α
x : α
hx : x ∈ periodicPts f
n : ℕ
⊢ f^[n] x ∈ periodicPts f
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is

Tactic:
·

Goal state after:
case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
m : l₁ ++ l₂ ∈ is :: is.permutationsAux []
left✝ : l₂ ≠ []
⊢ l₁ ++ t :: l₂ ++ ts ~ t :: ts ++ is
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x

pp: case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
f : α → α
x : α
h : minimalPeriod f x = 1
⊢ IsFixedPt f x
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is

pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
m : l₁ ++ l₂ ∈ is.permutationsAux []
⊢ l₁ ++ l₂ ~ is

Tactic:
·

Goal state after:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ∈ ts.permutationsAux (t :: is) → l ~ ts ++ t :: is
IH2 : ∀ (l : List α), l ∈ is.permutationsAux [] → l ~ is ++ []
l₁ l₂ : List α
left✝ : l₂ ≠ []
e : l₁ ++ l₂ = is
⊢ l₁ ++ l₂ ~ is
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
f : α → α
x : α
h : IsFixedPt f x
⊢ minimalPeriod f x = 1
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n

pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x

Tactic:
·

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f^[n] x ∣ minimalPeriod f x / (minimalPeriod f x).gcd n
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x

Tactic:
·

Goal state after:
case a
α : Type u_1
f : α → α
x : α
n : ℕ
h : 0 < (minimalPeriod f x).gcd n
⊢ minimalPeriod f x / (minimalPeriod f x).gcd n ∣ minimalPeriod f^[n] x
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

pp: case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
·

Goal state after:
case pos
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
·

Goal state after:
case inl
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
is' : List α
p' : is' ~ t :: is
e : l = is' ++ ts
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_1
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) →
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)

pp: case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)

Tactic:
·

Goal state after:
case pos.refine_1
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
⊢ (r (f^[minimalPeriod f x - succ 0] x) (f^[0] x) ∧ ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)) →
    ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl.nil
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts

pp: case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
·

Goal state after:
case inl.nil
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
p' : l₁ ++ [t] ~ t :: is
p : l₁ ++ [] ~ is
⊢ (∃ is' x, l₁ ++ [t] ++ ts = is' ++ t :: ts) ∨
    l₁ ++ [t] ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ [t] ++ ts = l₁_1 ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_1.inl
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

pp: case pos.refine_1.inr
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
·

Goal state after:
case pos.refine_1.inl
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n = minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts

Tactic:
·

Goal state after:
case inl.cons
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l₁ : List α
a : α
l₂' : List α
p' : l₁ ++ t :: a :: l₂' ~ t :: is
p : l₁ ++ a :: l₂' ~ is
⊢ (∃ is' x, l₁ ++ t :: a :: l₂' ++ ts = is' ++ t :: ts) ∨
    l₁ ++ t :: a :: l₂' ++ ts ∈ ts.permutationsAux (t :: is) ∨
      ∃ l₁_1 l₂, l₁_1 ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l₁ ++ t :: a :: l₂' ++ ts = l₁_1 ++ t :: l₂ ++ ts
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_1.inr
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)

Tactic:
·

Goal state after:
case pos.refine_1.inr
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
hr : r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
H : ∀ m < minimalPeriod f x - succ 0, r (f^[m] x) (f^[m.succ] x)
n : ℕ
hn : n < minimalPeriod f x - succ 0 + succ 0
hM' : n < minimalPeriod f x - succ 0
⊢ r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts

Tactic:
·

Goal state after:
case inr
α : Type u_1
t : α
ts is : List α
IH1 : ∀ (l : List α), l ~ t :: is ++ ts → (∃ is' x, l = is' ++ ts) ∨ l ∈ ts.permutationsAux (t :: is)
IH2 : ∀ (l : List α), l ~ [] ++ is → (∃ is' x, l = is' ++ is) ∨ l ∈ is.permutationsAux []
l : List α
p : l ~ is ++ t :: ts
m : l ∈ ts.permutationsAux (t :: is)
⊢ (∃ is' x, l = is' ++ t :: ts) ∨
    l ∈ ts.permutationsAux (t :: is) ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ is.permutations ∧ l₂ ≠ [] ∧ l = l₁ ++ t :: l₂ ++ ts
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = [].nextOr x d

pp: case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Tactic:
·

Goal state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
⊢ [y].nextOr x d = [].nextOr x d
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)

Tactic:
·

Goal state after:
case pos.refine_2
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∈ periodicPts f
hx' : 0 < minimalPeriod f x
hM : minimalPeriod f x - succ 0 + succ 0 = minimalPeriod f x
H : ∀ n < minimalPeriod f x - succ 0 + succ 0, r (f^[n] x) (f^[n + 1] x)
⊢ r (f^[minimalPeriod f x - succ 0] x) (f^[0] x)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d

Tactic:
·

Goal state after:
case cons
α : Type u_1
inst✝ : DecidableEq α
y x d : α
h : x ≠ y
z : α
zs : List α
⊢ (y :: z :: zs).nextOr x d = (z :: zs).nextOr x d
Module: Mathlib.Dynamics.PeriodicPts.Defs

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)

Tactic:
·

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : α → α
x : α
hx : x ∉ periodicPts f
⊢ Cycle.Chain r (periodicOrbit f x) ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : x ∈ [].dropLast → [].nextOr x d = [].nextOr x d'
x_mem : x ∈ [y].dropLast
⊢ [y].nextOr x d = [y].nextOr x d'

pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d d' y : α
IH : x ∈ [].dropLast → [].nextOr x d = [].nextOr x d'
x_mem : x ∈ [y].dropLast
⊢ [y].nextOr x d = [y].nextOr x d'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d d' y z : α
zs : List α
IH : x ∈ (z :: zs).dropLast → (z :: zs).nextOr x d = (z :: zs).nextOr x d'
x_mem : x ∈ (y :: z :: zs).dropLast
h : ¬x = y
⊢ (y :: z :: zs).nextOr x d = (y :: z :: zs).nextOr x d'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d y : α
IH : [].nextOr x d ≠ d → x ∈ []
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]

pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d y : α
IH : [].nextOr x d ≠ d → x ∈ []
h : [y].nextOr x d ≠ d
⊢ x ∈ [y]
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs

Tactic:
·

Goal state after:
case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
⊢ x ∈ y :: z :: zs
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ : List α
⊢ ∀ (a : List α),
    a ∈ l✝.permutations' →
      flatMap (permutations'Aux y✝) (permutations'Aux x✝ a) ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ a)

Tactic:
intro l'

Goal state after:
case swap
α : Type u_1
s t : List α
x✝ y✝ : α
l✝ l' : List α
⊢ l' ∈ l✝.permutations' →
    flatMap (permutations'Aux y✝) (permutations'Aux x✝ l') ~ flatMap (permutations'Aux x✝) (permutations'Aux y✝ l')
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : x = y
⊢ x ∈ y :: z :: zs

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : x = y
⊢ x ∈ y :: z :: zs
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d y z : α
zs : List α
IH : (z :: zs).nextOr x d ≠ d → x ∈ z :: zs
h : (y :: z :: zs).nextOr x d ≠ d
hx : ¬x = y
⊢ x ∈ y :: z :: zs
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ih : (∀ x ∈ [], x ∈ xs') → [].nextOr x d ∈ xs'
hxs' : ∀ x ∈ [y], x ∈ xs'
⊢ [y].nextOr x d ∈ xs'

pp: case cons.cons
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
⊢ (y :: z :: zs).nextOr x d ∈ xs'

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y : α
ih : (∀ x ∈ [], x ∈ xs') → [].nextOr x d ∈ xs'
hxs' : ∀ x ∈ [y], x ∈ xs'
⊢ [y].nextOr x d ∈ xs'
Module: Mathlib.Data.List.Permutation

Goal state before:
pp: case succ.refine_1
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
x✝ : [].length < n + 1
⊢ [].permutations ~ [].permutations'

pp: case succ.refine_2
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts✝ : List α
h✝ : ts✝.length < n + 1
ts : List α
t : α
x✝ : ts.length < n + 1 → ts.permutations ~ ts.permutations'
h : (ts ++ [t]).length < n + 1
⊢ (ts ++ [t]).permutations ~ (ts ++ [t]).permutations'

Tactic:
·

Goal state after:
case succ.refine_1
α : Type u_1
n : ℕ
IH : ∀ (ts : List α), ts.length < n → ts.permutations ~ ts.permutations'
ts : List α
h : ts.length < n + 1
x✝ : [].length < n + 1
⊢ [].permutations ~ [].permutations'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'

pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : x = y
⊢ z ∈ xs'
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
x d : α
xs' : List α
hd : d ∈ xs'
y z : α
zs : List α
ih : (∀ x ∈ z :: zs, x ∈ xs') → (z :: zs).nextOr x d ∈ xs'
hxs' : ∀ x ∈ y :: z :: zs, x ∈ xs'
h : ¬x = y
⊢ (z :: zs).nextOr x d ∈ xs'
Module: Mathlib.Algebra.Star.Subalgebra

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S : StarSubalgebra R A
h : ∀ (x : A), x ∈ S
x : A
⊢ x ∈ S ↔ x ∈ ⊤

Tactic:
exact ⟨fun _ => mem_top, fun _ => h x⟩

Goal state after:
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

pp: case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt (f ∘ g) (minimalPeriod g x * minimalPeriod (f ∘ g) x) x
Module: Mathlib.Dynamics.PeriodicPts.Lemmas

Goal state before:
pp: case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
f✝ : α → α
x : α
g✝ : α → α
h✝ : Function.Commute f✝ g✝
hco✝ : (minimalPeriod f✝ x).Coprime (minimalPeriod g✝ x)
f g : α → α
h : Function.Commute f g
hco : (minimalPeriod f x).Coprime (minimalPeriod g x)
⊢ IsPeriodicPt g (minimalPeriod g x * minimalPeriod (f ∘ g) x) x