mathlib-initiative/mathlib-tactics huggingface dataset:
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 ν
⊢ (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν + ν'] 0

Tactic:
simp only [rnDeriv_eq_zero, MutuallySingular.add_right_iff]

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 ν
⊢ μ.singularPart ν ⟂ₘ ν ∧ μ.singularPart ν ⟂ₘ ν'
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 : ν ≪ ν + ν'
⊢ μ.rnDeriv (ν + ν') =ᵐ[ν] μ.rnDeriv ν

Tactic:
rw [haveLebesgueDecomposition_add μ ν']

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n k : ℕ
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : k + 1 ≤ s.card
⊢ k < s.card

Tactic:
exact (lt_add_one k).trans_le s_card

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
rw [coverEntropyInf_image_of_comap _ h F]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf S F
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
⊢ μ.rnDeriv ν ≤ᵐ[ν] 1 ↔ μ ≤ ν

Tactic:
refine ⟨fun h s ↦ ?_, fun h ↦ rnDeriv_le_one_of_le h⟩

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν ≤ᵐ[ν] 1
s : Set α
⊢ μ s ≤ ν s
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
withDensity_congr_ae h,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
h : μ.rnDeriv ν =ᵐ[ν] 1
⊢ ν.withDensity 1 = ν
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
⊢ coverEntropyInf T F = ⨆ i, ⨆ (_ : p i), coverEntropyInfEntourage T F (s i)

Tactic:
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm
    (iSup₂_mono' fun i h_i ↦ ⟨s i, HasBasis.mem_of_mem h h_i, le_refl _⟩)
  obtain ⟨i, h_i, si_U⟩ := (HasBasis.mem_iff h).1 U_uni
  exact (coverEntropyInfEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyInfEntourage T F (s i)) i h_i)

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

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

Tactic:
nth_rw 2 [← Measure.withDensity_rnDeriv_eq μ ν hμν]
  rw [setLIntegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf hs]
  simp only [Pi.mul_apply]

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
s : Subalgebra F E :=
  { carrier := {x | ∃ (hx : x ∈ solvableByRad F E), motive x hx}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯,
    zero_mem' := ⋯, algebraMap_mem' := ⋯ }
⊢ s.IsAlgebraic

Tactic:
by
    rintro x ⟨hx, hx'⟩
    apply isAlgebraic_solvableByRad
    exact hx

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

Goal state before:
pp: α : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : NonAssocRing R
inst✝² : NonAssocRing S
inst✝¹ : CompatibleRing R
inst✝ : CompatibleRing S
f : R ≃[ring] S
⊢ ∀ (x y : R), f.toFun (x * y) = f.toFun x * f.toFun y

Tactic:
intro x y
        simpa using! f.map_fun mulFunc ![x, y]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize v (termOfFreeCommRing p) = (FreeCommRing.lift v) p

Tactic:
rw [termOfFreeCommRing]

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : CompatibleRing R
p : FreeCommRing α
v : α → R
⊢ Term.realize v (Classical.choose ⋯) = (FreeCommRing.lift v) p
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : DecidableEq α
v : β → M
v' : α → M
l✝ : ℕ
_f✝ : L.Functions l✝
_ts✝ : Fin l✝ → L.Term α
ih :
  ∀ (a : Fin l✝) {f : ↥(_ts✝ a).varFinset → β},
    (∀ (a_1 : ↥(_ts✝ a).varFinset), v (f a_1) = v' ↑a_1) → realize v ((_ts✝ a).restrictVar f) = realize v' (_ts✝ a)
f : ↥(func _f✝ _ts✝).varFinset → β
hv' : ∀ (a : ↥(func _f✝ _ts✝).varFinset), v (f a) = v' ↑a
i : Fin l✝
⊢ ∀ (a : ↥(_ts✝ i).varFinset), v ((f ∘ Set.inclusion ⋯) a) = v' ↑a

Tactic:
by simp [Function.comp_apply, hv']

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ⨆ i, #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

pp: case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0

Tactic:
ciSup_le_iff' bddAbove_of_small

Goal state after:
case refine_1
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i) ∧ ∀ (i : ℕ), #(L.Term (α ⊕ Fin i)) ≤ max ℵ₀ #(α ⊕ (i : ℕ) × L.Functions i)

case refine_1
L : Language
α : Type u'
⊢ ⨆ i, #(L.Term (α ⊕ Fin i)) ≠ 0
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case refine_2
L : Language
α : Type u'
⊢ ℵ₀ ≤ #((n : ℕ) × L.Term (α ⊕ Fin n)) ∧ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))

Tactic:
← infinite_iff

Goal state after:
case refine_2
L : Language
α : Type u'
⊢ Infinite ((n : ℕ) × L.Term (α ⊕ Fin n)) ∧ #(α ⊕ (i : ℕ) × L.Functions i) ≤ #((n : ℕ) × L.Term (α ⊕ Fin n))
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
⊢ ∃ x, eval x p = 0

Tactic:
have h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n} :=
    Theory.Model.mono h (by simp [Theory.ACF])

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : K ⊨ genericMonicPolyHasRoot '' {n | 0 < n}
⊢ ∃ x, eval x p = 0
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: case hS
p : ℕ
hp : Nat.Prime p ∨ p = 0
⊢ (Theory.ACF p).IsSatisfiable

Tactic:
exact ACF_isSatisfiable hp

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case mp
L : Language
T : L.Theory
⊢ T.IsComplete → T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N

Tactic:
intro hcomp

Goal state after:
case mp
L : Language
T : L.Theory
hcomp : T.IsComplete
⊢ T.IsSatisfiable ∧ ∀ (M N : T.ModelType), ↑M ≅[L] ↑N
Module: Mathlib.GroupTheory.OreLocalization.Cardinality

Goal state before:
pp: case inl
R : Type u
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type v
inst✝ : MulAction R X
hc : ∀ (s s' : ↥S), Commute s s'
h✝ : Finite X
this : lift.{v, max u v} #(OreLocalization S X) ≤ lift.{max u v, v} #X
⊢ #(OreLocalization S X) ≤ lift.{u, v} #X

Tactic:
rwa [lift_umax.{v, u}, lift_id'] at this

Goal state after:
Module: Mathlib.FieldTheory.Finite.Extension

Goal state before:
pp: k : Type u_1
inst✝⁴ : Field k
inst✝³ : Finite k
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP k p
n : ℕ
inst✝ : NeZero n
⊢ IsSplittingField k (Extension k p n) (X ^ Nat.card k ^ n - X)

Tactic:
have := Fintype.ofFinite (Extension k p n)
  convert! FiniteField.isSplittingField_sub (Extension k p n) k
  · rw [Fintype.card_eq_nat_card, natCard_extension]

Goal state after:
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝⁷ : Field R
inst✝⁶ : Differential R
a✝ b : R
F : Type u_2
inst✝⁵ : Field F
inst✝⁴ : Differential F
inst✝³ : CharZero F
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : FiniteDimensional F K
default : { _a // DifferentialAlgebra F K } := ⟨differentialFiniteDimensional F K, ⋯⟩
x✝ : { _a // DifferentialAlgebra F K }
a : Differential K
ha : DifferentialAlgebra F K
x : K
| (fun x_1 ↦ (aeval x) (mapCoeffs (minpoly F x)) + (aeval x) (derivative (minpoly F x)) * x_1) x′

Tactic:
apply (@deriv_aeval_eq _ _ _ _ _ default.1 _ default.2 _ _).symm

Goal state after:
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Tactic:
cases nonempty_fintype σ

Goal state after:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ FiniteDimensional K (R σ K)

Tactic:
cases nonempty_fintype σ

Goal state after:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ FiniteDimensional K (R σ K)
Module: Mathlib.FieldTheory.Finite.Polynomial

Goal state before:
pp: σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
⊢ (evalᵢ σ K).ker = ⊥

Tactic:
cases nonempty_fintype σ

Goal state after:
case intro
σ K : Type u
inst✝² : Fintype K
inst✝¹ : Field K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ (evalᵢ σ K).ker = ⊥
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: case inl
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
h : Finite K
this : Finite L
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
exact exists_linearIndependent_algEquiv_apply_of_finite K L

Goal state after:
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁶ : CommRing K
inst✝⁵ : CommRing L
inst✝⁴ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝³ : ExpChar M p
inst✝² : ExpChar K p
inst✝¹ : PerfectRing M p
inst✝ : IsPRadical i p
x : L
n : ℕ
y : K
h : i y = x ^ p ^ n
⊢ liftAux i j p x = (iterateFrobeniusEquiv M p n).symm (j y)

Tactic:
rw [liftAux]
  have h' := Classical.choose_spec (lift_aux i p x)
  set n' := (Classical.choose (lift_aux i p x)).1
  replace h := congr($(h.symm) ^ p ^ n')
  rw [← pow_mul, mul_comm, pow_mul, ← h', ← map_pow, ← map_pow, ← sub_eq_zero, ← map_sub,
    ← RingHom.mem_ker] at h
  obtain ⟨m, h⟩ := mem_pNilradical.1 (IsPRadical.ker_le i p h)
  refine (iterateFrobeniusEquiv M p (m + n + n')).injective ?_
  conv_lhs => rw [iterateFrobeniusEquiv_add_apply, RingEquiv.apply_symm_apply]
  rw [add_assoc, add_comm n n', ← add_assoc,
    iterateFrobeniusEquiv_add_apply (m := m + n'), RingEquiv.apply_symm_apply,
    iterateFrobeniusEquiv_def, iterateFrobeniusEquiv_def,
    ← sub_eq_zero, ← map_pow, ← map_pow, ← map_sub,
    add_comm m, add_comm m, pow_add, pow_mul, pow_add, pow_mul, ← sub_pow_expChar_pow, h, map_zero]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n + 1, ↑x)

Tactic:
suffices R K p (n, (x : K)) (Nat.succ n, frobenius K p (x : K)) by
      rwa [map_natCast] at this

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x n : ℕ
ih : ↑x = mk K p (n, ↑x)
⊢ R K p (n, ↑x) (n.succ, (frobenius K p) ↑x)
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
inter : (⇑((ad (↥k) D) a))^[p ^ m] = 0
⊢ (⇑((ad (↥k) D) a))^[n] = 0

Tactic:
rw [(Nat.sub_eq_iff_eq_add hn).1 rfl, Function.iterate_add, inter, Pi.comp_zero,
    iterate_map_zero, Function.const_zero]

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
⊢ ∃ x ∉ ⊥, IsSeparable L x

Tactic:
set φ := Subalgebra.equivOfEq (⊥ : Subalgebra L D) (.center L D) hcenter.symm

Goal state after:
L : Type u_2
D : Type u_3
inst✝⁴ : Field L
inst✝³ : DivisionRing D
inst✝² : Algebra L D
inst✝¹ : Algebra.IsAlgebraic L D
inst✝ : IsCentral L D
hneq : ⊥ ≠ ⊤
hcenter : Subalgebra.center L D = ⊥
ntrivial : k ≠ ⊤
φ : ↥⊥ ≃ₐ[L] ↥(Subalgebra.center L D) := ⊥.equivOfEq (Subalgebra.center L D) ⋯
⊢ ∃ x ∉ ⊥, IsSeparable L x
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Cardinal.lift.{u, v} (Module.rank R ↥⊥) = Cardinal.lift.{v, u} (Module.rank R R)
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)

Tactic:
rw [Module.rank_self, Cardinal.lift_one, Cardinal.lift_eq_one] at this

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
hf : Flat R ↥A ∨ Flat R ↥B
hc : ∀ (a b : ↥(A ⊓ B)), Commute ↑a ↑b
hinj : Function.Injective ⇑(algebraMap R S)
a✝ : Nontrivial R
this : Module.rank R ↥⊥ = 1
⊢ 1 ≤ Module.rank R ↥(A ⊓ B)
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
this✝ : FiniteDimensional E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional F ↥E'
h_finrank_eq : Module.finrank F ↥E⟮a⟯ = Module.finrank F ↥E'
h_trace_eq : (trace F ↥E⟮a⟯) (AdjoinSimple.gen E a) = (trace F ↥E') (AdjoinSimple.gen E a)
a' : ↥E' := AdjoinSimple.gen E a
⊢ (normalizedTrace F K) a = (↑(Module.finrank F ↥E'))⁻¹ • (trace F ↥E') (AdjoinSimple.gen E a)

Tactic:
← normalizedTrace_eq_of_finiteDimensional_apply F,

Goal state after:
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
this✝ : FiniteDimensional E ↥E⟮a⟯
E' : IntermediateField F K := IntermediateField.restrictScalars F E⟮a⟯
this : FiniteDimensional F ↥E'
h_finrank_eq : Module.finrank F ↥E⟮a⟯ = Module.finrank F ↥E'
h_trace_eq : (trace F ↥E⟮a⟯) (AdjoinSimple.gen E a) = (trace F ↥E') (AdjoinSimple.gen E a)
a' : ↥E' := AdjoinSimple.gen E a
⊢ (normalizedTrace F K) a = (normalizedTrace F ↥E') (AdjoinSimple.gen E a)
Module: Mathlib.FieldTheory.PurelyInseparable.Exponent

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsPurelyInseparable K L
a : L
n : ℕ
h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range
p : ℕ
h✝ : ExpChar K p
hp : Nat.Prime p
hchar✝ : CharP K p
y : K
hy : (algebraMap K L) y = a ^ ringExpChar K ^ n
f : K[X] := X ^ ringExpChar K ^ n - C y
⊢ (aeval a) f = 0

Tactic:
rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
hi :
  i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))
H : Function.Injective ⇑(Ideal.Quotient.mk M)
⊢ M = ⊥

Tactic:
RingHom.injective_iff_ker_eq_bot,

Goal state after:
F : Type u
inst✝⁴ : Field F
A : Type v
inst✝³ : Field A
B : Type w
inst✝² : Field B
inst✝¹ : Algebra F A
inst✝ : Algebra F B
M : Ideal (A ⊗[F] B)
hM : M.IsMaximal
K : Type (max v w) := A ⊗[F] B ⧸ M
this : Field K := Ideal.Quotient.field M
i : A ⊗[F] B →ₐ[F] K := IsScalarTower.toAlgHom F (A ⊗[F] B) K
fa : A →ₐ[F] K := i.comp Algebra.TensorProduct.includeLeft
fb : B →ₐ[F] K := i.comp Algebra.TensorProduct.includeRight
hi :
  i =
    (fa.range.mulMap fb.range).comp
      ↑(Algebra.TensorProduct.congr (AlgEquiv.ofInjective fa ⋯) (AlgEquiv.ofInjective fb ⋯))
H : RingHom.ker (Ideal.Quotient.mk M) = ⊥
⊢ M = ⊥
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
h✝ : PerfectField E
eq : perfectClosure F E = ⊥
p : ℕ := ringExpChar F
this : ExpChar E p
x : F
y : E
h : (frobenius E p) y = (algebraMap F E) x
⊢ (algebraMap F E) x = y ^ ringExpChar F ^ 1

Tactic:
by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]

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 * (x.denom * y.denom)).natDegree = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree

Tactic:
← Polynomial.natDegree_mul (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy),

Goal state after:
K : Type u
inst✝ : Field K
x y : K⟮X⟯
hx : x ≠ 0
hy : y ≠ 0
⊢ ((x * y).num * (x.denom * y.denom)).natDegree = (x.num * y.num).natDegree + (x * y).denom.natDegree
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 * (x.denom * y.denom)).natDegree = (x.num * y.num * (x * y).denom).natDegree

Tactic:
RatFunc.num_denom_mul

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : Algebra.Transcendental K K⟮X⟯
⊢ False

Tactic:
rw [Algebra.transcendental_iff_not_isAlgebraic] at tr

Goal state after:
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
H : IsAlgebraic K f
this : Algebra.IsAlgebraic K ↥K⟮f⟯
tr : ¬Algebra.IsAlgebraic K K⟮X⟯
⊢ False
Module: Mathlib.FieldTheory.PurelyInseparable.Tower

Goal state before:
pp: F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this : Algebra.IsSeparable F ↥F⟮x⟯
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree

Tactic:
have := (isSeparable_adjoin_simple_iff_isSeparable _ _).2 hsep'

Goal state after:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
x : K
hsep : IsSeparable F x
inst✝ : IsPurelyInseparable F E
hi : IsIntegral F x
hi' : IsIntegral E x
hsep' : IsSeparable E x
this✝ : Algebra.IsSeparable F ↥F⟮x⟯
this : Algebra.IsSeparable E ↥E⟮x⟯
⊢ (Polynomial.map (algebraMap F E) (minpoly F x)).natDegree = (minpoly E x).natDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝ : Field E
A : Subfield E
⊢ Module.rank ↥A ↥⊥ = 1

Tactic:
IntermediateField.rank_bot

Goal state after:
E : Type v
inst✝ : Field E
A : Subfield E
⊢ 1 = 1
Module: Mathlib.Geometry.Convex.Cone.DualFinite

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
S T : Finset M
⊢ dual p (↑S ∪ ↑T) = dual p ↑S ⊓ dual p ↑T

Tactic:
dual_union

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : IsOrderedRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : M →ₗ[R] N →ₗ[R] R
S T : Finset M
⊢ dual p ↑S ⊓ dual p ↑T = dual p ↑S ⊓ dual p ↑T
Module: Mathlib.FieldTheory.RatFunc.Luroth

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
⊢ Polynomial.C (c E) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E) = Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
rw [map_mul, mul_assoc]
  conv =>
    enter [1, 2]
    rw [← Polynomial.smul_eq_C_mul, algebraMap_smul, ← Φ'_map, eq_C_content_mul_primPart (Φ' E)]
  rw [Polynomial.map_mul, map_C, ← mul_assoc, ← C_mul, inv_mul_cancel₀, map_one, one_mul]
  · rw [ne_eq, FaithfulSMul.algebraMap_eq_zero_iff, content_eq_zero_iff]
    exact Φ'_ne_zero h

Goal state after: