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

Goal state before:
pp: α : Type u
M : Matroid α
X Y : Set α
inst✝ : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
⊢ M.cRk X = M.cRk Y

Tactic:
← cRk_closure,

Goal state after:
α : Type u
M : Matroid α
X Y : Set α
inst✝ : M.InvariantCardinalRank
hXY : M.closure X = M.closure Y
⊢ M.cRk (M.closure X) = M.cRk Y
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ ¬Disjoint C K → (C ∩ K).Nontrivial

Tactic:
disjoint_iff_inter_eq_empty,

Goal state after:
α : Type u_1
M : Matroid α
C K : Set α
hC : M.IsCircuit C
hK : M.IsCocircuit K
⊢ ¬C ∩ K = ∅ → (C ∩ K).Nontrivial
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (¬∃ C, M.IsCircuit C) ↔ M.IsBase M.E

Tactic:
not_exists,

Goal state after:
α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ M.IsBase M.E
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ M.IsBasis ((⋂ i ∈ A, X i) ∩ I) (⋂ i ∈ A, X i)

Tactic:
refine (hI.inter_left _).isBasis_of_subset_of_subset_closure inter_subset_left ?_

Goal state after:
α : Type u_2
M : Matroid α
I : Set α
ι : Type u_4
hI : M.Indep I
X : ι → Set α
A : Set ι
hA : A.Nonempty
h : ∀ i ∈ A, M.IsBasis (X i ∩ I) (X i)
⊢ ⋂ i ∈ A, X i ⊆ M.closure ((⋂ i ∈ A, X i) ∩ I)
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ toENat M.cRank = M.eRank

Tactic:
obtain h | h := M.rankFinite_or_rankInfinite
  · obtain ⟨B, hB⟩ := M.exists_isBase
    rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]
  simp [rankInfinite_iff_aleph0_le_cRank.1 h]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
⊢ AlgebraicIndependent R x ↔ Transcendental R (x default)

Tactic:
rw [transcendental_iff_injective, algebraicIndependent_iff_injective_aeval]

Goal state after:
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Unique ι
⊢ Injective ⇑(aeval x) ↔ Injective ⇑(Polynomial.aeval (x default))
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, and_iff_left hS]

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
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
⊢ AlgebraicIndependent R Subtype.val

Tactic:
let f : t.map (Embedding.subtype (· ∈ s)) → s := fun x =>
    ⟨x.1, by
      obtain ⟨x, h⟩ := x
      rw [Finset.mem_map] at h
      obtain ⟨a, _, rfl⟩ := h
      simp only [Subtype.coe_prop, Embedding.coe_subtype]⟩

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : Set A
li : AlgebraicIndependent R Subtype.val
t : Finset ↑s
f : ↥(Finset.map (Embedding.subtype fun x ↦ x ∈ s) t) → ↑s := fun x ↦ ⟨↑x, ⋯⟩
⊢ AlgebraicIndependent R Subtype.val
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M✶.Indep I ↔ M'✶.Indep I)

Tactic:
intro I hIE

Goal state after:
α : Type u_2
M M' : Matroid α
h : M.E = M'.E
hsp : ∀ S ⊆ M.E, M.Spanning S ↔ M'.Spanning S
hsp' : M.Spanning = M'.Spanning
I : Set α
hIE : I ⊆ M.E
⊢ M✶.Indep I ↔ M'✶.Indep I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
⊢ M.closure ∅ = M.E ↔ M = loopyOn M.E

Tactic:
refine ⟨fun h ↦ ext_closure ?_, fun h ↦ by rw [h, loopyOn_closure_eq, loopyOn_ground]⟩

Goal state after:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
⊢ ∀ (X : Set α), M.closure X = (loopyOn M.E).closure X
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ range (⇑f ∘ x) ⊆ ⇑f '' s

Tactic:
Set.range_comp

Goal state after:
ι : Type u
R : Type u_2
A : Type v
A' : Type v'
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing A'
inst✝¹ : Algebra R A
inst✝ : Algebra R A'
x : ι → A
f : A →ₐ[R] A'
h : Injective ⇑f
H : IsTranscendenceBasis R (⇑f ∘ x)
s : Set A
hs : AlgebraicIndepOn R _root_.id s
hs' : range x ⊆ s
⊢ ⇑f '' range x ⊆ ⇑f '' s
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
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
⊢ lift.{v, v} (trdeg R A) = trdeg R A'

Tactic:
e.lift_trdeg_eq,

Goal state after:
R : Type u_2
A : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
A' : Type v
inst✝¹ : CommRing A'
inst✝ : Algebra R A'
e : A ≃ₐ[R] A'
⊢ lift.{v, v} (trdeg R A') = trdeg R A'
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
rw [mem_fixedBy, smul_left_cancel_iff]
  rfl

Goal state after:
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✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
ι' : Type u
y : ι' → A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ #ι = #ι'

Tactic:
rw [← lift_id #ι, lift_cardinalMk_eq hx hy, lift_id]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
⊢ natSepDegree 1 = 0

Tactic:
rw [← C_1, natSepDegree_C]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (map (algebraMap F f.SplittingField) f).natDegree ≠ Zero.zero

Tactic:
by rwa [natDegree_map]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : Irreducible f
q : ℕ
h✝ : ExpChar F q
hf : HasSeparableContraction q f
⊢ hf.degree ∣ f.natDegree

Tactic:
exact hf.dvd_degree

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
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } = (minpoly F α).natSepDegree

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ Fintype.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } = (minpoly F α).natSepDegree
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : TopologicalSpace R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : ModuleFilterBasis R M
BR : RingFilterBasis R
BM : AddGroupFilterBasis M
smul : ∀ {U : Set M}, U ∈ BM → ∃ V ∈ BR, ∃ W ∈ BM, V • W ⊆ U
smul_left : ∀ (x₀ : R) {U : Set M}, U ∈ BM → ∃ V ∈ BM, V ⊆ (fun x ↦ x₀ • x) ⁻¹' U
smul_right : ∀ (m₀ : M) {U : Set M}, U ∈ BM → ∃ V ∈ BR, V ⊆ (fun x ↦ x • m₀) ⁻¹' U
x✝ : TopologicalSpace R := BR.topology
⊢ ∀ {U : Set M}, U ∈ BM.sets → ∃ V ∈ 𝓝 0, ∃ W ∈ BM.sets, V • W ⊆ U

Tactic:
by
      intro U U_in
      rcases smul U_in with ⟨V, V_in, W, W_in, H⟩
      exact ⟨V, BR.toAddGroupFilterBasis.mem_nhds_zero V_in, W, W_in, H⟩

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : ¬IsAlgebraic F α
this : finrank F ↥F⟮α⟯ = 0
⊢ finSepDegree F ↥F⟮α⟯ ∣ 0

Tactic:
exact dvd_zero _

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case neg
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hfd : ¬FiniteDimensional F E
⊢ finSepDegree F E ∣ 0

Tactic:
exact dvd_zero _

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

Goal state before:
pp: case intro
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 ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
⊢ B.dualSubmodule (Submodule.span R (Set.range ⇑b)) = Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Tactic:
apply le_antisymm

Goal state after:
case intro.a
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 ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
⊢ B.dualSubmodule (Submodule.span R (Set.range ⇑b)) ≤ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

case a
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 ι
inst✝ : DecidableEq ι
hB : B.Nondegenerate
b : Basis ι S M
val✝ : Fintype ι
⊢ Submodule.span R (Set.range ⇑(B.dualBasis hB b)) ≤ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
Module: Mathlib.FieldTheory.Galois.Infinite

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
σ : Gal(K/k)
h : σ ∈ (↑L.fixingSubgroup)ᶜ
y : K
yL : y ∈ ↑L
ne : y ∉ fun a ↦ σ • a = a
f : Gal(K/k)
hf : f ∈ σ • ↑(adjoin k {y}).fixingSubgroup
g : Gal(K/k)
hg : g ∈ ↑(adjoin k {y}).fixingSubgroup
eq : σ • g = f
this : g y = y
⊢ ¬σ (g y) = y

Tactic:
simpa only [this, ne_eq, AlgEquiv.smul_def] using! ne

Goal state after:
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
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ IntermediateField.fixedField L.fixingSubgroup = L

Tactic:
apply le_antisymm

Goal state after:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ IntermediateField.fixedField L.fixingSubgroup ≤ L

case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
⊢ L ≤ IntermediateField.fixedField L.fixingSubgroup
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
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
⊢ False

Tactic:
have := hL.out

Goal state after:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this : FiniteDimensional k ↥L
⊢ False
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
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Submodule.span R (Set.range (minpolyDiv R x).coeff) = Subalgebra.toSubmodule R[x]

Tactic:
apply le_antisymm

Goal state after:
case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Submodule.span R (Set.range (minpolyDiv R x).coeff) ≤ Subalgebra.toSubmodule R[x]

case a
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsIntegral R x
a✝ : Nontrivial S
⊢ Subalgebra.toSubmodule R[x] ≤ Submodule.span R (Set.range (minpolyDiv R x).coeff)
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
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
this : h ∈ σ • L'.fixingSubgroup.carrier
⊢ ∃ a ∈ σ • L'.fixingSubgroup.carrier, a ∉ (↑H).carrierᶜ

Tactic:
use h

Goal state after:
case h
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
H : ClosedSubgroup Gal(K/k)
inst✝ : IsGalois k K
σ : Gal(K/k)
hσ : σ ∈ (fixedField ↑H).fixingSubgroup
h✝ : σ ∉ ↑H
b : Set Gal(K/k)
sub : b ⊆ (fun y ↦ σ * y) ⁻¹' (↑H).carrierᶜ
gp : Subgroup Gal(K/k)
L : IntermediateField k K
eq✝ : (fun g ↦ g.carrier) L.fixingSubgroup = b
hL : L ∈ finiteExts k K
eq' : L.fixingSubgroup = gp
this✝ : FiniteDimensional k ↥L
L' : FiniteGaloisIntermediateField k K := ⋯
compl : σ • L'.fixingSubgroup.carrier ⊆ (↑H).carrierᶜ
fix : ∀ x ∈ lift (fixedField (Subgroup.map (restrictNormalHom ↥L'.toIntermediateField) ↑H)), σ x = x
h : Gal(K/k)
mem : h ∈ ↑↑H
eq : (restrictNormalHom ↥L'.toIntermediateField) h = (restrictNormalHom ↥L'.toIntermediateField) σ
this : h ∈ σ • L'.fixingSubgroup.carrier
⊢ h ∈ σ • L'.fixingSubgroup.carrier ∧ h ∉ (↑H).carrierᶜ
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
L : IntermediateField k K
inst✝ : Algebra.IsSeparable k ↥L
x : K
hx : x ∈ L
⊢ x ∈ ⊥

Tactic:
obtain ⟨y, hy⟩ := IsSepClosed.algebraMap_surjective k L ⟨x, hx⟩

Goal state after:
k : Type u
inst✝⁴ : Field k
K : Type v
inst✝³ : Field K
inst✝² : IsSepClosed k
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Algebra.IsSeparable k ↥L
x : K
hx : x ∈ L
y : k
hy : (algebraMap k ↥L) y = ⟨x, hx⟩
⊢ x ∈ ⊥
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
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) :=
  fun x ↦ Subgroup.map (restrictNormalHom ↥(adjoin k {x}).toIntermediateField) L.fixingSubgroup
f : ↥L → IntermediateField k K := fun x ↦ IntermediateField.lift (IntermediateField.fixedField (g ↑x))
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
⊢ ⨆ l, f l = L

Tactic:
apply le_antisymm

Goal state after:
case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) := ⋯
f : ↥L → IntermediateField k K := ⋯
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
⊢ ⨆ l, f l ≤ L

case a
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : IsGalois k K
h : L.fixingSubgroup.Normal
g : (x : K) → Subgroup Gal(↥(adjoin k {x}).toIntermediateField/k) := ⋯
f : ↥L → IntermediateField k K := ⋯
this✝ : ∀ (x : K), (g x).Normal
this : ∀ (l : ↥L), Normal k ↥(f l)
n : Normal k ↥(⨆ l, f l)
⊢ L ≤ ⨆ l, f l
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : finrank F ↥F⟮x⟯ = 1 ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range

Tactic:
IntermediateField.finrank_eq_one_iff

Goal state after:
case pos
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hdeg : finSepDegree F E = 1
H : Algebra.IsAlgebraic F E
x : E
hsep : IsSeparable F x
this : F⟮x⟯ = ⊥ ∧ finSepDegree (↥F⟮x⟯) E = 1
⊢ x ∈ (algebraMap F E).range
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
p q : R[X]
hp : p.IsPrimitive
r : K[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * r
⊢ p ∣ q

Tactic:
obtain ⟨r, rfl⟩ := (mul_map_mem_lifts_iff hp).mp ⟨q, mul_comm _ r ▸ hr⟩

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
p q : R[X]
hp : p.IsPrimitive
r : R[X]
hr : map (algebraMap R K) q = map (algebraMap R K) p * (mapRingHom (algebraMap R K)) r
⊢ p ∣ q
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: case refine_3
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
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
his' : ∀ x ∈ Finset.image (⇑bs') Finset.univ, IsIntegral A (y • x)
hy' : (algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
⊢ IsIntegral A
    ((bs'.map
        (let __src := (lmul K L) ((algebraMap A L) y);
        { toFun := fun x ↦ (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯,
          invFun := fun x ↦ ((algebraMap A L) y)⁻¹ * x, left_inv := ⋯, right_inv := ⋯ }))
      ⟨x', hx'⟩)

Tactic:
simp only [Algebra.smul_def, Finset.mem_image, Finset.mem_univ,
      true_and] at his'

Goal state after:
case refine_3
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
inst✝⁴ : Algebra K L
inst✝³ : Algebra A L
inst✝² : IsScalarTower A K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsDomain A
this : DecidableEq L := Classical.decEq L
s' : Finset L := IsNoetherian.finsetBasisIndex K L
bs' : Basis (↥(IsNoetherian.finsetBasisIndex K L)) K L := IsNoetherian.finsetBasis K L
y : A
hy : y ≠ 0
hy' : (algebraMap A L) y ≠ 0
x' : L
hx' : x' ∈ s'
his' : ∀ (x : L), (∃ a, bs' a = x) → IsIntegral A ((algebraMap A L) y * x)
⊢ IsIntegral A
    ((bs'.map
        (let __src := (lmul K L) ((algebraMap A L) y);
        { toFun := fun x ↦ (algebraMap A L) y * x, map_add' := ⋯, map_smul' := ⋯,
          invFun := fun x ↦ ((algebraMap A L) y)⁻¹ * x, left_inv := ⋯, right_inv := ⋯ }))
      ⟨x', hx'⟩)
Module: Mathlib.RingTheory.IsGaloisGroup.Defs

Goal state before:
pp: G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
⊢ ∃ a, (algebraMap A B') a = x'

Tactic:
obtain ⟨a, ha⟩ := hG.isInvariant.isInvariant (e.symm x') (fun g ↦ by
      apply e.injective
      simp [he, hx'])

Goal state after:
G : Type u_1
A : Type u_2
B : Type u_4
inst✝⁷ : Group G
inst✝⁶ : CommSemiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
inst✝³ : MulSemiringAction G B
hG : IsGaloisGroup G A B
B' : Type u_5
inst✝² : Semiring B'
inst✝¹ : Algebra A B'
inst✝ : MulSemiringAction G B'
e : B ≃ₐ[A] B'
he : ∀ (g : G) (x : B), e (g • x) = g • e x
x' : B'
hx' : ∀ (g : G), g • x' = x'
a : A
ha : (algebraMap A B) a = e.symm x'
⊢ ∃ a, (algebraMap A B') a = x'
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ ∃ g ∈ Finset.univ, g • b ∈ P

Tactic:
rw [← hP.prod_mem_iff, ← ha, ← P.mem_comap, ← P.under_def A,
      hPQ, Q.mem_comap, ha, hQ.prod_mem_iff]

Goal state after:
A : Type u_1
B : Type u_2
G : Type u_3
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G B
inst✝² : IsInvariant A B G
inst✝¹ : Finite G
inst✝ : SMulCommClass G A B
P✝ Q✝ : Ideal B
hP✝ : P✝.IsPrime
hQ✝ : Q✝.IsPrime
hPQ✝ : Ideal.under A P✝ = Ideal.under A Q✝
val✝ : Fintype G
P Q : Ideal B
hP : P.IsPrime
hQ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
b : B
hb : b ∈ ↑Q
a : A
ha : (algebraMap A B) a = ∏ g, g • b
⊢ ∃ i ∈ Finset.univ, i • b ∈ Q
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: A : Type u_7
B : Type u_8
C : Type u_9
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : CommRing C
inst✝¹ : Algebra A C
inst✝ : Algebra B C
e : A ≃+* B
he : (algebraMap B C).comp ↑e = algebraMap A C
x : C
⊢ e ((trace A C) x) = (trace B C) x

Tactic:
classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    let : Algebra A B := RingHom.toAlgebra e
    let : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.trace_eq_matrix_trace b,
      Algebra.trace_eq_matrix_trace (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he]))]
    rw [AddMonoidHom.map_trace]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [trace_eq_zero_of_not_exists_basis _ h, trace_eq_zero_of_not_exists_basis,
    LinearMap.zero_apply, LinearMap.zero_apply, map_zero]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

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

Goal state before:
pp: n a : ℕ
inst✝ : NeZero n
⊢ (↑a).valMinAbs = ↑a ↔ a ≤ n / 2

Tactic:
by
  refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩
  rw [← Int.natAbs_natCast a, ← ha]
  exact natAbs_valMinAbs_le (n := n) a

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

Goal state before:
pp: case pos.zero
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
H : ¬Algebra.IsSeparable K L
p : ℕ
hp : ExpChar K p
this : p ≠ 0
h₀ : FiniteDimensional K L
x : ↥(separableClosure K L)
hn : Algebra.IsSeparable K L
⊢ (trace K ↥(separableClosure K L)) (finrank (↥(separableClosure K L)) L • x) =
    0 ((algebraMap (↥(separableClosure K L)) L) x)

Tactic:
cases H hn

Goal state after: