awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ p.mulShift v (v * w) = p.config w
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ p.mulShift v (v * w) = p.config w
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ p.mulShift v (v * w) = p.config w
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ p.mulShift v (v * w) = p.config w
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
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 (mulShift h x) g
have hx₁ : ¬p.mulOccursInAt x (h * g)
Tactic: specialize hx p hp (h * g)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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)
⊢ ¬p.mulOccursInAt (mulShift h x) g
have contrapose! : ∀ (hx : p.mulOccursInAt (mulShift h x) g), p.mulOccursInAt x (h * g)
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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 | p.mulOccursInAt x g} = cylinder (Finset.image (fun (x : G) ↦ g * x) p.support) (p.mulShift g)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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)
⊢ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ x u = p.mulShift g u
have 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)
Tactic: rcases Finset.mem_image.mp hu with ⟨w, hw, rfl⟩
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
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.mulShift g (g * w)
have hx : x (g * w) = p.config w
Tactic: have hx : x (g * w) = p.config w := H w hw
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
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.config u
have hx : 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)
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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})
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
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)
⊢ IsClosed[Pi.topologicalSpace] {x : G → A | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}
have 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})
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
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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] {x : G → A | ∀ p ∈ F, ∀ (g : G), ¬p.mulOccursInAt x g}
have rw : IsClosed[Pi.topologicalSpace] (⋂ p ∈ F, ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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})
have refine : ∀ (p : Pattern A G), IsClosed[Pi.topologicalSpace] (⋂ (_ : p ∈ F), ⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
Tactic: refine isClosed_iInter (fun p => ?_)
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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})
have refine : ∀ (hp : p ∈ F), IsClosed[Pi.topologicalSpace] (⋂ (v : G), {x : G → A | ¬p.mulOccursInAt x v})
Tactic: refine isClosed_iInter (fun hp => ?_)
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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})
have refine : ∀ (v : G), IsClosed[Pi.topologicalSpace] {x : G → A | ¬p.mulOccursInAt x v}
Tactic: refine isClosed_iInter (fun v => ?_)
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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}ᶜ
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (hypothesis)
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
⊢ IsClosed[Pi.topologicalSpace] {x : G → A | ¬p.mulOccursInAt x v}
have this : 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
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
Goal:
A : Type u_3
G : Type u_4
inst : Finite A
inst_1 : Inhabited A
U : Finset G
⊢ Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}
have intro : ∀ (val : Fintype A), Set.Finite (α := Pattern A G) {p : Pattern A G | p.support = U}
Tactic: cases nonempty_fintype A
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ 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)
have 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 := sorry }
          sorry :
        { 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 }
        sorry)))
  (Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom) { config := cfg, support := dom, condition := cond } sorry)
Tactic: subst hU
Cleared hypotheses: U, hU
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ 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 } ⋯)
have 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 := sorry }
              sorry :
            { 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 } sorry))) :
    Pattern A G) =
  (↑(Subtype.mk (p := fun (p : Pattern A G) ↦ p.support = dom)
        { config := cfg, support := dom, condition := cond : Pattern A G } sorry) :
    Pattern A G)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ (↑((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)
have a : (fun (g : G) ↦ if h : g ∈ dom then cfg g else default) = cfg
Tactic: simp only [Pattern.mk.injEq, and_true]
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ (fun (g : G) ↦ if h : g ∈ dom then cfg g else default) = cfg
have a : ∀ (g : G), (if h : g ∈ dom then cfg g else default) = cfg g
Tactic: funext g
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
g : G
⊢ (if h : g ∈ dom then cfg g else default) = cfg g
have pos : ∀ (hg : g ∈ dom), (if h : g ∈ dom then cfg g else default) = cfg g
Tactic: by_cases hg : g ∈ dom
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
g : G
pos : ∀ (hg : g ∈ dom), (if h : g ∈ dom then cfg g else default) = cfg g
⊢ (if h : g ∈ dom then cfg g else default) = cfg g
have neg : ∀ (hg : g ∉ dom), (if h : g ∈ dom then cfg g else default) = cfg g
Tactic: by_cases hg : g ∈ dom
-- Lean 4 proof step from Mathlib.Dynamics.SymbolicDynamics.Basic (goal)
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
⊢ (fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G))
      ((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 }))
        f) =
    f
have h : ∀ (i : ↥U),
  (fun (p : { p : Pattern A G // p.support = U }) (i : ↥U) ↦ (↑p : Pattern A G).config (↑i : G))
      ((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 := sorry }
              sorry :
            { p : Pattern A G // p.support = U }))
        f)
      i =
    f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage (goal)
Goal:
X : Type u_1
T : X → X
U : SetRel X X
inst : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
n : ℕ
⊢ dynEntourage T U n ∈ 𝓤 X
have rw : ⋂ (k : (↑(Ico 0 n) : Type)), (map T T)^[(↑k : ℕ)] ⁻¹' U ∈ 𝓤 X
Tactic: rw [dynEntourage_eq_inter_Ico T U n]