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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).IsBase (f '' M.E \ f '' B) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)

Tactic:
← hf.image_sdiff_subset hB,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ ((M.map f hf).IsBase (f '' (M.E \ B)) ∧ ∃ u ⊆ M.E, f '' u = f '' B) ↔ (M✶.map f hf).IsBase (f '' B)
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
x : α
B : Set α
hB : M.IsBase B
hxE : x ∈ M.E
hxB : x ∉ B
⊢ x ∈ M.closure B

Tactic:
hB.closure_eq

Goal state after:
α : Type u_1
M : Matroid α
x : α
B : Set α
hB : M.IsBase B
hxE : x ∈ M.E
hxB : x ∉ B
⊢ x ∈ M.E
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:
restrictSubtype

Goal state after:
α : 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 ↾ X).comap Subtype.val).Finitary
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:
restrictSubtype

Goal state after:
α : 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 ↾ X).comap Subtype.val).RankFinite
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ (C : Set α), M₁.IsCircuit C ↔ M₂.IsCircuit C

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
⊢ M.eRk X ≤ n ↔ ∀ ⦃I : Set α⦄, I ⊆ X → M.Indep I → I.encard ≤ n

Tactic:
by
  refine ⟨fun h I hIX hI ↦ (hI.eRk_eq_encard.symm.trans_le ((M.eRk_mono hIX).trans h)), fun h ↦ ?_⟩
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.encard_eq_eRk]
  exact h hI.subset hI.indep

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

Goal state before:
pp: case inr.inr
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
x : α
hf : M.IsNonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep ({e, x} \ {x})

Tactic:
pair_sdiff_right hne,

Goal state after:
case inr.inr
α : Type u_1
M : Matroid α
e : α
he : M.IsNonloop e
x : α
hf : M.IsNonloop x
hne : e ≠ x
hi : ¬M.Indep {e, x}
⊢ M.Indep {e}
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hIfin : I.Finite
x✝ : I ⊆ X ∧ M.Indep I ∧ I.encard = M.eRk X
hIX : I ⊆ X
hI : M.Indep I
hcard : I.encard = M.eRk X
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsBasis' I X

Tactic:
rwa [hIfin.eq_of_subset_of_encard_le hIJ (hJ.encard_eq_eRk.trans hcard.symm).le]

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), ↑i ∈ C₀

pp: case refine_3
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), ↑i ∈ C ↑i

pp: case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ ⦃i i' : ↑X⦄, ↑i ∈ C ↑i' → i = i'

pp: case refine_5
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), z ∉ C ↑i

Tactic:
· simpa using fun e heX ↦ hXC₀ heX

Goal state after:
case refine_3
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), ↑i ∈ C ↑i

case refine_4
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ ⦃i i' : ↑X⦄, ↑i ∈ C ↑i' → i = i'

case refine_5
α : Type u_1
M : Matroid α
C₀ : Set α
hC₀ : M.IsCircuit C₀
X : Set α
S : Set (Set α)
z : α
hCS : ∀ C ∈ S, M.IsCircuit C
hXC₀ : X ⊆ C₀
hzC₀ : z ∈ C₀
hz : ∀ C ∈ S, z ∉ C
C : α → Set α
hC : (∀ x ∈ X, C x ∈ S) ∧ ∀ x ∈ X, C x ∩ X = {x}
⊢ ∀ (i : ↑X), z ∉ C ↑i
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
B : Set α
hB : M.IsBasis B X
⊢ M.eRank ≤ M.eRk X

Tactic:
by
    rw [← hB.encard_eq_eRk, ← (hB.isBase_of_spanning hX).encard_eq_eRank]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
⊢ M.closure B = M.E

Tactic:
hB.closure_eq

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
h : B = ∅
hB : M.IsBase B
⊢ M.E = M.E
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
x✝ : M.eRank = 0 ∧ M.E = X
h : M.eRank = 0
h' : M.E = X
⊢ M = loopyOn X

Tactic:
by rw [← h', ← eRank_eq_zero_iff, h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E \ M.closure (B \ {e})
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.Spanning (M.E \ X)

Tactic:
subset_sdiff

Goal state after:
α : Type u_1
M : Matroid α
e : α
B : Set α
hB : M.IsBase B
he : e ∈ B
hB' : Minimal M.Spanning B
X : Set α
hX : ¬M.Spanning (M.E \ X)
hXss : X ⊆ M.E ∧ Disjoint X (M.closure (B \ {e}))
f : α
hf : f ∈ M.E \ X
fcl : f ∉ M.closure (B \ {e})
⊢ M.Spanning (M.E \ X)
Module: Mathlib.RingTheory.Algebraic.MvPolynomial

Goal state before:
pp: case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ C x✝¹ = C x✝

Tactic:
← MvPolynomial.algebraMap_eq

Goal state after:
case refine_2
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Nontrivial R
i : σ
s : Set σ
f : R[X]
h : Transcendental (↥(supported R s)) ((Polynomial.aeval (X i)) f)
x✝¹ x✝ : R
heq : (algebraMap R ↥(supported R s)) x✝¹ = (algebraMap R ↥(supported R s)) x✝
⊢ (algebraMap R (MvPolynomial σ R)) x✝¹ = (algebraMap R (MvPolynomial σ R)) x✝
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case inr.inl
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : e ∈ M.fundCocircuit f B
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∉ M.E
⊢ f ∈ M.fundCircuit e B

Tactic:
rw [fundCocircuit, fundCircuit_eq_of_notMem_ground (by simpa)] at he
    contradiction

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ e ∈ M.closure B

Tactic:
hB.closure_eq

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
e f : α
he : M✶.Indep (insert f (M✶.E \ B) \ {e})
hne : e ≠ f
hB' : M✶.IsBase (M✶.E \ B)
hfE : f ∈ M.E
hfB : f ∈ B
heE : e ∈ M.E
heB : e ∉ B
⊢ e ∈ M.E
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : (expand F (q ^ m)) g = (expand F (q ^ (m + s))) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree

Tactic:
rw [pow_add, expand_mul, expand_inj (pow_pos (NeZero.pos q) m)] at h_expand

Goal state after:
F✝ : Type u_1
inst✝² : Field F✝
q✝ : ℕ
F : Type u_1
inst✝¹ : Field F
q : ℕ
hq : NeZero q
inst✝ : CharP F q
g g' : F[X]
m : ℕ
hg : g.Separable
hg' : g'.Separable
s : ℕ
h_expand : g = (expand F (q ^ s)) g'
hm : m ≤ m + s
⊢ g.natDegree = g'.natDegree
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: 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

Tactic:
rcases hg with ⟨hg, m, hm⟩
    let g' := Classical.choose hf
    obtain ⟨hg', m', hm'⟩ := Classical.choose_spec hf
    have : Fact q.Prime := ⟨by assumption⟩
    refine contraction_degree_eq_or_insep q g g' m m' ?_ hg hg'
    rw [hm, hm']

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

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
⊢ h • fixedBy α g = fixedBy α (h * g * h⁻¹)

Tactic:
ext a

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g h : G
a : α
⊢ a ∈ h • fixedBy α g ↔ a ∈ fixedBy α (h * g * h⁻¹)
Module: Mathlib.GroupTheory.GroupAction.FixedPoints

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
⊢ s ∈ fixedBy (Set α) g⁻¹

Tactic:
ext a

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ a ∈ g⁻¹ • s ↔ a ∈ s
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : IsSplittingField F E p
hp : p.Separable
⊢ Algebra.IsSeparable F ↥⊤

Tactic:
← (isSplittingField_iff_intermediateField.mp sp).2,

Goal state after:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
sp : IsSplittingField F E p
hp : p.Separable
⊢ Algebra.IsSeparable F ↥(IntermediateField.adjoin F (p.rootSet E))
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
⊢ ((UniqueFactorizationMonoid.factors f).prod * ↑u).Splits

Tactic:
refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits

Goal state after:
case refine_1
F : Type u_1
inst✝ : Field F
x✝ : PerfectField F
f : F[X]
hf : f.natSepDegree = 1
h : ∀ {f : F[X]}, Irreducible f → f.Separable
hf0 : f ≠ 0
u : F[X]ˣ
hu : (UniqueFactorizationMonoid.factors f).prod * ↑u = f
g : F[X]
hg : g ∈ UniqueFactorizationMonoid.factors f
⊢ g.Splits
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h✝ : ExpChar F p
x y : F
hy : eval y (X ^ p - C x) = 0
⊢ (frobenius F p) y = x

Tactic:
eval_sub,

Goal state after:
F : Type u_1
inst✝ : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h✝ : ExpChar F p
x y : F
hy : eval y (X ^ p) - eval y (C x) = 0
⊢ (frobenius F p) y = x
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
⊢ ¬σ (g y) = y

Tactic:
have : g y = y := (mem_fixingSubgroup_iff Gal(K/k)).mp hg y <|
        adjoin_simple_le_iff.mp le_rfl

Goal state after:
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
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ¬IsIntegral R x
⊢ minpolyDiv R x = 0

Tactic:
by
  delta minpolyDiv minpoly
  rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]

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✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
p : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬a * b = 0

Tactic:
← hab

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 : R[X]
hp : p.IsPrimitive
hi : Irreducible p
a b : K[X]
hab : map (algebraMap R K) p = a * b
c : R
c0 : c ≠ 0
hc : map (algebraMap R K) (integerNormalization R⁰ a) = C ((algebraMap R K) c) * a
d : R
d0 : d ≠ 0
hd : map (algebraMap R K) (integerNormalization R⁰ b) = C ((algebraMap R K) d) * b
hcd0 : ¬C (c * d) = 0
this : NormalizedGCDMonoid R
u : Rˣ
h1 : C (c * d) * (C ↑u * (integerNormalization R⁰ b).primPart * (integerNormalization R⁰ a).primPart) = C (c * d) * p
hu : c * d * ↑u = (integerNormalization R⁰ a).content * (integerNormalization R⁰ b).content
⊢ ¬map (algebraMap R K) p = 0
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
⊢ IsPurelyInseparable F E ↔ Subsingleton (Emb F E)

Tactic:
rw [isPurelyInseparable_iff_finSepDegree_eq_one, Field.finSepDegree, Nat.card_eq_one_iff_unique,
    and_iff_left_iff_imp]
  infer_instance

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)) = lift ⊤
⊢ adjoin E ↑(separableClosure F K) = S

Tactic:
rw [lift_top, lift_adjoin] at 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
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.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
⊢ adjoin E ↑(separableClosure F K) = separableClosure E K

Tactic:
by
  set S := separableClosure E K
  have h := congr_arg lift (adjoin_eq_of_isAlgebraic_of_isSeparable (F := F) S)
  rw [lift_top, lift_adjoin] at h
  have : IsScalarTower F S K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
  rw [← h, ← map_eq_of_separableClosure_eq_bot F (separableClosure_eq_bot E K)]
  simp only [S, coe_map, IsScalarTower.coe_toAlgHom', IntermediateField.algebraMap_apply]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: 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✝⁴ : FiniteDimensional K L
inst✝³ : Algebra.IsSeparable K L
ι : Type u_5
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (b i)
inst✝ : IsIntegrallyClosed A
⊢ (↑A (Algebra.linearMap C L)).range ≤ Submodule.span A (Set.range ⇑((traceForm K L).dualBasis ⋯ b))

Tactic:
← LinearMap.BilinForm.dualSubmodule_span_of_basis,

Goal state after:
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✝⁴ : FiniteDimensional K L
inst✝³ : Algebra.IsSeparable K L
ι : Type u_5
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
b : Basis ι K L
hb_int : ∀ (i : ι), IsIntegral A (b i)
inst✝ : IsIntegrallyClosed A
⊢ (↑A (Algebra.linearMap C L)).range ≤ (traceForm K L).dualSubmodule (Submodule.span A (Set.range ⇑b))
Module: Mathlib.FieldTheory.PurelyInseparable.Basic

Goal state before:
pp: case h
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : (algebraMap k K) a = y ^ q ^ n
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = (x ^ q ^ n) ⊗ₜ[k] 1 * 1 ⊗ₜ[k] (y ^ q ^ n)
⊢ x ⊗ₜ[k] y ^ q ^ n ∈ (algebraMap R (R ⊗[k] K)).range

Tactic:
rw [Algebra.TensorProduct.tmul_pow, this]

Goal state after:
case h
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁶ : Field k
inst✝⁵ : Field K
inst✝⁴ : Algebra k K
inst✝³ : CommRing R
inst✝² : Algebra k R
inst✝¹ : IsPurelyInseparable k K
q : ℕ
inst✝ : ExpChar k q
a✝ : Nontrivial (R ⊗[k] K)
hq : Nat.Prime q
x : R
y : K
n : ℕ
a : k
ha : (algebraMap k K) a = y ^ q ^ n
this : (x ^ q ^ n) ⊗ₜ[k] (y ^ q ^ n) = (x ^ q ^ n) ⊗ₜ[k] 1 * 1 ⊗ₜ[k] (y ^ q ^ n)
⊢ (x ^ q ^ n) ⊗ₜ[k] 1 * 1 ⊗ₜ[k] (y ^ q ^ n) ∈ (algebraMap R (R ⊗[k] K)).range
Module: Mathlib.RingTheory.DedekindDomain.IntegralClosure

Goal state before:
pp: 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✝⁴ : FiniteDimensional K L
inst✝³ : IsDomain A
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsPrincipalIdealRing A
inst✝ : IsTorsionFree A L
this✝¹ : Free A C
this✝ : IsNoetherian A C
this : IsLocalization (algebraMapSubmonoid C A⁰) L
b : Basis (Free.ChooseBasisIndex A C) K L := Basis.localizationLocalization K A⁰ L (Free.chooseBasis A C)
⊢ finrank A C = finrank K L

Tactic:
rw [Module.finrank_eq_card_chooseBasisIndex, Module.finrank_eq_card_basis b]

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

Goal state before:
pp: B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b (X - C b) = 0

Tactic:
eval_sub,

Goal state after:
B : Type u_2
G : Type u_3
inst✝³ : CommRing B
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : Fintype G
b : B
⊢ eval b X - eval b (C b) = 0
Module: Mathlib.RingTheory.Invariant.Basic

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : eval b (X - C b) ^ i * eval b X ^ j = eval b (X - C (↑↑f b)) ^ i * eval b X ^ j
⊢ f b = b

Tactic:
eval_sub,

Goal state after:
case neg
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : NoZeroDivisors B
b : B
i j : ℕ
p : A[X]
h : map (algebraMap A B) p = (X - C b) ^ i * X ^ j
f : B ≃ₐ[A] B
hi : i ≠ 0
ha : ¬b = 0
hf : (eval b X - eval b (C b)) ^ i * eval b X ^ j = (eval b X - eval b (C (↑↑f b))) ^ i * eval b X ^ j
⊢ f b = b
Module: Mathlib.RingTheory.Trace.Basic

Goal state before:
pp: case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ finrank K L = pb.dim

Tactic:
pb.finrank

Goal state after:
case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ pb.dim = pb.dim
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
i : ℕ
x : Kˣ
hx : ∀ (x_1 : Kˣ), x_1 ∈ Subgroup.zpowers x
⊢ x ^ i = 1 → ∀ (x : Kˣ), x ^ i = 1

Tactic:
· intro h y
    simp_rw [← mem_powers_iff_mem_zpowers] at hx
    rcases hx y with ⟨j, rfl⟩
    rw [← pow_mul, mul_comm, pow_mul, h, one_pow]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
⊢ X ^ q ^ m - X ≠ 0 ∧ eval x (X ^ q ^ m - X) = 0

Tactic:
eval_sub,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : Fintype K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Finite L
this : Fintype L
m : ℕ
lt : m < Module.finrank K L
pos : 0 < m
eq : frobeniusAlgHom K L ^ m = 1
x : L
x✝ : x ∈ univ.val
⊢ X ^ q ^ m - X ≠ 0 ∧ eval x (X ^ q ^ m) - eval x X = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ eval x (X ^ q - X) = 0

Tactic:
eval_sub,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
aux : X ^ q - X ≠ 0
x : K
⊢ eval x (X ^ q) - eval x X = 0
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ frobenius (ZMod p) p = RingHom.id (ZMod p)

Tactic:
ext a

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ (frobenius (ZMod p) p) a = (RingHom.id (ZMod p)) a
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: S : Type u_1
inst✝³ : CommRing S
inst✝² : IsDedekindDomain S
inst✝¹ : Free ℤ S
inst✝ : Module.Finite ℤ S
n : ℕ
⊢ absNorm (span {↑n}) = n ^ finrank ℤ S

Tactic:
simp [absNorm_span_singleton, Algebra.norm_natCast]

Goal state after:
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ Submonoid.map (algebraMap R S) M ≤ IsUnit.submonoid S

Tactic:
by
  rintro _ ⟨a, ha, rfl⟩
  exact IsLocalization.map_units S ⟨_, ha⟩

Goal state after: