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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ (ν.withDensity (μ.rnDeriv ν)).withDensity (μ.rnDeriv ν)⁻¹ = ν

Tactic:
change (ν.withDensity (μ.rnDeriv ν)).withDensity (fun x ↦ (μ.rnDeriv ν x)⁻¹) = ν

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
⊢ ((ν.withDensity (μ.rnDeriv ν)).withDensity fun x ↦ (μ.rnDeriv ν x)⁻¹) = ν
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: 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
⊢ IsTopologicallyTransitive M α

Tactic:
refine (isTopologicallyTransitive_iff_dense_iUnion_preimage M).mpr ?_

Goal state after:
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 α}, IsOpen U → U.Nonempty → Dense (⋃ m, (fun x ↦ m • x) ⁻¹' U)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_1
inst✝ : Field F
n : ℕ
hn : ¬n = 0
hn' : 0 < n
hn'' : X ^ n - 1 ≠ 0
σ τ : (X ^ n - 1).Gal
a : (X ^ n - 1).SplittingField
ha : a ^ n = 1
key : ∀ (σ : (X ^ n - 1).Gal), ∃ m, σ a = a ^ m
c : ℕ
hc : σ a = a ^ c
d : ℕ
hd : τ a = a ^ d
⊢ (σ * τ) a = (τ * σ) a

Tactic:
rw [σ.mul_apply, τ.mul_apply, hc, map_pow, hd, map_pow, hc, ← pow_mul, pow_mul']

Goal state after:
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:
· rw [ha, C_0, sub_zero]
    exact gal_X_pow_isSolvable n

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)

Tactic:
lintegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf

Goal state after:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← setIntegral_withDensity_eq_setIntegral_toReal_smul, withDensity_rnDeriv_eq _ _ hμν]

Goal state after:
case hf
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (μ.rnDeriv ν)

case hf_top
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ∞

case hs
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
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ν₂ : ν₂ ≪ μ
this : (ν₁ ∗ₘ ν₂).HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : G), (ν₁ ∗ₘ ν₂).rnDeriv μ x ∂μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top (ν₁ ∗ₘ ν₂) μ).ne

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
  simp only [card, mk_sum, mk_sigma, card_functions_sum, sum_add_distrib', lift_add, lift_sum,
    lift_lift, card_relations_sum, add_assoc,
    add_comm (Cardinal.sum fun i => (#(L'.Functions i)).lift)]

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
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
⊢ Function.Injective h.comp

Tactic:
intro f g hfg
  ext x; exact h.injective (congr_fun (congr_arg DFunLike.coe hfg) x)

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
f : M ≃[L] N
⊢ f.comp f.symm = refl L N

Tactic:
ext; rw [comp_apply, apply_symm_apply, refl_apply]

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]

Goal state after:
p : ℕ
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ (K ⊨ if p = 0 then (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} else if Nat.Prime p then {eqZero p} else {⊥}) ↔
    CharP K p
Module: Mathlib.ModelTheory.ElementaryMaps

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

Tactic:
by
    cases f
    cases g
    simpa only [ElementaryEmbedding.mk.injEq]

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_1
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔
    ∀ (xs : Fin 0 → N),
      ((L.lhomWithConstants M).onBoundedFormula φ).Realize
        (fun a ↦ Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) xs

Tactic:
LHom.realize_onBoundedFormula,

Goal state after:
case refine_1
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ φ.Realize ((constantMap ∘ Sum.inr) ∘ x) ↔
    ∀ (xs : Fin 0 → N), BoundedFormula.Realize φ (fun a ↦ Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) xs
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ (∀ (xs : Fin 0 → M),
      ((L.lhomWithConstants M).onBoundedFormula φ).Realize
        (fun a ↦ Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) xs) ↔
    φ.Realize x

Tactic:
LHom.realize_onBoundedFormula,

Goal state after:
case refine_2
L : Language
M : Type u_1
N✝ : Type u_2
P : Type u_3
Q : Type u_4
inst✝⁷ : L.Structure M
inst✝⁶ : L.Structure N✝
inst✝⁵ : L.Structure P
inst✝⁴ : L.Structure Q
N : Type u_5
inst✝³ : L.Structure N
inst✝² : L[[M]].Structure N
inst✝¹ : (L.lhomWithConstants M).IsExpansionOn N
inst✝ : N ⊨ L.elementaryDiagram M
n : ℕ
φ : L.Formula (Fin n)
x : Fin n → M
⊢ (∀ (xs : Fin 0 → M), BoundedFormula.Realize φ (fun a ↦ Term.realize default ((Constants.term ∘ Sum.inr ∘ x) a)) xs) ↔
    φ.Realize x
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ ((BoundedFormula.mapTermRelEquiv (fun x ↦ Term.constantsVarsEquivLeft) fun x ↦
              Equiv.sumEmpty (L.Relations x) Empty).symm
          φ).Realize
      x✝ default ↔
    φ.Realize (Sum.elim Subtype.val x✝) default

Tactic:
refine BoundedFormula.realize_mapTermRel_id ?_ (fun _ _ _ => rfl)

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L.BoundedFormula (↑A ⊕ α) 0
x✝ : α → M
⊢ ∀ (n : ℕ) (t : L.Term ((↑A ⊕ α) ⊕ Fin n)) (xs : Fin n → M),
    Term.realize (Sum.elim x✝ xs) (((fun x ↦ Term.constantsVarsEquivLeft) n).symm t) =
      Term.realize (Sum.elim (Sum.elim Subtype.val x✝) xs) t
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
classical
    refine Finset.induction definable_univ (fun i s _ h => ?_) s
    rw [Finset.inf_insert]
    exact (hf i).inter h

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

Goal state before:
pp: K✝ : Type u_1
p : ℕ
K : Type u_2
inst✝ : Language.ring.Structure K
h : K ⊨ Theory.ACF p
⊢ Field K

Tactic:
have := modelField_of_modelACF p K

Goal state after:
K✝ : Type u_1
p : ℕ
K : Type u_2
inst✝ : Language.ring.Structure K
h : K ⊨ Theory.ACF p
this : K ⊨ Theory.field
⊢ Field K
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
φ : L.Sentence
⊢ T ⊨ᵇ φ ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable

Tactic:
models_sentence_iff,

Goal state after:
L : Language
T : L.Theory
φ : L.Sentence
⊢ (∀ (M : T.ModelType), ↑M ⊨ φ) ↔ ¬(T ∪ {Formula.not φ}).IsSatisfiable
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

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

Tactic:
rintro ⟨M⟩
    let _ := fieldOfModelACF p M
    have := modelField_of_modelACF p M
    let _ := compatibleRingOfModelField M
    have := isAlgClosed_of_model_ACF p M
    infer_instance

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬T ⊨ᵇ Formula.not φ

Tactic:
models_sentence_iff,

Goal state after:
case inl
L : Language
T : L.Theory
h : T.IsComplete
φ : L.Sentence
hφ : T ⊨ᵇ φ
⊢ ¬∀ (M : T.ModelType), ↑M ⊨ Formula.not φ
Module: Mathlib.LinearAlgebra.FreeAlgebra

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max #↑s ℵ₀

Tactic:
max_comm

Goal state after:
case inr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : Set S
h✝ : Nontrivial R
⊢ #(List { x // x ∈ s }) ≤ max ℵ₀ #↑s
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inr.inr.inr.hbc
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ a ∣ c * b

Tactic:
rwa [mul_comm]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: case refine_2.inr.inr.inr.hz
a : Cardinal.{u}
ha : ℵ₀ ≤ a
b c : Cardinal.{u}
hbc : a ∣ b * c
hz : b * c ≠ 0
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → ∀ (b c : Cardinal.{u}), a ∣ b * c → b * c ≠ 0 → c ≤ b → a ∣ b ∨ a ∣ c
h : ¬c ≤ b
h✝ : b ≤ c
⊢ c * b ≠ 0

Tactic:
rwa [mul_comm]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Divisibility

Goal state before:
pp: n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑m < ℵ₀
⊢ n ∣ m

Tactic:
rw [hk, mul_lt_aleph0_iff] at this

Goal state after:
n m : ℕ
k : Cardinal.{u_1}
hk : ↑m = ↑n * k
this : ↑n = 0 ∨ k = 0 ∨ ↑n < ℵ₀ ∧ k < ℵ₀
⊢ n ∣ m
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
rank_inf : Fact (ℵ₀ ≤ Module.rank F E)
inst✝ : Algebra.IsAlgebraic F E
i : (Module.rank F E).ord.ToType
⊢ i ∈ Iio (φ (i⁺))

Tactic:
exact (lt_succ i).trans_le strictMono_leastExt.le_apply

Goal state after:
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (laurentAux r) (RatFunc.mk p 1) = RatFunc.mk ((taylor r) p) 1

Tactic:
mk_eq_div,

Goal state after:
R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (laurentAux r) ((algebraMap R[X] R⟮X⟯) p / (algebraMap R[X] R⟮X⟯) 1) = RatFunc.mk ((taylor r) p) 1
Module: Mathlib.FieldTheory.Laurent

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (algebraMap R[X] R⟮X⟯) ((taylor r) p) / (algebraMap R[X] R⟮X⟯) ((taylor r) 1) = RatFunc.mk ((taylor r) p) 1

Tactic:
mk_eq_div,

Goal state after:
R : Type u
inst✝¹ : CommRing R
r : R
p : R[X]
inst✝ : IsDomain R
⊢ (algebraMap R[X] R⟮X⟯) ((taylor r) p) / (algebraMap R[X] R⟮X⟯) ((taylor r) 1) =
    (algebraMap R[X] R⟮X⟯) ((taylor r) p) / (algebraMap R[X] R⟮X⟯) 1
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ a ^ p ^ m * x - x * a ^ p ^ m = 0

Tactic:
Subring.mem_center_iff.1 hm.2 x

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
p : ℕ
hchar : ExpChar D p
a : D
ha : a ∉ k
hinsep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
m : ℕ
hm : 1 ≤ m ∧ a ^ p ^ m ∈ k
n : ℕ
hn : p ^ m ≤ n
x : D
⊢ a ^ p ^ m * x - a ^ p ^ m * x = 0
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case splits'
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
hK : (primitiveRoots (finrank K L) K).Nonempty
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
⊢ (Polynomial.map (algebraMap K L) (X ^ finrank K L - C a)).Splits

Tactic:
rw [Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C,
      Polynomial.map_X]
    have ⟨_, hζ⟩ := hK
    rw [mem_primitiveRoots finrank_pos] at hζ
    exact X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) ha

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b

Tactic:
let E := F⟮a⟯ ⊔ F⟮b⟯

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : CharZero F
inst✝ : Algebra.IsIntegral F K
a b : K
E : IntermediateField F K := F⟮a⟯ ⊔ F⟮b⟯
⊢ normalizedTraceAux F K (a + b) = normalizedTraceAux F K a + normalizedTraceAux F K b
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
A B : IntermediateField F E
inst✝¹ : FiniteDimensional F ↥A
inst✝ : FiniteDimensional F ↥B
H : finrank F ↥(A ⊔ B) = finrank F ↥A * finrank F ↥B
⊢ finrank F ↥(A.toSubalgebra ⊔ B.toSubalgebra) = finrank F ↥A.toSubalgebra * finrank F ↥B.toSubalgebra

Tactic:
rwa [← sup_toSubalgebra_of_left]

Goal state after:
Module: Mathlib.FieldTheory.NormalizedTrace

Goal state before:
pp: F : Type u_3
E : Type u_4
K : Type u_5
inst✝¹² : Field F
inst✝¹¹ : Field E
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F E
inst✝⁸ : Algebra E K
inst✝⁷ : Algebra F K
inst✝⁶ : IsScalarTower F E K
inst✝⁵ : Algebra.IsIntegral F E
inst✝⁴ : Algebra.IsIntegral F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F E
inst✝¹ : Algebra.IsIntegral E K
inst✝ : CharZero E
a : K
⊢ (normalizedTrace F E) ((normalizedTrace E K) a) = (normalizedTrace F K) a

Tactic:
have : FiniteDimensional E E⟮a⟯ :=
    IntermediateField.adjoin.finiteDimensional (IsIntegral.isIntegral a)
  rw [normalizedTrace_def E K, inv_natCast_smul_eq (R := E) (S := F), map_smul,
    normalizedTrace_eq_of_finiteDimensional F E, LinearMap.smul_apply, ← smul_assoc,
    smul_eq_mul (a := _⁻¹), ← mul_inv, trace_trace, mul_comm,
    ← Nat.cast_mul, Module.finrank_mul_finrank, eq_comm]
  let E' := E⟮a⟯.restrictScalars F
  have : FiniteDimensional F E' := Module.Finite.trans E E⟮a⟯
  have h_finrank_eq : Module.finrank F E⟮a⟯ = Module.finrank F E' := rfl
  have h_trace_eq : trace F E⟮a⟯ (AdjoinSimple.gen E a) = trace F E' (AdjoinSimple.gen E a : E') :=
    rfl
  let a' : E' := AdjoinSimple.gen E a
  rw [h_finrank_eq, h_trace_eq, ← normalizedTrace_eq_of_finiteDimensional_apply F,
    ← normalizedTrace_intermediateField F K a']
  congr

Goal state after:
Module: Mathlib.FieldTheory.RatFunc.Degree

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree

Tactic:
← Polynomial.natDegree_mul x.denom_ne_zero y.denom_ne_zero,

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).num.natDegree + (x.denom * y.denom).natDegree = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A B : Subfield E
⊢ B = (algebraMap (↥(A ⊓ B)) E).fieldRange ↔ B ≤ A

Tactic:
algebraMap_ofSubfield,

Goal state after:
E : Type v
inst✝ : Field E
A B : Subfield E
⊢ B = (A ⊓ B).subtype.fieldRange ↔ B ≤ A
Module: Mathlib.Geometry.Convex.Hull

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s ⊆ (convexHull R) s

pp: R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s.Nonempty

Tactic:
· exact subset_convexHull_self

Goal state after:
R : Type u_1
X : Type u_2
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ConvexSpace R X
s : Set X
x : X
hs : (convexHull R) s = {x}
⊢ s.Nonempty
Module: Mathlib.Geometry.Convex.Cone.Face.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : DivisionRing R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
C F : PointedCone R M
hF : F.IsFaceOf C
x✝¹ : M
x✝ : x✝¹ ∈ C.lineal
hx : x✝¹ ∈ ↑C.toAddSubmonoid
hx' : x✝¹ ∈ ↑(-C.toAddSubmonoid)
⊢ x✝¹ ∈ ↑(-F.toAddSubmonoid)

Tactic:
· exact hF.mem_of_add_mem_left hx' hx (by simp)

Goal state after:
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : DiffeologicalSpace X
inst✝³ : IsDTopologyCompatible X
inst✝² : TopologicalSpace Y
inst✝¹ : DiffeologicalSpace Y
inst✝ : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ Continuous[inst✝⁵, inst✝²] f

Tactic:
convert! hf.continuous

Goal state after:
case e'_3
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : DiffeologicalSpace X
inst✝³ : IsDTopologyCompatible X
inst✝² : TopologicalSpace Y
inst✝¹ : DiffeologicalSpace Y
inst✝ : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ inst✝⁵ = dTopology

case e'_4
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : DiffeologicalSpace X
inst✝³ : IsDTopologyCompatible X
inst✝² : TopologicalSpace Y
inst✝¹ : DiffeologicalSpace Y
inst✝ : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ inst✝² = dTopology
Module: Mathlib.Geometry.Diffeology.Basic

Goal state before:
pp: case e'_4
X : Type u_1
Y : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : DiffeologicalSpace X
inst✝³ : IsDTopologyCompatible X
inst✝² : TopologicalSpace Y
inst✝¹ : DiffeologicalSpace Y
inst✝ : IsDTopologyCompatible Y
f : X → Y
hf : DSmooth f
⊢ inst✝² = dTopology

Tactic:
· rw [IsDTopologyCompatible.dTop_eq Y]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hps : ps ⊆ ↑s
p : P
h :
  (ps.Pairwise fun p₁ p₂ ↦ dist p₁ p = dist p₂ p) ↔
    ps.Pairwise fun p₁ p₂ ↦ dist p₁ ↑((orthogonalProjection s) p) = dist p₂ ↑((orthogonalProjection s) p)
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r

Tactic:
simp_rw [Set.pairwise_eq_iff_exists_eq] at h

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hps : ps ⊆ ↑s
p : P
h : (∃ z, ∀ x ∈ ps, dist x p = z) ↔ ∃ z, ∀ x ∈ ps, dist x ↑((orthogonalProjection s) p) = z
⊢ (∃ r, ∀ p₁ ∈ ps, dist p₁ p = r) ↔ ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) p) = r
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ f p -ᵥ f ↑((orthogonalProjection s) p) ∈ (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ

Tactic:
rw [← AffineIsometry.coe_toAffineMap, ← AffineMap.linearMap_vsub, Submodule.mem_orthogonal]

Goal state after:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup V
inst✝⁹ : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : NormedAddCommGroup V₂
inst✝⁷ : InnerProductSpace 𝕜 V₂
inst✝⁶ : MetricSpace P
inst✝⁵ : NormedAddTorsor V P
inst✝⁴ : MetricSpace P₂
inst✝³ : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst✝² : Nonempty ↥s
inst✝¹ : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst✝ : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ ∀ u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction,
    inner 𝕜 u (f.linear (p -ᵥ ↑((orthogonalProjection s) p))) = 0