mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
⊢ x = y

Tactic:
obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)

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 : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
⊢ x = y
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 : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.lTensor (↥M) (inclusion hN)).range
⊢ x = y

Tactic:
obtain ⟨x', hx'⟩ := h (show x ∈ {x, y} by simp)

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 : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.lTensor (↥M) (inclusion hN)).range
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
⊢ x = y
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
n : ℕ
a : ⨂[R]^n M
⊢ (cast R M ⋯) (mulEquiv (a ⊗ₜ[R] (tprod R) Fin.elim0)) = a

Tactic:
induction a using PiTensorProduct.induction_on with
  | smul_tprod r a =>
    rw [← TensorProduct.smul_tmul', map_smul, map_smul, ← gMul_def, tprod_mul_tprod R a _,
      cast_tprod]
    simp
  | add x y hx hy =>
    rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]

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
inst✝ : Flat R M
ι : Type u
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
⊢ LinearIndependent R v

Tactic:
rw [linearIndependent_iff']

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
⊢ ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • v i = 0 → ∀ i ∈ s, g i = 0
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)
t : ⨂[R] (i : ι), s i
x✝¹ : R
x✝ : (i : ι) → s i
⊢ (tprod R) x✝ ∈ Set.range ⇑(tprod R)

Tactic:
simp only [Set.mem_range, exists_apply_eq_apply]

Goal state after:
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
n : ℕ
⊢ algebraMap₀ ↑(n + 1) = algebraMap₀ ↑n + GradedMonoid.GOne.one

Tactic:
simp only [Nat.cast_succ, map_add, algebraMap₀_one]

Goal state after:
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
⊢ Semiring (⨁ (n : ℕ), ⨂[R]^n M)

Tactic:
by infer_instance

Goal state after:
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
⊢ Algebra R (⨁ (n : ℕ), ⨂[R]^n M)

Tactic:
by infer_instance

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
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : h.toFinset.inf id ^ n ≤ ann
⊢ ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I

Tactic:
← Finset.insert_erase (h.mem_toFinset.mpr hI),

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
n : ℕ
hn0 : n ≠ 0
h : ann.minimalPrimes.Finite
hn : (insert I (h.toFinset.erase I)).inf id ^ n ≤ ann
⊢ ∃ n, n ≠ 0 ∧ ∃ J, I ^ n * J ≤ ann ∧ ¬J ≤ I
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case refine_1
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x✝ : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
⊢ (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (x • (tprod R) y)) = x • (tprod R) y

Tactic:
simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply,
        smul_eq_mul, mul_one]

Goal state after:
case refine_1
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x✝ : ⨂[R] (i : ι), s i
x : R
y : (i : ι) → s i
⊢ x • (tprod R) isEmptyElim = x • (tprod R) y
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
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
i j : Fin (Nat.succ 0).succ
hij : ![a, b] i = ![a, b] j
⊢ i = j

Tactic:
by
    fin_cases i <;> fin_cases j
    · rfl
    · simp [hab] at hij
    · simp [hab.symm] at hij
    · rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝³ : CommSemiring R
M : Type u_8
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Subsingleton ι
i₀ : ι
x : M
⊢ (subsingletonEquiv i₀).symm x = (tprod R) fun x_1 ↦ x

Tactic:
by
  simp [LinearEquiv.symm_apply_eq, subsingletonEquiv_apply_tprod]

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 ∉ ⊥
H₁ : ⊥.colon {y} ≤ ⊥.colon {a • y}
⊢ b ∈ ⊥.colon {y}

Tactic:
rwa [H₁.eq_of_not_lt (h₃ _ ⟨l.trans H₁, by simpa, _, rfl⟩),
    mem_colon_singleton, smul_comm, smul_smul]

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
I : (FractionalIdeal R⁰ K)ˣ
⊢ I ∈ (toPrincipalIdeal R K).range ↔ ∃ x, spanSingleton R⁰ x = ↑I

Tactic:
by
  simp only [MonoidHom.mem_range, toPrincipalIdeal_eq_iff]
  constructor <;> rintro ⟨x, hx⟩
  · exact ⟨x, hx⟩
  · refine ⟨Units.mk0 x ?_, hx⟩
    rintro rfl
    simp [I.ne_zero.symm] at hx

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

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
⊢ x ≠ 0

Tactic:
rintro hx

Goal state after:
case refine_1.refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
x y : R
hy : y ∈ R⁰
hz : mk' (FractionRing R) x ⟨y, hy⟩ ≠ 0
h : spanSingleton R⁰ (mk' (FractionRing R) x ⟨y, hy⟩) * ↑↑I = ↑↑J
hx : x = 0
⊢ False
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J) →
    ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J

pp: case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) →
    ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J

Tactic:
· rintro ⟨z, hz, h⟩
    obtain ⟨x, ⟨y, hy⟩, rfl⟩ := IsLocalization.exists_mk'_eq R⁰ z
    refine ⟨x, y, ?_, mem_nonZeroDivisors_iff_ne_zero.mp hy, ?_⟩
    · rintro hx; apply hz
      rw [hx, IsFractionRing.mk'_eq_div, map_zero, zero_div]
    · exact (FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal _ hy).mp h

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ (∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J) →
    ∃ x, ∃ (_ : x ≠ 0), spanSingleton R⁰ x * ↑↑I = ↑↑J
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)ˣ
⊢ I ∈ Subgroup.map (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range ↔
    I ∈ (toPrincipalIdeal S L).range

Tactic:
simp only [MulEquiv.toMonoidHom_eq_coe, Subgroup.mem_map, MonoidHom.mem_range,
    toPrincipalIdeal_eq_iff, MonoidHom.coe_coe]

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
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_1, spanSingleton R⁰ ↑x_1 = ↑x) ∧ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) x = I) ↔
    ∃ x, spanSingleton S⁰ ↑x = ↑I
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
i : Bool
⊢ ContinuousOn (fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩) (bif i then C₁ else C₂)

Tactic:
cases i <;> rw [continuousOn_iff_continuous_domRestrict]

Goal state after:
case refine_2.false
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif false then C₁ else C₂).domRestrict fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩)

case refine_2.true
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h✝ : C₁ ∪ C₂ = univ
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ Continuous[instTopologicalSpaceSubtype, dZ]
    ((bif true then C₁ else C₂).domRestrict fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩)
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
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
e : Localization.AtPrime p.asIdeal ≃+* Rₚ :=
  (IsLocalization.algEquiv p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal) Rₚ).toRingEquiv
⊢ p ∈ freeLocus R M ↔ Free Rₚ Mₚ

Tactic:
apply Module.Free.iff_of_equiv (σ := e)

Goal state after:
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
p : PrimeSpectrum R
Rₚ : Type u_1
Mₚ : Type u_2
inst✝⁷ : CommRing Rₚ
inst✝⁶ : Algebra R Rₚ
inst✝⁵ : IsLocalization.AtPrime Rₚ p.asIdeal
inst✝⁴ : AddCommGroup Mₚ
inst✝³ : Module R Mₚ
f : M →ₗ[R] Mₚ
inst✝² : IsLocalizedModule p.asIdeal.primeCompl f
inst✝¹ : Module Rₚ Mₚ
inst✝ : IsScalarTower R Rₚ Mₚ
e : Localization.AtPrime p.asIdeal ≃+* Rₚ := ⋯
⊢ LocalizedModule p.asIdeal.primeCompl M ≃ₛₗ[↑e] Mₚ
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case neg
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
h : IsNormalClosure F K L
L' : Type ?u.22
inst✝¹ : Field L'
inst✝ : Algebra F L'
splits : ∀ (x : K), (Polynomial.map (algebraMap F L') (minpoly F x)).Splits
this : adjoin F (⨆ x, (minpoly F x).rootSet L) = ⊤
x : L
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L
y : K
hx : x ∈ (minpoly F y).rootSet L
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L') (minpoly F x)).Splits

Tactic:
simp [minpoly.eq_zero iy] at hx

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

Goal state before:
pp: case neg
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
h : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
L' : Type u_4
inst✝¹ : Field L'
inst✝ : Algebra F L'
x : L'
hx✝ : x ∈ ⨆ x, (minpoly F x).rootSet L'
y : K
hx : x ∈ (minpoly F y).rootSet L'
iy : ¬IsIntegral F y
⊢ (Polynomial.map (algebraMap F L) (minpoly F x)).Splits

Tactic:
simp [minpoly.eq_zero iy] at hx

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

Goal state before:
pp: F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ normalClosure F (↥(map (↑σ) K)) L = normalClosure F (↥K) L

Tactic:
simp_rw [normalClosure_def'', map_map]

Goal state after:
F : Type u_1
L : Type u_3
inst✝³ : Field F
inst✝² : Field L
inst✝¹ : Algebra F L
inst✝ : Normal F L
K : IntermediateField F L
σ✝ : L →ₐ[F] L
σ : Gal(L/F)
⊢ ⨆ f, map ((↑f).comp ↑σ) K = ⨆ f, map (↑f) K
Module: Mathlib.RingTheory.AlgebraicIndependent.Defs

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p : MvPolynomial ι' R
⊢ ∀ ⦃a₂ : MvPolynomial ι' R⦄, (aeval (x ∘ f)) p = (aeval (x ∘ f)) a₂ → p = a₂

Tactic:
q

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
hx : AlgebraicIndependent R x
f : ι' → ι
hf : Injective f
p q : MvPolynomial ι' R
⊢ (aeval (x ∘ f)) p = (aeval (x ∘ f)) q → p = q
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
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' (ιEE' γ - ιEE' (ιFE c) * eval₂ ιEE' x X) (Polynomial.map ιFE f) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots

Tactic:
eval₂_X,

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
x : (Polynomial.map ιFE g).SplittingField
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' (ιEE' γ - ιEE' (ιFE c) * x) (Polynomial.map ιFE f) = 0
⊢ ιEE' γ - ιEE' (ιFE c) * x ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots
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
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
⊢ E.val.fieldRange = E

Tactic:
IntermediateField.fieldRange_val

Goal state after:
F : Type u_1
K : Type u_2
inst✝³ : Field F
inst✝² : Field K
inst✝¹ : Algebra F K
E : IntermediateField F K
inst✝ : Normal F ↥E
f : ↥E →ₐ[F] K
g : Gal(↥E/F) := f.restrictNormal' ↥E
⊢ E = E
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
⊢ M.IsBase (insert f B \ {e})

Tactic:
rw [← insert_sdiff_singleton_comm hfe] at *

Goal state after:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
hfe : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X ∩ M.E) I ∧ X ∩ M.E ⊆ M.E

Tactic:
and_iff_left inter_subset_right,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
⊢ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ↔ Maximal (fun A ↦ M.Indep A ∧ A ⊆ X ∩ M.E) I
Module: Mathlib.Combinatorics.Matroid.Basic

Goal state before:
pp: α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I

Tactic:
exact hIX.indep

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

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

Tactic:
by simp [h, subset_empty_iff]

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

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

Tactic:
rw [← h]; rfl

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

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
h : M ↾ R <r M
h' : (M ↾ R).E = M.E
⊢ M = M ↾ R ↾ R

Tactic:
rw [show R = M.E from h', restrict_idem, restrict_ground_eq_self]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f✝ : α → β
E I : Set α
M : Matroid α
N✝ N : Matroid β
inst✝ : N.RankFinite
f : α → β
B : Set α
hB : N.IsBasis (f '' B) (f '' f ⁻¹' N.E) ∧ InjOn f B ∧ B ⊆ f ⁻¹' N.E
⊢ B.Finite

Tactic:
exact (hB.1.indep.finite.of_finite_image hB.2.1)

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ (I ∪ J) \ I, M.Dep (insert e I)

Tactic:
union_sdiff_left,

Goal state after:
α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
hJ : M.Indep J
hIJ : I.encard < J.encard
he : ∀ e ∈ J \ I, ¬M.Indep (insert e I)
⊢ ∀ e ∈ J \ I, M.Dep (insert e I)
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
inst✝ : M.RankFinite
⊢ M.IsRkFinite M.E

Tactic:
rwa [isRkFinite_ground_iff_rankFinite]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M.IsCircuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})

Tactic:
wlog hCE : C ⊆ M.E
  · exact iff_of_false (hCE ∘ IsCircuit.subset_ground) (fun h ↦ hCE h.1.subset_ground)
  simp [isCircuit_iff_minimal_not_indep hCE, ← not_indep_iff hCE,
    minimal_iff_forall_sdiff_singleton (P := (¬ M.Indep ·))
    (fun _ _ hY hYX hX ↦ hY <| hX.subset hYX)]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∈ X
h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
by
    simpa [subset_antisymm_iff, fundCircuit]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
heX : e ∉ M.E
h : ∀ a ∈ X, (∀ t ⊆ X, M.closure {e} ⊆ M.closure t → a ∈ t) → a = e
⊢ M.fundCircuit e X = {e}

Tactic:
by
    simpa [subset_antisymm_iff, fundCircuit]

Goal state after: