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

Goal state before:
pp: R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
⊢ map (⊤.mulMap ↑I) ⊤ = ⊤

Tactic:
map_top,

Goal state after:
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq✝ : ∀ (i : ↥S), a i * b i = ↑i
f : ↥↑I →ₗ[R] ↥S → R :=
  LinearMap.pi fun i ↦
    ↑(LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯).symm ∘ₗ (LinearMap.mulRight R (r ↑i • a i)).restrict ⋯
hf : ∀ (x : ↥↑I) (i : ↥S), (algebraMap R A) (f x i) = ↑x * r ↑i • a i
g : (↥S → R) →ₗ[R] ↥↑I := (lsum R (fun a ↦ R) ℕ) fun i ↦ toSpanSingleton R ↥↑I ⟨b i, ⋯⟩
hgf : g ∘ₗ f = LinearMap.id
m : A ⊗[R] ↥↑I →ₗ[R] A := mul' R A ∘ₗ lTensor A (↑I).subtype
eq : ↑(piScalarRight R R A ↥S) ∘ₗ lTensor A f = (LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ₗ m
this : Function.Injective (⇑(LinearMap.pi fun i ↦ LinearMap.mulRight R (r ↑i • a i)) ∘ ⇑m)
⊢ (⊤.mulMap ↑I).range = ⊤
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B' I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
⊢ False

Tactic:
obtain ⟨B', hB', hI₀B'⟩ := (hI _ hI₀I hI₀fin).exists_isBase_superset

Goal state after:
α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (X ∩ M.E)

Tactic:
by
  rw [IsBasis', IsBasis, and_iff_left inter_subset_right, maximal_iff_maximal_of_imp_of_forall]
  · exact fun I hI ↦ ⟨hI.1, hI.2.trans inter_subset_left⟩
  exact fun I hI ↦ ⟨I, rfl.le, hI.1, subset_inter hI.2 hI.1.subset_ground⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis' J X ∧ I ⊆ J

Tactic:
isBasis'_iff_isBasis_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
⊢ ∃ J, M.IsBasis J (X ∩ M.E) ∧ I ⊆ J
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
hI : M.Indep I
⊢ M.IsBasis I {x | M.IsBasis I (insert x I)}

Tactic:
by
  refine hI.isBasis_of_forall_insert (fun e he ↦ (?_ : M.IsBasis _ _))
    (fun e he ↦ ⟨fun hu ↦ he.2 ?_, he.1.subset_ground⟩)
  · rw [insert_eq_of_mem he]; exact hI.isBasis_self
  simpa using (hu.eq_of_isBasis he.1).symm

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis' I R
hI' : M.IsBasis' I' R
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
isBasis'_iff_isBasis_inter_ground

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R I I' : Set α
hI : M.Indep I
hIY : I ⊆ R
hIn : ¬M.IsBasis I (R ∩ M.E)
hI' : M.IsBasis I' (R ∩ M.E)
⊢ ∃ x ∈ I' \ I, M.Indep (insert x I) ∧ insert x I ⊆ R
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : B = E \ I
⊢ E \ B = I ∩ E

Tactic:
by rw [h, inter_comm I]; simp

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
⊢ N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X

Tactic:
refine ⟨hI.isBasis_of_forall_insert (image_mono h.subset) fun e he ↦ ?_, hinj, h.subset⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : (N.comap f).IsBasis I X
hI : N.Indep (f '' I)
hinj : InjOn f I
e : β
he : e ∈ f '' X \ f '' I
⊢ N.Dep (insert e (f '' I))
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ (N.comapOn E f).IsBase ((N.comapOn E f).E \ B) ↔ N✶.IsBase (f '' B) ∧ B ⊆ E

Tactic:
comapOn_isBase_iff_of_bijOn h,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ N.IsBase (f '' ((N.comapOn E f).E \ B)) ∧ (N.comapOn E f).E \ B ⊆ E ↔ N✶.IsBase (f '' B) ∧ B ⊆ E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
⊢ M.IsBasis I X

Tactic:
obtain ⟨I', hI', hII'⟩ := map_indep_iff.1 h.indep

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid α
I X : Set α
f : α → β
hf : InjOn f M.E
hI : I ⊆ M.E
hX : X ⊆ M.E
h : (M.map f hf).IsBasis (f '' I) (f '' X)
I' : Set α
hI' : M.Indep I'
hII' : f '' I = f '' I'
⊢ M.IsBasis I X
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis' (Subtype.val '' I) (Subtype.val '' X)

pp: α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X

Tactic:
isBasis'_iff_isBasis_inter_ground

Goal state after:
α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ M.IsBasis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.IsBasis (Subtype.val '' I) (Subtype.val '' X ∩ M.E)

α : Type u_1
M : Matroid α
Y : Set α
I X : Set ↑Y
⊢ (M ↾ Y).IsBasis ↑I ↑X → I ⊆ X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
⊢ M.IsNonloop e

Tactic:
by
  rw [← not_isLoop_iff (hK.subset_ground he), ← singleton_isCircuit]
  intro he'
  obtain ⟨f, ⟨rfl, -⟩, hfe⟩ := (he'.isCocircuit_inter_nontrivial hK ⟨e, by simp [he]⟩).exists_ne e
  exact hfe rfl

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

Goal state before:
pp: case refine_1
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₁.IsCircuit C
⊢ M₂.IsCircuit C

pp: case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
⊢ M₁.IsCircuit C

Tactic:
· obtain ⟨C', hC'C, hC'⟩ := ((not_indep_iff (by rwa [← hE])).1 (h₁ C hC)).exists_isCircuit_subset
    rwa [← hC.eq_of_not_indep_subset (h₂ C' hC') hC'C]

Goal state after:
case refine_2
α : Type u_1
M₁ M₂ : Matroid α
hE : M₁.E = M₂.E
h₁ : ∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C
h₂ : ∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C
C : Set α
hCE : C ⊆ M₁.E
hC : M₂.IsCircuit C
⊢ M₁.IsCircuit C
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ I.encard ≤ M.eRk X

Tactic:
← hI.eRk_eq_encard

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
x✝ : ∃ I ⊆ X, M.Indep I ∧ I.encard = n
I : Set α
hIX : I ⊆ X
hI : M.Indep I
hIc : I.encard = n
⊢ M.eRk I ≤ M.eRk X
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
I : Set α
h : I = ∅ ∨ ∃ x, I = {x}
hI : M.IsBasis I X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

Tactic:
obtain (rfl | ⟨e, rfl⟩) := h

Goal state after:
case refine_1.inl
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
hI : M.IsBasis ∅ X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}

case refine_1.inr
α : Type u_1
M : Matroid α
X : Set α
inst✝ : M.Nonempty
hX : X ⊆ M.E
e : α
hI : M.IsBasis {e} X
⊢ ∃ e ∈ M.E, X ⊆ M.closure {e}
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
aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
obtain ⟨T, hT, hTfin, hXT⟩ := aux

Goal state after:
α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
T : Set α
hT : T ⊆ Y
hTfin : T.Finite
hXT : X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I

Tactic:
exact hI.not_dep

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ (∃ x ∈ M.E, M.IsLoop x) ↔ ∃ x, M.IsCircuit x ∧ x.Subsingleton

Tactic:
refine ⟨fun ⟨e, _, he⟩ ↦ ⟨{e}, he.isCircuit, by simp⟩, fun ⟨C, hC, hCs⟩ ↦ ?_⟩

Goal state after:
α : Type u_1
M : Matroid α
x✝ : ∃ x, M.IsCircuit x ∧ x.Subsingleton
C : Set α
hC : M.IsCircuit C
hCs : C.Subsingleton
⊢ ∃ x ∈ M.E, M.IsLoop x
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
B : Set α
⊢ M.IsBasis B M.E ↔ M.Indep B ∧ M.closure B = M.E

Tactic:
isBasis_iff_indep_subset_closure,

Goal state after:
α : Type u_2
M : Matroid α
B : Set α
⊢ M.Indep B ∧ B ⊆ M.E ∧ M.E ⊆ M.closure B ↔ M.Indep B ∧ M.closure B = M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.Spanning (M.E \ K)

Tactic:
spanning_iff_ground_subset_closure

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
e : α
K : Set α
hC : M.IsCircuit C
he : C ∩ K = {e}
heC : e ∈ C
hK : ¬M.Spanning (M.E \ K) ∧ ∀ ⦃t : Set α⦄, t ⊂ K → M.Spanning (M.E \ t)
hKe : M.Spanning (M.E \ (K \ {e}))
⊢ M.E ⊆ M.closure (M.E \ K)
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
this : Transcendental (↥(supported R ∅)) ((Polynomial.aeval (X i)) f)
g : R ≃ₐ[R] ↥(supported R ∅) := (Algebra.botEquivOfInjective ⋯).symm.trans ((supported R ∅).equivOfEq ⊥ ⋯).symm
⊢ (algebraMap (↥(supported R ∅)) (MvPolynomial σ R)).comp ↑g =
    (↑(RingHom.id (MvPolynomial σ R))).comp (algebraMap R (MvPolynomial σ R))

Tactic:
ext1; rfl

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis' I X ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X

Tactic:
isBasis'_iff_isBasis_inter_ground

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I (M.closure (X ∩ M.E)) ∧ I ⊆ X
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
s : Set ι
i : ι
h : i ∉ s
⊢ AlgebraicIndepOn R x (insert i s) ↔ AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)

Tactic:
← algebraicIndependent_equiv (subtypeInsertEquivOption h).symm,

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
s : Set ι
i : ι
h : i ∉ s
⊢ AlgebraicIndependent R ((fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm) ↔
    AlgebraicIndepOn R x s ∧ Transcendental (↥(adjoin R (x '' s))) (x i)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: case refine_1
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
heE : e ∉ M.E
⊢ M.closure (I \ {e}) = M.closure I

pp: case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I

Tactic:
· rw [← closure_inter_ground, inter_comm, inter_sdiff_distrib_left,
      inter_singleton_eq_empty.mpr heE, sdiff_empty, inter_comm, closure_inter_ground]

Goal state after:
case refine_2
α : Type u_2
M : Matroid α
I : Set α
h : ∀ ⦃e : α⦄, e ∈ I → M.closure (I \ {e}) ≠ M.closure I
e : α
heI : e ∈ I
hin : e ∈ M.closure (I \ {e})
⊢ M.closure (I \ {e}) = M.closure I
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: ι : Type u_1
R : Type u_3
inst✝ : CommRing R
f : ι → Polynomial R
hf : ∀ (i : ι), Transcendental R (f i)
x : ι → MvPolynomial ι R := fun i ↦ (Polynomial.aeval (X i)) (f i)
t : Set ι
x✝¹ : t.Finite
x✝ : AlgebraicIndependent R fun i ↦ x ↑i
i : ι
hi : i ∉ t
a✝ : ι
h : a✝ ∈ t
⊢ {X a✝} ⊆ X '' t

Tactic:
simp_rw [singleton_subset_iff, Set.mem_image_of_mem _ h]

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 α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ x ∈ g⁻¹ • s ↔ x ∈ s

Tactic:
rw [Set.mem_inv_smul_set_iff]

Goal state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
s_ss_fixedBy : s ⊆ fixedBy α g
x : α
⊢ g • x ∈ s ↔ x ∈ s
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
⊢ ∃ s, IsTranscendenceBasis R Subtype.val

Tactic:
by
  simpa using exists_isTranscendenceBasis_superset
    ((algebraicIndependent_empty_iff R A).mpr (FaithfulSMul.algebraMap_injective R A))

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 α
s : Set α
g : G
s_subset : (fixedBy α g)ᶜ ⊆ s
a : α
⊢ a ∈ g⁻¹ • s ↔ a ∈ s

Tactic:
rw [Set.mem_inv_smul_set_iff]

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 : α
⊢ g • a ∈ s ↔ a ∈ s
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (f.aroots f.SplittingField).toFinset ≠ ∅

Tactic:
← Finset.nonempty_iff_ne_empty

Goal state after:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree ≠ 0
⊢ (f.aroots f.SplittingField).toFinset.Nonempty
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
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

Goal state after:
Module: Mathlib.FieldTheory.KrullTopology

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g

Tactic:
let φ := f⁻¹ * g

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsIntegral K L
f g : Gal(L/K)
hfg : f ≠ g
φ : Gal(L/K) := f⁻¹ * g
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) f g
Module: Mathlib.LinearAlgebra.BilinearForm.DualLattice

Goal state before:
pp: 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 ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
i : ι
r : R
hr : (algebraMap R S) r = (B x) (b i)
⊢ r • (B.dualBasis hB b) i ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Tactic:
apply Submodule.smul_mem

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 ι
x : M
hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))
i : ι
r : R
hr : (algebraMap R S) r = (B x) (b i)
⊢ (B.dualBasis hB b) i ∈ Submodule.span R (Set.range ⇑(B.dualBasis hB b))
Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
⊢ IsIntegral R s ↔ C p.leadingCoeff ∣ p

Tactic:
refine ⟨fun hInt ↦ ?_, fun ⟨q, hMul⟩ ↦ minpoly.ne_zero_iff.mp ?_⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
hInt : IsIntegral R s
⊢ C p.leadingCoeff ∣ p

case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
s : S
p : R[X]
hp : (Polynomial.aeval s) p = 0
h₀ : p ≠ 0
pmin : ∀ (q : R[X]), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree
x✝ : C p.leadingCoeff ∣ p
q : R[X]
hMul : p = C p.leadingCoeff * q
⊢ minpoly R s ≠ 0
Module: Mathlib.FieldTheory.Minpoly.MinpolyDiv

Goal state before:
pp: case succ.refine_1
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
⊢ (minpoly R x).coeff ((minpolyDiv R x).natDegree - (i + 1) + 1) • 1 ∈
    Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))

Tactic:
apply Submodule.smul_mem

Goal state after:
case succ.refine_1
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
⊢ 1 ∈ Submodule.span R ((fun x_1 ↦ x ^ x_1) '' Set.Iio (i + 1))
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 := ⋯
φ τ : Gal(K/k)
hτ : τ ∈ L'.fixingSubgroup.carrier
muleq : (fun x ↦ σ • x) τ = φ
sub' : σ • b ⊆ (↑H).carrierᶜ
⊢ τ ∈ L.fixingSubgroup.carrier

Tactic:
exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ)

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: K : Type v
inst✝² : Field K
k : Type u_1
inst✝¹ : CommSemiring k
inst✝ : IsSepClosed K
f : k →+* K
hf : Function.Injective ⇑f
p : k[X]
hp : p.degree ≠ 0
hsep : p.Separable
⊢ (map f p).degree ≠ 0

Tactic:
rwa [degree_map_eq_of_injective hf]

Goal state after:
Module: Mathlib.FieldTheory.IsSepClosed

Goal state before:
pp: k : Type u
inst✝⁵ : Field k
K : Type v
inst✝⁴ : Field K
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Normal F E
⊢ Normal F ↥(IntermediateField.normalClosure F (↥(separableClosure F E)) E)

Tactic:
exact normalClosure.normal F _ E

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

Goal state before:
pp: K : Type u_2
L : Type u_3
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_1
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : IsAlgClosed E
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
x : L
hxL : K[x] = ⊤
r : ℕ
hr : r < finrank K L
⊢ ∑ σ, map (↑σ) ((x ^ r / (aeval x) (derivative (minpoly K x))) • minpolyDiv K x) = X ^ r

Tactic:
by
  classical
  rw [← sub_eq_zero]
  have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h =>
    AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h)
  apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this
  · intro σ
    simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, eval_sub, eval_finsetSum,
      eval_smul, eval_map, eval₂_minpolyDiv_self, this.eq_iff, smul_eq_mul, mul_ite, mul_zero,
      Finset.sum_ite_eq', Finset.mem_univ, ite_true, eval_X_pow]
    rw [sub_eq_zero, div_mul_cancel₀]
    rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]
    exact (IsSeparable.isSeparable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
  · refine (Polynomial.natDegree_sub_le _ _).trans_lt
      (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)
    · simp only [Polynomial.map_smul,
        map_div₀, map_pow, RingHom.coe_coe, Function.comp_apply,
        Finset.mem_univ, forall_true_left, Finset.fold_max_lt, AlgHom.card]
      refine ⟨finrank_pos, ?_⟩
      intro σ
      exact ((Polynomial.natDegree_smul_le _ _).trans natDegree_map_le).trans_lt
        ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.isIntegral x)).trans_le
          (minpoly.natDegree_le _))
    · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]

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
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
⊢ IsSepClosed F

Tactic:
have := IsAlgClosure.isAlgClosed F (K := E)

Goal state after:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : IsAlgClosure F E
H : IsPurelyInseparable F E
this : IsAlgClosed E
⊢ IsSepClosed F