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

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
⊢ DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
have hI := Submodule.annihilator_top_inter_nonZeroDivisors hM

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
hM' : Module.IsTorsionBySet R M ↑⊤.annihilator
hI : (↑⊤.annihilator ∩ ↑(nonZeroDivisors R)).Nonempty
⊢ DirectSum.IsInternal fun p ↦ torsionBySet R M ↑(↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V' : Type u_3
V₂ : Type u_4
V₂' : Type u_5
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
a✝ b✝ : V →ₗ[K] V₂
hu : a✝ ∈ {u | u.HasNoetherianRange}
hv : b✝ ∈ {u | u.HasNoetherianRange}
⊢ a✝ + b✝ ∈ {u | u.HasNoetherianRange}

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V' : Type u_3
V₂ : Type u_4
V₂' : Type u_5
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
c : K
hu : V →ₗ[K] V₂
⊢ hu ∈ {u | u.HasNoetherianRange} → c • hu ∈ {u | u.HasNoetherianRange}

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h' : v ≈ v'
⊢ v ∘ₗ u ≈ v' ∘ₗ u

Tactic:
rw [equiv_iff_hasNoetherianRange] at *

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u : V →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h' : (v - v').HasNoetherianRange
⊢ (v ∘ₗ u - v' ∘ₗ u).HasNoetherianRange
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : u ≈ v
⊢ u' ∘ₗ u ≈ u' ∘ₗ v

Tactic:
rw [equiv_iff_hasNoetherianRange] at *

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : (u - v).HasNoetherianRange
⊢ (u' ∘ₗ u - u' ∘ₗ v).HasNoetherianRange
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
ι : Type u_4
s : Finset ι
P : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (P i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j
f : R ⧸ ∏ i ∈ s, P i ^ e i ≃+* ((i : ↥s) → R ⧸ P ↑i ^ e ↑i) :=
  quotientEquivPiOfFinsetProdEq (∏ i ∈ s, P i ^ e i) P e prime coprime ⋯
z : R
⊢ ∃ y,
    ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = f ((Ideal.Quotient.mk (∏ i ∈ s, P i ^ e i)) z) ⟨i, hi⟩

Tactic:
exact ⟨z, fun i _hi => rfl⟩

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
⊢ p ∈ supported R ↑p.vars

Tactic:
by
  rw [mem_supported]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝ : CommSemiring R
f g : R[X]
⊢ { toFun := ⇑derivative, map_add' := ⋯, map_smul' := ⋯ } (f * g) =
    f • { toFun := ⇑derivative, map_add' := ⋯, map_smul' := ⋯ } g +
      g • { toFun := ⇑derivative, map_add' := ⋯, map_smul' := ⋯ } f

Tactic:
by simp [mul_comm, add_comm, derivative_mul]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Polynomial

Goal state before:
pp: R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ ((mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x

Tactic:
suffices ((Finsupp.lapply i).comp
    (mvPolynomialBasis R σ).repr.toLinearMap).compDer (D _ _) = MvPolynomial.pderiv i by
    rw [← this]; rfl

Goal state after:
R : Type u
inst✝ : CommRing R
σ : Type u_1
x : MvPolynomial σ R
i : σ
⊢ (Finsupp.lapply i ∘ₗ ↑(mvPolynomialBasis R σ).repr).compDer (D R (MvPolynomial σ R)) = MvPolynomial.pderiv i
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
r : σ'
| Q.relation r

Tactic:
rw [← (Q.relation r).ofCoeff_coeff,
    ← Finsupp.sum_single (AddMonoidAlgebra.coeff <| Q.relation r)]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
r : σ'
| AddMonoidAlgebra.ofCoeff ((Q.relation r).coeff.sum Finsupp.single)
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case h.left
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⇑f
x' : Fin l → M := fun i ↦ x (Finsupp.single i 1)
this : ∑ i, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i, f' i * a' i j = 0
i : Fin l
⊢ x (Finsupp.basisSingleOne i) =
    (linearCombination R y' ∘ₗ linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) (Finsupp.basisSingleOne i)

Tactic:
simpa [linearCombination_apply, sum_fintype, Finsupp.single_apply] using ha'y' i

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Flat R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : N
x : N →ₗ[R] M
h : x f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
⊢ (x ∘ₗ ↑e) (e.symm f) = 0

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ 1 • m = 0

Tactic:
by simpa using h

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ↑(N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n)) = ↑(y • n)

Tactic:
simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = (algebraMap R S) y * ↑n
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ↑(Fin.cast ⋯ j) = ↑j

Tactic:
Fin.val_cast

Goal state after:
case e_6
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a✝ : ⨂[R]^na M
b✝ : ⨂[R]^nb M
c✝ : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
a : Fin na → M
b : Fin nb → M
c : Fin nc → M
j : Fin (na + (nb + nc))
⊢ ↑j = ↑j
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
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
⊢ (associatedPrimes R M).Nonempty

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)
  obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx
  exact ⟨P, hP⟩

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
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : P.IsPrime ∧ ∃ x, P = ⊥.colon {x}
hx : ⊥.colon {x} ≤ P
⊢ r ∈ ⊥.colon {x}

Tactic:
by rwa [mem_colon_singleton]

Goal state after:
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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : ⊤ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ N₁ ≤ N₂

Tactic:
by simp_all

Goal state after:
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
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
x✝ : ∃ x, (⊥.colon {N₁.mkQ x}).IsPrime ∧ N₂ = N₁ ⊔ A ∙ x
x : M
hx : (⊥.colon {N₁.mkQ x}).IsPrime
hx' : N₂ = N₁ ⊔ A ∙ x
hxN₂ : x ∈ N₂
this : ⊤ = (N₁ ⊔ A ∙ x).submoduleOf N₂
⊢ A ∙ x ≤ N₂

Tactic:
by simp_all

Goal state after:
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 ↑(RingEquiv.refl (FractionalIdeal R⁰ (FractionRing R)))) I)

Tactic:
RingEquiv.coe_monoidHom_refl,

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)
      ((Units.map (MonoidHom.id (FractionalIdeal R⁰ (FractionRing R)))) I)
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst✝¹] (U.ite (⇑f ⁻¹' s) (1 ⁻¹' s))

Tactic:
Set.ite,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst✝¹] (⇑f ⁻¹' s ∩ U ∪ 1 ⁻¹' s \ U)
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
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ q.asIdeal

Tactic:
rw [← Ideal.mem_comap, ← 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.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
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ q.asIdeal

Tactic:
rw [← Ideal.mem_comap, ← PrimeSpectrum.comap_asIdeal]
      convert! hr
      exact (residueField_comap _).le ⟨q.comap (algebraMap _ _), rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
inst✝⁵ : CommRing R
ι : Type u_1
inst✝⁴ : Finite ι
M : ι → Type u_2
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : ∀ (i : ι), Flat R (M i)
inst✝ : ∀ (i : ι), Module.Finite R (M i)
p : PrimeSpectrum R
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk (M i) p

Tactic:
by
  cases nonempty_fintype ι
  let f : (Π i, M i) →ₗ[R] Π i, LocalizedModule p.asIdeal.primeCompl (M i) :=
    .pi (fun i ↦ mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj i)
  let e : LocalizedModule p.asIdeal.primeCompl (Π i, M i) ≃ₗ[Localization.AtPrime p.asIdeal]
      Π i, LocalizedModule p.asIdeal.primeCompl (M i) :=
    IsLocalizedModule.linearEquiv p.asIdeal.primeCompl
      (mkLinearMap _ _) f |>.extendScalarsOfIsLocalization p.asIdeal.primeCompl _
  have (i : ι) : Free (Localization.AtPrime p.asIdeal)
      (LocalizedModule p.asIdeal.primeCompl (M i)) :=
    free_of_flat_of_isLocalRing
  simp_rw [rankAtStalk, e.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype]

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module.Invertible R M
f : N →ₗ[R] P
⊢ Function.Surjective ⇑(LinearMap.lTensor M f) ↔ Function.Surjective ⇑f

Tactic:
refine ⟨fun h ↦ ?_, LinearMap.lTensor_surjective _⟩
  rw [← leftCancelEquiv_comp_lTensor_comp_symm (linearEquiv R M) f]
  simpa using LinearMap.lTensor_surjective _ h

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = ↑α ^ n

Tactic:
norm_cast; rw [hn, Units.val_mk0]

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case hg
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] := ⋯
g : F[X] := ⋯
ιFE : F →+* E := ⋯
ιEE' : 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 := ⋯
p : (↥F⟮γ⟯)[X] := ⋯
h : E[X] := ⋯
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : h.Separable
⊢ eval β (Polynomial.map ιFE g) = 0

Tactic:
rw [eval_map_algebraMap, minpoly.aeval]

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase (insert f (B \ (B \ B')))

Tactic:
← singleton_union,

Goal state after:
case inr
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
B' : Set α
hB' : M.IsBase B'
hfB : f ∈ B'
h : B \ B' = {e}
hx : B' \ B = {f}
⊢ M.IsBase ({f} ∪ B \ (B \ B'))
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (unitsToPic R A).ker
⊢ I ∈ (Units.map ↑(spanSingleton R)).range

Tactic:
have e := (mk_eq_one_iff.mp h).some.symm

Goal state after:
case mp
R : Type u
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
I : (Submodule R A)ˣ
h : I ∈ (unitsToPic R A).ker
e : R ≃ₗ[R] ↥↑I
⊢ I ∈ (Units.map ↑(spanSingleton R)).range
Module: Mathlib.Combinatorics.Matroid.Dual

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
I B✝ X✝ : Set α
M : Matroid α
X I' : Set α
hI'E : I' ⊆ M.E
B : Set α
hB : M.IsBase B
hI'B : Disjoint I' B
hI'X : I' ⊆ X
B' : Set α
hB' : M.IsBase B'
hI : M.IsBasis (B' \ X) (M.E \ X)
hIB' : B' \ X ⊆ B'
hB'IB : B' ⊆ B' \ X ∪ B
J : Set α
hJE : J ⊆ M.E
B'' : Set α
hB'' : M.IsBase B''
hdj : Disjoint J B''
hJX : J ⊆ X
hXJ : X \ B' ∩ M.E ⊆ J
hI' : B'' ∩ X ∪ B' \ X ⊆ B'
B₁ : Set α
hB₁ : M.IsBase B₁
hI'B₁ : B'' ∩ X ∪ B' \ X ⊆ B₁
hB₁I : B₁ ⊆ B'' ∪ B' \ X
e : α
he : e ∈ B₁
heB'' : e ∈ B''
heX : e ∉ X
⊢ M.Indep (insert e (B' \ X))

Tactic:
exact hB₁.indep.subset (insert_subset he (subset_union_right.trans hI'B₁))

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

Goal state before:
pp: α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ M₁.toMatroid.E
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ M₁ = M₂

Tactic:
rw [h, restrict_ground_eq] at hR'

Goal state after:
α✝ : Type u_1
M : Matroid α✝
R✝ I X Y : Set α✝
N : Matroid α✝
α : Type u_2
M₁ M₂ : Matroidᵣ α
R : Set α
h : M₁.toMatroid = M₂.toMatroid ↾ R
R' : Set α
hR : R ⊆ R'
hR' : R' ⊆ R
h' : M₂.toMatroid = M₁.toMatroid ↾ R'
⊢ M₁ = M₂
Module: Mathlib.Combinatorics.Matroid.Rank.Finite

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite (insert e X) ↔ M.IsRkFinite X

Tactic:
← singleton_union,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
e : α
⊢ M.IsRkFinite ({e} ∪ X) ↔ M.IsRkFinite X
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
R : Set α
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E

Tactic:
by
  rw [← closure_empty, ← closure_empty, restrict_closure_eq', empty_inter]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
⊢ (M.comap f).closure ∅ = f ⁻¹' M.loops

Tactic:
comap_closure_eq,

Goal state after:
α : Type u_1
β : Type u_2
M : Matroid β
f : α → β
⊢ f ⁻¹' M.closure (f '' ∅) = f ⁻¹' M.loops
Module: Mathlib.Combinatorics.Matroid.Circuit

Goal state before:
pp: case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J})

pp: case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})

Tactic:
· gcongr 5 with J hJI; intro heJ
    simp only [restrict_closure_eq']
    refine (inter_subset_inter_left _ ?_).trans subset_union_left
    rwa [inter_eq_self_of_subset_left (hJI.trans hIR)]

Goal state after:
case a
α : Type u_1
M : Matroid α
I : Set α
e : α
R : Set α
hIR : I ⊆ R
heR : e ∈ R
hR : R ⊆ M.E
⊢ insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ⊆ M.closure J}) ⊆
    insert e (I ∩ ⋂₀ {J | J ⊆ I ∧ M.closure {e} ∩ R ⊆ (M ↾ R).closure J})
Module: Mathlib.Combinatorics.Matroid.Loop

Goal state before:
pp: α : Type u_1
M : Matroid α
E : Set α
h : M = loopyOn E
⊢ M.loops = E ∧ M.E = E

Tactic:
by simp [h, loops]

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

Goal state before:
pp: case refine_3
α : Type u_1
M : Matroid α
ι : Type u_2
C₀ : Set α
hC₀ : M.IsCircuit C₀
x : ι → α
C : ι → Set α
hC : ∀ (i : ι), M.IsCircuit (C i)
h_mem_C₀ : ∀ (i : ι), x i ∈ C₀
h_mem : ∀ (i : ι), x i ∈ C i
h_unique : ∀ ⦃i i' : ι⦄, x i ∈ C i' → i = i'
i : ι
hzC₀ : x i ∈ C₀
hzC : ∀ (i_1 : ι), x i ∉ C i_1
⊢ False

Tactic:
exact hzC _ (h_mem i)

Goal state after: