mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K

pp: case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ?refine_2.refine_1⟩ ∈ H.subgroupOf K

Tactic:
·

Goal state after:
case refine_2.refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ gv ∈ K
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ⋯⟩ ∈ H.subgroupOf K

Tactic:
·

Goal state after:
case refine_2.refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H K : Subgroup G
b✝ : α
gv : G
gp✝ : gv ∈ Subgroup.map K.subtype (H.subgroupOf K)
gp : gv ∈ H ∧ gv ∈ K
⊢ ⟨gv, ⋯⟩ ∈ H.subgroupOf K
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ IsPretransitive G α ↔ Subsingleton (orbitRel.Quotient G α)

Tactic:
refine ⟨fun _ ↦ ⟨fun a b ↦ ?_⟩, fun _ ↦ ⟨fun a b ↦ ?_⟩⟩

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b

pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : IsPretransitive G α
a b : orbitRel.Quotient G α
⊢ a = b
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x✝ : Subsingleton (orbitRel.Quotient G α)
a b : α
⊢ ∃ g, g • a = b
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ y : α
yh : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
z : α
zh : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
⊢ ∃ g, g • ⟨y, yh⟩ = ⟨z, zh⟩

Tactic:
rw [orbitRel.Quotient.mem_orbit, Quotient.eq''] at yh zh

Goal state after:
case h
G : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MulAction G β
a✝ y : α
yh✝ : y ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
yh : (orbitRel G α) y a✝
z : α
zh✝ : z ∈ orbitRel.Quotient.orbit (Quotient.mk'' a✝)
zh : (orbitRel G α) z a✝
⊢ ∃ g, g • ⟨y, yh✝⟩ = ⟨z, zh✝⟩
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length

pp: case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
·

Goal state after:
case nil
α : Type u_1
hl : [].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[] ∧ y ∈ ↑[]) ↔ 2 ≤ [].length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length

pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
hd : α
hl : [hd].Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑[hd] ∧ y ∈ ↑[hd]) ↔ 2 ≤ [hd].length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length

Tactic:
·

Goal state after:
case cons.cons
α : Type u_1
hd hd' : α
tl : List α
hl : (hd :: hd' :: tl).Nodup
⊢ (∃ x y, x ≠ y ∧ x ∈ ↑(hd :: hd' :: tl) ∧ y ∈ ↑(hd :: hd' :: tl)) ↔ 2 ≤ (hd :: hd' :: tl).length
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.nil
α : Type u_1
x y : α
hxy : x ≠ y
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) []
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) []
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [])

pp: case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

pp: case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
·

Goal state after:
case h.nil
α : Type u_1
x y : α
hxy : x ≠ y
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) []
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) []
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])

pp: case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
·

Goal state after:
case h.cons.nil
α : Type u_1
x y : α
hxy : x ≠ y
hd : α
hx : x ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
hy : y ∈ Quot.mk ⇑(IsRotated.setoid α) [hd]
⊢ 2 ≤ length (Quot.mk ⇑(IsRotated.setoid α) [hd])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))

Tactic:
·

Goal state after:
case h.cons.cons
α : Type u_1
x y : α
hxy : x ≠ y
hd hd' : α
tl : List α
hx : x ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
hy : y ∈ Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl)
⊢ 2 ≤ length (Quot.mk (⇑(IsRotated.setoid α)) (hd :: hd' :: tl))
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.nil
α : Type u_1
h : Subsingleton (Quot.mk ⇑(IsRotated.setoid α) [])
⊢ Nodup (Quot.mk ⇑(IsRotated.setoid α) [])

pp: case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
·

Goal state after:
case h.nil
α : Type u_1
h : Subsingleton (Quot.mk ⇑(IsRotated.setoid α) [])
⊢ Nodup (Quot.mk ⇑(IsRotated.setoid α) [])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))

Tactic:
·

Goal state after:
case h.cons
α : Type u_1
hd : α
tl : List α
h : Subsingleton (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
⊢ Nodup (Quot.mk (⇑(IsRotated.setoid α)) (hd :: tl))
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s

pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s

Tactic:
·

Goal state after:
case mp
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ H ≤ stabilizer G s → ∀ g ∈ H, g • s ⊆ s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s

Tactic:
·

Goal state after:
case mpr
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
⊢ (∀ g ∈ H, g • s ⊆ s) → H ≤ stabilizer G s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h.left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s

pp: case h.right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x ↦ g • x) (g⁻¹ • x) = x

Tactic:
·

Goal state after:
case h.left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ g⁻¹ • x ∈ s
Module: Mathlib.GroupTheory.GroupAction.Basic

Goal state before:
pp: case h.right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x ↦ g • x) (g⁻¹ • x) = x

Tactic:
·

Goal state after:
case h.right
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
H : Subgroup G
hyp : ∀ g ∈ H, g • s ⊆ s
g : G
hg : g ∈ H
x : α
hx : x ∈ s
⊢ (fun x ↦ g • x) (g⁻¹ • x) = x
Module: Mathlib.Data.Nat.Prime.Pow

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ (1 ^ k).minFac = minFac 1

pp: case inr
n k : ℕ
hk : k ≠ 0
hn : n ≠ 1
⊢ (n ^ k).minFac = n.minFac

Tactic:
·

Goal state after:
case inl
k : ℕ
hk : k ≠ 0
⊢ (1 ^ k).minFac = minFac 1
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
hab : (IsRotated.setoid α) [] []
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
·

Goal state after:
case nil.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
hab : (IsRotated.setoid α) [] []
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
·

Goal state after:
case nil.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
b : α
m : List α
hab : (IsRotated.setoid α) [] (b :: m)
⊢ (match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
·

Goal state after:
case cons.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
hab : (IsRotated.setoid α) (a :: l) []
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match [] with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])

Tactic:
·

Goal state after:
case cons.cons
α : Type u_1
r : α → α → Prop
c : Cycle α
a : α
l : List α
b : α
m : List α
hab : (IsRotated.setoid α) (a :: l) (b :: m)
⊢ (match a :: l with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])) ↔
    match b :: m with
    | [] => True
    | a :: m => IsChain r (a :: m ++ [a])
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons.succ.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
hn : [a].rotate (d + 1) = b :: m
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])

pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
·

Goal state after:
case cons.cons.succ.nil
α : Type u_1
r : α → α → Prop
c : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
hn : [a].rotate (d + 1) = b :: m
⊢ IsChain r ([a] ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

pp: case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mp
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k ≤ Nat.log 2 (p ^ k)

Tactic:
·

Goal state after:
case mp
p k : ℕ
hp' : Nat.Prime p
hk' : 0 < k
⊢ k ≤ Nat.log 2 (p ^ k)
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])

Tactic:
·

Goal state after:
case cons.cons.succ.cons
α : Type u_1
r : α → α → Prop
c✝ : Cycle α
d : ℕ
hd :
  ∀ (a : α) (l : List α) (b : α) (m : List α),
    (a :: l).rotate d = b :: m → (IsChain r (a :: l ++ [a]) ↔ IsChain r (b :: m ++ [b]))
a b : α
m : List α
c : α
s : List α
hn : (a :: c :: s).rotate (d + 1) = b :: m
⊢ IsChain r (a :: c :: s ++ [a]) ↔ IsChain r (b :: m ++ [b])
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
·

Goal state after:
case mpr
n : ℕ
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inl
⊢ (∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ p, p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k

pp: case inr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

Tactic:
·

Goal state after:
case inl
⊢ (∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ ∃ p, p ≤ 1 ∧ 1 = p ^ k ∧ Nat.Prime p) ↔
    ∃ k, k ≤ Nat.log 2 1 ∧ 0 < k ∧ 1 = Nat.minFac 1 ^ k
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mp
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k

pp: case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
·

Goal state after:
case inr.mp
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p

Tactic:
·

Goal state after:
case inr.mpr
n : ℕ
h : n ≠ 1
⊢ (∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ n = n.minFac ^ k) →
    ∃ k, k ≤ Nat.log 2 n ∧ 0 < k ∧ ∃ p, p ≤ n ∧ n = p ^ k ∧ Nat.Prime p
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr.refine_1
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ 0 < n

pp: case inr.mpr.refine_2
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ Nat.Prime n.minFac

Tactic:
·

Goal state after:
case inr.mpr.refine_1
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ 0 < n
Module: Mathlib.Algebra.IsPrimePow

Goal state before:
pp: case inr.mpr.refine_2
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ Nat.Prime n.minFac

Tactic:
·

Goal state after:
case inr.mpr.refine_2
n : ℕ
h : n ≠ 1
k : ℕ
hkle : k ≤ Nat.log 2 n
hk_pos : 0 < k
heq : n = n.minFac ^ k
⊢ Nat.Prime n.minFac
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod → ∃ a, a ∈ L ∧ p ∣ a

pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ L.prod

Tactic:
·

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ p ∣ L.prod → ∃ a, a ∈ L ∧ p ∣ a
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

pp: case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
·

Goal state after:
case mp.cons.inl
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_hd
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a

Tactic:
·

Goal state after:
case mp.cons.inr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
pp : Prime p
L_hd : M
L_tl : List M
L_ih : p ∣ L_tl.prod → ∃ a, a ∈ L_tl ∧ p ∣ a
h : p ∣ L_hd * L_tl.prod
hd : p ∣ L_tl.prod
⊢ ∃ a, a ∈ L_hd :: L_tl ∧ p ∣ a
Module: Mathlib.Data.List.Prime

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ L.prod

Tactic:
·

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
L : List M
pp : Prime p
⊢ (∃ a, a ∈ L ∧ p ∣ a) → p ∣ L.prod
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦[]⟧

pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦a :: l⟧

Tactic:
·

Goal state after:
case nil
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
⊢ Chain r (map f ⟦[]⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦[]⟧
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦a :: l⟧

Tactic:
·

Goal state after:
case cons
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Cycle β
a : β
l : List β
⊢ Chain r (map f ⟦a :: l⟧) ↔ Chain (fun a b ↦ r (f a) (f b)) ⟦a :: l⟧
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case nil
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil

pp: case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Tactic:
·

Goal state after:
case nil
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
p : Chain r₁ Cycle.nil
⊢ Chain r₂ Cycle.nil
Module: Mathlib.Data.List.Cycle

Goal state before:
pp: case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)

Tactic:
·

Goal state after:
case cons
α : Type u_1
s : Cycle α
r₁ r₂ : α → α → Prop
H : ∀ (a b : α), r₁ a b → r₂ a b
a✝¹ : α
l✝ : List α
a✝ : Chain r₁ ↑l✝ → Chain r₂ ↑l✝
p : Chain r₁ ↑(a✝¹ :: l✝)
⊢ Chain r₂ ↑(a✝¹ :: l✝)