mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
⊢ DenseRange fun x ↦ g ^ x

Tactic:
intro a
  by_contra h
  obtain ⟨V, hV₁, hVo, hV⟩ :
      ∃ V : Set G, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ m : ℤ, g ^ m ≠ a * x / y := by
    rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h
    have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
      Continuous.tendsto' (by fun_prop) _ _ (by simp)
    rw [nhds_prod_eq] at this
    simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h
  set s := ⋃ m : ℤ, g ^ m • V
  have hso : IsOpen s := isOpen_iUnion fun m ↦ hVo.smul _
  have hsne : s.Nonempty := ⟨1, mem_iUnion.2 ⟨0, by simpa⟩⟩
  have hd : Disjoint s (a • V) := by
    simp_rw [s, disjoint_iUnion_left, disjoint_left]
    rintro m _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
    apply hV y hy x hx m
    simp_all
  have hgs : (g * ·) ⁻¹' s = s := by
    simp only [s, preimage_iUnion, ← smul_eq_mul, preimage_smul]
    refine iUnion_congr_of_surjective _ (add_left_surjective (-1)) fun m ↦ ?_
    simp [zpow_add, mul_smul]
  cases hg.measure_self_or_compl_eq_zero hso.measurableSet hgs with
  | inl h => exact hso.measure_ne_zero _ hsne h
  | inr h =>
    refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)
    rwa [disjoint_right] at hd

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ (DenseRange fun x ↦ x • ↑a) ↔ Irrational (a / p)

Tactic:
by
  rw [← dense_addSubgroupClosure_pair_iff, DenseRange,
    ← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
    ← AddSubgroup.coe_zmultiples, ← AddSubgroup.coe_comap, ← AddMonoidHom.map_zmultiples,
    AddSubgroup.comap_map_eq, QuotientAddGroup.ker_mk', AddSubgroup.zmultiples_eq_closure,
    AddSubgroup.zmultiples_eq_closure, ← AddSubgroup.closure_union, insert_eq]

Goal state after:
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
⊢ Ergodic f volume

Tactic:
let e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x <| n - 1)

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
⊢ Ergodic f volume
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s)

Tactic:
rw [← hfν.measure_preimage hsm.nullMeasurableSet] at hνs

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hsm : MeasurableSet s
hνs : ν (f ⁻¹' s) = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ (μ.singularPart ν) (f ⁻¹' s) = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ ∀ᵐ (x : α) ∂μ, 0 < ν.rnDeriv μ x

Tactic:
refine (absolutelyContinuous_withDensity_rnDeriv hμν).ae_le ?_

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
⊢ {x | (fun x ↦ 0 < ν.rnDeriv μ x) x} ∈ ae (μ.withDensity (ν.rnDeriv μ))
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Tactic:
haveLebesgueDecomposition_add μ ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
      refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac
      exact hνν'.symm.withDensity

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝¹ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
⊢ ∃ y ∈ ↑(Finset.image (f ∘ g) s), (x, y) ∈ dynEntourage S (map φ φ ⁻¹' (V ○ V)) n

Tactic:
simp only [Finset.coe_image, comp_apply, mem_image, SetLike.mem_coe, ← h.preimage_dynEntourage,
    mem_preimage, map_apply, exists_exists_and_eq_and]

Goal state after:
case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝¹ : Nonempty X
s : Finset Y
s_cover : IsDynCoverOf T (φ '' F) V n ↑s
s_card : s.card ≤ t.card
s_inter : ∀ x ∈ s, (ball x (dynEntourage T V n) ∩ φ '' F).Nonempty
g : Y → Y
g_rel : ∀ x ∈ s, g x ∈ ball x (dynEntourage T V n)
g_mem : ∀ x ∈ s, g x ∈ φ '' F
f : Y → X
h✝ : ∀ y ∈ φ '' F, f y ∈ F
φ_f : ∀ y ∈ φ '' F, φ (f y) = y
x : X
hx : x ∈ F
⊢ ∃ a ∈ s, (φ x, φ (f (g a))) ∈ dynEntourage T (V ○ V) n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
U : SetRel X X
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 ↑{x}
⊢ ↑(#{x}) = 1

Tactic:
rw [Finset.card_singleton, Nat.cast_one]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
n : ℕ
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F univ n ↑{x}
⊢ ↑(#{x}) = 1

Tactic:
rw [Finset.card_singleton, Nat.cast_one]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ IntegrableOn (fun x ↦ (μ.rnDeriv ν x).toReal) t ν

Tactic:
exact integrableOn_toReal_rnDeriv hμt

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyEntourage T F univ = 0

Tactic:
rw [← expGrowthSup_const one_ne_zero one_ne_top, coverEntropyEntourage]
  simp only [coverMincard_univ T h, ENat.toENNReal_one]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ coverEntropyInfEntourage T F univ = 0

Tactic:
by
  rw [← expGrowthInf_const one_ne_zero one_ne_top, coverEntropyInfEntourage]
  simp only [coverMincard_univ T h, ENat.toENNReal_one]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ μ.rnDeriv ν x * ν.rnDeriv κ x = (μ.singularPart ν).rnDeriv κ x + μ.rnDeriv ν x * ν.rnDeriv κ x
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
⊢ coverEntropyInf T (closure F) = coverEntropyInf T F

Tactic:
by
  refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)
  obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni
  exact le_iSup₂_of_le V V_uni ((coverEntropyInfEntourage_antitone T (closure F) V_U).trans
    (coverEntropyInfEntourage_closure h F V V_uni))

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a / (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a / (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
Pi.mul_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ μ.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a / (ν.rnDeriv (μ + ν) a * (μ + ν).rnDeriv ξ a) =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : Group.IsSolvable t.prod.Gal
⊢ Group.IsSolvable (insert p t).prod.Gal

Tactic:
rw [Multiset.insert_eq_cons, Multiset.prod_cons]

Goal state after:
case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
p : F[X]
t : Multiset F[X]
hps : p ∈ s
a✝ : t ⊆ s
ht : Group.IsSolvable t.prod.Gal
⊢ Group.IsSolvable (p * t.prod).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ : (X ^ n - 1).Gal
⊢ ∀ (b : (X ^ n - 1).Gal), σ * b = b * σ

Tactic:
τ

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
⊢ σ * τ = τ * σ
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ : (X ^ n - C a).Gal
⊢ ∀ (b : (X ^ n - C a).Gal), σ * b = b * σ

Tactic:
τ

Goal state after:
case neg
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - C a ≠ 0
hn''' : X ^ n - 1 ≠ 0
mem_range : ∀ {c : (X ^ n - C a).SplittingField}, c ^ n = 1 → ∃ d, (algebraMap F (X ^ n - C a).SplittingField) d = c
σ τ : (X ^ n - C a).Gal
⊢ σ * τ = τ * σ
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
α : Type w'
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α

Tactic:
withConstants,

Goal state after:
L : Language
α : Type w'
⊢ (L.sum (constantsOn α)).card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α ⊕ Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) x = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) x

Tactic:
rcases x with x | x

Goal state after:
case inl
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : α
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inl x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inl x)

case inr
M : Type w
α : Type u'
β : Type v'
n m : ℕ
g : α → β ⊕ Fin n
v : β → M
xs : Fin (n + m) → M
x : Fin m
⊢ (Sum.elim v xs ∘ relabelAux g m) (Sum.inr x) = Sum.elim (Sum.elim v (xs ∘ castAdd m) ∘ g) (xs ∘ natAdd n) (Sum.inr x)
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case func
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term α
ih : ∀ (a : Fin l✝), realize xs (ts a) ∈ S
⊢ realize xs (func f ts) ∈ S

Tactic:
exact Substructure.fun_mem _ _ _ ih

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose ⋯) → M) ≃ (β → M)

pp: case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize fun a_1 ↦ Sum.elim v (?refine_1 a) a_1

Tactic:
· exact ⟨fun v => v ∘ e, fun v => v ∘ e.symm,
      fun _ => by simp [Function.comp_def],
      fun _ => by simp [Function.comp_def]⟩

Goal state after:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize fun a_1 ↦
        Sum.elim v ({ toFun := fun v ↦ v ∘ ⇑e, invFun := fun v ↦ v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } a) a_1
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case refine_1
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Fin (Classical.choose ⋯) → M) ≃ (γ → M)

pp: case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize (Sum.elim v (?refine_1 a))

Tactic:
· exact ⟨fun v => v ∘ e, fun v => v ∘ e.symm,
      fun _ => by simp [Function.comp_def],
      fun _ => by simp [Function.comp_def]⟩

Goal state after:
case refine_2
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
e : γ ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ ∀ (a : Fin (Classical.choose ⋯) → M),
    (Realize φ (fun x ↦ Sum.elim (fun x ↦ v x) (fun x ↦ a (Fin.cast ⋯ ((Classical.choice ⋯) x))) x) fun x ↦
        a (natAdd (Classical.choose ⋯) x)) ↔
      φ.Realize
        (Sum.elim v ({ toFun := fun v ↦ v ∘ ⇑e, invFun := fun v ↦ v ∘ ⇑e.symm, left_inv := ⋯, right_inv := ⋯ } a))
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ ∀ (M : (Theory.ACF p).ModelType), Infinite ↑M

Tactic:
rintro ⟨M⟩

Goal state after:
case hT
p : ℕ
hp : Nat.Prime p ∨ p = 0
M : Type
struc✝ : Language.ring.Structure M
is_model✝ : M ⊨ Theory.ACF p
nonempty'✝ : Nonempty M
⊢ Infinite ↑{ Carrier := M, struc := struc✝, is_model := is_model✝, nonempty' := nonempty'✝ }
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
h : T.IsComplete
M : Type u_1
N : Type u_2
inst✝⁵ : L.Structure M
inst✝⁴ : L.Structure N
inst✝³ : M ⊨ T
inst✝² : N ⊨ T
inst✝¹ : Nonempty M
inst✝ : Nonempty N
⊢ M ≅[L] N

Tactic:
rw [ElementarilyEquivalent, ← h.eq_complete_theory, ← h.eq_complete_theory]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
have hsurj : Surjective i := Quotient.mk''_surjective

Goal state after:
case inr
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Infinite X
key : ∀ (x : X) (s s' : ↥S), s • x = s' • x → Commute s s' → x /ₒ s = x /ₒ s'
i : X × ↥S → OreLocalization S X := fun x ↦ x.1 /ₒ x.2
hsurj : Surjective i
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ Theory.ACF 0 ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons

Tactic:
rw [ACF_zero_realize_iff_infinite_ACF_prime_realize]

Goal state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Finite α
inst✝ : Finite ι
φ : ring.Formula (α ⊕ ι)
mons : ι → Finset (ι →₀ ℕ)
⊢ {p | Theory.ACF ↑p ⊨ᵇ genericPolyMapSurjOnOfInjOn φ mons}.Infinite
Module: Mathlib.FieldTheory.FinTrdeg

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Cardinal.lift.{?u.25, u_2} (Algebra.trdeg K L) < Cardinal.aleph0

Tactic:
← hx.lift_cardinalMk_eq_trdeg,

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
ι : Type u_3
inst✝ : Finite ι
x : ι → L
hx : IsTranscendenceBasis K x
⊢ Cardinal.lift.{u_2, u_3} (Cardinal.mk ι) < Cardinal.aleph0
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) (p_1 + q) = (expand p) (p_1 + q)

Tactic:
simp only [map_add]

Goal state after:
case add
σ : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : MvPolynomial σ (ZMod p)
⊢ ∀ (p_1 q : MvPolynomial σ (ZMod p)),
    (frobenius (MvPolynomial σ (ZMod p)) p) p_1 = (expand p) p_1 →
      (frobenius (MvPolynomial σ (ZMod p)) p) q = (expand p) q →
        (frobenius (MvPolynomial σ (ZMod p)) p) p_1 + (frobenius (MvPolynomial σ (ZMod p)) p) q =
          (expand p) p_1 + (expand p) q