mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.AxGrothendieck

Goal state before:
pp: K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
hS : ∃ φ, S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S

Tactic:
rcases hS with ⟨φ, hφ⟩

Goal state after:
K : Type u_1
ι : Type u_2
inst✝³ : Field K
inst✝² : IsAlgClosed K
inst✝¹ : Finite ι
inst✝ : CompatibleRing K
c✝ : Set K
S : Set (ι → K)
ps : ι → MvPolynomial ι K
this : Fintype ι := Fintype.ofFinite ι
p : ℕ := ringChar K
c : Finset K
left✝ : ↑c ⊆ c✝
φ : ring.Formula (↑↑c ⊕ ι)
hφ : S = {v | φ.Realize (Sum.elim Subtype.val v)}
⊢ Set.MapsTo (fun v i ↦ (eval v) (ps i)) S S →
    Set.InjOn (fun v i ↦ (eval v) (ps i)) S → Set.SurjOn (fun v i ↦ (eval v) (ps i)) S S
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:
by
  cases nonempty_fintype σ
  rw [FiniteDimensional, ← IsNoetherian.iff_fg, IsNoetherian.iff_rank_lt_aleph0]
  simpa only [rank_R] using Cardinal.natCast_lt_aleph0

Goal state after:
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
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← compl_ofPred, nonempty_compl]

Goal state after:
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
ih : (y : (Module.rank F E).ord.ToType) → y < i → (Module.rank F E).ord.ToType
s : Set E := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.FieldTheory.Differential.Liouville

Goal state before:
pp: case refine_2
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)

Tactic:
trans ∑ _ : (K ≃ₐ[F] K), a

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ (algebraMap F K) a * ↑(Fintype.card Gal(K/F)) = ∑ x, ↑a

F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Differential F
inst✝⁶ : Differential K
inst✝⁵ : Algebra F K
inst✝⁴ : DifferentialAlgebra F K
inst✝³ : CharZero F
inst✝² : FiniteDimensional F K
inst✝¹ : IsGalois F K
a : F
ι : Type
inst✝ : Fintype ι
c : ι → F
hc : ∀ (x : ι), (c x)′ = 0
u : ι → K
v : K
h : ↑a = ∑ x, ↑(c x) * logDeriv (u x) + v′
this : CharZero K
ffb : fixedField ⊤ = ⊥
⊢ ∑ x, ↑a = ∑ x, (∑ x_1, ↑(c x_1) * logDeriv (x (u x_1)) + (x v)′)
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
f : ↥(adjoin F (⇑b ∘ φ '' Iio (i⁺))) →ₐ[F] Ē
⊢ ((succEquiv i) f).1 = f.comp (Subalgebra.inclusion ⋯)

Tactic:
ext
  rfl

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
e : PerfectClosure K p
x✝ : ℕ × K
n : ℕ
x : K
⊢ -Quot.mk (R K p) (n, x) + Quot.mk (R K p) (n, x) = 0

Tactic:
simp only [quot_mk_eq_mk, neg_mk, mk_add_mk, iterate_map_neg, neg_add_cancel, mk_zero_right]

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
K₀ : IntermediateField F K' := restrictScalars F ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
⊢ ↥(adjoin F ↑S) →ₐ[F] K

Tactic:
let M (ω : Ω) := Subalgebra.toSubmodule (K₀.comap ω).toSubalgebra

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 ⊥
FS : IntermediateField F E := adjoin F ↑S
Ω : Type (max u_2 u_3) := ↥FS →ₐ[F] K'
this : FiniteDimensional F ↥(adjoin F ↑S)
M : Ω → Submodule F ↥FS := fun ω ↦ Subalgebra.toSubmodule (comap ω K₀).toSubalgebra
⊢ ↥(adjoin F ↑S) →ₐ[F] K
Module: Mathlib.FieldTheory.PerfectClosure

Goal state before:
pp: case mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (⇑(frobenius L p))^[n] ((⇑(frobeniusEquiv L p).symm)^[n] (f ((of K p) x))) =
    (⇑(frobenius L p))^[n] (f (mk K p (n, x)))

Tactic:
← f.map_iterate_frobenius,

Goal state after:
case mk
K : Type u
inst✝⁵ : CommRing K
p : ℕ
inst✝⁴ : Fact (Nat.Prime p)
inst✝³ : CharP K p
L : Type v
inst✝² : CommSemiring L
inst✝¹ : CharP L p
inst✝ : PerfectRing L p
f : PerfectClosure K p →+* L
x✝ : PerfectClosure K p
n : ℕ
x : K
⊢ (⇑(frobenius L p))^[n] ((⇑(frobeniusEquiv L p).symm)^[n] (f ((of K p) x))) =
    f ((⇑(frobenius (PerfectClosure K p) p))^[n] (mk K p (n, x)))
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
⊢ Irreducible (X ^ (n * m) - C a)

Tactic:
have hm' : m ≠ 0 := by
    rintro rfl
    rw [pow_zero, ← C.map_one, ← map_sub] at hm
    exact not_irreducible_C _ hm

Goal state after:
K : Type u
inst✝ : Field K
n m : ℕ
a : K
hm : Irreducible (X ^ m - C a)
hn :
  ∀ (E : Type u) [inst : Field E] [inst_1 : Algebra K E] (x : E),
    minpoly K x = X ^ m - C a → Irreducible (X ^ n - C (AdjoinSimple.gen K x))
hm' : m ≠ 0
⊢ Irreducible (X ^ (n * m) - C a)
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
⊢ Nat.Prime q → q ∣ n → ∀ (b : ↥K⟮x⟯), b ^ q ≠ AdjoinSimple.gen K x

Tactic:
hq

Goal state after:
case prime_mul
p n : ℕ
hp : Nat.Prime p
IH :
  ∀ {K : Type u} [inst : Field K],
    Odd n → ∀ {a : K}, (∀ (p : ℕ), Nat.Prime p → p ∣ n → ∀ (b : K), b ^ p ≠ a) → Irreducible (X ^ n - C a)
K : Type u
inst✝² : Field K
hn : Odd (p * n)
a : K
ha : ∀ (p_1 : ℕ), Nat.Prime p_1 → p_1 ∣ p * n → ∀ (b : K), b ^ p_1 ≠ a
E : Type u
inst✝¹ : Field E
inst✝ : Algebra K E
x : E
hx : minpoly K x = X ^ p - C a
this : IsIntegral K x
q : ℕ
hq : Nat.Prime q
⊢ q ∣ n → ∀ (b : ↥K⟮x⟯), b ^ q ≠ AdjoinSimple.gen K x
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
⊢ Nat.Prime q → q ∣ p ^ n → ∀ (b : K), b ^ q ≠ a

Tactic:
hq

Goal state after:
K : Type u
inst✝ : Field K
p : ℕ
hp : Nat.Prime p
hp' : p ≠ 2
n : ℕ
a : K
ha : ∀ (b : K), b ^ p ≠ a
q : ℕ
hq : Nat.Prime q
⊢ q ∣ p ^ n → ∀ (b : K), b ^ q ≠ a
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⁻¹
c_eq : a * (⇑((ad (↥k) D) a))^[n - 1] b - (⇑((ad (↥k) D) a))^[n - 1] b * a = c
eq1 : c⁻¹ * a * (⇑((ad (↥k) D) a))^[n - 1] b - c⁻¹ * (⇑((ad (↥k) D) a))^[n - 1] b * a = 1
⊢ a * d - d * a = a * 1

Tactic:
rw [hd_def, ← eq1, mul_sub, mul_assoc _ _ a, sub_right_inj, hc',
      ← mul_assoc, ← mul_assoc, ← mul_assoc]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝¹ : Field K
n : ℕ
hζ : (primitiveRoots n K).Nonempty
a : K
H : Irreducible (X ^ n - C a)
inst✝ : NeZero n
⊢ Function.RightInverse (AdjoinRootXPowSubCEquivToRootsOfUnity hζ H) (↑(autAdjoinRootXPowSubC n a)).toFun

Tactic:
intro e
    have := Fact.mk H
    let : Algebra K K[n√a] := inferInstance
    apply AlgEquiv.coe_toAlgHom_injective
    apply AdjoinRoot.algHom_ext
    simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
      MonoidHom.toOneHom_coe, AlgEquiv.coe_toAlgHom, autAdjoinRootXPowSubC_root, Algebra.smul_def]
    rw [rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.val_mkOfPowEq_coe]
    split_ifs with h
    · obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
      rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul,
        ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
    · refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
H : Irreducible (X ^ n - C a)
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
α : L
hα : α ^ n = (algebraMap K L) a
inst✝ : NeZero n
ζ : K
hζ : IsPrimitiveRoot ζ n
m : ℤ
⊢ ((autEquivZmod H L hζ).symm (Multiplicative.ofAdd ↑m)) α = ζ ^ m • α

Tactic:
by
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  rw [← autEquivRootsOfUnity_smul ⟨ζ, (mem_primitiveRoots hn).mpr hζ⟩ H L hα]
  simp [MulEquiv.subgroupCongr_symm_apply, Subgroup.smul_def, Units.smul_def, autEquivZmod]

Goal state after:
Module: Mathlib.FieldTheory.KummerExtension

Goal state before:
pp: case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
⊢ q.Monic → (aeval α) q = 0 → (X ^ finrank K L - C a).degree ≤ q.degree

Tactic:
hq

Goal state after:
case refine_2
K : Type u
inst✝³ : Field K
L : Type u_1
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
a : K
α : L
ha : α ^ finrank K L = (algebraMap K L) a
hα : K⟮α⟯ = ⊤
q : K [X]
hq : q.Monic
⊢ (aeval α) q = 0 → (X ^ finrank K L - C a).degree ≤ q.degree
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e'_6
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 (IsScalarTower.toAlgHom F L' E).range
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
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
⊢ IsScalarTower.toAlgHom F L K = (IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)

Tactic:
ext; exact IsScalarTower.algebraMap_apply _ E K _

Goal state after:
Module: Mathlib.FieldTheory.LinearDisjoint

Goal state before:
pp: case e'_7
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 (IsScalarTower.toAlgHom F L' E).range
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
this :
  ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L E)).range.LinearDisjoint
    ((IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)).range
⊢ IsScalarTower.toAlgHom F L' K = (IsScalarTower.toAlgHom F E K).comp (IsScalarTower.toAlgHom F L' E)

Tactic:
ext; exact IsScalarTower.algebraMap_apply _ E K _

Goal state after:
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
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).lTensorOne (((algebraMap R ↥⊥) x' * y) ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) x' ⊗ₜ[R] a) * (toSubmodule A).lTensorOne (y ⊗ₜ[R] b)

Tactic:
← hy,

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 ↥⊥) y' = y
⊢ (toSubmodule A).lTensorOne (((algebraMap R ↥⊥) x' * (algebraMap R ↥⊥) y') ⊗ₜ[R] (a * b)) =
    (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) x' ⊗ₜ[R] a) *
      (toSubmodule A).lTensorOne ((algebraMap R ↥⊥) 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
y' : R
hy : (algebraMap R ↥⊥) y' = y
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] ((algebraMap R ↥⊥) x' * y)) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] (algebraMap R ↥⊥) x') * (toSubmodule A).rTensorOne (b ⊗ₜ[R] y)

Tactic:
← hy,

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 ↥⊥) y' = y
⊢ (toSubmodule A).rTensorOne ((a * b) ⊗ₜ[R] ((algebraMap R ↥⊥) x' * (algebraMap R ↥⊥) y')) =
    (toSubmodule A).rTensorOne (a ⊗ₜ[R] (algebraMap R ↥⊥) x') *
      (toSubmodule A).rTensorOne (b ⊗ₜ[R] (algebraMap R ↥⊥) y')
Module: Mathlib.RingTheory.LinearDisjoint

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ f (1 ⊗ₜ[R] b) = f (a ⊗ₜ[R] 1)

Tactic:
f,

Goal state after:
R : Type u
inst✝⁸ : CommRing R
A : Type v
inst✝⁷ : CommRing A
B : Type w
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Flat R A
inst✝² : Flat R B
inst✝¹ : Algebra.Transcendental R A
inst✝ : Algebra.Transcendental R B
H : IsField (A ⊗[R] B)
this✝⁴ : Field (A ⊗[R] B) := H.toField
a : A
b : B
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
fa : A →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeLeft
fb : B →ₐ[R] A ⊗[R] B := Algebra.TensorProduct.includeRight
hfa : Function.Injective ⇑fa
hfb : Function.Injective ⇑fb
this✝³ : IsDomain A
this✝² : IsDomain B
this✝¹ : IsDomain R
this✝ : Flat R ↥(toSubmodule fa.range)
key1 : Module.rank R ↥(fa.range ⊓ fb.range) ≤ 1
ga : R[X] →ₐ[R] A := aeval a
gb : R[X] →ₐ[R] B := aeval b
gab : R[X] →ₐ[R] A ⊗[R] B := fa.comp ga
hta : Function.Injective ⇑ga
htb : Function.Injective ⇑gb
htab : Function.Injective ⇑gab
algInst✝¹ : Algebra R[X] A := ga.toAlgebra
algInst✝ : Algebra R[X] B := gb.toAlgebra
f : A ⊗[R] B →ₐ[R] A ⊗[R[X]] B := Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B
this : Nontrivial (A ⊗[R[X]] B)
hf : Function.Injective ⇑f
⊢ (Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B) (1 ⊗ₜ[R] b) =
    (Algebra.TensorProduct.mapOfCompatibleSMul R[X] R R A B) (a ⊗ₜ[R] 1)
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
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
L1 L2 : IntermediateField F E
h1 : L1 ≤ perfectClosure F E
h2 : L2 ≤ perfectClosure F E
⊢ L1 ⊔ L2 ≤ perfectClosure F E

Tactic:
exact sup_le h1 h2

Goal state after:
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
hsep : ∀ (i : ι), IsSeparable F (v i)
h : LinearIndependent F v
E' : IntermediateField F E := adjoin F (Set.range v)
⊢ ∀ x ∈ Set.range v, IsSeparable F x

Tactic:
by
    rintro _ ⟨y, rfl⟩; exact hsep y

Goal state after:
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
  have := expChar_of_injective_algebraMap (algebraMap F E).injective p
  have := PerfectRing.ofSurjective F p fun x ↦ by
    obtain ⟨y, h⟩ := surjective_frobenius E p (algebraMap F E x)
    have : y ∈ perfectClosure F E := ⟨1, x, by rw [← h, pow_one, frobenius_def, ringExpChar.eq F p]⟩
    obtain ⟨z, rfl⟩ := eq ▸ this
    simp only [Algebra.ofId] at h
    exact ⟨z, (algebraMap F E).injective (by rw [RingHom.map_frobenius]; rw [h])⟩
  exact PerfectRing.toPerfectField F p

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

Goal state before:
pp: K : Type u
inst✝ : Field K
x y : K⟮X⟯
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ (x + y).intDegree ≤ max x.intDegree y.intDegree

Tactic:
by_cases hx : x = 0
  · simp [hx]
  rw [intDegree_add hxy, ←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hx y.denom_ne_zero,
    mul_comm y.denom, ←
    natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree hy x.denom_ne_zero,
    le_max_iff, sub_le_sub_iff_right, Int.ofNat_le, sub_le_sub_iff_right, Int.ofNat_le, ←
    le_max_iff, mul_comm y.num]
  exact natDegree_add_le _ _

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 : ℕ
z : F
hz : (algebraMap F E) z = y ^ q ^ n
⊢ (algebraMap E K) (y ^ q ^ n) = x ^ q ^ n

Tactic:
← hy,

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
⊢ (algebraMap E K) (y ^ q ^ n) = (IsScalarTower.toAlgHom F E K).toRingHom y ^ q ^ n
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
⊢ (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree

Tactic:
natDegree_minpolyX

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

Goal state before:
pp: case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ (φ E).natDegree = m E

Tactic:
rw [← Φ_natDegree_eq_φ_natDegree h, Φ_natDegree_eq_θ_natDegree h]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
E : IntermediateField K K⟮X⟯
h : ¬E = ⊥
⊢ (θ E).natDegree = m E