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

Goal state before:
pp: case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
⊢ (mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) (∀' f✝)).Realize v xs ↔
    (∀' f✝).Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')

Tactic:
simp only [mapTermRel, Realize, realize_castLE_of_eq h, ih3 (hmn.trans k.le_succ)]

Goal state after:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n' m : ℕ
v : α → M
k : ℕ
f✝ : L.BoundedFormula α (k + 1)
ih3 :
  ∀ {xs : Fin (k + 1 + n') → M},
    m ≤ k + 1 →
      ((mapTermRel (fun x t ↦ Term.liftAt n' m t) (fun x ↦ id) (fun x ↦ castLE ⋯) f✝).Realize v xs ↔
        f✝.Realize v (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n'))
xs : Fin (k + n') → M
hmn : m ≤ k
h : k + 1 + n' = k + n' + 1
⊢ (∀ (x : M), f✝.Realize v ((snoc xs x ∘ Fin.cast h) ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n')) ↔
    ∀ (x : M), f✝.Realize v (snoc (xs ∘ fun i ↦ if ↑i < m then castAdd n' i else i.addNat n') x)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
⊢ (do
        let a ← (listDecode t.listEncode).head?
        pure (some a)).join =
    some t

Tactic:
by
    have h := listDecode_encode_list [t]
    rw [flatMap_singleton] at h
    simp only [Option.join, h, head?_cons, Option.pure_def, Option.bind_eq_bind, Option.bind_some,
      id_eq]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case var
L : Language
M : Type w
inst✝ : L.Structure M
S : L.Substructure M
α : Type u_3
xs : α → M
h : ∀ (a : α), xs a ∈ S
a : α
⊢ realize xs (var a) ∈ S

Tactic:
| var a =>

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
v : α → M
R : L.Relations 2
t₁ t₂ : L.Term α
⊢ (R.formula₂ t₁ t₂).Realize v ↔ RelMap R ![Term.realize v t₁, Term.realize v t₂]

Tactic:
by
  rw [Relations.formula₂, realize_rel, iff_eq_eq]
  refine congr rfl (funext (Fin.cases ?_ ?_))
  · simp only [Matrix.cons_val_zero]
  · simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔
    f✝.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a) ∘ Sum.inl)
      (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a) ∘ Sum.inr)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

Tactic:
simp only [Sum.elim_comp_inl, Sum.elim_comp_inr] at h

Goal state after:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ (relabel (Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm)) f✝.toFormula).Realize v
      (snoc default a) ↔
    f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)

Tactic:
rw [← h, realize_relabel, Formula.Realize, iff_iff_eq]

Goal state after:
case all
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n n✝ : ℕ
f✝ : L.BoundedFormula α (n✝ + 1)
ih3 : ∀ (v : α ⊕ Fin (n✝ + 1) → M), f✝.toFormula.Realize v ↔ f✝.Realize (v ∘ Sum.inl) (v ∘ Sum.inr)
v : α ⊕ Fin n✝ → M
a : M
h :
  f✝.toFormula.Realize (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) ↔ f✝.Realize (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)
⊢ Realize f✝.toFormula
      (Sum.elim v (snoc default a ∘ castAdd 0) ∘
        Sum.elim (Sum.inl ∘ Sum.inl) (Sum.map Sum.inr id ∘ ⇑finSumFinEquiv.symm))
      (snoc default a ∘ natAdd 1) =
    Realize f✝.toFormula (Sum.elim (v ∘ Sum.inl) (snoc (v ∘ Sum.inr) a)) default
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ x✝ ∈ {v | φ.Realize (Sum.elim Subtype.val v)} ↔
    x✝ ∈
      {v |
        Formula.Realize
          (BoundedFormula.restrictFreeVar φ fun x ↦
            Sum.casesOn (motive := fun x ↦ x ∈ BoundedFormula.freeVarFinset φ → ↑↑A0 ⊕ α) (↑x)
              (fun x hx ↦ Sum.inl ⟨↑x, ⋯⟩) (fun x x_1 ↦ Sum.inr x) ⋯)
          (Sum.elim Subtype.val v)}

Tactic:
simp only [Formula.Realize, mem_ofPred_eq, Finset.coe_sort_coe]

Goal state after:
case mp
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
φ : L.Formula (↑A ⊕ α)
A0 : Finset M := Finset.image Subtype.val (BoundedFormula.freeVarFinset φ).toLeft
x✝ : α → M
⊢ BoundedFormula.Realize φ (Sum.elim Subtype.val x✝) default ↔
    (BoundedFormula.restrictFreeVar φ fun x ↦
          Sum.rec (motive := fun x ↦ x ∈ BoundedFormula.freeVarFinset φ → ↥A0 ⊕ α) (fun val hx ↦ Sum.inl ⟨↑val, ⋯⟩)
            (fun val x ↦ Sum.inr val) ↑x ⋯).Realize
      (Sum.elim Subtype.val x✝) default
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]), p.Monic → Irreducible p → ∃ x, eval x p = 0

Tactic:
intro p

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h : K ⊨ Theory.ACF p✝
p : K[X]
⊢ p.Monic → Irreducible p → ∃ x, eval x p = 0
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)
⊢ I.radical ≤ vanishingIdeal k (zeroLocus K I)

Tactic:
intro p

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
⊢ p ∈ I.radical → p ∈ vanishingIdeal k (zeroLocus K I)
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), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ

Tactic:
intro p

Goal state after:
φ : 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
⊢ ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ
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 ↑φ ⋯)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ
⊢ (↑s)ᶜ ⊆ fun p ↦ ∀ (M : (Theory.ACF ↑p).ModelType) (v : Empty → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs

Tactic:
intro p

Goal state after:
φ : 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 ↑φ ⋯)
hs : ∀ (p : Nat.Primes), ∀ ψ ∈ T0, p ∉ s → Theory.ACF ↑p ⊨ᵇ ψ
p : Nat.Primes
⊢ p ∈ (↑s)ᶜ →
    p ∈ fun p ↦ ∀ (M : (Theory.ACF ↑p).ModelType) (v : Empty → ↑M) (xs : Fin 0 → ↑M), BoundedFormula.Realize φ v xs
Module: Mathlib.FieldTheory.Differential.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0
⊢ logDeriv a = 0

Tactic:
unfold logDeriv at *

Goal state after:
R : Type u_1
inst✝¹ : Field R
inst✝ : Differential R
a : R
h : a′ = 0
⊢ a′ / a = 0
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 : WithTop (Module.rank F E).ord.ToType
hi : IsSuccPrelimit i
f : ↑(limit (embFunctor F E) i)
j : ↑(Iio i)
this : Nonempty ↑(Iio i)
⊢ embFunctor F E ⋯ (Subalgebra.iSupLift (fun x ↦ (filtration ↑x).toSubalgebra) ⋯ ↑f ⋯ (filtration i).toSubalgebra ⋯) =
    ↑f j

Tactic:
apply Subalgebra.iSupLift_comp_inclusion

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
a : PerfectClosure K p
⊢ 0 * a = 0

Tactic:
refine Quot.inductionOn a fun ⟨m, x⟩ => ?_
      rw [zero_def, quot_mk_eq_mk, mk_mul_mk]
      simp only [zero_add, iterate_zero, id_eq, iterate_map_zero, zero_mul, mk_zero_right]

Goal state after:
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + (z2 + (y.1 + z1))] x.2 = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2

Tactic:
rw [← add_assoc, iterate_add_apply, ih1]

Goal state after:
case mp.trans
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x✝ y✝ x y z : ℕ × K
H1 : Relation.EqvGen (R K p) x y
H2 : Relation.EqvGen (R K p) y z
z1 : ℕ
ih1 : (⇑(frobenius K p))^[y.1 + z1] x.2 = (⇑(frobenius K p))^[x.1 + z1] y.2
z2 : ℕ
ih2 : (⇑(frobenius K p))^[z.1 + z2] y.2 = (⇑(frobenius K p))^[y.1 + z2] z.2
⊢ (⇑(frobenius K p))^[z.1 + z2] ((⇑(frobenius K p))^[x.1 + z1] y.2) = (⇑(frobenius K p))^[x.1 + (z2 + (y.1 + z1))] z.2
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
⊢ Bijective fun x ↦ x ^ p

Tactic:
simp_rw [← frobenius_def]
    let f : PerfectClosure K p → PerfectClosure K p := fun e ↦
      liftOn e (fun x => mk K p (x.1 + 1, x.2)) fun x y H =>
      match x, y, H with
      | _, _, R.intro n x => Quot.sound (R.intro _ _)
    refine bijective_iff_has_inverse.mpr ⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_,
      fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_⟩ <;>
      simp only [f, liftOn_mk, frobenius_mk, mk_succ_pow]

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 : K
n : ℕ
ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p ((n + 1, x).1, (n + 1, x).2 ^ p)) =
    (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x))

Tactic:
mk_succ_pow

Goal state after:
case succ
K : Type u
inst✝² : CommRing K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP K p
x : K
n : ℕ
ih : (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)) = (of K p) x
⊢ (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, (n + 1, x).2)) =
    (⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x))
Module: Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality

Goal state before:
pp: F : Type u
E : Type v
inst✝⁵ : CommRing F
inst✝⁴ : Nontrivial F
inst✝³ : CommRing E
inst✝² : IsDomain E
inst✝¹ : Algebra F E
ι : Type w
x : ι → E
inst✝ : Nonempty ι
hx : IsTranscendenceBasis F x
K : Subalgebra F E := adjoin F (range x)
this✝ : Algebra.IsAlgebraic (↥K) E
this : Infinite ↥K
⊢ #E ≤ #↥K

Tactic:
simpa only [sup_eq_left.2 (aleph0_le_mk K)] using Algebra.IsAlgebraic.cardinalMk_le_max K E

Goal state after:
Module: Mathlib.FieldTheory.JacobsonNoether

Goal state before:
pp: D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
⊢ False

Tactic:
have c_eq : a * (ad k D a)^[n - 1] b - (ad k D a)^[n - 1] b * a = c := by
    rw [hc_def, ← Nat.sub_add_cancel hn, Function.iterate_succ_apply' (ad k D a) _ b]; rfl

Goal state after:
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Algebra.IsAlgebraic (↥k) D
H : k ≠ ⊤
p : ℕ
hp : ExpChar D p
insep : ∀ (x : D), IsSeparable (↥k) x → x ∈ k
a : D
ha : a ∉ k
ha₀ : a ≠ 0
b : D
hb1 : ((ad (↥k) D) a) b ≠ 0
n : ℕ
hn : 0 < n
c : D := (⇑((ad (↥k) D) a))^[n] b
hb : c ≠ 0 ∧ (⇑((ad (↥k) D) a))^[n + 1] b = 0
hc_def : c = (⇑((ad (↥k) D) a))^[n] b
x✝ : Invertible c := { invOf := c⁻¹, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
hc : a * c = c * a
d : D := c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hd_def : d = c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b
hc' : c⁻¹ * a = a * c⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
⊢ False
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case pos
K : Type u
inst✝¹ : Field K
a : K
h : a = 0
hζ : (primitiveRoots 1 K).Nonempty
H : Irreducible (X ^ 1 - C a)
inst✝ : NeZero 1
__spread✝⁻⁰ : ↥(rootsOfUnity 1 K) →* Gal(K[1√a]/K) := autAdjoinRootXPowSubC 1 a
η : ↥(rootsOfUnity 1 K)
this✝² : Fact (Irreducible (X ^ 1 - C a))
this✝¹ : IsDomain K[1√a]
this✝ : Algebra K K[1√a] := inferInstance
this : ↑η = 1
⊢ 1 = (of (X ^ 1 - C a)) ↑↑η

Tactic:
simp only [this, Units.val_one, map_one]

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
A : Subalgebra R S
⊢ A.LinearDisjoint ⊥

Tactic:
rw [Subalgebra.LinearDisjoint, Algebra.toSubmodule_bot]
  exact Submodule.LinearDisjoint.one_right _

Goal state after:
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ restrictScalars R (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val).range = ⊤

Tactic:
← H'

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
A B : Subalgebra R S
H : A.LinearDisjoint B
H' : A ⊔ B = ⊤
⊢ restrictScalars R (Algebra.TensorProduct.productLeftAlgHom (Algebra.ofId (↥A) S) B.val).range = A ⊔ B
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsAlgebraic K L
x : L
c : ConjRootClass K L
⊢ (aeval x) c.minpoly = 0 ↔ mk K x = c

Tactic:
induction c
  simpa [← isConjRoot_iff_aeval_eq_zero (Algebra.IsIntegral.isIntegral _)] using comm

Goal state after:
Module: Mathlib.FieldTheory.Minpoly.ConjRootClass

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ (map (algebraMap K L) c.minpoly).roots.card = (map (algebraMap K L) c.minpoly).natDegree

Tactic:
rw [← splits_iff_card_roots]

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : Normal K L
c : ConjRootClass K L
inst✝ : Fintype ↑c.carrier
⊢ (map (algebraMap K L) c.minpoly).Splits
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥) x' = x
⊢ (toSubmodule A).lTensorOne ((x * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne (x ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)

Tactic:
obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
x y : ↥⊥
a b : ↥A
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R S) y' = ↑y
⊢ (toSubmodule A).lTensorOne ((x * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne (x ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)
Module: Mathlib.LinearAlgebra.TensorProduct.Subalgebra

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (x * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] x) * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)

Tactic:
obtain ⟨y', hy⟩ := Algebra.mem_bot.1 y.2

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Semiring T
inst✝ : Algebra R T
A : Subalgebra R S
a b : ↥A
x y : ↥⊥
x' : R
hx : (algebraMap R ↥⊥) x' = x
y' : R
hy : (algebraMap R S) y' = ↑y
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] (x * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] x) * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)
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 : IsField (↥A ⊗[F] L)
this : SMulCommClass F ↥A ↥A
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)

Tactic:
have : SMulCommClass F A.toSubalgebra A.toSubalgebra := ‹SMulCommClass F A A›

Goal state after:
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 : IsField (↥A ⊗[F] L)
this✝ : SMulCommClass F ↥A ↥A
this : SMulCommClass F ↥A.toSubalgebra ↥A.toSubalgebra
⊢ IsField (↥A.toSubalgebra ⊗[F] ↥(IsScalarTower.toAlgHom F L E).range)
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 = ⊥
⊢ PerfectField F

Tactic:
let p := ringExpChar F

Goal state after:
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
⊢ PerfectField F
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
⊢ (↥E)⟮ X⟯ = ⊤

Tactic:
by
  rw [← restrictScalars_eq_top_iff (K := K), IntermediateField.restrictScalars_adjoin,
    _root_.eq_top_iff]
  exact le_trans (le_of_eq RatFunc.adjoin_X.symm) (adjoin.mono _ _ _ (by simp))

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

Goal state before:
pp: case neg.a
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
this : (f.minpolyX ↥K⟮f⟯).natDegree ≤ max f.num.natDegree f.denom.natDegree
⊢ (f.minpolyX ↥K⟮f⟯).natDegree ≤ max f.num.natDegree f.denom.natDegree

Tactic:
exact this

Goal state after:
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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝² : Algebra ↥M ↥L := i.toAlgebra
this✝¹ : SMul ↥M ↥L := this✝².toSMul
this✝ : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
this : extendScalars hi = adjoin ↥M ↑E'
x : K
y : E
hy : (IsScalarTower.toAlgHom F E K).toRingHom y = x
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap (↥M) K).range

Tactic:
obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y

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
S : Set K
inst✝¹ : IsPurelyInseparable F E
M : IntermediateField F K := adjoin F S
inst✝ : Algebra.IsAlgebraic F ↥M
L : IntermediateField E K := adjoin E S
E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange
j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)
hi : M ≤ restrictScalars F L
i : ↥M →+* ↥L := Subsemiring.inclusion hi
this✝² : Algebra ↥M ↥L := i.toAlgebra
this✝¹ : SMul ↥M ↥L := this✝².toSMul
this✝ : IsScalarTower F ↥M ↥L
q : ℕ
h✝ : ExpChar F q
this : extendScalars hi = adjoin ↥M ↑E'
x : K
y : E
hy : (IsScalarTower.toAlgHom F E K).toRingHom y = x
n : ℕ
z : F
hz : (algebraMap F E) z = y ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap (↥M) K).range
Module: Mathlib.FieldTheory.RatFunc.IntermediateField

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ Module.finrank (↥K⟮f⟯) K⟮X⟯ = max f.num.natDegree f.denom.natDegree

Tactic:
← (IntermediateField.adjoinXEquiv K⟮f⟯).toLinearEquiv.finrank_eq,

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : K⟮X⟯
hf : ¬∃ c, f = C c
⊢ Module.finrank ↥K⟮f⟯ ↥(↥K⟮f⟯)⟮ X⟯ = max f.num.natDegree f.denom.natDegree
Module: Mathlib.FieldTheory.Relrank

Goal state before:
pp: E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : E →+* L
⊢ Subring.map f (A ⊓ B).toSubring = (map f A ⊓ map f B).toSubring

Tactic:
by rw [← map_inf]; rfl

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

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
⊢ inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y)

Tactic:
unfold inftyValuationDef

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F⟮X⟯
x y : F⟮X⟯
⊢ (if x + y = 0 then 0 else exp (x + y).intDegree) ≤
    max (if x = 0 then 0 else exp x.intDegree) (if y = 0 then 0 else exp y.intDegree)