mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: case refine_2
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : 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✝
x✝¹ : U✝.Nonempty
b : M
x✝ : α
⊢ x✝ ∈ (fun x ↦ b • x) ⁻¹' ⋃ m, (fun x ↦ m • x) ⁻¹' U✝ → x✝ ∈ ⋃ m, (fun x ↦ m • x) ⁻¹' U✝

Tactic:
·

Goal state after:
case refine_2
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : 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✝
x✝¹ : U✝.Nonempty
b : M
x✝ : α
⊢ x✝ ∈ (fun x ↦ b • x) ⁻¹' ⋃ m, (fun x ↦ m • x) ⁻¹' U✝ → x✝ ∈ ⋃ m, (fun x ↦ m • x) ⁻¹' U✝
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
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

pp: case inr.inr
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
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:
·

Goal state after:
case inr.inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
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
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case refine_1
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)

pp: case refine_2
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U

Tactic:
·

Goal state after:
case refine_1
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)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case refine_2
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U

Tactic:
·

Goal state after:
case refine_2
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case h0
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ 0

pp: case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
·

Goal state after:
case h0
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞

Tactic:
·

Goal state after:
case ht
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ μ.rnDeriv ν =ᵐ[ν] fun x ↦ μ.rnDeriv (μ + ν) x / ν.rnDeriv (μ + ν) x

Tactic:
filter_upwards [rnDeriv_add_self ν μ, rnDeriv_self_add μ ν, μ.rnDeriv_lt_top ν]
      with a ha1 ha2 ha_lt_top
  rw [ha1, ha2, ENNReal.div_eq_inv_mul, inv_inv, ENNReal.div_eq_inv_mul, ← mul_assoc,
      ENNReal.mul_inv_cancel, one_mul]
  · simp
  · simp [ha_lt_top.ne]

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
⊢ Group.IsSolvable (Multiset.prod 0).Gal

pp: case h₂
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]},
    a ∈ s → s_1 ⊆ s → Group.IsSolvable s_1.prod.Gal → Group.IsSolvable (insert a s_1).prod.Gal

Tactic:
·

Goal state after:
case h₁
F : Type u_1
inst✝ : Field F
s : Multiset F[X]
hs : ∀ p ∈ s, Group.IsSolvable p.Gal
⊢ Group.IsSolvable (Multiset.prod 0).Gal
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
⊢ ∀ {a : F[X]} {s_1 : Multiset F[X]},
    a ∈ s → s_1 ⊆ s → Group.IsSolvable s_1.prod.Gal → Group.IsSolvable (insert a s_1).prod.Gal

Tactic:
·

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

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
hn : n = 0
⊢ Group.IsSolvable (X ^ n - 1).Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable fun x ↦ (map f μ).rnDeriv (map f ν) (f x)

pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable fun x ↦ (map f μ).rnDeriv (map f ν) (f x)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)

pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
⊢ ∫⁻ (x : α) in s, (map f μ).rnDeriv (map f ν) (f x) ∂ν = ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable (μ.rnDeriv ν)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n - C a).Gal

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
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
·

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n - C a).Gal
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
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
⊢ Group.IsSolvable (X ^ n - C a).Gal

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
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
·

Goal state after:
case pos
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
⊢ Group.IsSolvable (X ^ n - C a).Gal
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 ν
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
have : SigmaFinite (map f ν) := hf.sigmaFinite_map

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this : SigmaFinite (map f ν)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (μ.singularPart ν).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)

pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (μ.singularPart ν).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm) = AlgHom.id R (MvPolynomial κ R)

pp: case refine_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e.symm).comp (MvPolynomial.rename ⇑e) = AlgHom.id R (MvPolynomial ι R)

pp: case refine_3
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial κ R ≃+* ↥(Algebra.adjoin R (Set.range w))

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm) = AlgHom.id R (MvPolynomial κ R)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case refine_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e.symm).comp (MvPolynomial.rename ⇑e) = AlgHom.id R (MvPolynomial ι R)

pp: case refine_3
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ MvPolynomial κ R ≃+* ↥(Algebra.adjoin R (Set.range w))

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
⊢ (MvPolynomial.rename ⇑e.symm).comp (MvPolynomial.rename ⇑e) = AlgHom.id R (MvPolynomial ι R)
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
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι

pp: R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)

Tactic:
·

Goal state after:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{max v w, u} #R ≤ Cardinal.lift.{max u v, w} #ι
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
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)

Tactic:
·

Goal state after:
R : Type u
K : Type v
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsAlgClosed K
ι : Type w
v : ι → K
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ ℵ₀ ≤ max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
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
⊢ (map i (X ^ n - 1)).Splits

pp: case neg
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
⊢ (map i (X ^ n - 1)).Splits

Tactic:
·

Goal state after:
case pos
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
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
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
⊢ (map i (X ^ n - 1)).Splits

Tactic:
have hs' : Multiset.card s = n := by
    rw [← h.natDegree_eq_card_roots, natDegree_map, natDegree_X_pow_sub_C]

Goal state after:
case neg
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
⊢ (map i (X ^ n - 1)).Splits
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
⊢ funMap (ϕ.onFunction f) xs = funMap f xs

pp: case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs

Tactic:
·

Goal state after:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f ↦ ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r ↦ ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
⊢ funMap (ϕ.onFunction f) xs = funMap f xs