mathlib-initiative/mathlib-tactics huggingface dataset:
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
S : Submonoid R
⊢ freeLocus (Localization S) (LocalizedModule S M) = comap (algebraMap R (Localization S)) ⁻¹' freeLocus R M

Tactic:
ext p
  simp only [Set.mem_preimage]
  let p' := p.asIdeal.comap (algebraMap R _)
  have hp' : S ≤ p'.primeCompl := fun x hx H ↦
    p.isPrime.ne_top (Ideal.eq_top_of_isUnit_mem _ H (IsLocalization.map_units _ ⟨x, hx⟩))
  let Rₚ := Localization.AtPrime p'
  let Mₚ := LocalizedModule p'.primeCompl M
  let : Algebra (Localization S) Rₚ :=
    IsLocalization.localizationAlgebraOfSubmonoidLe _ _ S p'.primeCompl hp'
  have : IsScalarTower R (Localization S) Rₚ :=
    IsLocalization.localization_isScalarTower_of_submonoid_le ..
  have : IsLocalization.AtPrime Rₚ p.asIdeal := by
    have := IsLocalization.isLocalization_of_submonoid_le (Localization S) Rₚ _ _ hp'
    apply IsLocalization.isLocalization_of_is_exists_mul_mem _
      (Submonoid.map (algebraMap R (Localization S)) p'.primeCompl)
    · rintro _ ⟨x, hx, rfl⟩; exact hx
    · rintro ⟨x, hx⟩
      obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
      refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
      rw [IsLocalization.mk'_eq_mul_mk'_one]
      exact Ideal.mul_mem_right _ _ H
  let : Module (Localization S) Mₚ := Module.compHom Mₚ (algebraMap _ Rₚ)
  have : IsScalarTower R (Localization S) Mₚ :=
    ⟨fun r r' m ↦ show algebraMap _ Rₚ (r • r') • m = _ by
      simp [p', Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]; rfl⟩
  have : IsScalarTower (Localization S) Rₚ Mₚ :=
    ⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩
  let l := (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
    (LocalizedModule.mkLinearMap p'.primeCompl M)).extendScalarsOfIsLocalization S
    (Localization S)
  have : IsLocalizedModule p.asIdeal.primeCompl l := by
    have : IsLocalizedModule p'.primeCompl (l.restrictScalars R) :=
      inferInstanceAs (IsLocalizedModule p'.primeCompl
        (IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap S M)
        (LocalizedModule.mkLinearMap p'.primeCompl M)))
    have : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl) l :=
      IsLocalizedModule.of_restrictScalars p'.primeCompl ..
    apply IsLocalizedModule.of_exists_mul_mem
      (Algebra.algebraMapSubmonoid (Localization S) p'.primeCompl)
    · rintro _ ⟨x, hx, rfl⟩; exact hx
    · rintro ⟨x, hx⟩
      obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq S x
      refine ⟨algebraMap _ _ s.1, x, fun H ↦ hx ?_, by simp⟩
      rw [IsLocalization.mk'_eq_mul_mk'_one]
      exact Ideal.mul_mem_right _ _ H
  rw [mem_freeLocus_of_isLocalization (R := Localization S) p Rₚ Mₚ l]
  rfl

Goal state after:
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✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t

Tactic:
have : Module.Free _ _ := hx

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ t ⊆ freeLocus R M, IsOpen t ∧ x ∈ t
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✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
⊢ ∃ U, IsOpen U ∧ ⟨x, hx⟩ ∈ U ∧ ∀ x' ∈ U, rankAtStalk M ↑x' = rankAtStalk M ↑⟨x, hx⟩

Tactic:
have : Module.Free _ _ := hx

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x✝ : ↑(freeLocus R M)
x : PrimeSpectrum R
hx : x ∈ freeLocus R M
this : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
⊢ ∃ U, IsOpen U ∧ ⟨x, hx⟩ ∈ U ∧ ∀ x' ∈ U, rankAtStalk M ↑x' = rankAtStalk M ↑⟨x, hx⟩
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
M : IndepMatroid α
B B' : Set α
hB : Maximal M.Indep B
hB' : Maximal M.Indep B'
e : α
he : e ∈ B \ B'
hnotmax : ¬Maximal M.Indep (B \ {e})
f : α
hf : f ∈ B' \ (B \ {e})
hfB : M.Indep (insert f (B \ {e}))
⊢ f ≠ e

Tactic:
rintro rfl; exact he.2 hf.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✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
⊢ FiniteDimensional F E

Tactic:
have := isAlgebraic_of_finite_intermediateField F E

Goal state after:
F : Type u_1
E : Type u_2
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
IF : Type (max 0 u_2) := { K // ∃ x, K = F⟮x⟯ }
this : Algebra.IsAlgebraic F E
⊢ FiniteDimensional F E
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
this : Finite ↑(B₀ \ I)
x : α
x✝ : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
hxI : x ∉ I
⊢ f ⟨x, ⋯⟩ ⊆ iUnion f ∪ B₀ ∩ I

Tactic:
apply subset_union_of_subset_left

Goal state after:
α : Type u_1
E : Set α
Indep : Set α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I
indep_aug :
  ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I
subset_ground : ∀ (I : Set α), Indep I → I ⊆ E
htofin : ∀ (I : Set α) (e : α), Indep I → ¬Indep (insert e I) → ∃ I₀ ⊆ I, I₀.Finite ∧ ¬Indep (insert e I₀)
I B : Set α
hI : Indep I
hImax : ¬Maximal Indep I
hBmax : Maximal Indep B
e : α
heI : e ∉ I
hins : Indep (insert e I)
heB : e ∉ B
hcon : ∀ x ∈ B \ I, ¬Indep (insert x I)
heBdep : ¬Indep (insert e B)
B₀ : Set α
hB₀B : B₀ ⊆ B
hB₀fin : B₀.Finite
hB₀e : ¬Indep (insert e B₀)
hB₀ : Indep B₀
f : ↑(B₀ \ I) → Set α
hf : ∀ (b : ↑(B₀ \ I)), f b ⊆ I ∧ (f b).Finite ∧ ¬Indep (insert (↑b) (f b))
this : Finite ↑(B₀ \ I)
x : α
x✝ : x ∈ B₀ \ (iUnion f ∪ B₀ ∩ I)
hi : Indep (insert x (iUnion f ∪ B₀ ∩ I))
hxB₀ : x ∈ B₀
hxn : x ∉ iUnion f ∪ B₀ ∩ I
hxI : x ∉ I
⊢ f ⟨x, ⋯⟩ ⊆ iUnion f
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: case refine_2
α : Type u_1
M M' : Matroid α
X : Set α
h : ∀ I ⊆ X, M.Indep I ↔ M'.Indep I
I : Set α
hI : I ⊆ X
⊢ (M ↾ X).Indep I ↔ (M' ↾ X).Indep I

Tactic:
rw [restrict_indep_iff, and_iff_left hI, restrict_indep_iff, and_iff_left hI, h _ hI]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : (M ↾ R).Dep X
⊢ M.Dep X

Tactic:
restrict_dep_iff

Goal state after:
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : ¬M.Indep X ∧ X ⊆ R
⊢ M.Dep X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
e : α
hI : M.Indep I
hInt : I.Nontrivial
he : e ∈ M.closure I
h : ∀ f ∈ I, e ∉ M.closure (I \ {f})
heI : e ∈ I
f : α
hf : f ∈ I
hne : f ≠ e
⊢ e ∈ I \ {f}

Tactic:
by simp [heI, hne.symm]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ M.fundCircuit e X = {e}

Tactic:
suffices h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e by
    simpa [subset_antisymm_iff, fundCircuit]

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
⊢ ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankPos
B : Set α
hB : M.IsBase B
⊢ 1 ≤ M.eRank

Tactic:
← hB.encard_eq_eRank,

Goal state after:
α : Type u_1
M : Matroid α
inst✝ : M.RankPos
B : Set α
hB : M.IsBase B
⊢ 1 ≤ B.encard
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:
rw [← not_isLoop_iff (hK.subset_ground he), ← singleton_isCircuit]

Goal state after:
α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
⊢ ¬M.IsCircuit {e}
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
K : Set α
hK : M.IsCocircuit K
he : e ∈ K
he' : M.IsCircuit {e}
⊢ e ∈ {e} ∩ K

Tactic:
by simp [he]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ M.eRank ≠ ⊤ ↔ M.RankFinite

Tactic:
← hB.encard_eq_eRank,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard ≠ ⊤ ↔ M.RankFinite
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
exact hJ.indep

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (f '' B).encard = M.eRank

Tactic:
← hB.encard_eq_eRank,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : M.IsBase B
⊢ (f '' B).encard = B.encard
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

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

Tactic:
← hB.encard_eq_eRank,

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

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

Tactic:
← hB.encard_eq_eRank,

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.IsBase B
⊢ B.encard + M✶.eRank = M.E.encard
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
I : Set α
he : M.IsColoop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.closure I

Tactic:
exact he.notMem_closure_of_notMem h

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
M : Matroid α
hf : InjOn f M.E
X : Set α
hX : X ⊆ M.E
⊢ lift.{u, v} ((M.map f hf).cRk (f '' X)) = lift.{v, u} (M.cRk X)

Tactic:
by
  nth_rw 1 [cRk, cRank, le_antisymm_iff, lift_iSup bddAbove_of_small, cRk, cRank, cRk, cRank]
  nth_rw 2 [lift_iSup bddAbove_of_small]
  simp only [ciSup_le_iff bddAbove_of_small, Subtype.forall, isBase_restrict_iff',
    isBasis'_iff_isBasis hX, isBasis'_iff_isBasis (show f '' X ⊆ (M.map f hf).E from image_mono hX)]
  refine ⟨fun I hI ↦ ?_, fun I hI ↦ ?_⟩
  · obtain ⟨I, X', hIX, rfl, hXX'⟩ := map_isBasis_iff'.1 hI
    rw [mk_image_eq_of_injOn_lift _ _ (hf.mono hIX.indep.subset_ground), lift_le]
    obtain rfl : X = X' := by rwa [hf.image_eq_image_iff hX hIX.subset_ground] at hXX'
    exact hIX.cardinalMk_le_cRk
  rw [← mk_image_eq_of_injOn_lift _ _ (hf.mono hI.indep.subset_ground), lift_le]
  exact (hI.map hf).cardinalMk_le_cRk

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
B : Set α
he : e ∈ B
hB : M.IsBase B
⊢ e ∉ M.E \ B

Tactic:
by simp [he]

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

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ #↑(I \ J) = #↑(J \ I)

Tactic:
rw [← lift_inj.{u, v}, ← mk_image_eq_of_injOn_lift _ _ (hfI.mono sdiff_subset),
    ← mk_image_eq_of_injOn_lift _ _ (hfJ.mono sdiff_subset), lift_inj, hfI.image_sdiff,
    hfJ.image_sdiff, ← sdiff_union_sdiff_cancel inter_subset_left (image_inter_subset f I J),
    inter_comm, sdiff_inter_self_eq_sdiff, mk_union_of_disjoint, hI.cardinalMk_sdiff_comm hJ,
    ← sdiff_union_sdiff_cancel inter_subset_left (image_inter_subset f J I), inter_comm,
    sdiff_inter_self_eq_sdiff, mk_union_of_disjoint, inter_comm J I]

Goal state after:
α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' J \ f '' I) ((f '' I ∩ f '' J) \ f '' (J ∩ I))

α : Type u
β : Type v
f✝ : α → β
M✝ : Matroid α
I✝ J✝ B B' X✝ Y : Set α
M : Matroid β
inst✝ : M.InvariantCardinalRank
f : α → β
I J X : Set α
hI✝ : (M.comap f).IsBasis I X
hJ✝ : (M.comap f).IsBasis J X
hI : M.IsBasis (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
hJ : M.IsBasis (f '' J) (f '' X)
hfJ : InjOn f J
hJX : J ⊆ X
⊢ Disjoint (f '' I \ f '' J) ((f '' J ∩ f '' I) \ f '' (I ∩ J))
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: α : Type u
M : Matroid α
⊢ M.RankInfinite ↔ ¬M.cRank < ℵ₀

Tactic:
← rankFinite_iff_cRank_lt_aleph0,

Goal state after:
α : Type u
M : Matroid α
⊢ M.RankInfinite ↔ ¬M.RankFinite
Module: Mathlib.Combinatorics.Matroid.Rank.Cardinal

Goal state before:
pp: case inl
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ toENat #↑B = M.eRank

Tactic:
← hB.encard_eq_eRank,

Goal state after:
case inl
α : Type u
M : Matroid α
h : M.RankFinite
B : Set α
hB : M.IsBase B
⊢ toENat #↑B = B.encard
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
h : ¬Injective ⇑(algebraMap R A)
this : IsEmpty { s // AlgebraicIndepOn R _root_.id s }
⊢ trdeg R A = 0

Tactic:
trdeg,

Goal state after:
R : Type u_2
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : ¬Injective ⇑(algebraMap R A)
this : IsEmpty { s // AlgebraicIndepOn R _root_.id s }
⊢ ⨆ ι, Cardinal.mk ↑↑ι = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: R : Type u_3
S : Type u
A : Type v
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✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{v, u} (trdeg R S) + lift.{u, v} (trdeg S A) ≤ lift.{u, v} (trdeg R A)

Tactic:
trdeg,

Goal state after:
R : Type u_3
S : Type u
A : Type v
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✝² : Nontrivial R
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S A
⊢ lift.{v, u} (⨆ ι, #↑↑ι) + lift.{u, v} (⨆ ι, #↑↑ι) ≤ lift.{u, v} (⨆ ι, #↑↑ι)
Module: Mathlib.RingTheory.Polynomial.SeparableDegree

Goal state before:
pp: F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ ∃ m_1, g.natDegree * q ^ m_1 = ((expand F (q ^ m)) g).natDegree

Tactic:
use m

Goal state after:
case h
F : Type u_1
inst✝ : CommSemiring F
q : ℕ
g : F[X]
m : ℕ
hf : IsSeparableContraction q ((expand F (q ^ m)) g) g
⊢ g.natDegree * q ^ m = ((expand F (q ^ m)) g).natDegree
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)

Tactic:
coindep_iff_compl_spanning,

Goal state after:
α : Type u_2
M : Matroid α
S : Set α
hS : S ⊆ M.E
⊢ M.Spanning S ↔ M.Spanning (M.E \ (M.E \ S))
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E

Tactic:
coindep_iff_compl_spanning,

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
hK : X ⊆ M.E
⊢ M.Spanning (M.E \ X) ↔ M.closure (M.E \ X) = M.E
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 α
hIE : I ⊆ M.E
⊢ M.Coindep I ↔ M'.Coindep I

Tactic:
coindep_iff_compl_spanning,

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.Spanning (M.E \ I) ↔ M'.Coindep I
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 α
hIE : I ⊆ M.E
⊢ M.Spanning (M.E \ I) ↔ M'.Coindep I

Tactic:
coindep_iff_compl_spanning,

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.Spanning (M.E \ I) ↔ M'.Spanning (M'.E \ I)
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ M.Spanning X ∧ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ X → X = t

Tactic:
and_iff_right hX

Goal state after:
α : Type u_2
M : Matroid α
X : Set α
hX : M.Spanning X
h : ∀ ⦃Y : Set α⦄, M.Spanning Y → Y ⊆ X → X = Y
⊢ ∀ ⦃t : Set α⦄, M.Spanning t → t ⊆ X → X = t
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x

Tactic:
by_cases hxI : x ∈ I

Goal state after:
case pos
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∈ I
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x

case neg
α : Type u_2
β : Type u_3
M : Matroid β
f : α → β
X I : Set α
hI : (M.comap f).IsBasis' I X
hI' : M.IsBasis' (f '' I) (f '' X)
hIinj : InjOn f I
x : α
hxE : f x ∈ M.E
hxI : x ∉ I
⊢ M.Indep (f '' insert x I) → InjOn f (insert x I) → x ∈ I ↔ M.Indep (f '' insert x I) → ∃ x_1 ∈ I, f x_1 = f x
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: 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'
f : A →ₐ[R] A'
hf : Injective ⇑f
a✝ : Nontrivial R
⊢ lift.{v', v} (trdeg R A) ≤ lift.{v, v'} (trdeg R A')

Tactic:
trdeg,

Goal state after:
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'
f : A →ₐ[R] A'
hf : Injective ⇑f
a✝ : Nontrivial R
⊢ lift.{v', v} (⨆ ι, #↑↑ι) ≤ lift.{v, v'} (trdeg R A')
Module: Mathlib.RingTheory.AlgebraicIndependent.Basic

Goal state before:
pp: 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'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
⊢ lift.{v, v'} (trdeg R A') ≤ lift.{v', v} (trdeg R A)

Tactic:
trdeg,

Goal state after:
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'
f : A →ₐ[R] A'
hf : Surjective ⇑f
a✝ : Nontrivial R
⊢ lift.{v, v'} (⨆ ι, #↑↑ι) ≤ lift.{v', v} (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
inst✝ : Algebra.IsIntegral R S
a✝ : Nontrivial S
this : Nontrivial R
⊢ AlgebraicIndependent S x

Tactic:
exact hx.extendScalars S

Goal state after:
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
inst✝¹ : FaithfulSMul R S
inst✝ : Algebra.IsAlgebraic R S
⊢ IsTranscendenceBasis R x ↔ IsTranscendenceBasis S x

Tactic:
by
  simp_rw [IsTranscendenceBasis, IsAlgebraic.algebraicIndependent_iff R S]

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

Goal state before:
pp: ι : Type u
ι' : Type u'
R : Type u_1
A : Type w
x : ι → A
y : ι' → A
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors A
hx : IsTranscendenceBasis R x
hy : IsTranscendenceBasis R y
⊢ lift.{u', u} #ι = lift.{u, u'} #ι'

Tactic:
by
  rw [← lift_inj.{_, w}, lift_lift, lift_lift, ← lift_lift.{w, u'}, hx.lift_cardinalMk_eq_trdeg,
    ← lift_lift.{w, u}, hy.lift_cardinalMk_eq_trdeg, lift_lift, lift_lift]

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: G : Type u
inst✝ : Group G
B : GroupFilterBasis G
⊢ B.N 1 = B.filter

Tactic:
by
  simp only [N, one_mul, map_id']

Goal state after:
Module: Mathlib.Topology.Algebra.FilterBasis

Goal state before:
pp: case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ Tendsto (fun x ↦ x⁻¹) (𝓝 1) (𝓝 1)

Tactic:
rw [basis.tendsto_iff basis]

Goal state after:
case refine_2
G : Type u
inst✝ : Group G
B✝ B : GroupFilterBasis G
this : TopologicalSpace G := B.topology
basis : (𝓝 1).HasBasis (fun V ↦ V ∈ B) id
basis' : (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ i.1 ∈ B ∧ i.2 ∈ B) fun i ↦ id i.1 ×ˢ id i.2
⊢ ∀ ib ∈ B, ∃ ia ∈ B, ∀ x ∈ id ia, x⁻¹ ∈ id ib