mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mpr
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
h : ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
⊢ ∀ {n : Fin k → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n

Tactic:
n

Goal state after:
case mpr
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
h : ∀ (M' : Submodule R M), M'.FG → Injective ⇑(rTensor N M'.subtype)
k : ℕ
m : Fin k → M
n : Fin k → N
⊢ ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ M.LinearDisjoint N ↔ (equivOpposite.symm (MulOpposite.op N)).LinearDisjoint (equivOpposite.symm (MulOpposite.op M))

Tactic:
simp only [linearDisjoint_iff, mulMap_op, LinearMap.coe_comp,
    LinearEquiv.coe_coe, EquivLike.comp_injective, EquivLike.injective_comp]

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
C0 : motive 0
x : FreeAddMonoid (R × ((i : ι) → (fun i ↦ s i) i))
⊢ ∀ (x : R × ((i : ι) → (fun i ↦ s i) i)) (xs : FreeAddMonoid (R × ((i : ι) → (fun i ↦ s i) i))),
    motive ↑xs → motive ↑(FreeAddMonoid.of x + xs)

Tactic:
simp_rw [AddCon.coe_add]

Goal state after:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
tprodCoeff : ∀ (r : R) (f : (i : ι) → s i), motive (PiTensorProduct.tprodCoeff R r f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
C0 : motive 0
x : FreeAddMonoid (R × ((i : ι) → (fun i ↦ s i) i))
⊢ ∀ (x : R × ((i : ι) → s i)) (xs : FreeAddMonoid (R × ((i : ι) → s i))),
    motive ↑xs → motive (↑(FreeAddMonoid.of x) + ↑xs)
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
x : GradedMonoid fun i ↦ ⨂[R]^i M
⊢ (cast R M ⋯) (r • x).snd = (GradedMonoid.mk 0 ((↑algebraMap₀).toAddMonoidHom r) * x).snd

Tactic:
by
    rw [← LinearEquiv.eq_symm_apply, cast_symm]
    exact (algebraMap₀_mul r x.snd).symm

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case «1».«0»
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
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
hij : ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩) = ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩)
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = (fun i ↦ i) ⟨0, ⋯⟩

Tactic:
simp [hab.symm] at hij

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 : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
⊢ Ideal.span {z} * K ≤ ann

Tactic:
Ideal.span_singleton_mul_le_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 : span R ↑s = ⊤
z : R := ∏ y ∈ s, f y
hz : z ∉ I
hz' : K ≤ N.colon {z • x}
⊢ ∀ z_1 ∈ K, z * z_1 ∈ ann
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ g.ker.FG

Tactic:
rw [h.linearMap_ker_eq, LinearMap.range_eq_map]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
inst✝³ : IsLocalRing R
hg : Surjective ⇑g
h : Exact ⇑f ⇑g
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
hf : Function.Injective ⇑(LinearMap.lTensor k f)
⊢ (Submodule.map f ⊤).FG
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
hab : a * b ∈ ⊥.colon {y}
⊢ a ∈ ⊥.colon {y} ∨ b ∈ ⊥.colon {y}

Tactic:
rw [or_iff_not_imp_left]

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H : IsNoetherianRing R
x : M
hx : x ≠ 0
y : M
h₃ : ∀ I ∈ {P | ⊥.colon {x} ≤ P ∧ P ≠ ⊤ ∧ ∃ y, P = ⊥.colon {y}}, ¬⊥.colon {y} < I
l : ⊥.colon {x} ≤ ⊥.colon {y}
h₁ : ⊥.colon {y} ≠ ⊤
a b : R
hab : a * b ∈ ⊥.colon {y}
⊢ a ∉ ⊥.colon {y} → b ∈ ⊥.colon {y}
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mpr
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
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite R ↥l.ker
⊢ ∃ l', l' ∘ₗ l = LinearMap.id

Tactic:
have H : Function.Injective ((LinearMap.ker l).subtype.lTensor k) := by
      apply_fun (LinearMap.lTensor k) at hl'
      rw [LinearMap.lTensor_comp, LinearMap.lTensor_id] at hl'
      exact Function.HasLeftInverse.injective ⟨l'.lTensor k, DFunLike.congr_fun hl'⟩

Goal state after:
case mpr
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
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
⊢ ∃ l', l' ∘ₗ l = LinearMap.id
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I : Ideal R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ f, Function.Injective ⇑f

Tactic:
by
  rw [isAssociatedPrime_iff, and_congr_right_iff]
  refine fun _ ↦ ⟨fun ⟨x, h⟩ ↦ ?_, fun ⟨f, h⟩ ↦ ⟨(f ∘ₗ mkQ I) 1, ?_⟩⟩
  · replace h : I = ker (toSpanSingleton R M x) := by simp [h, SetLike.ext_iff]
    exact ⟨liftQ _ _ h.le, ker_eq_bot.mp (ker_liftQ_eq_bot' _ _ h)⟩
  · conv_lhs => rw [← I.ker_mkQ, ← ker_comp_of_ker_eq_bot (mkQ I) (ker_eq_bot_of_injective h)]
    simp [SetLike.ext_iff, ← Ideal.Quotient.algebraMap_eq, Algebra.algebraMap_eq_smul_one]

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

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h✝ : Disjoint ↑I ↑(nonZeroDivisors A)
x : A
hP : I ≤ ⊥.colon {x}
prime : (⊥.colon {x}).IsPrime
h : x = 0
⊢ ⊥.colon {x} = ⊤

Tactic:
by simp [h]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ ∃ r ∉ p, ∃ s, r • x = s ⊗ₜ[R] 1

Tactic:
refine ⟨r * y, p.primeCompl.mul_mem hrt.1 hrt.2, y • a, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ (r * y) • x = (y • a) ⊗ₜ[R] 1
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : Nontrivial G
hn : _root_.commutator G = ⊤
n : ℕ
h : derivedSeries G n = ⊤
⊢ derivedSeries G (n + 1) = ⊤

Tactic:
rwa [derivedSeries_succ, h]

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
inst✝ : Flat R M
⊢ IsLocallyConstant (rankAtStalk M)

Tactic:
let e : freeLocus R M ≃ₜ PrimeSpectrum R :=
    (Homeomorph.setCongr freeLocus_eq_univ).trans (Homeomorph.Set.univ (PrimeSpectrum R))
  convert! isLocallyConstant_rankAtStalk_freeLocus.comp_continuous e.symm.continuous

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⟩

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
h : rankAtStalk M = 0
⊢ Subsingleton M
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, f.fieldRange).val x ∈ ⇑(⨆ f, f.fieldRange).val '' ↑(⨆ f, f.fieldRange)

Tactic:
← IntermediateField.coe_map,

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, f.fieldRange).val x ∈ ↑(IntermediateField.map (⨆ f, f.fieldRange).val (⨆ f, f.fieldRange))
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:
by
  apply of_algebraMap_eq'
  ext x
  exact algebraMap_apply F K L x

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hf
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
⊢ eval (eval β (C γ - C (ιFE c) * X)) (Polynomial.map ιFE f) = 0

Tactic:
eval_sub,

Goal state after:
case hf
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
⊢ eval (eval β (C γ) - eval β (C (ιFE c) * X)) (Polynomial.map ιFE f) = 0
Module: Mathlib.RingTheory.AlgebraicIndependent.Adjoin

Goal state before:
pp: ι : Type u_1
F : Type u_2
E : Type u_3
x : ι → E
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
hx : AlgebraicIndependent F x
i : FractionRing (MvPolynomial ι F) →ₐ[F] E := IsFractionRing.liftAlgHom ⋯
⊢ (↑i).comp (algebraMap (MvPolynomial ι F) (FractionRing (MvPolynomial ι F))) = ↑(aeval x)

Tactic:
ext <;> simp [i]

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
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits

Tactic:
have hF : Normal F E := by
    have : IsSplittingField F E (∏ i ∈ s, minpoly F i.snd) := by
      refine isSplittingField_iSup ?_ fun i _ => adjoin_rootSet_isSplittingField ?_
      · exact Finset.prod_ne_zero_iff.mpr fun i _ => minpoly.ne_zero ((h i.1).isIntegral i.2)
      · simpa [Polynomial.map_map] using! ((h i.1).splits i.2).map (algebraMap (t i.1) K)
    apply Normal.of_isSplittingField (∏ i ∈ s, minpoly F i.2)

Goal state after:
F : Type u_1
K : Type u_2
inst✝² : Field F
inst✝¹ : Field K
inst✝ : Algebra F K
ι : Type u_3
t : ι → IntermediateField F K
h : ∀ (i : ι), Normal F ↥(t i)
x : ↥(⨆ i, t i)
s : Finset ((i : ι) × ↥(t i))
hx : ↑x ∈ ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
E : IntermediateField F K := ⨆ i ∈ s, adjoin F ((minpoly F i.snd).rootSet K)
hF : Normal F ↥E
⊢ (Polynomial.map (algebraMap F ↥(⨆ i, t i)) (minpoly F x)).Splits
Module: Mathlib.FieldTheory.Normal.Basic

Goal state before:
pp: case inl
F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : K
h : (minpoly F x).natDegree < 2
⊢ (map (algebraMap F K) (minpoly F x)).Splits

pp: case inr
F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : K
h : (minpoly F x).natDegree = 2
⊢ (map (algebraMap F K) (minpoly F x)).Splits

Tactic:
· exact Splits.of_natDegree_le_one <| natDegree_map_le.trans (by rwa [Nat.le_iff_lt_add_one])

Goal state after:
case inr
F✝ : Type u_1
K✝ : Type u_2
inst✝¹² : Field F✝
inst✝¹¹ : Field K✝
inst✝¹⁰ : Algebra F✝ K✝
K₁ : Type u_3
K₂ : Type u_4
K₃ : Type u_5
inst✝⁹ : Field K₁
inst✝⁸ : Field K₂
inst✝⁷ : Field K₃
inst✝⁶ : Algebra F✝ K₁
inst✝⁵ : Algebra F✝ K₂
inst✝⁴ : Algebra F✝ K₃
ϕ : K₁ →ₐ[F✝] K₂
χ : K₁ ≃ₐ[F✝] K₂
ψ : K₂ →ₐ[F✝] K₃
ω : K₂ ≃ₐ[F✝] K₃
F : Type u_6
K : Type u_7
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
x : K
h : (minpoly F x).natDegree = 2
⊢ (map (algebraMap F K) (minpoly F x)).Splits
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)

Tactic:
by simp [h]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case neg.refine_1
F✝ : Type u_1
E✝ : Type u_2
inst✝⁵ : Field F✝
inst✝⁴ : Field E✝
inst✝³ : Algebra F✝ E✝
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
m n : ℕ
hneq : m ≠ n
heq : F⟮α ^ m⟯ = F⟮α ^ n⟯
hmn : m < n
r s : F[X]
h : α ^ m * (aeval (α ^ n)) s - (aeval (α ^ n)) r = 0
hm : 0 < m
hzero : s ≠ 0
f : F[X] := X ^ m * (expand F n) s - (expand F n) r
⊢ f ≠ 0

Tactic:
have : f.coeff (n * s.natDegree + m) ≠ 0 := by
      have hn : 0 < n := by linarith only [hm, hmn]
      have hndvd : ¬ n ∣ n * s.natDegree + m := by
        rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]
        exact Nat.not_dvd_of_pos_of_lt hm hmn
      simp only [f, coeff_sub, coeff_X_pow_mul, s.coeff_expand_mul' hn, coeff_natDegree,
        coeff_expand hn r, hndvd, ite_false, sub_zero]
      exact leadingCoeff_ne_zero.2 hzero
    intro h
    simp only [h, coeff_zero, ne_eq, not_true_eq_false] at this

Goal state after:
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.Indep I ∧ I ⊆ X ↔ (M' ↾ X).Indep I

Tactic:
and_iff_left hI,

Goal state after:
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.Indep I ↔ (M' ↾ X).Indep I
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.Indep I ↔ M'.Indep I ∧ I ⊆ X

Tactic:
and_iff_left hI,

Goal state after:
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.Indep I ↔ M'.Indep I
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : R = M.E
⊢ M ↾ R = M

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤r M
⊢ N.E ⊆ M.E

Tactic:
obtain ⟨R, hR, rfl⟩ := h; exact hR

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

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase B ↔ M.IsBase (M.E \ (M.E \ B))

Tactic:
sdiff_sdiff_cancel_left hB

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : B ⊆ M.E
⊢ M.IsBase B ↔ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.IndepAxioms

Goal state before:
pp: α : Type u_1
Indep : Set α → Prop
M : Matroid α
h : ∀ (I : Set α), M.Indep I ↔ Indep I
⊢ ∀ (x : Set α), M.Indep x = Indep x

Tactic:
by simp [h]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.Coindep X ↔ M.Indep X

Tactic:
Coindep,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶✶.Indep X ↔ M.Indep X
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : N.Dep X
hNM : N ≤r M
⊢ M.Dep X

Tactic:
by
  obtain ⟨R, hR, rfl⟩ := hNM
  rw [restrict_dep_iff] at hX
  exact ⟨hX.1, hX.2.trans hR⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

Tactic:
Coindep,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ M✶.Indep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Map

Goal state before:
pp: case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ (N.comap f).Dep (insert e I)

Tactic:
suffices N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
    by simpa [← not_indep_iff hIE, injOn_insert heI, h.2.1, image_insert_eq]

Goal state after:
case refine_2.refine_2
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
I X : Set α
h : N.IsBasis (f '' I) (f '' X) ∧ InjOn f I ∧ I ⊆ X
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
hIE : insert e I ⊆ (N.comap f).E
⊢ N.Indep (insert (f e) (f '' I)) → ∃ x ∈ I, f x = f e
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ B, M.IsBase B ∧ Disjoint X B) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X)

Tactic:
subset_sdiff

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ B, M.IsBase B ∧ Disjoint X B) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E \ B

Tactic:
subset_sdiff

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ (∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X) ∧ X ⊆ M.E ↔ ∃ B, M.IsBase B ∧ X ⊆ M.E ∧ Disjoint X B
Module: Mathlib.Combinatorics.Matroid.Minor.Restrict

Goal state before:
pp: α : Type u_1
M : Matroid α
I X J : Set α
e : α
hIX : M.IsBasis I X
hJX : M.IsBasis J X
he : e ∈ I \ J
y : α
hy : y ∈ J \ I
h : (M ↾ X).IsBase (insert y (I \ {e}))
⊢ M.IsBasis (insert y (I \ {e})) X

Tactic:
by rwa [isBase_restrict_iff] at h

Goal state after: