mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
hXY : X ⊆ Y
hY : Y ⊆ M.E
I I' : Set α
hI : M.IsBasis I X
hI' : M.IsBasis I' Y
hII' : I ⊆ I'
⊢ M.IsBasis (I ∪ I' \ I) Y

Tactic:
by rwa [union_sdiff_self, union_eq_self_of_subset_left hII']

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u_5
inst✝³ : CommRing R
inst✝² : IsFractionRing R R
I J : Ideal R
inst✝¹ : Module.Invertible R ↥I
inst✝ : Module.Invertible R ↥J
h : Pic.mk R (↥I ⊗[R] ↥J) = 1
e✝ : ↥I ⊗[R] ↥J ≃ₗ[R] R
e : R ≃ₗ[R] ↥(I * J)
x✝ : R
⊢ x✝ * ↑(e 1) = (Subtype.val ∘ ⇑e) x✝

Tactic:
rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one, Function.comp_apply]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
⊢ (M ↾ Y ↾ X).IsBase I

Tactic:
M.restrict_restrict_eq hXY,

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
⊢ (M ↾ X).IsBase I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ (∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty) ∧
    e ∈ M.E ∧ M.E \ B ∩ (M.E \ X) ⊆ M.E

Tactic:
and_iff_right he.1.1,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
⊢ (∀ (B_1 : Set α), M.IsBase B_1 → (insert e (M.E \ B ∩ (M.E \ X)) ∩ B_1).Nonempty) ∧ M.E \ B ∩ (M.E \ X) ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : M.E \ (B ∪ X) ∩ B' ∪ {e} ∩ B' = ∅
⊢ False

Tactic:
union_empty_iff,

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
B X : Set α
hB : M.IsBase B
hBX : M.IsBasis (B ∩ X) X
e : α
he : (e ∈ M.E ∧ e ∉ X) ∧ e ∈ B
B' : Set α
hB' : M.IsBase B'
hem : M.E \ (B ∪ X) ∩ B' = ∅ ∧ {e} ∩ B' = ∅
⊢ False
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
I : Set α
N : Matroid β
⊢ (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I

Tactic:
rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]
  refine ⟨by grind, ?_⟩
  rintro (⟨hI, hIE⟩ | hI)
  · exact ⟨fun h ↦ (hI h).elim, hIE⟩
  rw [iff_true_intro hI.1, iff_true_intro hI.2, implies_true, true_and]
  simpa using hI.1.subset_ground

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : ↑M.E ↪ β
I : Set β
⊢ (M.mapSetEmbedding f).Indep I ↔ ∃ I₀, M.Indep (Subtype.val '' I₀) ∧ I = ⇑f '' I₀

Tactic:
simp only [mapSetEmbedding_indep_iff, subset_range_iff_exists_image_eq]
  constructor
  · rintro ⟨hI, I, rfl⟩
    exact ⟨I, by rwa [preimage_image_eq _ f.injective] at hI, rfl⟩
  rintro ⟨I, hI, rfl⟩
  rw [preimage_image_eq _ f.injective]
  exact ⟨hI, _, rfl⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
⊢ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀

Tactic:
have h' : I ⊆ f '' M.E := by
    intro e he
    obtain ⟨I₀, hI₀, h_eq⟩ := hI {e} (by simpa) (by simp)
    exact image_mono hI₀.subset_ground <| h_eq.subset rfl

Goal state after:
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M : Matroid α
N : Matroid β
inst✝ : M.Finitary
f : α → β
hf : InjOn f M.E
I : Set β
hI : ∀ J ⊆ I, J.Finite → (M.map f hf).Indep J
h' : I ⊆ f '' M.E
⊢ ∃ I₀, M.Indep I₀ ∧ I = f '' I₀
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (M.restrictSubtype X).map Subtype.val ⋯ = M ↾ X

Tactic:
by
  simp [restrictSubtype, map_comap]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X✝ I : Set α
M : Matroid α
inst✝ : M.Finitary
X : Set α
⊢ (M.restrictSubtype X).Finitary

Tactic:
by
  rw [restrictSubtype]; infer_instance

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ : Set α
M✝ : Matroid α
N : Matroid β
E X✝ I : Set α
M : Matroid α
inst✝ : M.RankFinite
X : Set α
⊢ (M.restrictSubtype X).RankFinite

Tactic:
by
  rw [restrictSubtype]; infer_instance

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
⊢ (M.comap f).loops = f ⁻¹' M.loops

Tactic:
by
  rw [loops, comap_closure_eq, image_empty, loops]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
x✝¹ : Z ⊆ X
heZ : e ∉ Z
x✝ : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T

Tactic:
obtain ⟨S, hSY, hSfin, -, heS⟩ := exists_mem_finite_closure_of_mem_closure (hXY heX)

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
e : α
Z : Set α
heX : e ∈ X
x✝¹ : Z ⊆ X
heZ : e ∉ Z
x✝ : ∃ T ⊆ Y, T.Finite ∧ Z ⊆ M.closure T
T : Set α
hTY : T ⊆ Y
hTfin : T.Finite
hT : Z ⊆ M.closure T
S : Set α
hSY : S ⊆ Y
hSfin : S.Finite
heS : e ∈ M.closure S
⊢ ∃ T ⊆ Y, T.Finite ∧ insert e Z ⊆ M.closure T
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
⊢ M.closure J ∩ I = J

Tactic:
have hJ := hI.subset hJI

Goal state after:
α : Type u_2
M : Matroid α
I J : Set α
hI : M.Indep I
hJI : J ⊆ I
hJ : M.Indep J
⊢ M.closure J ∩ I = J
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
i : σ
f : R[X]
hf : Transcendental R f
⊢ Transcendental R ((Polynomial.aeval (X i)) f)

Tactic:
have := transcendental_supported_polynomial_aeval_X R (Set.notMem_empty i) hf
  let g := (Algebra.botEquivOfInjective (MvPolynomial.C_injective σ R)).symm.trans
    (Subalgebra.equivOfEq _ _ supported_empty).symm
  rwa [Transcendental, ← isAlgebraic_ringHom_iff_of_comp_eq g (RingHom.id (MvPolynomial σ R))
    Function.injective_id (by ext1; rfl), RingHom.id_apply, ← Transcendental]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ ¬M.Spanning S ↔ M.closure S ⊂ M.E

Tactic:
rw [spanning_iff_closure_eq, ssubset_iff_subset_ne, iff_and_self,
    iff_true_intro (M.closure_subset_ground _)]
  exact fun _ ↦ trivial

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

Goal state before:
pp: R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
ι : Type u_3
s : Set ι
f : ι → A
hs : AlgebraicIndependent R fun x ↦ f ↑x
⊢ AlgebraicIndependent R fun x ↦ ↑x

Tactic:
convert! AlgebraicIndependent.image_of_comp s f id hs

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_3
inst✝² : Monoid G
inst✝¹ : MulAction G A
inst✝ : MulAction G B
f : A →ₑ[id] B
H : Submonoid G
a : A
ha : a ∈ MulAction.fixedPoints (↥H) A
⊢ f a ∈ MulAction.fixedPoints (↥H) B

Tactic:
by
  intro ⟨h, _⟩
  simp_all [← f.map_smul h a]

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

Goal state before:
pp: case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
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 A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
⊢ Algebra.IsAlgebraic (↥(Subalgebra.restrictScalars R Rxy)) A

Tactic:
change Algebra.IsAlgebraic Rxy A

Goal state after:
case inr
ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
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 A
x : ι → S
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis S y
h✝ : Nontrivial R
Rx : Subalgebra R S := adjoin R (range x)
Rxy : Subalgebra (↥Rx) A := adjoin (↥Rx) (range y)
⊢ Algebra.IsAlgebraic (↥Rxy) A
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
S : Type v
A : Type w
x : ι → A
y : ι' → A
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✝¹ : FaithfulSMul R A
inst✝ : NoZeroDivisors A
B : Set A
⊢ IsTranscendenceBasis R Subtype.val ↔ (indepMatroid R A).matroid.IsBase B

Tactic:
simp_rw [Matroid.isBase_iff_maximal_indep, isTranscendenceBasis_iff_maximal]; rfl

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
inst✝ : DecidableEq E
h : (map (algebraMap F E) f).Splits
⊢ f.natSepDegree = (map ((↑(SplittingField.lift f h)).comp (algebraMap F f.SplittingField)) f).roots.toFinset.card

Tactic:
← map_map,

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
f : F[X]
inst✝ : DecidableEq E
h : (map (algebraMap F E) f).Splits
⊢ f.natSepDegree = (map (↑(SplittingField.lift f h)) (map (algebraMap F f.SplittingField) f)).roots.toFinset.card
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F),

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ((f * g).aroots (AlgebraicClosure F)).toFinset.card ≤
    (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree ≤ f.natSepDegree + g.natSepDegree

Tactic:
simp_rw [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_mul h, Multiset.toFinset_add]
  exact Finset.card_union_le _ _

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

Tactic:
natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F),

Goal state after:
case neg
F : Type u
inst✝ : Field F
f g : F[X]
h : ¬f * g = 0
⊢ ((f * g).aroots (AlgebraicClosure F)).toFinset.card =
      (f.aroots (AlgebraicClosure F)).toFinset.card + (g.aroots (AlgebraicClosure F)).toFinset.card ↔
    f = 0 ∧ g = 0 ∨ IsCoprime f g
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
hi : Irreducible f
h : f.natSepDegree = 1
⊢ ∃ n y, (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - C y

Tactic:
obtain ⟨n, y, hf⟩ := (hm.natSepDegree_eq_one_iff_of_irreducible q hi).1 h
  cases id ‹ExpChar F q› with
  | zero =>
    simp_rw [one_pow, pow_one] at hf ⊢
    exact ⟨0, y, .inl rfl, hf⟩
  | prime hq =>
    refine ⟨n, y, (em _).imp id fun hn ⟨z, hy⟩ ↦ ?_, hf⟩
    have := expChar_of_injective_ringHom (R := F) C_injective q
    rw [hf, ← Nat.succ_pred hn, pow_succ, pow_mul, ← hy, frobenius_def, map_pow,
      ← sub_pow_expChar] at hi
    exact not_irreducible_pow hq.ne_one hi

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

Goal state before:
pp: F : Type u_1
E : Type u_3
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ IsGalois (↥⊥) E ↔ IsGalois F E

Tactic:
by
  constructor
  · intro h
    exact IsGalois.tower_top_of_isGalois (⊥ : IntermediateField F E) F E
  · intro h; infer_instance

Goal state after:
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
⊢ (minpoly F x).natSepDegree = 1 ↔ ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨n, y, h⟩ ↦ ?_⟩
  · have halg : IsIntegral F x := by_contra fun h' ↦ by
      simp only [eq_zero h', natSepDegree_zero, zero_ne_one] at h
    exact (minpoly.irreducible halg).natSepDegree_eq_one_iff_of_monic' q
      (minpoly.monic halg) |>.1 h
  rw [h, natSepDegree_expand _ q, natSepDegree_X_sub_C]

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
H : Subgroup Gal(E/F)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        (fixedField L.fixingSubgroup) ↔
    K ≤ fixedField L.fixingSubgroup

Tactic:
IntermediateField.le_iff_le,

Goal state after:
F : Type u_1
inst✝⁴ : Field F
E : Type u_2
inst✝³ : Field E
inst✝² : Algebra F E
H : Subgroup Gal(E/F)
K✝ : IntermediateField F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsGalois F E
K L : IntermediateField F E
⊢ { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := ⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup, invFun := fixedField ∘ ⇑OrderDual.ofDual,
          left_inv := ⋯, right_inv := ⋯ }
        (fixedField L.fixingSubgroup) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
⊢ Algebra.IsSeparable F ↥F⟮x⟯ ↔ IsSeparable F x

Tactic:
refine ⟨fun _ ↦ ?_, fun hsep ↦ ?_⟩
  · exact isSeparable_of_mem_isSeparable F E <| mem_adjoin_simple_self F x
  · have h := IsSeparable.isIntegral hsep
    have := adjoin.finiteDimensional h
    rwa [← finSepDegree_eq_finrank_iff,
      finSepDegree_adjoin_simple_eq_finrank_iff F E x h.isAlgebraic]

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
f : K →ₐ[k] K
s : Set K
inst✝ : Finite ↑s
⊢ normalClosure k (↥(IntermediateField.adjoin k (⇑f '' s))) K = normalClosure k (↥(IntermediateField.adjoin k s)) K

Tactic:
rw [← IntermediateField.adjoin_map, IntermediateField.normalClosure_map_eq]

Goal state after:
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
f : R[X]
hf : f.Monic
g : K[X]
hg : g ∣ map (algebraMap R K) f
g_ne_0 : g ≠ 0
lem : ∃ g', map (algebraMap R K) g' = g * C g.leadingCoeff⁻¹
⊢ ∃ g', map (algebraMap R K) g' * C g.leadingCoeff = g

Tactic:
by
    obtain ⟨g', hg'⟩ := lem
    use g'
    rw [hg', mul_assoc, ← C_mul, inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr g_ne_0), C_1, mul_one]

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

Goal state before:
pp: R : Type u_1
K : Type u_3
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
x : S
hx : IsIntegral R x
inst✝⁶ : IsDomain R
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R K
inst✝² : Algebra K S
inst✝¹ : IsScalarTower R K S
inst✝ : IsFractionRing R K
⊢ map ((algebraMap K S).comp (algebraMap R K)) (minpoly R x) /ₘ (X - C x) =
    map (algebraMap K S) (minpoly K x) /ₘ (X - C x)

Tactic:
← map_map,

Goal state after:
R : Type u_1
K : Type u_3
S : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : Field K
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
x : S
hx : IsIntegral R x
inst✝⁶ : IsDomain R
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsDomain S
inst✝³ : Algebra R K
inst✝² : Algebra K S
inst✝¹ : IsScalarTower R K S
inst✝ : IsFractionRing R K
⊢ map (algebraMap K S) (map (algebraMap R K) (minpoly R x)) /ₘ (X - C x) =
    map (algebraMap K S) (minpoly K x) /ₘ (X - C x)
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✝ : NormalizedGCDMonoid R
p : K[X]
h0 : p ≠ 0
h : IsUnit (integerNormalization R⁰ p).primPart
u : Rˣ
hu : C ↑u = (integerNormalization R⁰ p).primPart
⊢ IsUnit p

Tactic:
obtain ⟨c, c0, hc⟩ := integerNormalization_spec R⁰ p

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✝ : 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 • p
⊢ IsUnit p
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]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
⊢ map (algebraMap R K) (g' * f) = b • g * map (algebraMap R K) f

Tactic:
← hb₂,

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]
this : NormalizedGCDMonoid R := ⋯.some
x✝ : g * map (algebraMap R K) f ∈ lifts (algebraMap R K)
k : R[X]
hk : map (algebraMap R K) k = g * map (algebraMap R K) f
g' : R[X] := integerNormalization R⁰ g
b : R
hb₁ : b ∈ R⁰
hb₂ : map (algebraMap R K) g' = b • g
⊢ map (algebraMap R K) (g' * f) = map (algebraMap R K) g' * map (algebraMap R K) f
Module: Mathlib.FieldTheory.Galois.Infinite

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✝
K L : IntermediateField k K✝
⊢ { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        (IntermediateField.fixedField L.fixingSubgroup) ↔
    K ≤ IntermediateField.fixedField L.fixingSubgroup

Tactic:
IntermediateField.le_iff_le,

Goal state after:
k : Type u_1
K✝ : Type u_2
inst✝³ : Field k
inst✝² : Field K✝
inst✝¹ : Algebra k K✝
inst✝ : IsGalois k K✝
K L : IntermediateField k K✝
⊢ { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        K ≤
      { toFun := fun L ↦ { toSubgroup := L.fixingSubgroup, isClosed' := ⋯ },
          invFun := fun H ↦ IntermediateField.fixedField ↑H, left_inv := ⋯, right_inv := ⋯ }
        (IntermediateField.fixedField L.fixingSubgroup) ↔
    L.fixingSubgroup ≤ K.fixingSubgroup
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

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
inst✝ : IsPurelyInseparable F K
x : E
h✝ : (minpoly F ((algebraMap E K) x)).Separable
y : F
h : (algebraMap F K) y = (algebraMap E K) x
⊢ x ∈ (algebraMap F E).range

Tactic:
exact ⟨y, (algebraMap E K).injective (h.symm ▸ (IsScalarTower.algebraMap_apply F E K y).symm)⟩

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

Goal state before:
pp: F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
⊢ False

Tactic:
refine hx (finrank_adjoin_simple_eq_one_iff.mp (le_antisymm (this ▸ H) ?_))

Goal state after:
F✝ : Type u
E✝ : Type v
inst✝¹¹ : Field F✝
inst✝¹⁰ : Field E✝
inst✝⁹ : Algebra F✝ E✝
q✝ : ℕ
inst✝⁸ : ExpChar F✝ q✝
inst✝⁷ : IsPurelyInseparable F✝ E✝
inst✝⁶ : FiniteDimensional F✝ E✝
E : Type v
inst✝⁵ : Field E
q d : ℕ
IH :
  ∀ m < d,
    ∀ (F : Type v) [inst : Field F] [inst_1 : Algebra F E] [ExpChar F q] [IsPurelyInseparable F E]
      [FiniteDimensional F E], finrank F E = m → ∃ n, m = q ^ n
F : Type v
inst✝⁴ : Field F
inst✝³ : Algebra F E
inst✝² : ExpChar F q
inst✝¹ : IsPurelyInseparable F E
inst✝ : FiniteDimensional F E
hd : finrank F E = d
h : ¬⊥ = ⊤
x : E
hx : x ∉ ⊥
m : ℕ
y : F
e : minpoly F x = X ^ q ^ m - C y
this : finrank F ↥F⟮x⟯ = q ^ m
H : q ^ m ≤ 1
⊢ 1 ≤ finrank F ↥F⟮x⟯
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L

Tactic:
by
  refine ⟨fun _ _ _ ↦ IsPurelyInseparable.tower_bot F _ E,
    fun h ↦ isPurelyInseparable_iff.2 fun x ↦ ?_⟩
  have hx : IsIntegral F x := Algebra.IsIntegral.isIntegral x
  refine ⟨hx, fun _ ↦ ?_⟩
  obtain ⟨y, h⟩ := (h _ (adjoin.finiteDimensional hx)).inseparable' _ <|
    show Separable (minpoly F (AdjoinSimple.gen F x)) by rwa [minpoly_eq]
  exact ⟨y, congr_arg (algebraMap _ E) h⟩

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

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
inst✝ : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : lift (adjoin E ↑(separableClosure F ↥S)) = S
⊢ adjoin E ↑(separableClosure F K) = S

Tactic:
lift_adjoin

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
inst✝ : Algebra.IsAlgebraic F E
S : IntermediateField E K := separableClosure E K
h : adjoin E (Subtype.val '' ↑(separableClosure F ↥S)) = S
⊢ adjoin E ↑(separableClosure F K) = S
Module: Mathlib.Data.ZMod.ValMinAbs

Goal state before:
pp: case neg
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ (↑x.val - ↑n) * 2 ∈ Set.Ioc (-↑n) ↑n

Tactic:
refine ⟨?_, le_trans (mul_nonpos_of_nonpos_of_nonneg ?_ zero_le_two) <| Nat.cast_nonneg _⟩

Goal state after:
case neg.refine_1
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ -↑n < (↑x.val - ↑n) * 2

case neg.refine_2
n : ℕ
inst✝ : NeZero n
x : ZMod n
h : ¬↑x.val * 2 ≤ ↑n
⊢ ↑x.val - ↑n ≤ 0