awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
⊢ p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)

Tactic:
simp [Pattern.mulShift, hmem]

Premises used: SymbolicDynamics.FullShift.Pattern.mulShift
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
⊢ p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)

Tactic:
have h1 : p.mulShift v (v * w) = p.config (Classical.choose ex) := by
    simp [Pattern.mulShift, hmem]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
⊢ v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w

Tactic:
have hwv' : v * Classical.choose ex = v * w := (Classical.choose_spec ex).2
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w
⊢ Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = w

Tactic:
have h_eq : Classical.choose ex = w := mul_left_cancel hwv'
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)
hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w
h_eq : Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = w
rw : p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex) = p.config w
rw₁ rw₂ : p.config w = p.config w
⊢ p.mulShift v (v * w) = p.config w

Tactic:
rw [h1, h_eq]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
is is₁ is₂ :
  ∀ (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w)),
    p.mulShift v (v * w) = p.config w
is₃ :
  ∀ (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w))
    (ex : ∃ w' ∈ p.support, v * w' = v * w), p.mulShift v (v * w) = p.config w
is₄ :
  ∀ (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w))
    (ex : ∃ w' ∈ p.support, v * w' = v * w)
    (h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex)),
    p.mulShift v (v * w) = p.config w
is₅ :
  ∀ (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w))
    (ex : ∃ w' ∈ p.support, v * w' = v * w)
    (h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex))
    (hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w),
    p.mulShift v (v * w) = p.config w
is₆ :
  ∀ (hmem : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ v * x) p.support) (v * w))
    (ex : ∃ w' ∈ p.support, v * w' = v * w)
    (h1 : p.mulShift v (v * w) = p.config (Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex))
    (hwv' : v * Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = v * w)
    (h_eq : Classical.choose (p := fun (x : G) ↦ x ∈ p.support ∧ v * x = v * w) ex = w),
    p.mulShift v (v * w) = p.config w
⊢ p.mulShift v (v * w) = p.config w

Tactic:
classical
  -- (v * w) is in the translated support
  have hmem : (v * w) ∈ p.support.image (v * ·) :=
    Finset.mem_image.mpr ⟨w, hw, rfl⟩
  -- existential used in the branch
  have ex : ∃ w', w' ∈ p.support ∧ v * w' = v * w := by
    simpa [Finset.mem_image] using hmem
  -- open the `if` branch as returned by the definition
  have h1 : p.mulShift v (v * w) = p.config (Classical.choose ex) := by
    simp [Pattern.mulShift, hmem]
  -- the chosen witness equals w by left-cancellation
  have hwv' : v * Classical.choose ex = v * w := (Classical.choose_spec ex).2
  have h_eq : Classical.choose ex = w := mul_left_cancel hwv'
  rw [h1, h_eq]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Inhabited A
inst_1 : Monoid G
p : Pattern A G
x : G → A
g h : G
⊢ p.mulOccursInAt (mulShift g x) h ↔ p.mulOccursInAt x (g * h)

Tactic:
simp only [Pattern.mulOccursInAt, mulShift_apply, mul_assoc]

Premises used: SymbolicDynamics.FullShift.mulShift_apply, mul_assoc, SymbolicDynamics.FullShift.Pattern.mulOccursInAt
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Inhabited A
inst_1 : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
hx : x ∈ mulForbidden F
p : Pattern A G
hp : p ∈ F
g : G
⊢ ¬p.mulOccursInAt x (h * g)

Tactic:
specialize hx p hp (h * g)

Premises used: HMul.hMul
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Inhabited A
inst_1 : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : ¬p.mulOccursInAt x (h * g)
contrapose! : ∀ (hx : p.mulOccursInAt (mulShift h x) g), p.mulOccursInAt x (h * g)
⊢ ¬p.mulOccursInAt (mulShift h x) g

Tactic:
contrapose! hx
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Inhabited A
inst_1 : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : p.mulOccursInAt (mulShift h x) g
⊢ p.mulOccursInAt x (h * g)

Tactic:
simpa [mulOccursInAt_mulShift] using hx

Premises used: SymbolicDynamics.FullShift.Pattern.mulOccursInAt_mulShift
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
h :
  ∀ (x : G → A),
    Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x ↔
      x ∈ cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)
⊢ {x : G → A | p.mulOccursInAt x g} = cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)

Tactic:
ext x
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
h :
  Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x →
    x ∈ cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)
h₁ :
  x ∈ cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g) →
    Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x
⊢ Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x ↔
    x ∈ cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)

Tactic:
constructor
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x
u : G
hu : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ g * x) p.support) u
h :
  ∀ (w : G) (hw : w ∈ p.support)
    (hu : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ g * x) p.support) (g * w)),
    x (g * w) = p.mulShift g (g * w)
⊢ x u = p.mulShift g u

Tactic:
rcases Finset.mem_image.mp hu with ⟨w, hw, rfl⟩

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x
w : G
hw : w ∈ p.support
hu : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ g * x) p.support) (g * w)
⊢ x (g * w) = p.config w

Tactic:
have hx : x (g * w) = p.config w := H w hw
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x g} x
w : G
hw : w ∈ p.support
hu : Membership.mem (γ := Finset G) (Finset.image (fun (x : G) ↦ g * x) p.support) (g * w)
hx : x (g * w) = p.config w
⊢ x (g * w) = p.mulShift g (g * w)

Tactic:
simpa [Pattern.mulShift_apply_mul_left_of_mem (p := p) (v := g) (w := w) hw] using hx

Premises used: SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_mem
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)
u : G
hu : u ∈ p.support
⊢ x (g * u) = p.mulShift g (g * u)

Tactic:
have hx : x (g * u) = p.mulShift g (g * u) :=
      H (g * u) (Finset.mem_image_of_mem (g * ·) hu)
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : Inhabited A
G : Type u_2
inst_1 : Monoid G
inst_2 : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)
u : G
hu : u ∈ p.support
hx : x (g * u) = p.mulShift g (g * u)
⊢ x (g * u) = p.config u

Tactic:
simpa [Pattern.mulShift_apply_mul_left_of_mem (p := p) (v := g) (w := u) hu] using hx

Premises used: SymbolicDynamics.FullShift.Pattern.mulShift_apply_mul_left_of_mem
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
p : Pattern A G
g : G
⊢ IsOpen[Pi.topologicalSpace] {x : G → A | p.mulOccursInAt x g}

Tactic:
simpa [mulOccursInAt_eq_cylinder] using isOpen_cylinder _ _

Premises used: SymbolicDynamics.FullShift.isOpen_cylinder, SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinder
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h :
  ∀ (x : G → A),
    Membership.mem (γ := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} x ↔
      Membership.mem (γ := Set (G → A)) (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v}) x
⊢ Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
ext
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
x : G → A
⊢ Membership.mem (γ := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} x ↔
    Membership.mem (γ := Set (G → A)) (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v}) x

Tactic:
simp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
⊢ Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
have h_eq : {x | ∀ p ∈ F, ∀ v : G, ¬ p.mulOccursInAt x v}
    = ⋂ (p : Pattern A G) (hp : p ∈ F) (v : G), {x | ¬ p.mulOccursInAt x v} := by ext; simp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
rw : IsClosed[Pi.topologicalSpace] (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
⊢ IsClosed[Pi.topologicalSpace] {x : G → A | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}

Tactic:
rw [h_eq]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
⊢ IsClosed[Pi.topologicalSpace] (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
isClosed_iInter (fun p => ?_)

Premises used: isClosed_iInter
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
refine :
  ∀ (p : Pattern A G), IsClosed[Pi.topologicalSpace] (⋂ (_ : p ∈ F), ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
⊢ IsClosed[Pi.topologicalSpace] (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
refine isClosed_iInter (fun p => ?_)

Premises used: isClosed_iInter
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
⊢ IsClosed[Pi.topologicalSpace] (⋂ (_ : p ∈ F), ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
isClosed_iInter (fun hp => ?_)

Premises used: isClosed_iInter
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
refine : ∀ (hp : p ∈ F), IsClosed[Pi.topologicalSpace] (⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
⊢ IsClosed[Pi.topologicalSpace] (⋂ (_ : p ∈ F), ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
refine isClosed_iInter (fun hp => ?_)

Premises used: isClosed_iInter
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
hp : p ∈ F
⊢ IsClosed[Pi.topologicalSpace] (⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
isClosed_iInter (fun v => ?_)

Premises used: isClosed_iInter
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
hp : p ∈ F
refine : ∀ (v : G), IsClosed[Pi.topologicalSpace] {x : G → A | ¬p.mulOccursInAt x v}
⊢ IsClosed[Pi.topologicalSpace] (⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})

Tactic:
refine isClosed_iInter (fun v => ?_)

Premises used: isClosed_iInter
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
hp : p ∈ F
v : G
h :
  ∀ (x : G → A),
    Membership.mem (γ := Set (G → A)) {x : G → A | ¬p.mulOccursInAt x v} x ↔
      Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x v}ᶜ x
⊢ Eq (α := Set (G → A)) {x : G → A | ¬p.mulOccursInAt x v} {x : G → A | p.mulOccursInAt x v}ᶜ

Tactic:
ext
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
hp : p ∈ F
v : G
x : G → A
⊢ Membership.mem (γ := Set (G → A)) {x : G → A | ¬p.mulOccursInAt x v} x ↔
    Membership.mem (γ := Set (G → A)) {x : G → A | p.mulOccursInAt x v}ᶜ x

Tactic:
simp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
hp : p ∈ F
v : G
⊢ Eq (α := Set (G → A)) {x : G → A | ¬p.mulOccursInAt x v} {x : G → A | p.mulOccursInAt x v}ᶜ

Tactic:
have : {x | ¬ p.mulOccursInAt x v} = {x | p.mulOccursInAt x v}ᶜ := by ext; simp
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : DiscreteTopology A
F : Set (Pattern A G)
h_eq :
  Eq (α := Set (G → A)) {x : G → A | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v}
    (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
p : Pattern A G
hp : p ∈ F
v : G
this : Eq (α := Set (G → A)) {x : G → A | ¬p.mulOccursInAt x v} {x : G → A | p.mulOccursInAt x v}ᶜ
⊢ IsClosed[Pi.topologicalSpace] {x : G → A | ¬p.mulOccursInAt x v}

Tactic:
simpa [this, isClosed_compl_iff] using isOpen_mulOccursInAt (A := A) (G := G) p v

Premises used: SymbolicDynamics.FullShift.isOpen_mulOccursInAt, isClosed_compl_iff
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_1
inst : TopologicalSpace A
inst_1 : Inhabited A
G : Type u_2
inst_2 : Monoid G
inst_3 : IsLeftCancelMul G
inst_4 : T1Space A
p : Pattern A G
g : G
⊢ IsClosed[Pi.topologicalSpace] {x : G → A | p.mulOccursInAt x g}

Tactic:
simpa [mulOccursInAt_eq_cylinder] using isClosed_cylinder _ _

Premises used: SymbolicDynamics.FullShift.isClosed_cylinder, SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinder
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
intro : ∀ (val : Fintype A), Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}
⊢ Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}

Tactic:
cases nonempty_fintype A

Premises used: nonempty_fintype
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
val : Fintype A
f : ↥U → A
g : G
hg : g ∉ U
⊢ Eq.{u_3 + 1} (α := A) (if h : g ∈ U then f (Subtype.mk (p := fun (x : G) ↦ x ∈ U) g h) else default) default

Tactic:
simp [hg]
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
hU : dom = U
subst :
  Eq (α := { p : Pattern A G // p.support = dom })
    ((fun (f : ↥dom → A) ↦
        (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
            { config := fun (g : G) ↦ if h : g ∈ dom then f (Subtype.mk (p := fun (x : G) ↦ x ∈ dom) g h) else default,
              support := dom, condition := ⋯ }
            ⋯ :
          { p : Pattern A G // p.support = dom }))
      ((fun (p : { p : Pattern A G // p.support = dom }) (i : ↥dom) ↦ (↑p : Pattern A G).config (↑i : G))
        (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom) { config := cfg, support := dom, condition := cond }
          ⋯)))
    (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom) { config := cfg, support := dom, condition := cond } ⋯)
⊢ Eq (α := { p : Pattern A G // p.support = U })
    ((fun (f : ↥U → A) ↦
        (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U)
            { config := fun (g : G) ↦ if h : g ∈ U then f (Subtype.mk (p := fun (x : G) ↦ x ∈ U) g h) else default,
              support := U, condition := ⋯ }
            ⋯ :
          { p : Pattern A G // p.support = U }))
      ((fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G))
        (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U) { config := cfg, support := dom, condition := cond }
          hU)))
    (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = U) { config := cfg, support := dom, condition := cond } hU)

Tactic:
subst hU
-- Module: Mathlib.Dynamics.SymbolicDynamics.Basic
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
val : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
a :
  (↑((fun (f : ↥dom → A) ↦
            (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
                {
                  config := fun (g : G) ↦
                    if h : g ∈ dom then f (Subtype.mk (p := fun (x : G) ↦ x ∈ dom) g h) else default,
                  support := dom, condition := ⋯ }
                ⋯ :
              { p : Pattern A G // p.support = dom }))
          ((fun (p : { p : Pattern A G // p.support = dom }) (i : ↥dom) ↦ (↑p : Pattern A G).config (↑i : G))
            (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
              { config := cfg, support := dom, condition := cond } ⋯))) :
      Pattern A G) =
    (↑(Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
          { config := cfg, support := dom, condition := cond : Pattern A G } ⋯) :
      Pattern A G)
⊢ Eq (α := { p : Pattern A G // p.support = dom })
    ((fun (f : ↥dom → A) ↦
        (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
            { config := fun (g : G) ↦ if h : g ∈ dom then f (Subtype.mk (p := fun (x : G) ↦ x ∈ dom) g h) else default,
              support := dom, condition := ⋯ }
            ⋯ :
          { p : Pattern A G // p.support = dom }))
      ((fun (p : { p : Pattern A G // p.support = dom }) (i : ↥dom) ↦ (↑p : Pattern A G).config (↑i : G))
        (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom) { config := cfg, support := dom, condition := cond }
          ⋯)))
    (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom) { config := cfg, support := dom, condition := cond } ⋯)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext