mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
x : ι → A
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
S : Type u_3
B : Type u_4
FRS : Type u_5
FAB : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : CommRing B
inst✝⁴ : Algebra S B
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
H : AlgebraicIndependent R x
hf : Surjective ⇑f
hg : Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
⊢ AlgebraicIndependent S (⇑g ∘ x)

Tactic:
rw [algebraicIndependent_iff] at H ⊢
  intro p hp
  obtain ⟨q, rfl⟩ := map_surjective (f : R →+* S) hf p
  rw [H q (hg (by rwa [map_zero, ← RingHom.coe_coe g, map_aeval, ← h, ← eval₂Hom_map_hom,
    ← aeval_eq_eval₂Hom])), map_zero]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
hF : ExpChar F q
g : F[X]
hg : IsSeparableContraction q f g
⊢ g.natDegree = hf.degree

Tactic:
cases hF

Goal state after:
case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
hg : IsSeparableContraction 1 f g
⊢ g.natDegree = hf.degree

case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hg : IsSeparableContraction q f g
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
⊢ g.natDegree = hf.degree
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : g.Separable
m : ℕ
hm : (expand F (1 ^ m)) g = f
⊢ g.natDegree = hf.degree

Tactic:
rw [one_pow, expand_one] at hm

Goal state after:
case zero
F : Type u_1
inst✝¹ : Field F
f g : F[X]
inst✝ : CharZero F
hf : HasSeparableContraction 1 f
left✝ : g.Separable
m : ℕ
hm : g = f
⊢ g.natDegree = hf.degree
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : NoZeroDivisors S
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsIntegral R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
simp_rw [IsTranscendenceBasis, IsIntegral.algebraicIndependent_iff R S]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : NoZeroDivisors S
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsAlgebraic R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
simp_rw [IsTranscendenceBasis, IsAlgebraic.algebraicIndependent_iff R S]

Goal state after:
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A),
    ((matroid R A).Indep B ∧ B ⊆ insert x B ∧ ∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔
      x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)

Tactic:
hB.1.1.1,

Goal state after:
R : Type u_1
A : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FaithfulSMul R A
inst✝ : IsDomain A
s B : Set A
hB : (matroid R A).IsBasis B s
⊢ ∀ (x : A),
    (True ∧ B ⊆ insert x B ∧ ∀ a ∈ insert x B, IsAlgebraic (↥(adjoin R B)) a) ↔
      x ∈ ↑(algebraicClosure (↥(adjoin R s)) A)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
alg : Algebra.IsAlgebraic (↥(adjoin R s)) A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
⊢ trdeg R A ≤ #↑s

Tactic:
rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *

Goal state after:
case pos
R : Type u_1
A : Type w
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
s : Set A
inst✝ : NoZeroDivisors A
h : Injective ⇑(algebraMap R A)
this✝ : IsDomain A
this : FaithfulSMul R A
alg : (matroid R A).Spanning s
⊢ (matroid R A).cRank ≤ #↑s
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
le : lift.{w, u} #ι ≤ lift.{u, w} (trdeg R A)
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this✝ : Bijective (rangeFactorization x)
this : IsDomain A
⊢ IsTranscendenceBasis R Subtype.val

Tactic:
rw [← matroid_spanning_iff, ← matroid_cRank_eq] at *

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : NoZeroDivisors A
inst✝¹ : FaithfulSMul R A
inst✝ : Finite ι
le : lift.{w, u} #ι ≤ lift.{u, w} (matroid R A).cRank
toFun✝ : ι → ↑(range x)
h : Injective toFun✝
this✝ : Bijective (rangeFactorization x)
this : IsDomain A
alg : (matroid R A).Spanning (range x)
⊢ IsTranscendenceBasis R Subtype.val
Module: Mathlib.FieldTheory.SeparableDegree

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))

Tactic:
refine Infinite.of_injective f fun m n h ↦ ?_

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
m n : ℕ
h : f m = f n
⊢ m = n
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case inr
ι : Type u
R : Type u_1
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfulSMul R S
inst✝ : NoZeroDivisors S
i j : ι
v : ι → S
H₁ : IsTranscendenceBasis R fun x ↦ v ↑x
H₂ : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j)
ne : j ≠ i
this : IsAlgebraic (↥(adjoin R (v '' {j}ᶜ))) (v j) → IsTranscendenceBasis R fun x ↦ v ↑x
⊢ IsTranscendenceBasis R fun x ↦ v ↑x

Tactic:
exact this H₂

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

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Nat.card Gal(E/F) = 1 * finrank (↥(fixedField ⊤)) E

Tactic:
one_mul,

Goal state after:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
h : Nat.card Gal(E/F) = finrank F E
p : 0 < finrank (↥(fixedField ⊤)) E
⊢ Nat.card Gal(E/F) = finrank (↥(fixedField ⊤)) E
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = (0 - x) ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
zero_sub,

Goal state after:
case refine_2
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = (-x) ^ q ^ n
⊢ ∃ n, x ^ q ^ n ∈ (algebraMap F E).range
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ - -(1 * x ^ q ^ n) = x ^ q ^ n

Tactic:
one_mul,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Ring E
inst✝¹ : IsDomain E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
x : E
this✝ : ExpChar E q
this : ExpChar E[X] q
x✝ : ∃ n, Polynomial.map (algebraMap F E) (minpoly F x) = (X - C x) ^ q ^ n
n : ℕ
h : (algebraMap F E) ((minpoly F x).coeff 0) = -1 * x ^ q ^ n
⊢ - -x ^ q ^ n = x ^ q ^ n
Module: Mathlib.FieldTheory.Galois.Basic

Goal state before:
pp: F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Polynomial.eval x (Polynomial.map ((algebraMap K E).comp (algebraMap F K)) p) = 0

Tactic:
←
      IsScalarTower.algebraMap_eq

Goal state after:
F : Type u_1
inst✝⁶ : Field F
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝³ : Field K
inst✝² : Algebra F K
inst✝¹ : Algebra K E
inst✝ : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
h : IsIntegral K x
h1 : p ≠ 0
⊢ Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
⊢ insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K

Tactic:
have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl

Goal state after:
F : Type u
inst✝² : Field F
K : Type v
inst✝¹ : Field K
inst✝ : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
this✝ : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ insepDegree (↥E₂) K ≤ insepDegree (↥E₁) K
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
inst✝³ : Field F
K : Type v
inst✝² : Field K
inst✝¹ : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
inst✝ : Module.Finite (↥E₁) K
this : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
⊢ finInsepDegree (↥E₂) K ≤ finInsepDegree (↥E₁) K

Tactic:
have : IsScalarTower E₁ E₂ K := .of_algebraMap_eq' rfl

Goal state after:
F : Type u
inst✝³ : Field F
K : Type v
inst✝² : Field K
inst✝¹ : Algebra F K
E₁ E₂ : IntermediateField F K
H : E₁ ≤ E₂
inst✝ : Module.Finite (↥E₁) K
this✝ : Algebra ↥E₁ ↥E₂ := (inclusion H).toAlgebra
this : IsScalarTower (↥E₁) (↥E₂) K
⊢ finInsepDegree (↥E₂) K ≤ finInsepDegree (↥E₁) K
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case inr
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
H :
  ∀ (E : Type v) [inst : Field E] [inst_1 : Algebra F E] [Algebra.IsSeparable F E],
    FiniteDimensional F E → finSepDegree F E = finrank F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E = finrank F E

Tactic:
rw [finrank_of_infinite_dimensional hfd]
    obtain ⟨L, h, h'⟩ := exists_lt_finrank_of_infinite_dimensional hfd (finSepDegree F E)
    have hd := finSepDegree_mul_finSepDegree_of_isAlgebraic F L E
    rw [H L h] at hd
    by_cases hd' : finSepDegree L E = 0
    · rw [← hd, hd', mul_zero]
    linarith only [h', hd, Nat.le_mul_of_pos_right (finrank F L) (Nat.pos_of_ne_zero hd')]

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

Goal state before:
pp: k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
x : K
L : FiniteGaloisIntermediateField k K
⊢ adjoin k {x} ≤ L ↔ x ∈ L.toIntermediateField

Tactic:
simp only [le_iff, adjoin_val, IntermediateField.normalClosure_le_iff_of_normal,
    IntermediateField.adjoin_le_iff, Set.singleton_subset_iff, SetLike.mem_coe]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.ClosedSubgroup

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : TopologicalSpace G
A B : ClosedSubgroup G
h : ↑A = ↑B
⊢ A = B

Tactic:
ext
  rw [h]

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

Goal state before:
pp: case inr
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
L : IntermediateField F E'
inst✝ : IsGalois F E'
this : ∀ (L : IntermediateField F E'), FiniteDimensional F ↥L → finrank F ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional F ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField F ↥L
hL' : L.fixingSubgroup.index < finrank F ↥(lift L')
i : ↥L' ≃ₗ[F] ↥(lift L') := ↑(liftAlgEquiv L')
hfd : FiniteDimensional F ↥(lift L')
⊢ False

Tactic:
this _ hfd

Goal state after:
case inr
F : Type u_1
E' : Type u_3
inst✝³ : Field F
inst✝² : Field E'
inst✝¹ : Algebra F E'
L : IntermediateField F E'
inst✝ : IsGalois F E'
this : ∀ (L : IntermediateField F E'), FiniteDimensional F ↥L → finrank F ↥L = L.fixingSubgroup.index
hnfd : ¬FiniteDimensional F ↥L
h : L.fixingSubgroup.FiniteIndex
L' : IntermediateField F ↥L
hL' : L.fixingSubgroup.index < (lift L').fixingSubgroup.index
i : ↥L' ≃ₗ[F] ↥(lift L') := ↑(liftAlgEquiv L')
hfd : FiniteDimensional F ↥(lift L')
⊢ False
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type ?u.5
S : Type ?u.7
M : Type ?u.9
inst✝⁶ : CommRing R
inst✝⁵ : Field S
inst✝⁴ : AddCommGroup M
inst✝³ : Algebra R S
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
B : BilinForm S M
N : Submodule R M
r : R
a : M
ha : a ∈ {x | ∀ y ∈ N, (B x) y ∈ 1}
y : M
hy : y ∈ N
⊢ (B (r • a)) y ∈ 1

Tactic:
convert! (1 : Submodule R S).smul_mem r (ha y hy)
    rw [← IsScalarTower.algebraMap_smul S r a]
    simp only [algebraMap_smul, map_smul_of_tower, LinearMap.smul_apply]

Goal state after:
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: R : Type u_4
S : Type u_2
M : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field S
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : IsScalarTower R S M
B : BilinForm S M
ι : Type u_1
inst✝ : Finite ι
hB : B.Nondegenerate
hB' : B.IsSymm
b : Basis ι S M
⊢ B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

Tactic:
classical
  let := b.finiteDimensional_of_finite
  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
    dualBasis_dualBasis hB hB']

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

Goal state before:
pp: R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ map (algebraMap R S) (minpoly R x) /ₘ (X - C x) * (X - C x) = map (algebraMap R S) (minpoly R x)

Tactic:
mul_comm,

Goal state after:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ (X - C x) * (map (algebraMap R S) (minpoly R x) /ₘ (X - C x)) = map (algebraMap R S) (minpoly R x)
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : f.IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
hdeg : f.degree = 0
⊢ IsUnit f

Tactic:
rw [eq_C_of_degree_eq_zero hdeg] at hf ⊢

Goal state after:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
hinj : Function.Injective ⇑φ
f : R[X]
hf : (C (f.coeff 0)).IsPrimitive
h : IsUnit (map φ f)
u : Sˣ
hu : C ↑u = map φ f
hdeg : f.degree = 0
⊢ IsUnit (C (f.coeff 0))
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) a' * (1 * Polynomial.map (algebraMap R K) b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b

Tactic:
one_mul,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H : Polynomial.map (algebraMap R K) p = Polynomial.map (algebraMap R K) a' * Polynomial.map (algebraMap R K) b'
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ.refine_2
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
i : ℕ
IH :
  i ≤ (minpolyDiv R x).natDegree →
    (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈
      Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio i)
hi : i + 1 ≤ (minpolyDiv R x).natDegree
⊢ ((minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) - x ^ i) * x ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
· rw [← tsub_tsub, tsub_add_cancel_of_le (le_tsub_of_add_le_left (b := 1) hi)]
      apply SetLike.le_def.mp ?_
        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
          (Submodule.mem_span_singleton_self x))
      rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
      apply Submodule.span_mono
      rintro _ ⟨j, hj, rfl⟩
      rw [Set.mem_Iio] at hj
      exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ x j⟩

Goal state after:
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
⊢ ∃ r, IsUnit r ∧ C r = map (algebraMap R K) (C ((integerNormalization R⁰ p).content * ↑u))

Tactic:
refine
    ⟨algebraMap R K ((integerNormalization R⁰ p).content * ↑u), isUnit_iff_ne_zero.2 fun con => ?_,
      by simp⟩

Goal state after:
case hu
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
c : R
c0 : c ∈ R⁰
hc : map (algebraMap R K) (integerNormalization R⁰ p) = C ((algebraMap R K) c) * p
con : (algebraMap R K) ((integerNormalization R⁰ p).content * ↑u) = 0
⊢ False
Module: Mathlib.RingTheory.Polynomial.GaussLemma

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
⊢ map (algebraMap R K) f * g ∈ lifts (algebraMap R K) ↔ g ∈ lifts (algebraMap R K)

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
f : R[X]
hf : f.IsPrimitive
g : K[X]
⊢ g * map (algebraMap R K) f ∈ lifts (algebraMap R K) ↔ g ∈ lifts (algebraMap R K)
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : (aeval x) (1 * X + C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x

Tactic:
one_mul,

Goal state after:
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
inst✝ : Algebra.IsSeparable k K
x : K
hq : (minpoly k x).leadingCoeff = 1
hsep : IsSeparable k x
h : (minpoly k x).degree = 1
this : (aeval x) (X + C ((minpoly k x).coeff 0)) = 0
⊢ (algebraMap k K) (-(minpoly k x).coeff 0) = x
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_2
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ z * (algebraMap A L) ↑m = m • z

Tactic:
mul_comm,

Goal state after:
case refine_2
A : Type u_1
K : Type u_2
inst✝¹⁴ : CommRing A
inst✝¹³ : Field K
inst✝¹² : Algebra A K
inst✝¹¹ : IsFractionRing A K
L : Type u_3
inst✝¹⁰ : Field L
C : Type u_4
inst✝⁹ : CommRing C
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A L
inst✝⁶ : IsScalarTower A K L
inst✝⁵ : Algebra C L
inst✝⁴ : IsIntegralClosure C A L
inst✝³ : Algebra A C
inst✝² : IsScalarTower A C L
inst✝¹ : IsDomain A
inst✝ : Algebra.IsAlgebraic K L
this✝¹ : IsDomain C
this✝ : IsTorsionFree A L
this : IsTorsionFree A C
z : L
m : ↥A⁰
hm : IsIntegral A (m • z)
x : C
hx : (algebraMap C L) x = m • z
⊢ (algebraMap A L) ↑m * z = m • z
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ ↑a.val * 2 = ↑n + 1 ↔ 2 * ↑a.val = ↑(n + 1)

Tactic:
mul_comm,

Goal state after:
case pos
n : ℕ
a : ZMod (n + 1)
h : a.val ≤ n.succ / 2
⊢ 2 * ↑a.val = ↑n + 1 ↔ 2 * ↑a.val = ↑(n + 1)
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod (n + 1)
h : ¬a.val ≤ n.succ / 2
⊢ 2 * a.val = n + 1 → a.val ≤ n.succ / 2

Tactic:
· rw [mul_comm]
    exact fun h => (Nat.le_div_iff_mul_le zero_lt_two).2 h.le

Goal state after:
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: n : ℕ
a : ZMod n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

Tactic:
by_cases h2a : 2 * a.val = n

Goal state after:
case pos
n : ℕ
a : ZMod n
h2a : 2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

case neg
n : ℕ
a : ZMod n
h2a : ¬2 * a.val = n
⊢ (-a).valMinAbs.natAbs = a.valMinAbs.natAbs