mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
hx : (algebraMap S S') x ∈ Submodule.span R ↑s
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
⊢ (algebraMap R S) y' • ↑s = y' • ↑s

Tactic:
simp_rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx : y' • (algebraMap S S') x ∈ y' • Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)

Tactic:
hx₁,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx : y' • (algebraMap S S') x ∈ Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
m : ↑↑s
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
⊢ k • 0 = 0

Tactic:
smul_zero

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : PrimeSpectrum R
inst✝ : Module.Finite R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
H : ∀ m ∈ ↑s, ∃ x, x • m = 0 ∧ x ∉ p.asIdeal
x : { a // a ∈ ↑s } → R
hx : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 • ↑x_1 = 0
hx' : ∀ (x_1 : { a // a ∈ ↑s }), x x_1 ∉ p.asIdeal
m : ↑↑s
k : R
hk : ∏ i ∈ s.attach, x i = x m * k
⊢ 0 = 0
Module: Mathlib.Data.Fin.Parity

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

Tactic:
rintro ⟨l, rfl⟩

Goal state after:
n : ℕ
l : Fin (n + n)
⊢ Even ↑(l + l)
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin (n + n)
inst✝ : NeZero (n + n)
⊢ Odd k → Odd ↑k

Tactic:
rintro ⟨l, rfl⟩

Goal state after:
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ↑(2 * l + 1)
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
k : Fin (n + 1)
i : Fin n
hki : k ≠ k.succAbove i
j : Fin n
hkj : k ≠ k.succAbove j
hvij : v (k.succAbove i) = v (k.succAbove j)
hij : k.succAbove i ≠ k.succAbove j
x✝ : k ≠ k.succAbove i ∧ k ≠ k.succAbove j
⊢ (-1) ^ ↑k • 0 = 0

Tactic:
smul_zero

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
N : Type u_4
N₂ : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup N₂
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R N
inst✝ : Module R N₂
n : ℕ
f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 1) → M
k : Fin (n + 1)
i : Fin n
hki : k ≠ k.succAbove i
j : Fin n
hkj : k ≠ k.succAbove j
hvij : v (k.succAbove i) = v (k.succAbove j)
hij : k.succAbove i ≠ k.succAbove j
x✝ : k ≠ k.succAbove i ∧ k ≠ k.succAbove j
⊢ 0 = 0
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
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
⊢ Function.Injective ⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N))

Tactic:
have := hf.comp H

Goal state after:
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this : Function.Injective (⇑f ∘ ⇑(M.mulMap N))
⊢ Function.Injective ⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) 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
N : Submodule R S
⊢ Function.Injective ⇑((Subalgebra.toSubmodule ⊥).mulMap N)

Tactic:
mulMap_one_left_eq

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
⊢ Function.Injective ⇑(N.subtype ∘ₗ ↑N.lTensorOne)
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
φ : MultilinearMap R s E
z : R
f : (i : ι) → s i
i : ι
hf : f i = 0
⊢ z • 0 = 0

Tactic:
smul_zero

Goal state after:
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) • y ∈ ⊥
ha : a • y ∉ ⊥
c : R
hc : c • y = 0
⊢ a • 0 = 0

Tactic:
smul_zero

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) • y ∈ ⊥
ha : a • y ∉ ⊥
c : R
hc : c • y = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
c : R
hc : c ∈ T
⊢ normalize b * id c ∈ span {x}

Tactic:
span,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
c : R
hc : c ∈ T
⊢ normalize b * id c ∈ R ∙ x
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((Units.map (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R)))) I)

Tactic:
Units.map_id,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ Quot.mk (⇑(QuotientGroup.leftRel (toPrincipalIdeal R (FractionRing R)).range)) I =
    (QuotientGroup.mk' (toPrincipalIdeal R (FractionRing R)).range)
      ((MonoidHom.id (FractionalIdeal R⁰ (FractionRing R))ˣ) I)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
⊢ (associatedPrimes A M).Finite

Tactic:
induction ‹Module.Finite A M› using
    IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime A with
  | subsingleton N => simp [associatedPrimes.eq_empty_of_subsingleton]
  | quotient N p f =>
    have := associatedPrimes.eq_singleton_of_isPrimary p.2.isPrimary
    simp [LinearEquiv.AssociatedPrimes.eq f, this]
  | exact N₁ N₂ N₃ f g hf _ hfg h₁ h₃ =>
    exact (h₁.union h₃).subset (associatedPrimes.subset_union_of_exact hf hfg)

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
⊢ includeRight ((algebraMap R p.ResidueField) (r * y)) * x = (y • a) ⊗ₜ[R] 1

Tactic:
smul_tmul,

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
⊢ includeRight ((algebraMap R p.ResidueField) (r * y)) * x = a ⊗ₜ[R] (y • 1)
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
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M

Tactic:
let : Module (Localization S) Mₚ := Module.compHom Mₚ (algebraMap _ Rₚ)

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ₚ)
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ comap (algebraMap R (Localization S)) p ∈ freeLocus R M
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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ r ∉ Ideal.comap (algebraMap R (p.asIdeal.Fiber S)) q.asIdeal

Tactic:
← PrimeSpectrum.comap_asIdeal

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
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ r ∉ (comap (algebraMap R (p.asIdeal.Fiber S)) q).asIdeal
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
f : R
⊢ ↑(basicOpen f) ⊆ freeLocus R M ↔ Projective (Localization.Away f) (LocalizedModule.Away f M)

Tactic:
rw [← freeLocus_eq_univ_iff, freeLocus_localization,
    Set.preimage_eq_univ_iff, localization_away_comap_range _ f]

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

Goal state before:
pp: case inr.refine_2
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
j' : E →ₐ[↥F⟮x⟯] L := IsSplittingField.lift E (Polynomial.map (algebraMap F ↥F⟮x⟯) p) ?inr.refine_1
⊢ a ∈ (↑j).range

pp: case inr.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ (Polynomial.map (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits

Tactic:
· change a ∈ j.range
      rw [← IsSplittingField.adjoin_rootSet_eq_range E p j,
            IsSplittingField.adjoin_rootSet_eq_range E p (j'.restrictScalars F)]
      exact ⟨x, (j'.commutes _).trans (algHomAdjoinIntegralEquiv_symm_apply_gen F hx _)⟩

Goal state after:
case inr.refine_1
F : Type u_1
inst✝² : Field F
E : Type u_3
inst✝¹ : Field E
inst✝ : Algebra F E
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
this✝ : FiniteDimensional F E
hx : IsIntegral F x
L : Type u_1 := (p * minpoly F x).SplittingField
hL1 : (Polynomial.map (algebraMap F (p * minpoly F x).SplittingField) p).Splits
j : E →ₐ[F] L := IsSplittingField.lift E p hL1
hL2 : (Polynomial.map (↑j) (Polynomial.map (algebraMap F E) (minpoly F x))).Splits
a : L
ha : a ∈ (Polynomial.map (algebraMap F L) (minpoly F x)).roots
this : Algebra (↥F⟮x⟯) L := ((algHomAdjoinIntegralEquiv F hx).symm ⟨a, ha⟩).toAlgebra
⊢ (Polynomial.map (algebraMap (↥F⟮x⟯) L) (Polynomial.map (algebraMap F ↥F⟮x⟯) p)).Splits
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 : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
Rp : Type u := Localization P.primeCompl
e✝ : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
| (e y • 1) ⊗ₜ[Rp] e x

Tactic:
smul_tmul,

Goal state after:
R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ LocalizedModule.mkLinearMap P.primeCompl M
ff : (P : Ideal R) →
  [inst : P.IsMaximal] → M ⊗[R] M →ₗ[R] LocalizedModule P.primeCompl M ⊗[R] LocalizedModule P.primeCompl M :=
  fun P [P.IsMaximal] ↦ map (f P) (f P)
P : Ideal R
x✝ : P.IsMaximal
Rp : Type u := Localization P.primeCompl
e✝ : LocalizedModule P.primeCompl M ≃ₗ[Rp] Rp
e : LocalizedModule P.primeCompl M ≃ₗ[R] Rp
x y : LocalizedModule P.primeCompl M
| 1 ⊗ₜ[Rp] (e y • e 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✝ : 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
γ : 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
x : (Polynomial.map ιFE g).SplittingField
hc : -(ιEE' γ - ιEE' (ιFE c) * x - ιEE' α) / (x - ιEE' β) ≠ (ιEE'.comp ιFE) c
hx : eval₂ ιEE' x h = 0
a : ¬x = ιEE' β
⊢ -(ιEE' α + ιEE' ((algebraMap F E) c) * ιEE' β - ιEE' (ιFE c) * x - ιEE' α) = ιEE' (ιFE c) * (x - ιEE' β)

Tactic:
ring

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

Goal state before:
pp: case refine_1
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
hIb : M.IsBase I
⊢ False

pp: case refine_2
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B

Tactic:
· obtain ⟨I', hII', hI', hne⟩ := hInotmax
    exact hne <| hIb.eq_of_subset_indep hII' hI'

Goal state after:
case refine_2
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
hB : M.Indep B ∧ ∀ ⦃t : Set α⦄, M.Indep t → B ⊆ t → B = t
hInotmax : ∃ x, M.Indep x ∧ I ⊆ x ∧ ¬I = x
⊢ M.IsBase B
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
⊢ False

Tactic:
obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_isBase hnb hB'

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False

Tactic:
exact hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
⊢ False

Tactic:
have hle := ncard_le_ncard hI₀B' hB'.finite

Goal state after:
α : Type u_1
M✝ : Matroid α
B✝ B'✝ I✝ J D X : Set α
e f : α
M : Matroid α
inst✝ : M.RankFinite
I : Set α
hI : ∀ J ⊆ I, J.Finite → M.Indep J
h : I.Infinite
B : Set α
hB : M.IsBase B
I₀ : Set α
hI₀I : I₀ ⊆ I
hI₀fin : I₀.Finite
hI₀card : I₀.ncard = B.ncard + 1
B' : Set α
hB' : M.IsBase B'
hI₀B' : I₀ ⊆ B'
hle : I₀.ncard ≤ B'.ncard
⊢ False
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis I X ↔ (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E

Tactic:
rw [IsBasis, maximal_subset_iff]

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ ((M.Indep I ∧ I ⊆ X) ∧ ∀ ⦃t : Set α⦄, M.Indep t ∧ t ⊆ X → I ⊆ t → I = t) ∧ X ⊆ M.E ↔
    (M.Indep I ∧ I ⊆ X ∧ ∀ ⦃J : Set α⦄, M.Indep J → I ⊆ J → J ⊆ X → I = J) ∧ X ⊆ M.E
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
E B I X R J : Set α✝
α : Type u_2
⊢ ExchangeProperty fun x ↦ x = ∅

Tactic:
rintro _ _ rfl; simp

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hI : M.IsBasis I X
hXY : X ⊆ Y
⊢ (M ↾ Y).IsBasis I X

Tactic:
rwa [← isBase_restrict_iff, M.restrict_restrict_eq hXY, isBase_restrict_iff]

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

Goal state before:
pp: α : Type u_1
I E B : Set α
hB : B ⊆ E
h : E \ B = I ∩ E
⊢ B = E \ I

Tactic:
by rw [← sdiff_sdiff_cancel_left hB, h, sdiff_inter_self_eq_sdiff]

Goal state after: