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

Goal state before:
pp: K : Type u_1
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₃
u u' : V₃ →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h : u.IsQuasiInverse v
h' : u'.IsQuasiInverse v'
hu : u ≈ u'
⊢ v ∘ₗ u' ∘ₗ v' ≈ v ∘ₗ u ∘ₗ v'

Tactic:
by grw [hu]

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
⊢ ∃ b, ∀ i ∈ s, IsInteger f (↑b • g i)

Tactic:
choose sec hsec using (fun i ↦ IsLocalizedModule.surj S f (g i))

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
M' : Type u_3
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
⊢ ∃ b, ∀ i ∈ s, IsInteger f (↑b • g i)
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: case mp
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x✝ : M'
⊢ x✝ ∈ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach → x✝ ∈ commonDenomOfFinset S f s • ↑s

Tactic:
rintro ⟨_, ⟨x, -, rfl⟩, rfl⟩

Goal state after:
case mp
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
x : ↥s
⊢ f ((fun t ↦ integerMultiple S f s id t) x) ∈ commonDenomOfFinset S f s • ↑s
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ supported R s = (rename Subtype.val).range

Tactic:
by
  rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename_eq_aeval]
  congr

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

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

Tactic:
classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) := ⋯
⊢ ↑(p ^ (pOrder hM y - k) • ⟨p ^ k • x, h⟩) = ↑0

Tactic:
coe_smul_of_tower,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsDomain R
p : R
hp : Irreducible p
hM : IsTorsion' M ↥(Submonoid.powers p)
dec : (x : M) → Decidable (x = 0)
x y : M
k : ℕ
hM' : IsTorsionBy R M (p ^ pOrder hM y)
h : p ^ k • x ∈ R ∙ y
hk : k ≤ pOrder hM y
f : (R ⧸ R ∙ p ^ (pOrder hM y - k) * p ^ k) ≃ₗ[R] ↥(R ∙ y) :=
  (R ∙ p ^ (pOrder hM y - k) * p ^ k).quotEquivOfEq (torsionOf R M y) ?pos.refine_1✝ ≪≫ₗ
    quotTorsionOfEquivSpanSingleton R M y
⊢ p ^ (pOrder hM y - k) • ↑⟨p ^ k • x, h⟩ = ↑0
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ R ∙ p ^ finZeroElim i)

Tactic:
Set.range_eq_empty,

Goal state after:
case h
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin 0 → M
hs : Submodule.span R ∅ = ⊤
⊢ Nonempty (M ≃ₗ[R] ⨁ (i : Fin 0), R ⧸ R ∙ p ^ finZeroElim i)
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i j : σ
h : j ≠ i
⊢ (pderiv i) (X j) = 0

Tactic:
classical simp [h]

Goal state after:
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ R ∙ p ^ k i)

Tactic:
| succ d IH =>

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) f = derivative f • (AEval.of R M a) (d a)

Tactic:
simpa using AEval.of_aeval_smul _ _ _

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case mp
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
hα_mem : α ∈ J.rootSet
hα_not : (rootSystem H).root α ∉ q
hα_nz : (↑α).IsNonZero
hne : ∀ (χ : Weight K (↥H) L), Weight.toLinear K (↥H) L χ ∈ q → ⇑χ ≠ ⇑↑α
h_le : LieSubmodule.restr J H ≤ ⨆ χ, ⨆ (_ : χ ≠ ⇑↑α), genWeightSpace L χ
h_disj : Disjoint ((fun χ ↦ genWeightSpace L χ) ⇑↑α) (rootSpace H ⇑↑α)
⊢ False

Tactic:
exact (α : Weight K H L).genWeightSpace_ne_bot L (disjoint_self.mp h_disj)

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
b : ι' → S
s : S
⊢ ∃ a, (aeval (Sum.elim P.val b)) a = s

Tactic:
use rename Sum.inl (P.σ s)
    simp [aeval_rename]

Goal state after:
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a.convert_4.add.hf
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
p q : MvPolynomial (ι' ⊕ ι) R
hp :
  (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) p)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom p)
hq :
  (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) q)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom q)
⊢ Function.HasFiniteSupport fun i_1 ↦ if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) p)) else 0

Tactic:
refine (((support p).map e).finite_toSet.subset ?_)

Goal state after:
case a.convert_4.add.hf
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this✝ : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
p q : MvPolynomial (ι' ⊕ ι) R
hp :
  (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) p)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom p)
hq :
  (∑ᶠ (i_1 : (ι' →₀ ℕ) × (ι →₀ ℕ)), if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) q)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom q)
⊢ (Function.support fun i_1 ↦ if i_1.1 = i then (aeval P.val) ((monomial i_1.2) (coeff (e.symm i_1) p)) else 0) ⊆
    ↑(Finset.map (↑e).toEmbedding p.support)
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝²³ : CommRing R
inst✝²² : CommRing S
inst✝²¹ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝²⁰ : CommRing R'
inst✝¹⁹ : CommRing S'
inst✝¹⁸ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁷ : Algebra R R'
inst✝¹⁶ : Algebra S S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹³ : CommRing R''
inst✝¹² : CommRing S''
inst✝¹¹ : Algebra R'' S''
P'' : Extension R'' S''
inst✝¹⁰ : Algebra R R''
inst✝⁹ : Algebra S S''
inst✝⁸ : Algebra R S''
inst✝⁷ : IsScalarTower R R'' S''
inst✝⁶ : Algebra R' R''
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra R' S''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : IsScalarTower R R' R''
inst✝¹ : IsScalarTower S S' S''
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
this✝² : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S S'
this✝ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this : IsScalarTower P.Ring P'.Ring S'
x : R
⊢ (algebraMap R S') x = (algebraMap S S') ((algebraMap P.Ring S) ((algebraMap R P.Ring) x))

Tactic:
rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]

Goal state after:
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ((↑(2 * l) + ↑1) % (n + n))

Tactic:
val_mul,

Goal state after:
n : ℕ
inst✝ : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ((↑2 * ↑l % (n + n) + ↑1) % (n + n))
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even ↑k

Tactic:
by
  refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(even_of_odd · k), even_of_val⟩⟩
  rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]
  exact fun hn ↦ (even_iff_of_even hn).mp hk

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

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

Tactic:
exact h.antisymm (Submodule.le_of_le_smul_of_le_jacobson_bot h'
      (by rw [jacobson_eq_maximalIdeal]; exact bot_ne_top) this)

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

Goal state before:
pp: case insert.specialize_2
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
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
⊢ ∑ i ∈ s, f i • (v + fun x ↦ c x • v ↑n) i = 0

Tactic:
rw [Finset.sum_coe_sort _ (fun i ↦ f i • v i), s.sum_insert hn, add_comm, hfn] at hfv
    simp_rw [Pi.add_apply, smul_add, s.sum_add_distrib, c, smul_smul, ← s.sum_smul, ← mul_assoc,
      ← s.sum_mul, mul_neg, s.sum_neg_distrib, ← hfv]
    congr 4
    exact s.sum_congr rfl fun i hi ↦ by rw [if_neg (ne_of_mem_of_not_mem hi hn)]

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✝ : Subsingleton M
⊢ associatedPrimes R M = ∅

Tactic:
by
  ext; simp only [Set.mem_empty_iff_false, iff_false]
  apply not_isAssociatedPrime_of_subsingleton

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J ∈ {I.radical}

Tactic:
rw [Set.mem_singleton_iff]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ J ∈ associatedPrimes R (R ⧸ I) ↔ J = I.radical
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0
⊢ ↑((toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero) * I) =
    ↑((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)

Tactic:
val_mul,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
fd_ne_zero : (algebraMap R (FractionRing R)) ↑(↑I).den ≠ 0
⊢ ↑((toPrincipalIdeal R (FractionRing R)) (Units.mk0 ((algebraMap R (FractionRing R)) ↑(↑I).den) fd_ne_zero)) * ↑I =
    ↑((FractionalIdeal.mk0 (FractionRing R)) ⟨integralRep ↑I, ⋯⟩)
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
⊢ ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)

Tactic:
intro P

Goal state after:
R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
P : Ideal R
⊢ ∀ (x : P.IsMaximal), Projective (Localization.AtPrime P) (LocalizedModule P.primeCompl 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 ∉ (comap (algebraMap R (p.asIdeal.Fiber S)) q).asIdeal

Tactic:
convert! hr

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
⊢ comap (algebraMap R (p.asIdeal.Fiber S)) q = p
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
n✝ : ℕ
hn : derivedSeries G (n✝ + 1) = ⊥
⊢ ∀ (a b : G), a * b = b * a

Tactic:
· rw [IsSimpleGroup.derivedSeries_succ] at hn
      intro a b
      rw [← mul_inv_eq_one, mul_inv_rev, ← mul_assoc, ← mem_bot, ← hn, commutator_eq_closure]
      exact subset_closure ⟨a, b, rfl⟩

Goal state after:
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' ↦ Multiset.map (fun β' ↦ -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c

Tactic:
obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset s'

Goal state after:
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := (Polynomial.map ϕ f).roots
sg : Multiset E := (Polynomial.map ϕ g).roots
s : Finset E := (sf.bind fun α' ↦ Multiset.map (fun β' ↦ -(α' - α) / (β' - β)) sg).toFinset
s' : Finset F := s.preimage ⇑ϕ ⋯
c : F
hc : c ∉ s'
⊢ ∃ c, ∀ α' ∈ (Polynomial.map ϕ f).roots, ∀ β' ∈ (Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ≠ ϕ c
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • β
⊢ β ∈ F⟮γ⟯

Tactic:
let p := EuclideanDomain.gcd ((f.map (algebraMap F F⟮γ⟯)).comp
    (C (AdjoinSimple.gen F γ) - (C ↑c : F⟮γ⟯[X]) * X)) (g.map (algebraMap F F⟮γ⟯))

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)
⊢ β ∈ F⟮γ⟯
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
K : IntermediateField F L
inst✝ : Normal F L
⊢ normalClosure F (↥K) L = ⨆ f, map f K

Tactic:
refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
  · exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)
  · exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)

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

Goal state before:
pp: case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : normalClosure F (↥K₁) L ≤ K₂
⊢ K₁ ≤ K₂

Tactic:
normalClosure_le_iff

Goal state after:
case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
⊢ K₁ ≤ K₂
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: 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)ˣ
T T' : Finset A
hT : ↑T ⊆ ↑↑I⁻¹
hT' : ↑T' ⊆ ↑↑I
S : Finset A := Finset.image₂ (fun x1 x2 ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ ↑S ∧ ∑ a ∈ S, r a • a = 1
a : ↥S → A
ha : ∀ (i : ↥S), a i ∈ T
b : ↥S → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = ↑i
i : ↥S
x : A
hx : x ∈ ↑I
⊢ (LinearMap.mulRight R (r ↑i • a i)) x ∈ (Algebra.linearMap R A).range

Tactic:
rw [← one_eq_range, ← I.mul_inv]; exact mul_mem_mul hx (I⁻¹.1.smul_mem _ <| hT <| ha i)

Goal state after:
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: case mp.refine_1
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
e' : R ≃ₗ[R] ↥↑I⁻¹
h : ↑I = R ∙ ↑(↑e 1)
h' : ↑I⁻¹ = R ∙ ↑(↑e' 1)
this : R ∙ ↑(e 1) * ↑(e' 1) = 1
r : Rˣ
hr : ↑(e 1) * ↑(e' 1) = (algebraMap R A) ↑r
⊢ ∃ b, (↑e 1).1 * b = 1

Tactic:
exact ⟨e' 1 * algebraMap R A r.inv, by simp [← mul_assoc, hr, ← map_mul]⟩

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

Goal state before:
pp: α : Type u_1
M✝ : Matroid α
R✝ I X Y : Set α
M : Matroid α
R : Set α
⊢ ∀ X ⊆ R, ExistsMaximalSubsetProperty (fun I ↦ M.Indep I ∧ I ⊆ R) X

Tactic:
rintro A hAR I ⟨hI, _⟩ hIA

Goal state after:
α : Type u_1
M✝ : Matroid α
R✝ I✝ X Y : Set α
M : Matroid α
R A : Set α
hAR : A ⊆ R
I : Set α
hI : M.Indep I
right✝ : I ⊆ R
hIA : I ⊆ A
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ M.Indep I ∧ I ⊆ R) K ∧ K ⊆ A) J
Module: Mathlib.Combinatorics.Matroid.Constructions

Goal state before:
pp: α : Type u_1
E R : Set α
h : R ⊆ E
⊢ freeOn E ↾ R = freeOn R

Tactic:
by
  simp [h, eq_freeOn_iff]

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

Goal state before:
pp: α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).IsBase ∅

Tactic:
simpa [uniqueBaseOn_isBase_iff hIE] using Ne.symm <| hI.ne_empty

Goal state after: