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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : FiniteType R S
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] S
hf : Function.Surjective ⇑f
⊢ Function.Surjective ⇑(aeval fun i ↦ f (X i))

Tactic:
rwa [aeval_unique f] at hf

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

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
G : Type w₀
⊢ { G := G, R := PEmpty.{w₁ + 1}, relation := fun r ↦ PEmpty.casesOn (fun x ↦ G →₀ A) r }.solutionFinsupp.IsPresentation

Tactic:
exact Relations.solutionFinsupp_isPresentation _

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
i : ι
⊢ n i =
    ∑ j,
      (match j with
        | ⟨(kj, snd), property⟩ => ↑kj i) •
        match j with
        | ⟨(fst, yj), property⟩ => yj

Tactic:
apply_fun finsuppScalarLeft R N ι at hkn

Goal state after:
case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : (finsuppScalarLeft R N ι) ((rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2)) = (finsuppScalarLeft R N ι) en
⊢ n i =
    ∑ j,
      (match j with
        | ⟨(kj, snd), property⟩ => ↑kj i) •
        match j with
        | ⟨(fst, yj), property⟩ => yj
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case refine_1
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
x : ↥Q.ker
n : ι' →₀ ℕ
r : S
⊢ (Q.comp P).Ring

Tactic:
refine rename ?_ (P.σ r) * monomial ?_ 1
    exacts [Sum.inr, n.mapDomain Sum.inl]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: case e'_3.refine_2.refine_2
R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
this :
  (rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)) ∘ₗ ↑(TensorProduct.lid R M).symm).ker =
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype).range
x x✝¹ x✝ : ↥(LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker ⊗[R] M
⊢ (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝¹ ∈ (⨅ i, I i) • ⊤ →
    (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) x✝ ∈ (⨅ i, I i) • ⊤ →
      (↑(TensorProduct.lid R M) ∘ₗ rTensor M (LinearMap.pi fun i ↦ Submodule.mkQ (I i)).ker.subtype) (x✝¹ + x✝) ∈
        (⨅ i, I i) • ⊤

Tactic:
simpa using! add_mem

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} → ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
· intro H m
    by_cases h : (Submodule.span R {m}).annihilator = ⊤
    · rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h
      exact ⟨1, one_mem _, by simpa using h⟩
    obtain ⟨n, hn⟩ : f ∈ (Submodule.span R {m}).annihilator.radical := by
      rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
      rintro p ⟨hp, hp'⟩
      simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)
    exact ⟨_, ⟨n, rfl⟩, (Submodule.mem_annihilator_span_singleton _ _).mp hn⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
⊢ Module.Finite Rₚ Sₚ

Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]

Goal state after:
R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
this : algebraMap Rₚ Sₚ = IsLocalization.map Sₚ (algebraMap R S) ⋯
⊢ Module.Finite Rₚ Sₚ
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
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
v : Fin n → M
⊢ (Matrix.of fun i j ↦ (f j) (v i)).det = 0

Tactic:
exact Matrix.det_zero_of_column_eq hij (by simp [hf])

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ 𝔪 ≤ ⊥.jacobson

Tactic:
jacobson_eq_maximalIdeal

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ 𝔪 ≤ 𝔪

case h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
this : N₂ ≤ N₁ ⊔ 𝔪 • N₂
⊢ ⊥ ≠ ⊤
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: case tmul
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
a : ↥M
b : ↥N
⊢ (M.mulMap N) (a ⊗ₜ[R] b) ∈ M * N

Tactic:
exact mul_mem_mul a.2 b.2

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
φ : R × ((i : ι) → s i) → F
C0 : ∀ (r : R) (f : (i : ι) → s i) (i : ι), f i = 0 → φ (r, f) = 0
C0' : ∀ (f : (i : ι) → s i), φ (0, f) = 0
C_add :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (m₁ m₂ : s i),
    φ (r, update f i m₁) + φ (r, update f i m₂) = φ (r, update f i (m₁ + m₂))
C_add_scalar : ∀ (r r' : R) (f : (i : ι) → s i), φ (r, f) + φ (r', f) = φ (r + r', f)
C_smul :
  ∀ [inst : DecidableEq ι] (r : R) (f : (i : ι) → s i) (i : ι) (r' : R), φ (r, update f i (r' • f i)) = φ (r' * r, f)
x y : FreeAddMonoid (R × ((i : ι) → s i))
hxy : Eqv R s x y
inst : DecidableEq ι
z : R
f : (i : ι) → s i
i : ι
m₁ m₂ : s i
⊢ (FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i m₁) + FreeAddMonoid.of (z, update f i m₂)) =
    (FreeAddMonoid.lift φ) (FreeAddMonoid.of (z, update f i (m₁ + m₂)))

Tactic:
simp [FreeAddMonoid.lift_eval_of, @C_add inst]

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

Goal state before:
pp: case smul_tprod
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : Fin n → M
⊢ (cast R M ⋯) (mulEquiv ((r • (tprod R) a) ⊗ₜ[R] (tprod R) Fin.elim0)) = r • (tprod R) a

Tactic:
rw [← TensorProduct.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
    simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case mp
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:
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]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝ : Free R (N ⧸ l.range)
this : Projective R ↥l.range
⊢ Exact ⇑l.ker.subtype ⇑(LinearMap.codRestrict l.range l ⋯)

Tactic:
rw [LinearMap.exact_iff, LinearMap.ker_rangeRestrict, Submodule.range_subtype]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅H, H⁆ < H

Tactic:
← H.range_subtype,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSolvable G
H : Subgroup G
hH : Nontrivial ↥H
⊢ ⁅H.subtype.range, H.subtype.range⁆ < H.subtype.range
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q₁ q₂ : ↑(comap (algebraMap R S) ⁻¹' {p})
H : q₁ ≤ q₂
x : p.asIdeal.Fiber S
r : R
hx : (algebraMap R (p.asIdeal.Fiber S)) r * x ∈ ((preimageEquivFiber R S p) q₁).asIdeal
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ ((preimageEquivFiber R S p) q₂).asIdeal

Tactic:
rw [← q₂.2] at hr; simpa [IsScalarTower.algebraMap_apply R S q₂.1.asIdeal.ResidueField]

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:
intro a b
      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
p q : PrimeSpectrum R
hpq : p ≤ q
⊢ rankAtStalk M p = rankAtStalk M q

Tactic:
let S := Localization.AtPrime q.asIdeal

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
p q : PrimeSpectrum R
hpq : p ≤ q
S : Type uR := Localization.AtPrime q.asIdeal
⊢ rankAtStalk M p = rankAtStalk M q
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case right
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.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
f : K →ₐ[F] L
⊢ f.fieldRange ≤ ((⨆ f, f.fieldRange).val.comp (f.codRestrict (⨆ f, f.fieldRange).toSubalgebra ⋯)).fieldRange

Tactic:
val,

Goal state after:
case right
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.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
f : K →ₐ[F] L
⊢ f.fieldRange ≤ ((⨆ f, f.fieldRange).val.comp (f.codRestrict (⨆ f, f.fieldRange).toSubalgebra ⋯)).fieldRange
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : R →ₗ[R] M
hf : Function.Surjective ⇑f
r₁ r₂ : R
eq : f r₁ = f r₂
m : M
⊢ (fun x1 x2 ↦ x1 • x2) r₁ m = (fun x1 x2 ↦ x1 • x2) r₂ m

Tactic:
obtain ⟨r, rfl⟩ := hf m
    simp_rw [← map_smul, smul_eq_mul, mul_comm _ r, ← smul_eq_mul, map_smul, eq]

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

Goal state before:
pp: case right
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.IsAlgebraic F K
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
x : ↥(⨆ f, f.fieldRange)
x✝ : x ∈ ⊤
f : K →ₐ[F] L
⊢ f.fieldRange ≤
    IntermediateField.map (⨆ f, f.fieldRange).val (f.codRestrict (⨆ f, f.fieldRange).toSubalgebra ⋯).fieldRange

Tactic:
rw [AlgHom.map_fieldRange, val, AlgHom.val_comp_codRestrict]

Goal state after:
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
ϕ : F →+* E
α β : E
f g : F[X]
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
let sf := (f.map ϕ).roots

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
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)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)

Tactic:
have h_roots : ∀ x ∈ (h.map ιEE').roots, x = ιEE' β := by
    intro x hx
    rw [mem_roots_map h_ne_zero] at hx
    specialize hc (ιEE' γ - ιEE' (ιFE c) * x) (by
      have f_root := root_left_of_root_gcd hx
      rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
      exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root)
    specialize hc x (by
      rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
      exact root_right_of_root_gcd hx)
    by_contra a
    apply hc
    apply (div_eq_iff (sub_ne_zero.mpr a)).mpr
    simp only [γ, Algebra.smul_def, map_add, map_mul, RingHom.comp_apply]
    ring

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
h_ne_zero : h ≠ 0
h_sep : h.Separable
h_root : eval β h = 0
h_splits : (Polynomial.map ιEE' h).Splits
h_roots : ∀ x ∈ (Polynomial.map ιEE' h).roots, x = ιEE' β
⊢ Polynomial.map (algebraMap (↥F⟮γ⟯) E) p = C h.leadingCoeff * (X - C β)
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ I ⊆ Y ∧ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J

Tactic:
and_iff_right hIY

Goal state after:
α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hIY : I ⊆ Y
hYX : Y ⊆ X
⊢ ∀ (J : Set α), M.Indep J → I ⊆ J → J ⊆ Y → I = J
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
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)

Tactic:
obtain ⟨e, he, hi⟩ := (hI.indep_restrict_of_subset hIX).exists_insert_of_not_isBase hI' hJ

Goal state after:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.Indep I
hIX : I ⊆ X
hI' : ¬(M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
e : α
he : e ∈ J \ I
hi : (M ↾ X).Indep (insert e I)
⊢ ∃ e ∈ J \ I, M.Indep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
⊢ ∀ (I : Set β),
    M.Indep ((fun x ↦ ↑(invFunOn (⇑f) univ x)) '' I) ∧ InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) I ∧ I ⊆ range ⇑f ↔
      M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f

Tactic:
← and_assoc,

Goal state after:
case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
⊢ ∀ (I : Set β),
    (M.Indep ((fun x ↦ ↑(invFunOn (⇑f) univ x)) '' I) ∧ InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) I) ∧ I ⊆ range ⇑f ↔
      M.Indep (Subtype.val '' ⇑f ⁻¹' I) ∧ I ⊆ range ⇑f
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
I : Set ↑M.E
⊢ M.Indep ↑I → InjOn (fun x ↦ ↑(invFunOn (⇑f) univ x)) (⇑f '' I)

Tactic:
rintro - x hx y hy

Goal state after:
case inr
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ : Set α
M✝ : Matroid α
N : Matroid β
M : Matroid α
f : ↑M.E ↪ β
e : α
he : e ∈ M.E
x✝¹ : Nonempty ↑M.E
x✝ : Nonempty α
I : Set ↑M.E
x : β
hx : x ∈ ⇑f '' I
y : β
hy : y ∈ ⇑f '' I
⊢ (fun x ↦ ↑(invFunOn (⇑f) univ x)) x = (fun x ↦ ↑(invFunOn (⇑f) univ x)) y → x = y
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀

Tactic:
exact ⟨B, hB, rfl⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α ↪ β
⊢ ∃ B₀, M.IsBase B₀ ∧ ⇑f '' B = ⇑f '' B₀

Tactic:
exact ⟨B, hB, rfl⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

Tactic:
by_cases he : e ∈ M.E

Goal state after:
case pos
α : Type u_1
M : Matroid α
e : α
he : e ∈ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops

case neg
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ ¬M.IsNonloop e ↔ M.closure {e} = M.loops
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

Tactic:
by_cases he : e ∈ M.E

Goal state after:
case pos
α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
he : e ∈ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C

case neg
α : Type u_1
M : Matroid α
e : α
inst✝ : M✶.RankPos
he : e ∉ M.E
⊢ M.IsColoop e ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ M.E \ C
Module: Mathlib.Combinatorics.Matroid.Closure

Goal state before:
pp: α : Type u_2
X Y : Set α
M : Matroid α
hXY : X ⊆ Y
hX : X ⊆ M.E
⊢ X ⊆ M.closure Y

Tactic:
rw [← closure_inter_ground]; exact M.subset_closure_of_subset (subset_inter hXY hX)

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

Goal state before:
pp: α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y ↔ M.IsBasis' I Y ∧ I ⊆ X

Tactic:
iff_self_and

Goal state after:
α : Type u
X Y : Set α
M : Matroid α
hYX : Y ⊆ X
⊢ ∀ ⦃I : Set α⦄, M.IsBasis' I Y → I ⊆ X
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: α : Type u_1
M : Matroid α
X Y : Set α
inst✝ : M.Finitary
hX : X.Finite
hXY : X ⊆ M.closure Y
aux : ∃ T ⊆ Y, T.Finite ∧ X ⊆ M.closure T
⊢ ∃ I ⊆ Y, I.Finite ∧ M.Indep I ∧ X ⊆ M.closure I

Tactic:
obtain ⟨T, hT, hTfin, hXT⟩ := aux
    obtain ⟨I, hI⟩ := M.exists_isBasis' T
    exact ⟨_, hI.subset.trans hT, hTfin.subset hI.subset, hI.indep, by rwa [hI.closure_eq_closure]⟩

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
M : Matroid β
f : α → β
X I : Set α
hI : M.IsBasis' (f '' I) (f '' X)
hfI : InjOn f I
hIX : I ⊆ X
⊢ #↑(f '' I) ≤ ⨆ B, #↑↑B

Tactic:
exact hI.cardinalMk_le_cRk

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

Goal state before:
pp: α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X ↦ ¬M.Spanning (M.E \ X) ∧ X ⊆ M.E) K

Tactic:
rw [isCocircuit_iff_minimal_compl_nonspanning]
  exact minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1)
    (fun X hX ↦ ⟨X ∩ M.E, inter_subset_left, by rwa [sdiff_inter_self_eq_sdiff],
      inter_subset_right⟩)

Goal state after: