mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = sum fun p ↦ #↑{x | x ∈ p.aroots L}

Tactic:
by

Goal state after:
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✝³ : IsFiniteMeasure ν₁
inst✝² : IsFiniteMeasure ν₂
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ

Tactic:
by

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
⊢ (sum fun x ↦ ℵ₀) = lift.{v, u} #R[X] * ℵ₀

Tactic:
by

Goal state after:
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✝² : SigmaFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : SigmaFinite ν₁
inst✝ : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ AEMeasurable ((ν₁ ∗ₘ ν₂).rnDeriv μ) μ

Tactic:
by

Goal state after:
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✝² : SigmaFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : SigmaFinite ν₁
inst✝ : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ AEMeasurable (ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ) μ

Tactic:
by

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} #R[X]) ℵ₀) ℵ₀ ≤ max (max (lift.{v, u} (max #R ℵ₀)) ℵ₀) ℵ₀

Tactic:
by

Goal state after:
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✝² : SigmaFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : SigmaFinite ν₁
inst✝ : SigmaFinite ν₂
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (ν₁ ∗ₘ ν₂).rnDeriv μ =ᵐ[μ] ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ

Tactic:
by

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

Goal state before:
pp: R : Type u_1
K : Type u_3
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
ι : Type u_4
v : ι → K
inst✝ : IsAlgClosed K
hv : IsTranscendenceBasis R v
this : Nontrivial R := RingHom.domain_nontrivial (algebraMap R K)
⊢ IsAlgClosed K

Tactic:
by

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

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Cardinality

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

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type u
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #L ≤ max #R ℵ₀

Tactic:
by

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

Goal state before:
pp: 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
⊢ ↥(Algebra.adjoin R (Set.range v)) ≃+* ↥(Algebra.adjoin R (Set.range w))

Tactic:
by

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

Goal state before:
pp: 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
⊢ K ≃+* L

Tactic:
by

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.{max u w, v} #K ≤ Cardinal.lift.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀)

Tactic:
by

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.{max u w, v} (max #↥(Algebra.adjoin R (Set.range v)) ℵ₀) =
    Cardinal.lift.{v, max u w} (max #(MvPolynomial ι R) ℵ₀)

Tactic:
by

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

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
K' : Type u
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
hv : IsTranscendenceBasis R v'
⊢ #K' ≤ max (max #R #ι') ℵ₀

Tactic:
by

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
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max v w, u} #R ≤ ℵ₀

Tactic:
by

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
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
h : Cardinal.lift.{max u v, w} #ι < ℵ₀
⊢ Cardinal.lift.{max u v, w} #ι ≤ ℵ₀

Tactic:
by

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
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 ≤ ℵ₀

Tactic:
by

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
by

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
⊢ (map i (X ^ n - C a)).degree ≠ 0

Tactic:
by

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
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
⊢ max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀ = Cardinal.lift.{max u v, w} #ι

Tactic:
by

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
⊢ b ≠ 0

Tactic:
by

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
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K
this✝ : ℵ₀ ≤ Cardinal.lift.{max u v, w} #ι
this : Cardinal.lift.{max u w, v} #K = Cardinal.lift.{max u v, w} #ι
⊢ Cardinal.lift.{u, max v w} (Cardinal.lift.{w, v} #K) = Cardinal.lift.{u, max v w} (Cardinal.lift.{v, w} #ι)

Tactic:
by

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
⊢ s.card = n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
K' : Type u
inst✝³ : Field K'
inst✝² : Algebra R K'
inst✝¹ : IsAlgClosed K'
ι' : Type u
v' : ι' → K'
inst✝ : Nontrivial R
hv : IsTranscendenceBasis R v'
hR : #R ≤ ℵ₀
hK : ℵ₀ < #K'
⊢ #K' = #ι'

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
F G : L →ᴸ L'
h_fun : F.onFunction = G.onFunction
h_rel : F.onRelation = G.onRelation
⊢ F = G

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
F : L →ᴸ L'
⊢ LHom.id L' ∘ᴸ F = F

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
F : L →ᴸ L'
⊢ F ∘ᴸ LHom.id L = F

Tactic:
by

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.inl val)) x✝ = funMap (Sum.inl val) x✝

Tactic:
by

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

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

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

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

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
⊢ ℵ₀ < #L

Tactic:
by

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

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
⊢ L.card = (sum fun l ↦ lift.{v, u} #(L.Functions l)) + sum fun l ↦ lift.{u, v} #(L.Relations l)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: ⊢ Language.empty.card = 0

Tactic:
by

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 (i a⁻¹) * C (i a) = 1

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
⊢ IsEmpty Language.empty.Symbols

Tactic:
by

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

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Functions i) = lift.{u', u} #(L.Functions i) + lift.{u, u'} #(L'.Functions i)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
i : ℕ
⊢ #((L.sum L').Relations i) = lift.{v', v} #(L.Relations i) + lift.{v, v'} #(L'.Relations i)

Tactic:
by

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

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
⊢ (L.sum L').card = lift.{max u' v', max u v} L.card + lift.{max u v, max u' v'} L'.card

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
s : Set K
hs : IsTranscendenceBasis ℤ Subtype.val
t : Set L
ht : IsTranscendenceBasis ℤ Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
inst✝¹ : CharZero K
inst✝ : CharZero L
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M →[L] N
h : f.toFun = g.toFun
⊢ f = g

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
⊢ ℵ₀ < #L

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N →[L] P
hmn : M →[L] N
n✝ : ℕ
x✝¹ : L.Functions n✝
x✝ : Fin n✝ → M
⊢ (⇑hnp ∘ ⇑hmn) (funMap x✝¹ x✝) = funMap x✝¹ ((⇑hnp ∘ ⇑hmn) ∘ x✝)

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
⊢ Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t

Tactic:
by

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
⊢ map i (X ^ n - 1) = C (i a⁻¹) * (map i (X ^ n - C a)).comp (C b * X)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
f g : M ↪[L] N
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: 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
⊢ ϕ.IsExpansionOn M

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ Function.Injective fun x ↦ x.toHom

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.IsAlgebraic
f : M →[L] N
hf : Function.Injective ⇑f
⊢ (ofInjective hf).toHom = f

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: L : Language
L' : Language
M : Type w
inst✝ : L.Structure M
L'' : Language
e'✝ : L' ≃ᴸ L''
e✝ e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: α : Type u'
⊢ (constantsOn α).card = #α

Tactic:
by

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
M : Type w
N : Type w'
inst✝³ : L.Structure M
inst✝² : L.Structure N
P : Type u_1
inst✝¹ : L.Structure P
Q : Type u_2
inst✝ : L.Structure Q
hnp : N ↪[L] P
hmn : M ↪[L] N
⊢ ∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M), (⇑hnp ∘ ⇑hmn) (funMap f x) = funMap f ((⇑hnp ∘ ⇑hmn) ∘ x)

Tactic:
by

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

Goal state before:
pp: K : Type u
L : Type v
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : IsAlgClosed K
inst✝² : IsAlgClosed L
p : ℕ
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
⊢ Nonempty (K ≃+* L)

Tactic:
by

Goal state after: