Theorem: OnCycleFactors.k_cycle_apply (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
by_cases hx : x ∈ g.support
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Equiv.Perm.support g
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∈ Equiv.Perm.support g
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
simp only [mem_support_iff_exists_Kf a] at hx
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : ∃ c i, x = Kf a 1 (c, i)
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : ∃ c i, x = Kf a 1 (c, i)
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
obtain ⟨d, j, rfl⟩ := hx
State after:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))

State before:
case pos.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))
Tactic:
by_cases hcd : c = d
State after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))

State before:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))
Tactic:
rw [hcd, Equiv.Perm.Basis.Kf_apply',
  k_apply a d _ hτ, k_apply a d _ hτ, ← Equiv.Perm.Basis.Kf_apply']
State after:
case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ τ d = τ d

case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ d = 1 d

State before:
case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ τ d = τ d

case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ d = 1 d
Tactic:
rfl
State after:
case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ d = 1 d

State before:
case pos.hd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : c = d
⊢ d = 1 d
Tactic:
simp only [Equiv.Perm.coe_one, id.def]
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ k a τ (↑c (Kf a 1 (d, j))) = ↑(τ c) (k a τ (Kf a 1 (d, j)))
Tactic:
rw [Equiv.Perm.Basis.Kf_apply'' a,
  k_apply a _ _ hτ, Equiv.Perm.Basis.Kf_apply'' a]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ τ c ≠ τ d

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ τ c ≠ τ d

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d
Tactic:
exact (Equiv.injective τ).ne_iff.mpr hcd
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c d : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
j : ℤ
hcd : ¬c = d
⊢ c ≠ 1 d
Tactic:
exact hcd
State after:
no goals

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
suffices ∀ (c : g.cycleFactorsFinset), (c : Equiv.Perm α) x = x by
  simp only [this, k_apply_of_not_mem_support x hx]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ↑c x = x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
⊢ ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ↑c x = x
Tactic:
intro c
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ↑c x = x

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ ↑c x = x
Tactic:
rw [← Equiv.Perm.not_mem_support]
State after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ x ∉ Equiv.Perm.support ↑c

State before:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ x ∉ Equiv.Perm.support ↑c
Tactic:
apply Finset.not_mem_mono _ hx
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ Equiv.Perm.support ↑c ⊆ Equiv.Perm.support g

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c✝ : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
⊢ Equiv.Perm.support ↑c ⊆ Equiv.Perm.support g
Tactic:
exact Equiv.Perm.mem_cycleFactorsFinset_support_le c.prop
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Equiv.Perm α
a : Equiv.Perm.Basis g
τ : Equiv.Perm { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
hτ :
  ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), (Equiv.Perm.support ↑(τ c)).card = (Equiv.Perm.support ↑c).card
c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }
x : α
hx : x ∉ Equiv.Perm.support g
this : ∀ (c : { x // x ∈ Equiv.Perm.cycleFactorsFinset g }), ↑c x = x
⊢ k a τ (↑c x) = ↑(τ c) (k a τ x)
Tactic:
simp only [this, k_apply_of_not_mem_support x hx]
State after:
no goals