mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
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 ≠ ∞
⊢ μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
by
  have : SigmaFinite (ν.withDensity f) := SigmaFinite.withDensity_of_ne_top hf_ne_top
  refine (withDensity_absolutelyContinuous' hf hf_ne_zero).ae_eq ?_
  refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm
  · exact (hf.inv.mono_ac (withDensity_absolutelyContinuous _ _)).mul
      (Measure.measurable_rnDeriv _ _).aemeasurable
  · ext1 s hs
    conv_lhs => rw [← Measure.withDensity_rnDeriv_eq _ _ hμν]
    rw [zero_add, withDensity_apply _ hs, withDensity_apply _ hs]
    rw [setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀ _ _ _ hs]
    · 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)]
    · refine ae_restrict_of_ae ?_
      filter_upwards [hf_ne_top] with x hx using hx.lt_top
    · exact hf.restrict

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
⊢ IsClosed[Pi.topologicalSpace] (⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v})

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

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
⊢ IsClosed[Pi.topologicalSpace] (⋂ (_ : p ∈ F), ⋂ v, {x | ¬p.mulOccursInAt x v})
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst✝ : U.IsRefl
⊢ (dynEntourage T U n).IsRefl

Tactic:
simp only [dynEntourage, map_iterate]

Goal state after:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst✝ : U.IsRefl
⊢ SetRel.IsRefl (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst✝ : U.IsSymm
⊢ (dynEntourage T U n).IsSymm

Tactic:
simp only [dynEntourage, map_iterate]

Goal state after:
X : Type u_1
T : X → X
U V : SetRel X X
m n : ℕ
x y : X
inst✝ : U.IsSymm
⊢ SetRel.IsSymm (⋂ k, ⋂ (_ : k < n), map T^[k] T^[k] ⁻¹' U)
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
⊢ ↑((fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ dom then f ⟨g, h⟩ else default, support := dom, condition := ⋯ }, ⋯⟩)
        ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, ⋯⟩)) =
    ↑⟨{ config := cfg, support := dom, condition := cond }, ⋯⟩

Tactic:
simp only [Pattern.mk.injEq, and_true]

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
⊢ (fun g ↦ if h : g ∈ dom then cfg g else default) = cfg
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
m : ℕ
inst✝ : U.IsSymm
n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m ↑s
⊢ IsDynCoverOf T ∅ (U ○ U) (m * n) ↑∅ ∧ #∅ ≤ #s ^ n

Tactic:
by simp

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νν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᵐ[ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x
hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν).rnDeriv (ν + ν') x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x =
    (μ.singularPart ν).rnDeriv ν x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x

Tactic:
hx₃,

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

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑⟨u₁ ∩ u₂, ⋯⟩ ⊆ ↑⟨u₁, hu₁⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
u₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑⟨u₁ ∩ u₂, ⋯⟩ ⊆ ↑⟨u₂, hu₂⟩

Tactic:
by simp

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_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
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x

Tactic:
hx₃,

Goal state after:
α : 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
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ ∅

Tactic:
← ball_empt

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, z) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : 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 ≠ ∞
⊢ ∀ (a : α), 0 a ≤ (fun x ↦ (μ.rnDeriv ν x).toReal) a

Tactic:
by simp

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 = expGrowthSup fun x ↦ 1

Tactic:
coverEntropyEntourage

Goal state after:
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
⊢ (expGrowthSup fun n ↦ ↑(coverMincard T F univ n)) = expGrowthSup fun x ↦ 1
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ (μ.rnDeriv ν a + 1)⁻¹ ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv ν a + 1 ≠ 0

Tactic:
by simp

Goal state after:
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]
⊢ ∀ {s_1 : Multiset F[X]}, p ∈ s → s_1 ⊆ s → Group.IsSolvable s_1.prod.Gal → Group.IsSolvable (insert p s_1).prod.Gal

Tactic:
t

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]
⊢ p ∈ s → t ⊆ s → Group.IsSolvable t.prod.Gal → Group.IsSolvable (insert p t).prod.Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).1 ⟂ₘ μ

Tactic:
by simp

Goal state after:
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
⊢ max (max (lift.{v, u} (max #R ℵ₀)) ℵ₀) ℵ₀ = max (lift.{v, u} #R) ℵ₀

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{v, max u w} (max (max (max (Cardinal.lift.{w, u} #R) (Cardinal.lift.{u, w} #ι)) ℵ₀) ℵ₀) =
    max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀

Tactic:
by simp

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
⊢ (X ^ n - C a).natDegree = n

Tactic:
natDegree_X_pow_sub_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
⊢ n = n
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L'').Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Functions n✝), funMap ((ϕ.sumElim ψ).onFunction (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L'').Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L''.Functions n✝), funMap ((ϕ.sumElim ψ).onFunction (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L'').Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Relations n✝), RelMap ((ϕ.sumElim ψ).onRelation (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁵ : L.Structure M✝
ϕ : L →ᴸ L'
L''✝ : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst✝⁴ : L.Structure M
inst✝³ : L'.Structure M
inst✝² : L''.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L'').Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L''.Relations n✝), RelMap ((ϕ.sumElim ψ).onRelation (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L₁).Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Functions n✝), funMap ((ϕ.sumMap ψ).onFunction (Sum.inl val)) x✝ = funMap (Sum.inl val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
f : (L.sum L₁).Functions n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L₁.Functions n✝), funMap ((ϕ.sumMap ψ).onFunction (Sum.inr val)) x✝ = funMap (Sum.inr val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L₁).Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L.Relations n✝), RelMap ((ϕ.sumMap ψ).onRelation (Sum.inl val)) x✝ = RelMap (Sum.inl val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M✝ : Type w
inst✝⁶ : L.Structure M✝
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst✝⁵ : L.Structure M
inst✝⁴ : L'.Structure M
inst✝³ : L₁.Structure M
inst✝² : L₂.Structure M
inst✝¹ : ϕ.IsExpansionOn M
inst✝ : ψ.IsExpansionOn M
n✝ : ℕ
R : (L.sum L₁).Relations n✝
x✝ : Fin n✝ → M
⊢ ∀ (val : L₁.Relations n✝), RelMap ((ϕ.sumMap ψ).onRelation (Sum.inr val)) x✝ = RelMap (Sum.inr val) x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg.hq
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : ¬x = 0
⊢ Group.IsSolvable (map (algebraMap F (X ^ n - 1).SplittingField) (X ^ n - C x)).Gal

Tactic:
rw [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C]
    apply gal_X_pow_sub_C_isSolvable_aux
    rw [map_id]
    have key := SplittingField.splits (X ^ n - 1 : F[X])
    rwa [Polynomial.map_sub, Polynomial.map_pow, map_X,
      Polynomial.map_one] at key

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Ring.FreeCommRing

Goal state before:
pp: α : Type u_1
p : FreeCommRing α
⊢ Term.realize FreeCommRing.of (-1) = -1

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
a b : α
⊢ a = b ↔ var a = var b

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
a✝ : α
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
⊢ ¬var a✝ = func _f✝ _ts✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : (n : ℕ) → DecidableEq (L.Functions n)
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
a✝ : α
⊢ ¬func _f✝ _ts✝ = var a✝

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
g : α ≃ β
t : L.Term α
⊢ relabel (⇑g.symm) (relabel (⇑g) t) = t

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
g : α ≃ β
t : L.Term β
⊢ relabel (⇑g) (relabel (⇑g.symm) t) = t

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n ≃ L'.Relations n
n : ℕ
φ : L.BoundedFormula α n
⊢ mapTermRel (fun n ↦ ⇑(ft n).symm) (fun n ↦ ⇑(fr n).symm) (fun x ↦ id)
      (mapTermRel (fun n ↦ ⇑(ft n)) (fun n ↦ ⇑(fr n)) (fun x ↦ id) φ) =
    φ

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
n✝ : ℕ
ft : (n : ℕ) → L.Term (α ⊕ Fin n) ≃ L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n ≃ L'.Relations n
n : ℕ
φ : L'.BoundedFormula β n
⊢ mapTermRel (fun n ↦ ⇑(ft n)) (fun n ↦ ⇑(fr n)) (fun x ↦ id)
      (mapTermRel (fun n ↦ ⇑(ft n).symm) (fun n ↦ ⇑(fr n).symm) (fun x ↦ id) φ) =
    φ

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
t : L.Term α
s : Set α
h : ↑t.varFinset ⊆ s
v : α → M
⊢ ∀ (a : ↥t.varFinset), (v ∘ Subtype.val) (Set.inclusion h a) = v ↑a

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ Theory.fieldOfChar p ↔ CharP K p

Tactic:
simp only [Theory.fieldOfChar, Theory.model_union_iff,
    (show (Theory.field.Model K) by infer_instance), true_and]
  split_ifs with hp0 hp
  · subst hp0
    simp only [Theory.model_iff, Set.mem_image, Set.mem_ofPred_eq, Sentence.Realize,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Formula.realize_not,
      realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]
    exact ⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩
  · simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize, forall_eq,
      realize_eqZero, ← CharP.charP_iff_prime_eq_zero hp]
  · simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize,
      forall_eq, Formula.realize_bot, false_iff]
    intro H
    cases (CharP.char_is_prime_or_zero K p) <;> simp_all

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
inst✝ : DecidableEq α
γ : Type u_4
t : L.Term (α ⊕ γ)
s : Set α
h : ↑t.varFinsetLeft ⊆ s
v : α → M
xs : γ → M
⊢ ∀ (a : ↥t.varFinsetLeft), Sum.elim (v ∘ Subtype.val) xs (Sum.inl (Set.inclusion h a)) = v ↑a

Tactic:
by simp

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case equal
L : Language
L' : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : L'.Structure M
ft : (n : ℕ) → L.Term (α ⊕ Fin n) → L'.Term (β ⊕ Fin n)
fr : (n : ℕ) → L.Relations n → L'.Relations n
n : ℕ
v : α → M
v' : β → M
h1 : ∀ (n : ℕ) (t : L.Term (α ⊕ Fin n)) (xs : Fin n → M), realize (Sum.elim v' xs) (ft n t) = realize (Sum.elim v xs) t
h2 : ∀ (n : ℕ) (R : L.Relations n) (x : Fin n → M), RelMap (fr n R) x = RelMap R x
n✝ : ℕ
t₁✝ t₂✝ : L.Term (α ⊕ Fin n✝)
xs : Fin n✝ → M
⊢ (mapTermRel ft fr (fun x ↦ id) (equal t₁✝ t₂✝)).Realize v' xs ↔ (equal t₁✝ t₂✝).Realize v xs

Tactic:
simp [mapTermRel, Realize, h1]

Goal state after: