mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
inst✝³ : L.Structure M
inst✝² : L.Structure N
α : Type u'
F : Type u_4
inst✝¹ : EquivLike F M N
inst✝ : L.StrongHomClass F M N
g : F
φ : L.Formula α
v : α → M
⊢ φ.Realize (⇑g ∘ v) ↔ φ.Realize v

Tactic:
by
  rw [Formula.Realize, Formula.Realize, ← realize_boundedFormula g φ, iff_eq_eq,
    Unique.eq_default (g ∘ default)]

Goal state after:
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type u_1
L : Language
inst✝¹ : L.Structure M
α : Type u_2
β : Type u_3
A : Set M
f : (α → M) → M
inst✝ : Finite α
g : (β → M) → α → M
hg : DefinableMap L A g
hf : DefinableFun L A f
G : (Option β → M) → Option α → M :=
  fun w j ↦
    match j with
    | none => w none
    | some i => g (w ∘ some) i
hG : DefinableMap L A G
⊢ DefinableFun L A fun v ↦ f (g v)

Tactic:
simpa [DefinableFun, G, tupleGraph] using! hf.preimage_map hG

Goal state after:
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ ∃ N, lift.{max u v w, w} κ ≤ #↑N

Tactic:
refine ⟨(N.is_model.mono Set.subset_union_left).bundled.reduct _, ?_⟩

Goal state after:
L : Language
T : L.Theory
κ : Cardinal.{w}
M : Type w'
inst✝² : L.Structure M
inst✝¹ : M ⊨ T
inst✝ : Infinite M
N : ((L.lhomWithConstants (Quotient.out κ)).onTheory T ∪ L.distinctConstantsTheory Set.univ).ModelType
⊢ lift.{max u v w, w} κ ≤ #↑(ModelType.reduct (L.lhomWithConstants (Quotient.out κ)) ⋯.bundled)
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
f : (α → M) → M
g : α → (β → M) → M
hf : A.TermDefinable L f
hg : ∀ (i : α), A.TermDefinable L (g i)
⊢ A.TermDefinable L fun b ↦ f fun x ↦ g x b

Tactic:
obtain ⟨φ, rfl⟩ := hf

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
β : Type u_1
g : α → (β → M) → M
hg : ∀ (i : α), A.TermDefinable L (g i)
φ : L[[↑A]].Term α
⊢ A.TermDefinable L fun b ↦ (fun v ↦ Term.realize v φ) fun x ↦ g x b
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: case refine_1
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : T ⊨ᵇ φ
M : ((L.lhomWithConstants α).onTheory T).ModelType
⊢ ↑M ⊨ Formula.equivSentence φ

pp: case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
⊢ φ.Realize v

Tactic:
· let := (L.lhomWithConstants α).reduct M
    rw [Formula.realize_equivSentence]
    have : M ⊨ T := (LHom.onTheory_model _ _).1 M.is_model -- why isn't M.is_model inferInstance?
    let M' := Theory.ModelType.of T M
    exact h M' (fun a => (L.con a : M)) _

Goal state after:
case refine_2
L : Language
T : L.Theory
α : Type w
φ : L.Formula α
h : (L.lhomWithConstants α).onTheory T ⊨ᵇ Formula.equivSentence φ
M : T.ModelType
v : α → ↑M
⊢ φ.Realize v
Module: Mathlib.RingTheory.Nullstellensatz

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}

Tactic:
radical_eq_sInf

Goal state after:
k : Type u_1
K : Type u_2
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Type u_3
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}
x : σ → K
hx : x ∈ zeroLocus K I
⊢ p ∈ vanishingIdeal k {x}
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: φ : Language.ring.Sentence
T0 : Finset Language.ring.Sentence
hT0 : ↑T0 ⊆ Theory.ACF 0
h : ↑T0 ⊨ᵇ φ
f : (ψ : Language.ring.Sentence) → ψ ∈ Theory.ACF 0 → { s // ∀ q ∉ s, Theory.ACF ↑q ⊨ᵇ ψ }
s : Finset Nat.Primes := T0.attach.biUnion fun φ ↦ ↑(f ↑φ ⋯)
p : Nat.Primes
ψ : Language.ring.Sentence
hψ : ψ ∈ T0
hpψ : ∀ (x : Language.ring.Sentence) (x_1 : x ∈ T0), p ∉ ↑(f x ⋯)
⊢ Theory.ACF ↑p ⊨ᵇ ψ

Tactic:
exact (f ψ (hT0 hψ)).2 p (hpψ _ hψ)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
ι : Type u_2
s : Multiset ι
f : ι → R
h : ∀ x ∈ s, f x ≠ 0
⊢ logDeriv (Multiset.map f s).prod = (Multiset.map (fun x ↦ logDeriv (f x)) s).sum

Tactic:
by
  induction s using Multiset.induction_on
  · simp
  · rename_i h₂
    simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.prod_cons]
    rw [← h₂]
    · apply logDeriv_mul
      · simp [h]
      · simp_all
    · simp_all

Goal state after:
Module: Mathlib.Topology.Separation.Connected

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : ConnectedSpace X
inst✝¹ : Nontrivial X
inst✝ : T1Space X
x : X
⊢ (𝓝[≠] x).NeBot

Tactic:
by
  by_contra contra
  rw [not_neBot, ← isOpen_singleton_iff_punctured_nhds] at contra
  replace contra := nonempty_inter isOpen_compl_singleton
    contra (compl_union_self _) (Set.nonempty_compl_of_nontrivial _) (singleton_nonempty _)
  simp [compl_inter_self {x}] at contra

Goal state after:
Module: Mathlib.FieldTheory.Galois.NormalBasis

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Infinite K
⊢ ∃ x, LinearIndependent K fun σ ↦ σ x

Tactic:
by
  classical
  /- Choose a basis `e` of `L` over `K` and form the matrix `M` with entries
    `∑ₖ i⁻¹j(eₖ)Xₖ` where `i,j ∈ Gal(L/K)` and `Xₖ`s are independent variables. -/
  have e := Module.Free.chooseBasis K L
  let M : Matrix Gal(L/K) Gal(L/K) (MvPolynomial _ L) :=
    .of fun i j ↦ ∑ k, i.symm (j (e k)) • .X k
  /- By [ConradLinearChar] Lemma 3.4, there exists `{xₖ} ⊆ L` such that `∑ₖ j(eₖ)xₖ = 1`
    if `j = 1` and `∑ₖ j(eₖ)xₖ = 0` otherwise. -/
  have hq : Submodule.span L (Set.range fun k (j : Gal(L/K)) ↦ j (e k)) = ⊤ := by
    apply span_flip_eq_top_iff_linearIndependent.mpr <|
      ((linearIndependent_algHom_toLinearMap K L L).comp _
        (algEquivEquivAlgHom K L).injective).map' _ (e.constr L).symm.ker
  /- If we evaluate `M` at `Xₖ = xₖ`, the determinant of `M` evaluates to 1. -/
  obtain ⟨c, hc⟩ : ∃ c : _ → L, M.det.eval c = 1 := by
    obtain ⟨g, hg⟩ := (Submodule.mem_span_range_iff_exists_fun _).mp
      (hq ▸ Submodule.mem_top (x := Pi.single 1 1))
    simp_rw [RingHom.map_det]
    refine ⟨g, congr(Matrix.det $(?_)).trans Matrix.det_one⟩
    ext i j
    simpa [M, Pi.single_apply, inv_mul_eq_one, mul_comm, Matrix.one_apply]
      using! congr($hg (i⁻¹ * j))
  /- Therefore `det M` is nonzero. -/
  have hM : M.det ≠ 0 := fun h0 ↦ by
    simpa [hc] using! congr(($h0).eval c)
  /- Since `K` is infinite, we may evaluate `det M` at some point with coordinates in `K`
    and get a nonzero value. The coordinates give rise to an element of `L` via the basis `e`. -/
  obtain ⟨b, hb⟩ : ∃ b : _ → K, M.det.eval (algebraMap K L ∘ b) ≠ 0 := by
    by_contra! h
    refine hM (MvPolynomial.funext_set _
      (fun _ ↦ Set.infinite_range_of_injective (algebraMap K L).injective) fun x hx ↦ ?_)
    obtain ⟨x, rfl⟩ := Set.range_piMap _ ▸ hx
    simpa using! h x
  /- This element of `L` is exactly what we want: we simply need to show the first row of the
    evaluated matrix is `K`-linearly independent. But since the other rows are obtained from the
    first row by applying a `K`-endomorphism, it suffices to show that the columns are linearly
    independent, which follows from the nonzeroness of the evaluated determinant. -/
  refine ⟨∑ k, b k • e k, Fintype.linearIndependent_iff.mpr fun a ha ↦
    funext_iff.mp <| (algebraMap K L).injective.comp_left ?_⟩
  simp_rw [Function.comp_def, map_zero]
  rw [RingHom.map_det, RingHom.mapMatrix_apply] at hb
  refine Matrix.eq_zero_of_mulVec_eq_zero hb (funext fun i ↦ i.injective ?_)
  simp_rw [M, Pi.zero_apply, map_zero, ← ha]
  simp [Algebra.smul_def, Matrix.mulVec_eq_sum, mul_comm]

Goal state after:
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case refine_1
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
⊢ ⇑b ∘ φ '' Iio i ⊆ ⇑b '' Iio (φ i)

Tactic:
rw [image_comp]

Goal state after:
case refine_1
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
⊢ ⇑b '' φ '' Iio i ⊆ ⇑b '' Iio (φ i)
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case pos
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : Nonempty ↑(Iio i)
⊢ (fun f ↦ Subalgebra.iSupLift (fun x ↦ ((fun j ↦ filtration ↑j) x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯)
      ((fun f ↦ ⟨fun j ↦ embFunctor F E ⋯ f, ⋯⟩) f) =
    f

Tactic:
ext ⟨x, hx⟩

Goal state after:
case pos
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : Nonempty ↑(Iio i)
x : E
hx : x ∈ (filtration i).toSubalgebra
⊢ ((fun f ↦ Subalgebra.iSupLift (fun x ↦ ((fun j ↦ filtration ↑j) x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯)
        ((fun f ↦ ⟨fun j ↦ embFunctor F E ⋯ f, ⋯⟩) f))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩
Module: Mathlib.FieldTheory.CardinalEmb

Goal state before:
pp: case a
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
rank_inf : ℵ₀ ≤ Module.rank F E
this : Fact (ℵ₀ ≤ Module.rank F E)
⊢ (Cardinal.prod fun x ↦ 2) ≤ Cardinal.prod fun i ↦ #(Cardinal.factor ↑i)

Tactic:
exact prod_le_prod _ _ Emb.Cardinal.two_le_deg

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hn : Odd n
r : R
hr : (X ^ n - C x).IsRoot r
⊢ r ^ n - x = 0

Tactic:
by simpa using hr

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

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
n : ℕ
hk : Odd (-↑n)
r : R
hr : x = r ^ n
⊢ x = r⁻¹ ^ (-↑n)

Tactic:
by simpa using hr

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic

Goal state before:
pp: X✝ Y✝ Z : Type u
inst✝¹⁴ : Group X✝
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : IsTopologicalGroup X✝
inst✝¹¹ : CompactSpace X✝
inst✝¹⁰ : TotallyDisconnectedSpace X✝
inst✝⁹ : Group Y✝
inst✝⁸ : TopologicalSpace Y✝
inst✝⁷ : IsTopologicalGroup Y✝
inst✝⁶ : CompactSpace Y✝
inst✝⁵ : TotallyDisconnectedSpace Y✝
inst✝⁴ : Group Z
inst✝³ : TopologicalSpace Z
inst✝² : IsTopologicalGroup Z
inst✝¹ : CompactSpace Z
inst✝ : TotallyDisconnectedSpace Z
X Y : ProfiniteGrp.{u_1}
f : X ⟶ Y
x✝ : IsIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
i : (forget₂ ProfiniteGrp.{u_1} Profinite).obj X ≅ (forget₂ ProfiniteGrp.{u_1} Profinite).obj Y :=
  asIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
⊢ IsIso f

Tactic:
let e : X ≃ₜ* Y :=
      { CompHausLike.homeoOfIso i with
          map_mul' := map_mul f.hom }

Goal state after:
X✝ Y✝ Z : Type u
inst✝¹⁴ : Group X✝
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : IsTopologicalGroup X✝
inst✝¹¹ : CompactSpace X✝
inst✝¹⁰ : TotallyDisconnectedSpace X✝
inst✝⁹ : Group Y✝
inst✝⁸ : TopologicalSpace Y✝
inst✝⁷ : IsTopologicalGroup Y✝
inst✝⁶ : CompactSpace Y✝
inst✝⁵ : TotallyDisconnectedSpace Y✝
inst✝⁴ : Group Z
inst✝³ : TopologicalSpace Z
inst✝² : IsTopologicalGroup Z
inst✝¹ : CompactSpace Z
inst✝ : TotallyDisconnectedSpace Z
X Y : ProfiniteGrp.{u_1}
f : X ⟶ Y
x✝ : IsIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
i : (forget₂ ProfiniteGrp.{u_1} Profinite).obj X ≅ (forget₂ ProfiniteGrp.{u_1} Profinite).obj Y :=
  asIso ((forget₂ ProfiniteGrp.{u_1} Profinite).map f)
e : ↑X.toProfinite.toTop ≃ₜ* ↑Y.toProfinite.toTop :=
  let __src := CompHausLike.homeoOfIso i;
  { toEquiv := __src.toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
⊢ IsIso f
Module: Mathlib.FieldTheory.IsRealClosed.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Field R
inst✝ : IsRealClosed R
x : R
hx : IsSquare x
n : ℕ
hk : -↑n ≠ 0
r : R
hr : x = r ^ n
⊢ x = r⁻¹ ^ (-↑n)

Tactic:
by simpa using hr

Goal state after:
Module: Mathlib.FieldTheory.Isaacs

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let K₀ := (⊥ : IntermediateField K K').restrictScalars F

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
alg : Algebra.IsAlgebraic F E
h : ∀ (x : E), ∃ y, (aeval y) (minpoly F x) = 0
S : Finset E
p : K[X] := ∏ x ∈ S, Polynomial.map (algebraMap F K) (minpoly F x)
K' : Type u_3 := p.SplittingField
splits : ∀ s ∈ S, (Polynomial.map (algebraMap F K') (minpoly F s)).Splits
K₀ : IntermediateField F K' := restrictScalars F ⊥
⊢ ↥(adjoin F ↑S) →ₐ[F] K
Module: Mathlib.FieldTheory.IsPerfectClosure

Goal state before:
pp: K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
h : (⇑(frobenius K p))^[(0, 0).1 + n] (0, x).2 = (⇑(frobenius K p))^[(0, x).1 + n] (0, 0).2
⊢ x ∈ pNilradical K p

Tactic:
simp_rw [zero_add, ← coe_iterateFrobenius, map_zero] at h

Goal state after:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
h : (iterateFrobenius K p n) x = 0
⊢ x ∈ pNilradical K p
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 : IntermediateField F E
L : Type w
inst✝¹⁰ : Field L
inst✝⁹ : Algebra F L
inst✝⁸ : Algebra L E
inst✝⁷ : IsScalarTower F L E
H : A.LinearDisjoint L
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : Algebra F K
inst✝⁴ : Algebra L K
inst✝³ : IsScalarTower F L K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : IsScalarTower L E K
⊢ (IntermediateField.map (IsScalarTower.toAlgHom F E K) A).LinearDisjoint L

Tactic:
by
  rw [linearDisjoint_iff] at H ⊢
  have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
  rw [← AlgHom.range_comp] at this
  convert! this
  ext; exact IsScalarTower.algebraMap_apply L E K _

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: F : Type u
E : Type v
inst✝²⁰ : Field F
inst✝¹⁹ : Field E
inst✝¹⁸ : Algebra F E
L : Type w
inst✝¹⁷ : Field L
inst✝¹⁶ : Algebra F L
inst✝¹⁵ : Algebra L E
inst✝¹⁴ : IsScalarTower F L E
L' : Type u_1
inst✝¹³ : Field L'
inst✝¹² : Algebra F L'
inst✝¹¹ : Algebra L' E
inst✝¹⁰ : IsScalarTower F L' E
H : (IsScalarTower.toAlgHom F L E).fieldRange.LinearDisjoint L'
K : Type u_2
inst✝⁹ : Field K
inst✝⁸ : Algebra F K
inst✝⁷ : Algebra L K
inst✝⁶ : IsScalarTower F L K
inst✝⁵ : Algebra L' K
inst✝⁴ : IsScalarTower F L' K
inst✝³ : Algebra E K
inst✝² : IsScalarTower F E K
inst✝¹ : IsScalarTower L E K
inst✝ : IsScalarTower L' E K
⊢ (IsScalarTower.toAlgHom F L K).fieldRange.LinearDisjoint L'

Tactic:
rw [linearDisjoint_iff] at H ⊢
  have := H.map (IsScalarTower.toAlgHom F E K) (RingHom.injective _)
  simp_rw [AlgHom.fieldRange_toSubalgebra, ← AlgHom.range_comp] at this
  rw [AlgHom.fieldRange_toSubalgebra]
  convert! this <;> (ext; exact IsScalarTower.algebraMap_apply _ E K _)

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
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⟮a⟯))⁻¹ • (trace F ↥E⟮a⟯) (AdjoinSimple.gen E a)

Tactic:
rw [h_finrank_eq, h_trace_eq, ← normalizedTrace_eq_of_finiteDimensional_apply F,
    ← normalizedTrace_intermediateField F K a']

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 K) ↑a'
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : (finrank R ↥A).Coprime 0
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : finrank R ↥B = 0
⊢ A.LinearDisjoint B

Tactic:
Nat.coprime_zero_right

Goal state after:
case pos
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
A B : Subalgebra R S
inst✝³ : Free R ↥A
inst✝² : Free R ↥B
inst✝¹ : Free ↥A ↥(Algebra.adjoin ↥A ↑B)
inst✝ : Free ↥B ↥(Algebra.adjoin ↥B ↑A)
H : finrank R ↥A = 1
a✝ : Nontrivial R
h1 : ¬finrank R ↥A = 0
h2 : finrank R ↥B = 0
⊢ A.LinearDisjoint B
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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) =
    Subalgebra.toSubmodule (adjoin F ((fun x ↦ x ^ q ^ n) '' Set.univ)).toSubalgebra

Tactic:
adjoin_toSubalgebra_of_isAlgebraic fun x _ ↦ Algebra.IsAlgebraic.isAlgebraic x,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) =
    Subalgebra.toSubmodule (Algebra.adjoin F ((fun x ↦ x ^ q ^ n) '' Set.univ))
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
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
this : Submonoid.closure ↑(MonoidHom.mrange (powMonoidHom (q ^ n))) = MonoidHom.mrange (powMonoidHom (q ^ n))
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) = Submodule.span F ↑(Submonoid.closure (Set.range fun x ↦ x ^ q ^ n))

Tactic:
simp only [MonoidHom.mrange, powMonoidHom, MonoidHom.coe_mk, OneHom.coe_mk,
    Submonoid.coe_copy] at this

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q n : ℕ
hF : ExpChar F q
ι : Type u_1
v : ι → E
inst✝ : Algebra.IsSeparable F E
h : Submodule.span F (Set.range v) = ⊤
this :
  Submonoid.closure (Set.range fun x ↦ x ^ q ^ n) =
    (Submonoid.map { toFun := fun x ↦ x ^ q ^ n, map_one' := ⋯, map_mul' := ⋯ } ⊤).copy (Set.range fun x ↦ x ^ q ^ n) ⋯
⊢ Submodule.span F (Set.range fun x ↦ v x ^ q ^ n) = Submodule.span F ↑(Submonoid.closure (Set.range fun x ↦ x ^ q ^ n))
Module: Mathlib.FieldTheory.PurelyInseparable.PerfectClosure

Goal state before:
pp: case hdeg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ (minpoly F a).natDegree ≤ (minpoly F ((iterateFrobenius E q n) a)).natDegree

Tactic:
← IntermediateField.adjoin.finrank hai,

Goal state after:
case hdeg
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
q : ℕ
hF : ExpChar F q
inst✝ : ExpChar E q
n : ℕ
a : E
hsep : IsSeparable F a
hai : IsIntegral F a
hapi : IsIntegral F ((iterateFrobenius E q n) a)
⊢ finrank F ↥F⟮a⟯ ≤ (minpoly F ((iterateFrobenius E q n) a)).natDegree
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : K⟮X⟯
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

Tactic:
by_cases hf : ∃ c, f = C c
  · obtain ⟨c, rfl⟩ := hf
    simp
  apply le_antisymm
  · have : (f.minpolyX K⟮f⟯).natDegree ≤ _ := natDegree_sub_le _ _
    rw [natDegree_map, natDegree_C_mul fun H ↦ hf ⟨0, by simpa [map_zero] using congr($(H).val)⟩,
      natDegree_map] at this
    exact this
  · exact max_le (natDegree_num_le_natDegree_minpolyX f hf) <| le_natDegree_of_ne_zero
      fun H ↦ hf (f.eq_C_of_minpolyX_coeff_eq_zero congr($(H).val))

Goal state after:
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 ((algebraMap K[X] K⟮X⟯) (Φ' E).content)⁻¹ *
      (Polynomial.C ((algebraMap K[X] K⟮X⟯) (b E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)) =
    Polynomial.map (algebraMap K[X] K⟮X⟯) (Φ E)

Tactic:
enter [1, 2]

Goal state after:
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : E ≠ ⊥
| Polynomial.C ((algebraMap K[X] K⟮X⟯) (b E)) * Polynomial.map (algebraMap (↥E) K⟮X⟯) (φ E)
Module: Mathlib.FieldTheory.RatFunc.Valuation

Goal state before:
pp: case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

Tactic:
by_cases hy : y = 0

Goal state after:
case pos
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree

case neg
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
hx : ¬x = 0
hy : ¬y = 0
⊢ (if x * y = 0 then 0 else exp (x * y).intDegree) =
    (if x = 0 then 0 else exp x.intDegree) * if y = 0 then 0 else exp y.intDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A : IntermediateField F E
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
rw [← relrank_mul_rank_top (show A ≤ ⊤ from le_top), IntermediateField.rank_top, mul_one]

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

Goal state before:
pp: X : Type u_1
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : FiniteDimensional ℝ X
u : Set X
⊢ TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), ContDiff ℝ ∞ p → IsOpen (p ⁻¹' u)

Tactic:
refine ⟨fun hu _ _ hp ↦ IsOpen.preimage (hp.continuous) hu, fun h ↦ ?_⟩
      rw [← toEuclidean.preimage_symm_preimage u]
      exact toEuclidean.continuous.isOpen_preimage _ (h _ toEuclidean.symm.contDiff)

Goal state after: