awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr₃ : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
  coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₃ inr₄ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr₅ : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
  coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₃ inr₄ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₅ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr₆ : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n) (t : Finset X)
  (t_cover : IsDynCoverOf T G U n (↑t : Set X)) (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
  coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₃ inr₄ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₅ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₆ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have inr₇ : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n) (t : Finset X)
  (t_cover : IsDynCoverOf T G U n (↑t : Set X)) (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
  coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₃ inr₄ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₅ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₆ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₇ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n), coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have rcases : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n) (t : Finset X)
  (t_cover : IsDynCoverOf T G U n (↑t : Set X)) (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
  IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
inl : ∀ (hF : coverMincard T F U n = ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr inr₁ : ∀ (hF : coverMincard T F U n < ⊤), coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₂ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n = ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₃ inr₄ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₅ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₆ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
    coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
inr₇ :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n), coverMincard T (F ∪ G) U n ≤ (↑(s.card + t.card) : ℕ∞)
rcases :
  ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
    (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n)
    (t : Finset X) (t_cover : IsDynCoverOf T G U n (↑t : Set X))
    (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n), IsDynCoverOf T (F ∪ G) U n (↑(s ∪ t) : Set X)
⊢ coverMincard T (F ∪ G) U n ≤ coverMincard T F U n + coverMincard T G U n
have rcases₁ : ∀ (hF : coverMincard T F U n < ⊤) (hG : coverMincard T G U n < ⊤) (s : Finset X)
  (s_cover : IsDynCoverOf T F U n (↑s : Set X)) (s_coverMincard : (↑s.card : ℕ∞) = coverMincard T F U n) (t : Finset X)
  (t_cover : IsDynCoverOf T G U n (↑t : Set X)) (t_coverMincard : (↑t.card : ℕ∞) = coverMincard T G U n),
  IsDynCoverOf T (F ∪ G) U n ((↑s : Set X) ∪ (↑t : Set X))
Tactic: classical
  rcases eq_top_or_lt_top (coverMincard T F U n) with hF | hF
  · rw [hF, top_add]; exact le_top
  rcases eq_top_or_lt_top (coverMincard T G U n) with hG | hG
  · rw [hG, add_top]; exact le_top
  obtain ⟨s, s_cover, s_coverMincard⟩ := (coverMincard_finite_iff T F U n).1 hF
  obtain ⟨t, t_cover, t_coverMincard⟩ := (coverMincard_finite_iff T G U n).1 hG
  rw [← s_coverMincard, ← t_coverMincard, ← ENat.coe_add]
  apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))
  rw [s.coe_union t]
  exact s_cover.union t_cover
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)
have refine_1 : coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
refine_1 : coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)
⊢ coverEntropyEntourage T (F ∪ G) U = max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)
have refine_2 : max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)
have apply : ∀ (n : ℕ),
  (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤
    HAdd.hAdd (α := ℕ → ENNReal) (β := ℕ → ENNReal) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ENNReal))
      (fun (n : ℕ) ↦ (↑(coverMincard T G U n) : ENNReal)) n
Tactic: apply le_of_le_of_eq (expGrowthSup_monotone fun n ↦ ?_) expGrowthSup_add
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤
    HAdd.hAdd (α := ℕ → ENNReal) (β := ℕ → ENNReal) (fun (n : ℕ) ↦ (↑(coverMincard T F U n) : ENNReal))
      (fun (n : ℕ) ↦ (↑(coverMincard T G U n) : ENNReal)) n
have rw : (↑(coverMincard T (F ∪ G) U n) : ENNReal) ≤ (↑(coverMincard T F U n + coverMincard T G U n) : ENNReal)
Tactic: rw [Pi.add_apply, ← ENat.toENNReal_add]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
T : X → X
F G : Set X
inst : UniformSpace X
⊢ coverEntropy T (F ∪ G) = max (coverEntropy T F) (coverEntropy T G)
have simp : Eq (α := EReal) (⨆ U ∈ 𝓤 X, coverEntropyEntourage T (F ∪ G) U)
  (⨆ x ∈ 𝓤 X, max (coverEntropyEntourage T F x) (coverEntropyEntourage T G x))
Tactic: simp only [coverEntropy, ← iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)
have this : Eq (α := EReal) ((coverEntropy_supBotHom T : (a : Set X) → EReal) (s.sup F) : EReal)
  (s.sup ((⇑(coverEntropy_supBotHom T) : (a : Set X) → EReal) ∘ F) : EReal)
Tactic: have := map_finset_sup (coverEntropy_supBotHom T) s F
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (hypothesis)
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this :
  Eq (α := EReal) ((coverEntropy_supBotHom T : (a : Set X) → EReal) (s.sup F) : EReal)
    (s.sup ((⇑(coverEntropy_supBotHom T) : (a : Set X) → EReal) ∘ F) : EReal)
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)
have this₁ : coverEntropy T (⋃ x ∈ s, F x) = ⨆ a ∈ s, (coverEntropy T ∘ F) a
Tactic: rw [s.sup_set_eq_biUnion, s.sup_eq_iSup, coverEntropy_supBotHom, SupBotHom.coe_mk,
    SupHom.coe_mk] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.TopologicalEntropy.Subset (goal)
Goal:
X : Type u_1
ι : Type u_2
inst : UniformSpace X
T : X → X
F : ι → Set X
s : Finset ι
this : coverEntropy T (⋃ x ∈ s, F x) = ⨆ a ∈ s, (coverEntropy T ∘ F) a
⊢ coverEntropy T (⋃ i ∈ s, F i) = ⨆ i ∈ s, coverEntropy T (F i)
have rw : Eq (α := EReal) (⨆ a ∈ s, (coverEntropy T ∘ F) a) (⨆ i ∈ s, coverEntropy T (F i))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), m • U)
have simp : (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ (m : M), (V ∩ m • U).Nonempty) ↔
  ∀ {U : Set α}, IsOpen U → U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), (U_1 ∩ i • U).Nonempty
Tactic: simp only [isTopologicallyTransitive_iff, inter_comm, dense_iff_inter_open, inter_iUnion,
    nonempty_iUnion]
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
have simp : IsTopologicallyTransitive M α ↔
  ∀ {U : Set α},
    IsOpen U →
      U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ (i : M), ((fun (x : α) ↦ i • x) '' U_1 ∩ U).Nonempty
Tactic: simp only [dense_iff_inter_open, inter_iUnion, nonempty_iUnion, ← image_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
⊢ IsTopologicallyTransitive M α ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
have refine : ∀ (h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U),
  IsTopologicallyTransitive M α
Tactic: refine ⟨fun _ _ h₀ h₁ h₂ ↦ h₀.dense_of_preimage_smul_invariant M h₁ h₂, fun h₄ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
⊢ IsTopologicallyTransitive M α
have refine : ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
Tactic: refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr ?_
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
⊢ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
have refine_1 : ∀ {U : Set α} (hU : IsOpen U), U.Nonempty → Set.Nonempty.{u_2} (α := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
Tactic: refine fun hU _ ↦ h₄ (isOpen_iUnion fun a ↦ hU.preimage (h.1 a)) ?_ fun b _ ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
refine_1 :
  ∀ {U : Set α} (hU : IsOpen U), U.Nonempty → Set.Nonempty.{u_2} (α := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
⊢ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
have refine_2 : ∀ {U : Set α} (hU : IsOpen U),
  U.Nonempty →
    ∀ (b : M) (x : α),
      Membership.mem (γ := Set α) (preimage (β := α) (fun (x : α) ↦ b • x) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)) x →
        Membership.mem (γ := Set α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U) x
Tactic: refine fun hU _ ↦ h₄ (isOpen_iUnion fun a ↦ hU.preimage (h.1 a)) ?_ fun b _ ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
h : ContinuousConstSMul M α
h₄ : ∀ {U : Set α}, IsOpen U → U.Nonempty → (∀ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U ⊆ U) → Dense U
U : Set α
hU : IsOpen U
h_1 : U.Nonempty
b : M
x : α
⊢ Membership.mem (γ := Set α) (preimage (β := α) (fun (x : α) ↦ b • x) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)) x →
    Membership.mem (γ := Set α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U) x
have refine_2 : ∀ (x_1 : M) (h : (x_1 * b) • x ∈ U), ∃ (i : M), i • x ∈ U
Tactic: simp only [preimage_iUnion, mem_iUnion, mem_preimage, smul_smul, forall_exists_index]
-- Lean 4 proof step from Mathlib.Dynamics.Transitive (goal)
Goal:
M : Type u_1
α : Type u_2
inst : TopologicalSpace α
inst_1 : Monoid M
inst_2 : MulAction M α
inst_3 : IsMinimal M α
⊢ IsTopologicallyTransitive M α
have refine : ∀ {U : Set α} (h : IsOpen U) (hn : U.Nonempty), Dense.{u_2} (X := α) (⋃ (m : M), (fun (x : α) ↦ m • x) ⁻¹' U)
Tactic: refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr fun h hn ↦ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
⊢ IsSolvable.{u_1} s.prod.Gal
have h₁ : IsSolvable.{u_1} (Gal (F := F) (Multiset.prod 0))
Tactic: apply Multiset.induction_on' s
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
h₁ : IsSolvable.{u_1} (Gal (F := F) (Multiset.prod 0))
⊢ IsSolvable.{u_1} s.prod.Gal
have h₂ : ∀ {a : F[X]} {s_1 : Multiset F[X]},
  a ∈ s → s_1 ⊆ s → IsSolvable.{u_1} s_1.prod.Gal → IsSolvable.{u_1} (insert a s_1).prod.Gal
Tactic: apply Multiset.induction_on' s
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (goal)
Goal:
F : Type u_1
inst : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, IsSolvable.{u_1} p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
h : t ⊆ s
ht : IsSolvable.{u_1} t.prod.Gal
⊢ IsSolvable.{u_1} (insert p t).prod.Gal
have h₂ : IsSolvable.{u_1} (p * t.prod).Gal
Tactic: rw [Multiset.insert_eq_cons, Multiset.prod_cons]
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p)
hp : IsSolvable.{u_1} p.Gal
hq : IsSolvable.{u_1} (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) q))
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
⊢ IsSolvable.{u_1} q.Gal
have this : Fact (map (algebraMap F L) p).Splits
Tactic: haveI : Fact ((p.map (algebraMap F L)).Splits) := ⟨hpq⟩
-- Lean 4 proof step from Mathlib.FieldTheory.AbelRuffini (hypothesis)
Goal:
F : Type u_1
inst : Field F
p q : F[X]
hpq : Splits (R := q.SplittingField) (map (algebraMap F q.SplittingField) p)
hp : IsSolvable.{u_1} p.Gal
hq : IsSolvable.{u_1} (Gal (F := p.SplittingField) (map (algebraMap F p.SplittingField) q))
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := AlgEquiv.autCongr (IsSplittingField.algEquiv L (map (algebraMap F K) q))
⊢ IsSolvable.{u_1} q.Gal
have ϕ_inj : Function.Injective (α := Gal(L/K)) (β := (map (algebraMap F K) q).Gal)
  (⇑ϕ.toMonoidHom : (a : Gal(L/K)) → (map (algebraMap F K) q).Gal)
Tactic: have ϕ_inj : Function.Injective ϕ.toMonoidHom := ϕ.injective