mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: case succ
A : Type u
inst✝³ : CommRing A
inst✝² : IsNoetherianRing A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x✝ : Module.Finite A M
motive : (N : Type v) → [inst : AddCommGroup N] → [inst_1 : Module A N] → [Module.Finite A N] → Prop
subsingleton :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] [Subsingleton N], motive N
quotient :
  ∀ (N : Type v) [inst : AddCommGroup N] [inst_1 : Module A N] [inst_2 : Module.Finite A N] (p : PrimeSpectrum A)
    (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N
exact :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (N₃ : Type v)
    [inst_6 : AddCommGroup N₃] [inst_7 : Module A N₃] [inst_8 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂) (g : N₂ →ₗ[A] N₃),
    Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂
equiv :
  ∀ (N₁ : Type v) [inst : AddCommGroup N₁] [inst_1 : Module A N₁] [inst_2 : Module.Finite A N₁] (N₂ : Type v)
    [inst_3 : AddCommGroup N₂] [inst_4 : Module A N₂] [inst_5 : Module.Finite A N₂] (f : N₁ ≃ₗ[A] N₂),
    motive N₁ → motive N₂
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs1 : s.head = ⊥
hs2 : s.last = ⊤
n : ℕ
h : n + 1 < s.length + 1
hle : s.toFun ⟨n, ⋯⟩.castSucc ≤ s.toFun ⟨n, ⋯⟩.succ
p : PrimeSpectrum A
f : (↥(s.toFun ⟨n, ⋯⟩.succ) ⧸ (s.toFun ⟨n, ⋯⟩.castSucc).submoduleOf (s.toFun ⟨n, ⋯⟩.succ)) ≃ₗ[A] A ⧸ p.asIdeal
ih : motive ↥((s.toFun ⟨n, ⋯⟩.castSucc).submoduleOf (s.toFun ⟨n, ⋯⟩.succ))
⊢ motive ↥(s.toFun ⟨n + 1, h⟩)

Tactic:
exact exact _ _ _ _ _ (Submodule.injective_subtype _) (Submodule.mkQ_surjective _)
      (LinearMap.exact_subtype_mkQ _) ih (quotient _ p f)

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: case mpr
R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f✝ : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f✝ ∘ₗ g = id
I : Ideal R
hI : I.IsMaximal
this :
  id ∈
    ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
          (LocalizedModule I.primeCompl N))
        ((LocalizedModule.map I.primeCompl) f✝)).range
f : LocalizedModule I.primeCompl N →ₗ[Localization I.primeCompl] LocalizedModule I.primeCompl N
⊢ f ∈
      ((llcomp (Localization I.primeCompl) (LocalizedModule I.primeCompl N) (LocalizedModule I.primeCompl M)
            (LocalizedModule I.primeCompl N))
          ((LocalizedModule.map I.primeCompl) f✝)).range →
    f ∈ Submodule.localized₀ I.primeCompl (LocalizedModule.map I.primeCompl) ((llcomp R N M N) f✝).range

Tactic:
· rintro ⟨g, rfl⟩
      obtain ⟨⟨g, s⟩, rfl⟩ :=
        IsLocalizedModule.mk'_surjective I.primeCompl (LocalizedModule.map I.primeCompl) g
      simp only [Function.uncurry_apply_pair]
      refine ⟨f.comp g, ⟨g, rfl⟩, s, ?_⟩
      apply ((Module.End.isUnit_iff _).mp <| IsLocalizedModule.map_units
         (LocalizedModule.map I.primeCompl) s).injective
      simp only [Module.algebraMap_end_apply, ← Submonoid.smul_def, IsLocalizedModule.mk'_cancel',
        ← LinearMap.map_smul_of_tower]
      apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.ext I.primeCompl (LocalizedModule.mkLinearMap I.primeCompl N)
      · exact IsLocalizedModule.map_units (LocalizedModule.mkLinearMap I.primeCompl N)
      ext
      simp only [coe_comp, coe_restrictScalars, Function.comp_apply,
        LocalizedModule.mkLinearMap_apply, LocalizedModule.map_mk, llcomp_apply]

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_2
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsOpen[inst✝¹] ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})

Tactic:
← isClosed_compl_iff

Goal state after:
case refine_2
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsClosed[inst✝¹] ((fun x ↦ if x ∈ U then 0 else 1) ⁻¹' {1})ᶜ
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ map H.subtype ⁅⊤, ⊤⁆ = map ⁅H, H⁆.subtype ⊤

Tactic:
map_commutator,

Goal state after:
case h.zero
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = map ⁅H, H⁆.subtype ⊤
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ map H.subtype ⁅derivedSeries (↥H) (n + 1), derivedSeries (↥H) (n + 1)⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))

Tactic:
map_commutator,

Goal state after:
case h.succ
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
ih : map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
⊢ ⁅map H.subtype (derivedSeries (↥H) (n + 1)), map H.subtype (derivedSeries (↥H) (n + 1))⁆ =
    map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) (n + 1))
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
p q : PrimeSpectrum R
hpq : p ≤ q
S : Type uR := Localization.AtPrime q.asIdeal
⊢ rankAtStalk M p = rankAtStalk M q

Tactic:
obtain ⟨P, rfl⟩ : p ∈ Set.range (PrimeSpectrum.comap (algebraMap R S)) := by
    rw [PrimeSpectrum.localization_comap_range S q.asIdeal.primeCompl]
    exact disjoint_compl_left_iff.mpr hpq

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Flat R M
inst✝ : Module.Finite R M
q : PrimeSpectrum R
S : Type uR := Localization.AtPrime q.asIdeal
P : PrimeSpectrum S
hpq : comap (algebraMap R S) P ≤ q
⊢ rankAtStalk M (comap (algebraMap R S) P) = rankAtStalk M q
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: K : Type u_6
L : Type u_7
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Normal K L
x y : L
hy : IsAlgebraic K y
h_ev : (Polynomial.aeval x) (minpoly K y) = 0
⊢ ∃ σ, σ x = y

Tactic:
by
  have hx : IsAlgebraic K x := ⟨minpoly K y, ne_zero hy.isIntegral, h_ev⟩
  set f : K⟮x⟯ ≃ₐ[K] K⟮y⟯ := algEquiv hx (eq_of_root hy h_ev)
  have hxy : (liftNormal f L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = y := by
    rw [liftNormal_commutes f L, algEquiv_apply, AdjoinSimple.algebraMap_gen K y]
  exact ⟨(liftNormal f L), hxy⟩

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

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B : Set α
hB : Maximal M.Indep B ∧ B ⊆ M.E
⊢ ∃ B, Maximal M.Indep B

Tactic:
exact ⟨B, hB.1⟩

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
⊢ Finite (IntermediateField F E)

Tactic:
have := FiniteDimensional.of_exists_primitive_element F E h

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
h : ∃ α, F⟮α⟯ = ⊤
this : FiniteDimensional F E
⊢ Finite (IntermediateField F E)
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
x : Aˣ
x✝¹ x✝ : R
eq : (LinearMap.toSpanSingleton R A ↑x) x✝¹ = (LinearMap.toSpanSingleton R A ↑x) x✝
⊢ (fun r ↦ r • 1) x✝¹ = (fun r ↦ r • 1) x✝

Tactic:
by simpa using congr($eq * x.inv)

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 : Set α
⊢ ∀ ⦃I B : Set α⦄,
    M.Indep I ∧ I ⊆ R →
      ¬Maximal (fun I ↦ M.Indep I ∧ I ⊆ R) I →
        Maximal (fun I ↦ M.Indep I ∧ I ⊆ R) B → ∃ x ∈ B \ I, M.Indep (insert x I) ∧ insert x I ⊆ R

Tactic:
rintro I I' ⟨hI, hIY⟩ (hIn : ¬ M.IsBasis' I R) (hI' : M.IsBasis' I' R)
    rw [isBasis'_iff_isBasis_inter_ground] at hIn hI'
    obtain ⟨B', hB', rfl⟩ := hI'.exists_isBase
    obtain ⟨B, hB, hIB, hBIB'⟩ := hI.exists_isBase_subset_union_isBase hB'
    rw [hB'.inter_isBasis_iff_compl_inter_isBasis_dual, sdiff_inter_sdiff] at hI'
    have hss : M.E \ (B' ∪ (R ∩ M.E)) ⊆ M.E \ (B ∪ (R ∩ M.E)) := by
      apply sdiff_subset_sdiff_right
      rw [union_subset_iff, and_iff_left subset_union_right, union_comm]
      exact hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))
    have hi : M✶.Indep (M.E \ (B ∪ (R ∩ M.E))) := by
      rw [dual_indep_iff_exists]
      exact ⟨B, hB, disjoint_of_subset_right subset_union_left disjoint_sdiff_left⟩
    have h_eq := hI'.eq_of_subset_indep hi hss
      (sdiff_subset_sdiff_right subset_union_right)
    rw [h_eq, ← sdiff_inter_sdiff, ← hB.inter_isBasis_iff_compl_inter_isBasis_dual] at hI'
    obtain ⟨J, hJ, hIJ⟩ := hI.subset_isBasis_of_subset
      (subset_inter hIB (subset_inter hIY hI.subset_ground))
    obtain rfl := hI'.indep.eq_of_isBasis hJ
    have hIJ' : I ⊂ B ∩ (R ∩ M.E) := hIJ.ssubset_of_ne (fun he ↦ hIn (by rwa [he]))
    obtain ⟨e, he⟩ := exists_of_ssubset hIJ'
    exact ⟨e, ⟨⟨(hBIB' he.1.1).elim (fun h ↦ (he.2 h).elim) id,he.1.2⟩, he.2⟩,
      hI'.indep.subset (insert_subset he.1 hIJ), insert_subset he.1.2.1 hIY⟩

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

Goal state before:
pp: α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) j → Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ P K ∧ K ⊆ X) J

Tactic:
refine ⟨Y, hIY, ⟨hY, hYX⟩, fun K ⟨hPK, hKX⟩ hYK ↦ ?_⟩

Goal state after:
α : Type u_1
P : Set α → Prop
X : Set α
n : ℕ
hP : ∀ (Y : Set α), P Y → Y.encard ≤ ↑n
I : Set α
hI : P I
hIX : I ⊆ X
hfin : (ncard '' {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}).Finite
Y : Set α
hY' : ∀ ⦃j : Set α⦄, (fun x ↦ x ∈ {Y | P Y ∧ I ⊆ Y ∧ Y ⊆ X}) j → Y.ncard ≤ j.ncard → j.ncard ≤ Y.ncard
hY : P Y
hIY : I ⊆ Y
hYX : Y ⊆ X
K : Set α
x✝ : (fun K ↦ P K ∧ K ⊆ X) K
hYK : Y ⊆ K
hPK : P K
hKX : K ⊆ X
⊢ K ⊆ Y
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis' I X
hJ : M.IsBasis' J X
⊢ I.encard = J.encard

Tactic:
rw [← isBase_restrict_iff'] at hI hJ

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E ∧ I ⊆ M.E

Tactic:
and_iff_left hI.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J, e ∉ I → ¬M.Indep (insert e I) ∧ e ∈ M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hC : M.IsCircuit C
hCR : C ⊆ R
⊢ (M ↾ R).IsCircuit C

Tactic:
isCircuit_iff,

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hCR : C ⊆ R
hC : M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C
⊢ (M ↾ R).Dep C ∧ ∀ ⦃D : Set α⦄, (M ↾ R).Dep D → D ⊆ C → D = C
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).IsCircuit C → M.IsCircuit C ∧ C ⊆ R

Tactic:
isCircuit_iff,

Goal state after:
α : Type u_1
M : Matroid α
C R : Set α
hR : R ⊆ M.E
⊢ ((M ↾ R).Dep C ∧ ∀ ⦃D : Set α⦄, (M ↾ R).Dep D → D ⊆ C → D = C) →
    (M.Dep C ∧ ∀ ⦃D : Set α⦄, M.Dep D → D ⊆ C → D = C) ∧ C ⊆ R
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard = M.eRk M.E

Tactic:
hB.isBasis_ground.encard_eq_eRk

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.eRk M.E = M.eRk M.E
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Dep X
I : Set α
hI : M.IsBasis I X
⊢ I ≠ X

Tactic:
by rintro rfl; exact hI.indep.not_dep hX

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ M.eRk X = M.eRank

Tactic:
hX.eRk_eq

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : M.Spanning X
⊢ M.eRank = M.eRank
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X Y Y' : Set α
h : M.closure Y = M.closure Y'
⊢ M.closure (X ∪ Y) = M.closure (X ∪ Y')

Tactic:
by
  rw [← M.closure_union_closure_right_eq, h, M.closure_union_closure_right_eq]

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

Goal state before:
pp: α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
⊢ ¬(¬M.Indep (insert e I) ∧ I ⊆ M.E ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ I

Tactic:
and_iff_left hI.subset_ground

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
he : e ∈ M.E
⊢ ¬(¬M.Indep (insert e I) ∨ e ∈ I) ↔ M.Indep (insert e I) ∧ e ∉ 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.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E ∧ I ⊆ M.E → M.Indep (insert e I))

Tactic:
and_iff_left hI.subset_ground

Goal state after:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∉ I
⊢ M.Indep (insert e I) ↔ e ∈ M.E ∧ (e ∈ M.E → M.Indep (insert e I))
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
inst✝ : M.Loopless
he : e ∈ M.E
⊢ M.IsNonloop e

Tactic:
rw [← not_isLoop_iff, isLoop_iff, loops_eq_empty]
  exact notMem_empty _

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

Goal state before:
pp: case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ∧ f ≠ e ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
and_iff_left hne.symm

Goal state after:
case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_3
A : Type v
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
hx : AlgebraicIndependent R x
inst✝ : Algebra.IsAlgebraic R A
h : IsEmpty ι
⊢ IsEmpty ι

Tactic:
exact h

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

Goal state before:
pp: α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : Disjoint I X
⊢ False

Tactic:
disjoint_iff_inter_eq_empty

Goal state after:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I ∩ X = ∅
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Nontrivial R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ trdeg R S + trdeg S A ≤ trdeg R A

Tactic:
← (trdeg R S).lift_id,

Goal state after:
R : Type u_3
S : Type u
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Nontrivial R
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ Cardinal.lift.{u, u} (trdeg R S) + trdeg S A ≤ trdeg R A
Module: Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝ : IsScalarTower (↥Rt) (↥St) A
this : NoZeroDivisors ↥St
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)

Tactic:
have : NoZeroDivisors Rt := (Subalgebra.inclusion_injective _).noZeroDivisors
    (algebraMap Rt St) (map_zero _) (map_mul _)

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_4
x : ι → A
S : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
hx : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic R S
t : Set ι
fin : t.Finite
ind : AlgebraicIndependent S fun i ↦ x ↑i
i : ι
hi : i ∉ t
Rt : Subalgebra R A := adjoin R (x '' t)
St : Subalgebra S A := adjoin S (x '' t)
x✝ : Algebra ↥Rt ↥St := (Subalgebra.inclusion ⋯).toAlgebra
this✝¹ : IsScalarTower (↥Rt) (↥St) A
this✝ : NoZeroDivisors ↥St
this : NoZeroDivisors ↥Rt
⊢ Transcendental (↥(adjoin S (x '' t))) (x i)
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: case mpr
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
i : AlgebraicIndependent R x
⊢ (∀ (κ : Type w) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Surjective j) →
    IsTranscendenceBasis R x

Tactic:
· intro p
    use i
    intro w i' h
    specialize p w ((↑) : w → A) i' (fun i => ⟨x i, range_subset_iff.mp h i⟩) (by ext; simp)
    have q := congr_arg (fun s => ((↑) : w → A) '' s) p.range_eq
    rw [← image_univ, image_image] at q
    simpa using q

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
ind : AlgebraicIndependent R x
alg : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False

Tactic:
rw [show range x = Subtype.val '' range (Set.inclusion hxs) by
    rw [← range_comp, val_comp_inclusion, Subtype.range_val]] at alg

Goal state after:
ι : Type u
R : Type u_1
A : Type w
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
ind : AlgebraicIndependent R x
s : Set A
ind_s : AlgebraicIndepOn R _root_.id s
hxs : range x ⊆ s
alg : Algebra.IsAlgebraic (↥(adjoin R (Subtype.val '' range (Set.inclusion hxs)))) A
hxs' : ¬range x = s
this : ¬s ⊆ range x
a : A
has : a ∈ s
hax : a ∉ range x
⊢ False
Module: Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Goal state before:
pp: R : Type u_1
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ trdeg R S + trdeg S A = trdeg R A

Tactic:
← (trdeg R S).lift_id,

Goal state after:
R : Type u_1
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : Nontrivial R
A : Type v
inst✝⁶ : CommRing A
inst✝⁵ : NoZeroDivisors A
inst✝⁴ : Algebra R A
inst✝³ : Algebra S A
inst✝² : FaithfulSMul R S
inst✝¹ : FaithfulSMul S A
inst✝ : IsScalarTower R S A
⊢ lift.{v, v} (trdeg R S) + trdeg S A = trdeg R A
Module: Mathlib.FieldTheory.SeparableClosure

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
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), Algebra.IsSeparable F ↥(t i)
⊢ Algebra.IsSeparable F ↥(⨆ i, t i)

Tactic:
simp_rw [← le_separableClosure_iff] 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
ι : Type u_1
t : ι → IntermediateField F E
h : ∀ (i : ι), t i ≤ separableClosure F E
⊢ ⨆ i, t i ≤ separableClosure F E
Module: Mathlib.FieldTheory.SeparableClosure

Goal state before:
pp: F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
⊢ insepDegree F E = 1

Tactic:
by
  rw [insepDegree, (separableClosure.eq_top_iff F E).2 ‹_›, IntermediateField.rank_top]

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

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

Tactic:
rw [← finSepDegree_top F, ← finrank_top F E]
    refine induction_on_adjoin (fun K : IntermediateField F E ↦ finSepDegree F K ∣ finrank F K)
      (by simp_rw [finSepDegree_bot, IntermediateField.finrank_bot, one_dvd]) (fun L x h ↦ ?_) ⊤
    have hdvd := mul_dvd_mul h <| finSepDegree_adjoin_simple_dvd_finrank L E x
    set M := L⟮x⟯
    rwa [finSepDegree_mul_finSepDegree_of_isAlgebraic F L M,
      Module.finrank_mul_finrank F L M] at hdvd

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
p : R[X]
h : p.Monic
hp : Irreducible p
a b : K[X]
hₐ : ¬IsUnit a
a' : R[X]
ha : Polynomial.map (algebraMap R K) a' * C a.leadingCoeff = a
b' : R[X]
H :
  Polynomial.map (algebraMap R K) p =
    Polynomial.map (algebraMap R K) a' * (C a.leadingCoeff * C b.leadingCoeff * Polynomial.map (algebraMap R K) b')
hb : Polynomial.map (algebraMap R K) b' * C b.leadingCoeff = b
this : a.leadingCoeff * b.leadingCoeff = 1
⊢ IsUnit b

Tactic:
←
    C_mul,

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

Goal state before:
pp: case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
⊢ ∃ z, z ^ n = x

Tactic:
obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx

Goal state after:
case neg
k : Type u
inst✝¹ : Field k
inst✝ : IsSepClosed k
x : k
n : ℕ
hn : NeZero ↑n
hn' : 0 < n
this : (X ^ n - C x).degree ≠ 0
hx : ¬x = 0
z : k
hz : (X ^ n - C x).IsRoot z
⊢ ∃ z, z ^ n = x