mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case refine_2
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ ∀ (i : ↥(factors ⊤.annihilator).toFinset), Irreducible (IsPrincipal.generator ↑i)

Tactic:
rintro ⟨p, hp⟩

Goal state after:
case refine_2
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
p : Ideal R
hp : p ∈ (factors ⊤.annihilator).toFinset
⊢ Irreducible (IsPrincipal.generator ↑⟨p, hp⟩)
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: case zero
R : Type u
inst✝ : CommRing R
σ : Type u_1
⊢ (Finsupp.linearCombination (MvPolynomial σ R) fun x ↦ (D R (MvPolynomial σ R)) (MvPolynomial.X x))
      ((MvPolynomial.mkDerivation R fun x ↦ Finsupp.single x 1).liftKaehlerDifferential.toFun
        ((Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) 0)) =
    (Finsupp.linearCombination (MvPolynomial σ R) ⇑(D R (MvPolynomial σ R))) 0

Tactic:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom]
      rw [map_zero, map_zero, map_zero]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝² : CommRing R''
inst✝¹ : CommRing S''
inst✝ : Algebra R'' S''
P'' : Extension R'' S''
r s : S
x : P.Cotangent
⊢ (r * s) • x = r • s • x

Tactic:
by
    have := smul_eq_zero_of_mem (P.σ (r * s) - (P.σ r * P.σ s) : P.Ring) (by simp) x
    simpa only [sub_smul, mul_smul, sub_eq_zero] using! this

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
r : σ
⊢ (hom₁ pres) (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
simp [hom₁]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case add
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
p q : (Q.comp P).Ring
⊢ ∃ a, (Q.ofComp P).toAlgHom a = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q

Tactic:
use p + q

Goal state after:
case h
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
p q : (Q.comp P).Ring
⊢ (Q.ofComp P).toAlgHom (p + q) = (Q.ofComp P).toAlgHom p + (Q.ofComp P).toAlgHom q
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Extension R S
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ ⇑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ ⇑(LinearMap.baseChange A P.cotangentComplex) =
    ⇑(cotangentComplexBaseChange R S P.Ring A) ∘
      ⇑((LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv).symm ≪≫ₗ
          AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker)

Tactic:
← LinearEquiv.comp_symm_eq

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
P : Extension R S
A : Type u_1
inst✝³ : CommRing A
inst✝² : Algebra S A
inst✝¹ : Algebra P.Ring A
inst✝ : IsScalarTower P.Ring S A
⊢ (⇑(AlgebraTensorModule.cancelBaseChange P.Ring S A A Ω[P.Ring⁄R]) ∘ ⇑(LinearMap.baseChange A P.cotangentComplex)) ∘
      ⇑((LinearEquiv.baseChange S A (S ⊗[P.Ring] ↥P.ker) P.Cotangent P.cotangentEquiv).symm ≪≫ₗ
            AlgebraTensorModule.cancelBaseChange P.Ring S A A ↥P.ker).symm =
    ⇑(cotangentComplexBaseChange R S P.Ring A)
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin (n + n)
⊢ Even k ↔ Even ↑k

Tactic:
refine ⟨?_, even_of_val⟩

Goal state after:
n : ℕ
k : Fin (n + n)
⊢ Even k → Even ↑k
Module: Mathlib.Algebra.Module.SpanRankOperations

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
⊢ N.spanFinrank ≤ ⊤.spanFinrank

Tactic:
have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsLocalRing R
fg : N.FG
this : Module.Finite R ↥N := Module.Finite.iff_fg.mpr fg
s : Set (𝓀 ⊗[R] ↥N)
hs₁ : Cardinal.mk ↑s = ⊤.spanRank
hs₂ : span 𝓀 s = ⊤
hs₃ : s.Finite
⊢ N.spanFinrank ≤ ⊤.spanFinrank
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) • f ((j.succAbove i).removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

Tactic:
← (i.predAbove j).insertNth_self_removeNth (removeNth _ _),

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ ↑(j.succAbove i) •
        f
          ((i.predAbove j).insertNth ((j.succAbove i).removeNth v (i.predAbove j))
            ((i.predAbove j).removeNth ((j.succAbove i).removeNth v))) +
      (-1) ^ ↑j • f (j.removeNth v) =
    0
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
i j : Fin n
hij : i ≤ j
⊢ σ i ≤ σ j

Tactic:
have h'' := congr_fun this
    dsimp at h''
    rw [← a.map_rel_iff] at hij
    simpa only [← b.map_rel_iff, ← h'']

Goal state after:
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = tprodCoeff R (r • 1) (update f i x)

Tactic:
← smul_tprodCoeff (1 : R) _ i,

Goal state after:
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝⁷ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝⁶ : (i : ι) → AddCommMonoid (s i)
inst✝⁵ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
E : Type u_9
inst✝² : AddCommMonoid E
inst✝¹ : Module R E
F : Type u_10
inst✝ : AddCommMonoid F
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = tprodCoeff R 1 (update (update f i x) i (r • update f i x i))
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : LinearIndependent R m
hn : LinearIndependent R n
⊢ LinearIndependent R fun i ↦ ↑(m i.1) * ↑(n i.2)

Tactic:
by
  rw [LinearIndependent] at hm hn ⊢
  let i0 := (finsuppTensorFinsupp' R κ ι).symm
  let i1 := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
  let i2 := LinearMap.lTensor M (Finsupp.linearCombination R n)
  let i := mulMap M N ∘ₗ i2 ∘ₗ i1 ∘ₗ i0.toLinearMap
  have h1 : Function.Injective i1 := Module.Flat.rTensor_preserves_injective_linearMap _ hm
  have h2 : Function.Injective i2 := Module.Flat.lTensor_preserves_injective_linearMap _ hn
  have h : Function.Injective i := H.injective.comp h2 |>.comp h1 |>.comp i0.injective
  have : i = Finsupp.linearCombination R fun i ↦ (m i.1).1 * (n i.2).1 := by
    ext x
    simp [i, i0, i1, i2, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
  rwa [this] at h

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R ↑s) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
⊢ K ≤ N.colon {z • x}

Tactic:
rw [← hs, map_span, span_le, Set.image_subset_iff]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
x : M
inst✝ : IsNoetherianRing R
hx : x ∉ N
ann : Ideal R := N.colon {x}
hI : I ∈ ann.minimalPrimes
key : ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
J : Ideal R
hJI : ¬J ≤ I
n : ℕ := Nat.find key
hJ : I ^ n * J ≤ ann
K : Ideal R := I ^ (n - 1) * J
step1 : ∀ y ∈ K, I ≤ N.colon {y • x}
f : ↥K → R
g : ∀ (y : ↥K), f y ∈ N.colon {y • x}
h : ∀ (y : ↥K), f y ∉ I
s : Finset ↥K
hs : map (Submodule.subtype K) (span R ↑s) = K
z : R := ∏ y ∈ s, f y
hz : z ∉ I
⊢ ↑s ⊆ ⇑(Submodule.subtype K) ⁻¹' ↑(N.colon {z • x})
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
N : Submodule R M
I : Ideal R
inst✝ : IsNoetherianRing R
⊢ N.IsAssociatedPrime I ↔ I.IsPrime ∧ ∃ x, I = N.colon {x}

Tactic:
constructor
  · rintro ⟨hx, x, rfl⟩
    refine ⟨hx, exists_eq_colon_of_mem_minimalPrimes (x := x) ?_⟩
    rw [← Ideal.radical_minimalPrimes, Ideal.minimalPrimes_eq_subsingleton_self,
      Set.mem_singleton_iff]
  · rintro ⟨hx, x, rfl⟩
    exact ⟨hx, x, hx.radical.symm⟩

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
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (mk K) ((FractionalIdeal.mk0 K) I) = mk0 I

Tactic:
ClassGroup.mk0,

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
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (mk K) ((FractionalIdeal.mk0 K) I) = ((mk (FractionRing R)).comp (FractionalIdeal.mk0 (FractionRing R))) I
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
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (equiv K) (mk0 I) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)

Tactic:
ClassGroup.mk0,

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
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (equiv K) (((mk (FractionRing R)).comp (FractionalIdeal.mk0 (FractionRing R))) I) =
    (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)
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
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) ((Units.mapEquiv (ringEquivOfRingEquiv K L f).symm.toMulEquiv) I) = I

Tactic:
by simp [← Units.val_inj]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x},
      ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
tfae_have 4 → 3 := fun h x => h (f x)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x},
      ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
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
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ comap (algebraMap R A) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)

Tactic:
let Aₚ := Localization.AtPrime p.asIdeal

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : PrimeSpectrum A
hp : p ∈ comap (algebraMap R A) ⁻¹' freeLocus R M
Rₚ : Type uR := Localization.AtPrime (comap (algebraMap R A) p).asIdeal
Aₚ : Type u_1 := Localization.AtPrime p.asIdeal
⊢ p ∈ freeLocus A (A ⊗[R] M)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: X : Type u_3
hX : 5 ≤ Cardinal.mk X
h : Group.IsSolvable (Perm X)
key : Nonempty (Fin 5 ↪ X)
⊢ False

Tactic:
exact
    Equiv.Perm.not_isSolvable_fin_5 (Group.isSolvable_of_isSolvable_injective
      (Equiv.Perm.viaEmbeddingHom_injective (Nonempty.some key)))

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ ⊤ ≤ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K))

Tactic:
← s.span_eq,

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
h : Normal F K
inst✝ : FiniteDimensional F K
s : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F K)) F K := Module.Basis.ofVectorSpace F K
⊢ Submodule.span F (Set.range ⇑s) ≤ Subalgebra.toSubmodule (Algebra.adjoin F ((∏ x, minpoly F (s x)).rootSet K))
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
⊢ IsScalarTower F K ↥(normalClosure F K L)

Tactic:
apply of_algebraMap_eq'

Goal state after:
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
⊢ algebraMap F ↥(normalClosure F K L) = (algebraMap K ↥(normalClosure F K L)).comp (algebraMap F K)
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
⊢ β ∈ F⟮γ⟯

Tactic:
have map_g_ne_zero : g.map ιFE ≠ 0 := map_ne_zero (minpoly.ne_zero hβ)

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
p : (↥F⟮γ⟯)[X] :=
  EuclideanDomain.gcd
    ((Polynomial.map (algebraMap F ↥F⟮γ⟯) f).comp (C (AdjoinSimple.gen F γ) - C ⟨(algebraMap F E) c, ⋯⟩ * X))
    (Polynomial.map (algebraMap F ↥F⟮γ⟯) g)
h : E[X] := EuclideanDomain.gcd ((Polynomial.map ιFE f).comp (C γ - C (ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
⊢ β ∈ F⟮γ⟯
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type u_7
T : Type u_8
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* S
g : S →+* T
⊢ (mapRingHom g).comp (mapRingHom f) = mapRingHom (g.comp f)

Tactic:
algebraize [f, g, g.comp f]
  simp_rw [mapRingHom, mapAlgebra_comp_mapAlgebra]

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

Goal state before:
pp: F : Type u_1
inst✝⁷ : Field F
K₁ : Type u_3
inst✝⁶ : Field K₁
inst✝⁵ : Algebra F K₁
E : Type u_6
inst✝⁴ : Field E
inst✝³ : Algebra F E
inst✝² : Algebra K₁ E
inst✝¹ : IsScalarTower F K₁ E
inst✝ : Normal F K₁
h1 : Group.IsSolvable Gal(K₁/F)
h2 : Group.IsSolvable Gal(E/K₁)
⊢ Group.IsSolvable Gal(E/F)

Tactic:
let f : (E ≃ₐ[K₁] E) →* Gal(E/F) :=
    { toFun := fun ϕ =>
        AlgEquiv.ofAlgHom (ϕ.toAlgHom.restrictScalars F) (ϕ.symm.toAlgHom.restrictScalars F)
          (AlgHom.ext fun x => ϕ.apply_symm_apply x) (AlgHom.ext fun x => ϕ.symm_apply_apply x)
      map_one' := AlgEquiv.ext fun _ => rfl
      map_mul' := fun _ _ => AlgEquiv.ext fun _ => rfl }
  refine
    Group.isSolvable_of_ker_le_range f (AlgEquiv.restrictNormalHom K₁) fun ϕ hϕ =>
      ⟨{ ϕ with commutes' := fun x => ?_ }, AlgEquiv.ext fun _ => rfl⟩
  exact Eq.trans (ϕ.restrictNormal_commutes K₁ x).symm (congr_arg _ (AlgEquiv.ext_iff.mp hϕ x))

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

Goal state before:
pp: case inl
α : Type u_1
M✝ M : Matroid α
inst✝ : M.RankPos
hB : M.IsBase ∅
⊢ M.Nonempty

pp: case inr
α : Type u_1
M✝ M : Matroid α
inst✝ : M.RankPos
B : Set α
hB : M.IsBase B
e : α
heB : e ∈ B
⊢ M.Nonempty

Tactic:
· exact False.elim <| RankPos.empty_not_isBase hB

Goal state after:
case inr
α : Type u_1
M✝ M : Matroid α
inst✝ : M.RankPos
B : Set α
hB : M.IsBase B
e : α
heB : e ∈ B
⊢ M.Nonempty
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯

Tactic:
have β_in_K := sub_mem αxβ_in_K αyβ_in_K

Goal state after:
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ {α, β} ⊆ ↑F⟮α + x • β⟯
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = (x - y) • β

Tactic:
sub_smul

Goal state after:
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Finite (IntermediateField F E)
f : F → IntermediateField F E := fun x ↦ F⟮α + x • β⟯
x y : F
hneq : ¬x = y
heq : F⟮α + x • β⟯ = F⟮α + y • β⟯
αxβ_in_K : α + x • β ∈ F⟮α + x • β⟯
αyβ_in_K : α + y • β ∈ F⟮α + x • β⟯
β_in_K : α + x • β - (α + y • β) ∈ F⟮α + x • β⟯
⊢ α + x • β - (α + y • β) = x • β - y • β
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hI' : ¬M.IsBase I
hB : M.IsBase B
⊢ ∃ e ∈ B \ I, M.Indep (insert e I)

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.exists_isBase_superset
  obtain ⟨x, hxB', hx⟩ := exists_of_ssubset (hIB'.ssubset_of_ne (by (rintro rfl; exact hI' hB')))
  by_cases hxB : x ∈ B
  · exact ⟨x, ⟨hxB, hx⟩, hB'.indep.subset (insert_subset hxB' hIB')⟩
  obtain ⟨e, he, hBase⟩ := hB'.exchange hB ⟨hxB', hxB⟩
  exact ⟨e, ⟨he.1, notMem_subset hIB' he.2⟩,
    indep_iff.2 ⟨_, hBase, insert_subset_insert (subset_sdiff_singleton hIB' hx)⟩⟩

Goal state after:
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
inst✝² : Algebra.IsSeparable F E
A : Type u_5
inst✝¹ : Field A
inst✝ : Algebra F A
hA : ∀ (x : E), (Polynomial.map (algebraMap F A) (minpoly F x)).Splits
α : E
φ : E →ₐ[F] A
h : ∀ (ψ : E →ₐ[F] A), φ α = ψ α → φ = ψ
this : Algebra (↥F⟮α⟯) A := (φ.comp F⟮α⟯.val).toAlgebra
⊢ ∀ (x : E), (Polynomial.map (algebraMap (↥F⟮α⟯) A) (minpoly (↥F⟮α⟯) x)).Splits

Tactic:
· exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

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

Goal state before:
pp: case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.Indep (⋃ i, bif i then I else J)

Tactic:
← union_eq_iUnion

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I J X Y : Set α
hIX : M.IsBasis I X
hJY : M.IsBasis J Y
h : M.Indep (I ∪ J)
⊢ M.Indep (I ∪ J)