mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
⊢ x ∈ p₁.asIdeal → x ∈ p₂.asIdeal

Tactic:
hxp₁

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
⊢ x ∈ p₂.asIdeal
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
I' : Ideal R
hI : ↑I = ↑I'
x : R
hx : x ≠ 0
i : R
_hi : i ∈ I'
hy : x * i ≠ 0
h : I' = Ideal.span {i}
⊢ i ≠ 0

Tactic:
by grobner

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (equiv K') ((mk K) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)

Tactic:
ClassGroup.equiv,

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : Field K
inst✝⁵ : Algebra R K
inst✝⁴ : IsFractionRing R K
inst✝³ : IsDomain R
K' : Type u_3
inst✝² : Field K'
inst✝¹ : Algebra R K'
inst✝ : IsFractionRing R K'
I : (FractionalIdeal R⁰ K)ˣ
⊢ (QuotientGroup.congr (toPrincipalIdeal R (FractionRing R)).range (toPrincipalIdeal R K').range
        (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K').toMulEquiv) ⋯)
      ((mk K) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(canonicalEquiv R⁰ K K')) I)
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
⊢ Projective R M

Tactic:
have : Module.Finite R M := by infer_instance
  obtain ⟨s, hs⟩ := this
  let N := s →₀ R
  let f : N →ₗ[R] M := Finsupp.linearCombination R (Subtype.val : s → M)
  have hf : Function.Surjective f := by
    rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, Subtype.range_val]
    convert! hs
  have (I : Ideal R) (hI : I.IsMaximal) :=
    letI := H I hI
    Module.projective_lifting_property (LocalizedModule.map I.primeCompl f) LinearMap.id
    (LocalizedModule.map_surjective _ _ hf)
  obtain ⟨g, hg⟩ := LinearMap.split_surjective_of_localization_maximal _ this
  exact Module.Projective.of_split _ _ hg

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
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝² : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝¹ : IsScalarTower R (Localization S) Rₚ
this✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
r : R
r' : Localization S
m : Mₚ
⊢ (algebraMap (Localization S) Rₚ) (r • r') • m = r • r' • m

Tactic:
simp [p', Rₚ, Mₚ, Algebra.smul_def, ← IsScalarTower.algebraMap_apply, mul_smul]

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
p' : Ideal R := Ideal.comap (algebraMap R (Localization S)) p.asIdeal
hp' : S ≤ p'.primeCompl
Rₚ : Type uR := Localization.AtPrime p'
Mₚ : Type (max uR uM) := LocalizedModule p'.primeCompl M
this✝² : Algebra (Localization S) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization S) Rₚ S p'.primeCompl hp'
this✝¹ : IsScalarTower R (Localization S) Rₚ
this✝ : IsLocalization.AtPrime Rₚ p.asIdeal
this : Module (Localization S) Mₚ := compHom Mₚ (algebraMap (Localization S) Rₚ)
r : R
r' : Localization S
m : Mₚ
⊢ r •
      (algebraMap (Localization S) (Localization.AtPrime (Ideal.comap (algebraMap R (Localization S)) p.asIdeal))) r' •
        m =
    r • r' • m
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_3
hG : Group G
h : ∀ (a b : G), a * b = b * a
⊢ IsSolvable G

Tactic:
by
  let hG' : CommGroup G := { hG with mul_comm := h }
  cases hG
  infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b = b * a

Tactic:
refine (mem_bot.1 ?_).trans (mem_bot.1 ?_).symm <;>
        · rw [← hn]
          exact mem_top _

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✝¹ : Flat R M
inst✝ : Module.Finite R M
⊢ rankAtStalk M = 0 ↔ Subsingleton M

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ rankAtStalk_eq_zero_of_subsingleton⟩
  simp_rw [← support_eq_empty_iff (R := R), Set.eq_empty_iff_forall_notMem]
  intro p
  rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
h : Function.Injective ⇑(LinearMap.lTensor M f)
⊢ Function.Injective
    ⇑(↑(leftCancelEquiv P (linearEquiv R M)) ∘ₗ
        LinearMap.lTensor (Dual R M) (LinearMap.lTensor M f) ∘ₗ ↑(leftCancelEquiv N (linearEquiv R M)).symm)

Tactic:
simpa using Flat.lTensor_preserves_injective_linearMap _ h

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

Tactic:
by
  refine ⟨fun h ↦ ?_, LinearMap.lTensor_surjective _⟩
  rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]
  simpa using LinearMap.lTensor_surjective _ h

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
Q : Type u_3
A : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Module.Invertible R M
inst✝ : Module.Invertible R N
M' : Type u := Finite.reprₛ R M
⊢ toSkeleton (MonoidalCategoryStruct.tensorObj (SemimoduleCat.of R (Dual R M')) (SemimoduleCat.of R M')) = 1

Tactic:
exact Quotient.sound ⟨(Invertible.linearEquiv R _).toModuleIsoₛ⟩

Goal state after:
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
σ : Gal(L/K)
hσ : σ x = y
⊢ ∃ σ, σ y = x

Tactic:
use σ.symm

Goal state after:
case h
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
σ : Gal(L/K)
hσ : σ x = y
⊢ σ.symm y = x
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_3
E : Type u_4
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
⊢ F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E

Tactic:
by
  rw [← adjoin.finrank (IsIntegral.of_finite F α), ← finrank_top F E]
  refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩
  exact congr_arg (fun K : IntermediateField F E => finrank F K) h

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ I = ⋃ i, I

Tactic:
rw [iUnion_const]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep (⋃ i, I)

Tactic:
rw [iUnion_const]

Goal state after:
α : Type u_1
M : Matroid α
I : Set α
ι : Type u_2
inst✝ : Nonempty ι
X : ι → Set α
hI : ∀ (i : ι), M.IsBasis I (X i)
⊢ M.Indep I
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ (B'' ∩ X) \ J ⊆ B'

Tactic:
sdiff_subset_comm,

Goal state after:
α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
⊢ (B'' ∩ X) \ B' ⊆ J
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

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

Tactic:
rw [isBasis_iff_isBasis'_subset_ground, isBasis'_restrict_iff, restrict_ground_eq,
    and_congr_left_iff, ← isBasis'_iff_isBasis_inter_ground]

Goal state after:
α : Type u_1
M : Matroid α
R I X : Set α
⊢ X ⊆ R → (M.IsBasis' I (X ∩ R) ∧ I ⊆ R ↔ M.IsBasis' I X)
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I

Tactic:
isBasis_iff_maximal

Goal state after:
α : Type u_1
E I X J : Set α
hX : X ⊆ E
⊢ Maximal (fun I_1 ↦ (uniqueBaseOn I E).Indep I_1 ∧ I_1 ⊆ X) J ↔ J = X ∩ I
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
E : Set α
Indep : Set α → Prop
hM : ∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∃ M, E = M.E ∧ M.Indep = Indep

Tactic:
by
    obtain ⟨M, rfl, h⟩ := hM; refine ⟨_, rfl, funext (by simp [h])⟩

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

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

Tactic:
obtain ⟨I', hI', hII', hI'IJ⟩ :=
    (hI.indep_restrict_of_subset hIX).exists_isBase_subset_union_isBase (IsBasis.isBase_restrict hJ)

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hJ : M.IsBasis J X
I' : Set α
hI' : (M ↾ X).IsBase I'
hII' : I ⊆ I'
hI'IJ : I' ⊆ I ∪ J
⊢ ∃ I', M.IsBasis I' X ∧ I ⊆ I' ∧ I' ⊆ I ∪ J
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f.symm '' I)

Tactic:
by rintro ⟨I, hI, rfl⟩; simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) → M.Dep (⇑f.symm '' D)

Tactic:
by rintro ⟨I, hI, rfl⟩; simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) → M.IsBase (⇑f.symm '' B)

Tactic:
by rintro ⟨I, hI, rfl⟩; simpa

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

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M.eRank = M.eRk M.E

Tactic:
by
  rw [eRk, restrict_ground_eq_self]

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

Goal state before:
pp: α : Type u_1
I : Set α
e : α
M : Matroid α
⊢ (M ↾ univ).fundCircuit e I = M.fundCircuit e I

Tactic:
have aux (A B) : M.closure A ⊆ B ∪ univ \ M.E ↔ M.closure A ⊆ B := by
    refine ⟨fun h ↦ ?_, fun h ↦ h.trans subset_union_left⟩
    refine (subset_inter h (M.closure_subset_ground A)).trans ?_
    simp [union_inter_distrib_right]
  simp [fundCircuit, aux]

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
X : Set α
n : ℕ∞
h : n ≤ M.eRk X
⊢ ∃ I ⊆ X, M.Indep I ∧ I.encard = n

Tactic:
obtain ⟨J, hJ⟩ := M.exists_isBasis' X
    rw [← hJ.encard_eq_eRk] at h
    obtain ⟨I, hIJ, rfl⟩ := exists_subset_encard_eq h
    exact ⟨_, hIJ.trans hJ.subset, hJ.indep.subset hIJ, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X I : Set α
hI : M.IsBasis I (X ∩ M.E)
h : I = ∅
⊢ X ∩ M.E ⊆ M.loops

Tactic:
simpa [h] using! hI

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis I X

Tactic:
← Finite.eq_of_subset_of_encard_le (hX.finite_of_isBasis hJX) hIJ hI

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hX : M.IsRkFinite X
hIX : I ⊆ X
J : Set α
hI : I.encard ≤ J.encard
hJ : M.IsBasis J (I ∩ M.E)
hIJ : J ⊆ I
hXI : X ⊆ M.closure J
hJX : M.IsBasis J X
⊢ M.IsBasis J X
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
⊢ X ⊆ Fs i

Tactic:
obtain ⟨J, hIJ, hJ⟩ := hI.indep.subset_isBasis_of_subset (hI.subset.trans (iInter_subset _ i))

Goal state after:
α : Type u_2
M : Matroid α
ι : Type u_3
inst✝ : Nonempty ι
Fs : ι → Set α
hFs : ∀ (i : ι), M.IsFlat (Fs i)
I X : Set α
hI : M.IsBasis I (⋂ i, Fs i)
hIX : M.IsBasis I X
i : ι
J : Set α
hIJ : M.IsBasis J (Fs i)
hJ : I ⊆ J
⊢ X ⊆ Fs i
Module: Mathlib.Combinatorics.Matroid.Rank.ENat

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard

Tactic:
obtain ⟨I, hI⟩ := M✶.exists_isBasis X

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
hX : X ⊆ M.E
I : Set α
hI : M✶.IsBasis I X
⊢ M✶.eRk X + M.eRank = M.eRk (M.E \ X) + X.encard
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (∀ (x : Set α), M.IsBase x → x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
← and_imp,

Goal state after:
case e'_2
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ (∀ (x : Set α), M.IsBase x ∧ x ⊆ M.E → (x ∩ K).Nonempty) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty
Module: Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Goal state before:
pp: case e'_1.e'_4
ι : 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
⊢ (fun i_1 ↦ x ↑i_1) ∘ ⇑(subtypeInsertEquivOption h).symm = fun o ↦ o.elim (x i) fun i ↦ x ↑i

pp: case e'_2
ι : 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
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Transcendental (↥(adjoin R (range fun i ↦ x ↑i))) (x i)

Tactic:
· ext (_ | _) <;> rfl

Goal state after:
case e'_2
ι : 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
⊢ Transcendental (↥(adjoin R (x '' s))) (x i) ↔ Transcendental (↥(adjoin R (range fun i ↦ x ↑i))) (x i)
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
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i ↦ x ↑i
ndisj : ¬Disjoint s t
⊢ False

Tactic:
have ⟨i, hs, ht⟩ := Set.not_disjoint_iff.mp ndisj

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
hx : AlgebraicIndependent R x
inst✝ : Nontrivial A
s t : Set ι
ind : AlgebraicIndependent ↥(adjoin R (x '' s)) fun i ↦ x ↑i
ndisj : ¬Disjoint s t
i : ι
hs : i ∈ s
ht : i ∈ t
⊢ False
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:
by
  simp_rw [trdeg, lift_iSup bddAbove_of_small]
  simp_rw [Cardinal.ciSup_add_ciSup _ bddAbove_of_small _ bddAbove_of_small,
    add_comm (lift.{v, u} _), ← mk_sum]
  refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
  have := hs.sumElim_comp ht
  refine le_ciSup_of_le bddAbove_of_small ⟨_, this.to_subtype_range⟩ ?_
  rw [← lift_umax, mk_range_eq_of_injective this.injective, lift_id']

Goal state after:
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]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
g' : F[X] := Classical.choose hf
hg' : (Classical.choose hf).Separable
m' : ℕ
hm' : (expand F (q ^ m')) (Classical.choose hf) = f
this : Fact (Nat.Prime q)
⊢ f = (expand F (q ^ m')) g'

Tactic:
hm'

Goal state after:
case prime
F : Type u_1
inst✝ : Field F
q : ℕ
f : F[X]
hf : HasSeparableContraction q f
g : F[X]
hprime✝ : Nat.Prime q
hchar✝ : CharP F q
hg : g.Separable
m : ℕ
hm : (expand F (q ^ m)) g = f
g' : F[X] := Classical.choose hf
hg' : (Classical.choose hf).Separable
m' : ℕ
hm' : (expand F (q ^ m')) (Classical.choose hf) = f
this : Fact (Nat.Prime q)
⊢ f = f
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
s : { s // AlgebraicIndepOn R _root_.id s }
t : Set A
ht : ↑s ⊆ t ∧ IsTranscendenceBasis R Subtype.val
⊢ #↑↑s ≤ ⨆ ι, #↑↑ι

Tactic:
exact le_ciSup_of_le bddAbove_of_small ⟨t, ht.2⟩ (mk_le_mk_of_subset ht.1)

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

Goal state before:
pp: α : Type u_1
M : Type u_3
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : FaithfulSMul M α
m : M
⊢ fixedBy α m = Set.univ ↔ m = 1

Tactic:
by
  rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall]
  simp_rw [funext_iff, one_smul, mem_fixedBy]

Goal state after:
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
inst✝ : IsDomain A
s t : Set A
h✝ : AlgebraicIndepOn R _root_.id s ∧ s ⊆ t
alg : ∀ a ∈ t, IsAlgebraic (↥(adjoin R s)) a
a : A
ha : a ∉ s
h : AlgebraicIndepOn R _root_.id (insert a s) ∧ insert a s ⊆ t
⊢ IsAlgebraic (↥(adjoin R (_root_.id '' s))) (_root_.id a)

Tactic:
by
      rw [image_id]; exact alg _ <| h.2 <| mem_insert ..

Goal state after:
Module: Mathlib.FieldTheory.SeparableDegree

Goal state before:
pp: F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K✝ : Type w
inst✝¹ : Field K✝
inst✝ : Algebra F K✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))

Tactic:
have hi1 : Function.Injective i1 := by
    rw [IsScalarTower.coe_toAlgHom', IsScalarTower.algebraMap_eq _ K]
    exact (algebraMap K (AlgebraicClosure K)).injective.comp (IsFractionRing.injective _ _)

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
⊢ Infinite (Emb F (FractionRing (MvPolynomial ι F)))
Module: Mathlib.FieldTheory.SeparableDegree

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✝
H : Algebra.Transcendental F E
ι : Type v
x : ι → E
hx : IsTranscendenceBasis F x
this : Algebra.IsAlgebraic (↥(adjoin F (Set.range x))) E
i : ι
K : Type (max u v) := FractionRing (MvPolynomial ι F)
i1 : MvPolynomial ι F →ₐ[F] AlgebraicClosure K := IsScalarTower.toAlgHom F (MvPolynomial ι F) (AlgebraicClosure K)
hi1 : Function.Injective ⇑i1
f : ℕ → Emb F K := fun n ↦ IsFractionRing.liftAlgHom ⋯
m n : ℕ
h : MvPolynomial.X i ^ (m + 1) = MvPolynomial.X i ^ (n + 1)
⊢ m = n

Tactic:
simpa using congr(MvPolynomial.totalDegree $h)

Goal state after: