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

Goal state before:
pp: X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ (fun x ↦ g ^ n • x) ⁻¹' s = s

Tactic:
← smul_iterate,

Goal state after:
X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ (fun x ↦ g • x)^[n] ⁻¹' s = s
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ (s ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False

Tactic:
symmDiff_comm

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f z) ⁻¹' t) ∆ s) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun δ ↦ ENNReal.ofReal (min T (2 * δ))) (𝓝[<] ε) (𝓝 (ENNReal.ofReal (min T (2 * ε))))

Tactic:
refine ENNReal.tendsto_ofReal (Tendsto.min tendsto_const_nhds <| Tendsto.const_mul _ ?_)

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun x ↦ x) (𝓝[<] ε) (𝓝 ε)
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
⊢ μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T

Tactic:
have huj' : 1 ≤ (↑(n j) : ℝ) := by norm_cast

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : 1 ≤ ↑(n j)
⊢ μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : ⟨g, hg⟩ ≠ 0
⊢ AEDisjoint volume (⟨g, hg⟩ +ᵥ I) I

Tactic:
replace hg' : g ≠ 0 := by simpa only [Ne, AddSubgroup.mk_eq_zero] using hg'

Goal state after:
case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ AEDisjoint volume (⟨g, hg⟩ +ᵥ I) I
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ (T + T) / 2 / ↑n ≤ ‖g‖

Tactic:
add_self_div_two,

Goal state after:
case refine_2
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
hBg : g +ᵥ B = ball (g + x) (T / (2 * ↑n))
⊢ T / ↑n ≤ ‖g‖
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c

Tactic:
borelize X

Goal state after:
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ∃ c, g =ᵐ[μ] const α c
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
⊢ μ (f ⁻¹' s) = μ s

Tactic:
hfμ.measure_preimage hsm.nullMeasurableSet

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 : ν s = 0
hμs : (μ.singularPart ν) sᶜ = 0
⊢ μ s = μ s
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
L : Set X
hL₁ : IsClosed L
hL₂ : IsCompact L
hg : (fixedPoints g)ᶜ ⊆ L
⊢ (fixedPoints f ∩ fixedPoints g)ᶜ ⊆ K ∪ L

Tactic:
Set.compl_inter,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
f g : X → X
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
L : Set X
hL₁ : IsClosed L
hL₂ : IsCompact L
hg : (fixedPoints g)ᶜ ⊆ L
⊢ (fixedPoints f)ᶜ ∪ (fixedPoints g)ᶜ ⊆ K ∪ L
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, (f * fun a ↦ (f a)⁻¹ * μ.rnDeriv ν a) a ∂ν

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
· simp only [Pi.mul_apply]
      have : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν := by
        filter_upwards [hf_ne_zero, hf_ne_top] with x hx1 hx2
        simp [← mul_assoc, ENNReal.mul_inv_cancel, hx1, hx2]
      rw [lintegral_congr_ae (ae_restrict_of_ae this)]

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = ⨆ a, ⨆ (_ : IsDynNetIn T F U n ↑a), ↑a.card

Tactic:
exact biSup_congr (fun _ _ ↦ rfl)

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

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h✝ : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
s : Finset X
h : IsDynNetIn T F U n ↑s
a : ∀ᶠ (x : ℕ) in Filter.principal (Finset.card '' {s | IsDynNetIn T F U n ↑s}), ¬(fun x ↦ ↑x = ↑s.card) x
⊢ s.card ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}

Tactic:
by simpa using ⟨_, h, rfl⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
s F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
h' : IsDynCoverOf S F (map φ φ ⁻¹' V) n s
⊢ IsDynCoverOf T (φ '' F) V n (φ '' s)

Tactic:
by
  rintro _ ⟨x, hx, rfl⟩
  obtain ⟨y, hy, hxy⟩ := h' hx
  refine ⟨_, Set.mem_image_of_mem _ hy, show (x, y) ∈ map φ φ ⁻¹' dynEntourage T V n from ?_⟩
  rwa [h.preimage_dynEntourage V n]

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

Goal state before:
pp: X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x ↦ ball x (dynEntourage T univ n)
⊢ ↑s.card ≤ 1

Tactic:
simp only [ball, dynEntourage_univ, preimage_univ] at s_net

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
n : ℕ
s : Finset X
left✝ : ↑s ⊆ F
s_net : (↑s).PairwiseDisjoint fun x ↦ univ
⊢ ↑s.card ≤ 1
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
⊢ coverEntropy T (closure F) = coverEntropy T F

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropy_monotone T subset_closure)

Goal state after:
X : Type u_1
T : X → X
F : Set X
inst✝ : UniformSpace X
h : Continuous T
U : Set (X × X)
U_uni : U ∈ 𝓤 X
⊢ coverEntropyEntourage T (closure F) U ≤ coverEntropy T F
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 ξ
⊢ (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
have h_ac : μ + ν ≪ ξ := hμ.add_left hν

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 : μ + ν ≪ ξ
⊢ (fun x ↦ μ.rnDeriv ξ x / ν.rnDeriv ξ x) =ᵐ[μ + ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) = ((map f ν).withDensity ((map f μ).rnDeriv (map f ν))) s

Tactic:
withDensity_apply _ (hf.measurable hs),

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in f ⁻¹' s, μ.rnDeriv ν a ∂ν = ((map f ν).withDensity ((map f μ).rnDeriv (map f ν))) s
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{u, v} #L ≤ #((p : R[X]) × { x // x ∈ p.aroots L })

Tactic:
have := @lift_mk_le_lift_mk_of_injective L (Σ p : R[X], {x : L | x ∈ p.aroots L})
    (fun x : L =>
      let p := Classical.indefiniteDescription _ (Algebra.IsAlgebraic.isAlgebraic x)
      ⟨p.1, x, by
        dsimp
        have := (Polynomial.map_ne_zero_iff (FaithfulSMul.algebraMap_injective R L)).2 p.2.1
        rw [Polynomial.mem_roots this, Polynomial.IsRoot, Polynomial.eval_map,
          ← Polynomial.aeval_def, p.2.2]⟩)
    fun x y => by
      intro h
      simp only [Set.coe_ofPred, ne_eq, Set.mem_ofPred_eq, Sigma.mk.inj_iff] at h
      refine (Subtype.heq_iff_coe_eq ?_).1 h.2
      simp only [h.1, forall_true_iff]
  rwa [lift_umax, lift_id'.{v}] at this

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
⊢ (∀ (a : ℕ), IsEmpty (Language.empty.Functions a)) ∧ ∀ (a : ℕ), IsEmpty (Language.empty.Relations a)

Tactic:
exact ⟨fun _ => inferInstance, fun _ => inferInstance⟩

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
⊢ ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) = fun c ↦ C b * (X - C (c / b))

Tactic:
ext1 c

Goal state after:
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n = i a
hb' : b ≠ 0
s : Multiset E := (map i (X ^ n - C a)).roots
hs : map i (X ^ n - C a) = (Multiset.map (fun x ↦ X - C x) s).prod
hs' : s.card = n
C_mul_C : C (i a⁻¹) * C (i a) = 1
key1 : map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)
c : E
⊢ ((fun q ↦ q.comp (C b * X)) ∘ fun c ↦ X - C c) c = C b * (X - C (c / b))
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ solvableByRad F E ≤ algebraicClosure F E

Tactic:
refine solvableByRad_le fun x n hn hx ↦ ?_

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
hn : n ≠ 0
hx : x ^ n ∈ algebraicClosure F E
⊢ x ∈ algebraicClosure F E
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case func
L : Language
α : Type u'
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
_ts_ih✝ : ∀ (a : Fin l✝), ((_ts✝ a).substFunc fun {n} ↦ Functions.term) = _ts✝ a
⊢ ((func _f✝ _ts✝).substFunc fun {n} ↦ Functions.term) = func _f✝ _ts✝

Tactic:
simp only [substFunc, Functions.term, subst, ‹∀ _, _›]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case rad
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
n : ℕ
y : E
hn : n ≠ 0
hy : y ^ n ∈ solvableByRad F E
hy' : Group.IsSolvable (minpoly F (y ^ n)).Gal
⊢ Group.IsSolvable (minpoly F y).Gal

Tactic:
| rad n y hn hy hy' =>

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ f₁✝.imp f₂✝ = id (f₁✝.imp f₂✝)

Tactic:
id

Goal state after:
case imp
L : Language
α : Type u'
n n✝ : ℕ
f₁✝ f₂✝ : L.BoundedFormula α n✝
ih1 : (LHom.id L).onBoundedFormula f₁✝ = id f₁✝
ih2 : (LHom.id L).onBoundedFormula f₂✝ = id f₂✝
⊢ f₁✝.imp f₂✝ = f₁✝.imp f₂✝
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ f✝.all = id f✝.all

Tactic:
id

Goal state after:
case all
L : Language
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : (LHom.id L).onBoundedFormula f✝ = id f✝
⊢ f✝.all = f✝.all
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
n : ℕ
t : L[[α]].Term (β ⊕ Fin n)
v : β → M
xs : Fin n → M
⊢ realize (Sum.elim (Sum.elim (fun a ↦ ↑(L.con a)) v) xs) (constantsVarsEquivLeft t) = realize (Sum.elim v xs) t

Tactic:
simp only [constantsVarsEquivLeft, realize_relabel, Equiv.coe_trans, Function.comp_apply,
    constantsVarsEquiv_apply, relabelEquiv_symm_apply]
  refine _root_.trans ?_ realize_constantsToVars
  congr 1; funext x -- Note: was previously rcongr x
  rcases x with (a | (b | i)) <;> simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
k : ℕ
f : L.BoundedFormula α k
v : α → M
xs : Fin k → M
f' : L.BoundedFormula α k
tail✝ : List (L.BoundedFormula α k)
tail_ih✝ : (List.foldr imp f tail✝).Realize v xs = ((∀ i ∈ tail✝, i.Realize v xs) → f.Realize v xs)
⊢ (List.foldr imp f (f' :: tail✝)).Realize v xs = ((∀ i ∈ f' :: tail✝, i.Realize v xs) → f.Realize v xs)

Tactic:
by_cases f'.Realize v xs <;> simp [*]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
⊢ ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') (last k) =
    snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x (last k)

Tactic:
simp only [Function.comp_apply, val_last, snoc_last]

Goal state after:
case all.refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
x : M
⊢ snoc xs x (Fin.cast h (if k < m then castAdd n' (last k) else (last k).addNat n')) = x
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
⊢ s ∈ (closure L).closed ↔ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f s

Tactic:
refine ⟨fun h n f => ?_, fun h => ?_⟩
  · rw [← h]
    exact Substructure.fun_mem _ _
  · have h' : closure L s = ⟨s, h⟩ := closure_eq_of_le (refl _) subset_closure
    exact congr_arg _ h'

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
⊢ IsEmpty ↥⊥

Tactic:
by
  refine (isEmpty_subtype _).2 (fun x => ?_)
  have h : (∅ : Set M) ∈ (closure L).closed := by
    rw [mem_closed_iff]
    intro n f
    cases n
    · exact isEmptyElim f
    · intro x hx
      simp only [mem_empty_iff_false, forall_const] at hx
  rw [← closure_empty, ← SetLike.mem_coe, h]
  exact Set.notMem_empty _

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
v : α ⊕ Fin n✝ → M
⊢ (equal t₁✝ t₂✝).toFormula.Realize v ↔ (equal t₁✝ t₂✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
simp [BoundedFormula.Realize]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case rel
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ l✝ : ℕ
R✝ : L.Relations l✝
ts✝ : Fin l✝ → L.Term (α ⊕ Fin n✝)
v : α ⊕ Fin n✝ → M
⊢ (rel R✝ ts✝).toFormula.Realize v ↔ (rel R✝ ts✝).Realize (v ∘ Sum.inl) (v ∘ Sum.inr)

Tactic:
simp [BoundedFormula.Realize]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : A.Definable L s
hAB : A ⊆ B
⊢ B.Definable L s

Tactic:
rw [definable_iff_empty_definable_with_params] at *

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : ∅.Definable L[[↑A]] s
hAB : A ⊆ B
⊢ ∅.Definable L[[↑B]] s
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
r : L.Relations 2
⊢ M ⊨ r.transitive ↔ ∀ ⦃a b c : M⦄, RelMap r ![a, b] → RelMap r ![b, c] → RelMap r ![a, c]

Tactic:
exact forall₃_congr fun _ _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ realize_rel₂

Goal state after: