mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
c : A
hc : c * a = y * b
⊢ (algebraMap A K) (y * b) * ((algebraMap A K) a)⁻¹ ∈ 1

Tactic:
← hc,

Goal state after:
case refine_2
A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsDedekindDomain A
I✝ : Ideal A
hNF : ¬IsField A
I : Ideal A
hI0✝ : I ≠ ⊥
hI1 : I ≠ ⊤
hM : I.IsMaximal
hI0 : ⊥ < I
a : A
haI : a ∈ I
ha0 : a ≠ 0
J : Ideal A := span {a}
hJ0 : J ≠ ⊥
hJI : J ≤ I
Z : Multiset (PrimeSpectrum A)
hle : (I ::ₘ Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
hnle : ¬(Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ J
b : A
hbZ : b ∈ (Multiset.map PrimeSpectrum.asIdeal Z).prod
hbJ : b ∉ J
hnz_fa : (algebraMap A K) a ≠ 0
y : A
h_Iy : y ∈ I
hy₀ : (algebraMap A K) y ∈ ↑I
c : A
hc : c * a = y * b
⊢ (algebraMap A K) (c * a) * ((algebraMap A K) a)⁻¹ ∈ 1
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (RingHom.id R) z • (IsLocalization.map P' (RingHom.id R) ⋯) x

Tactic:
RingHom.id_apply

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ z • (IsLocalization.map P' (RingHom.id R) ⋯) x = z • (IsLocalization.map P' (RingHom.id R) ⋯) x
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
I J : FractionalIdeal S P
⊢ (∀ z ∈ I, x * z ∈ J) → ∀ (i : P), (∃ z, z • x = i) → ∀ j ∈ I, i * j ∈ J

Tactic:
rintro h _ ⟨z, rfl⟩ zI hzI
    rw [Algebra.smul_mul_assoc]
    exact Submodule.smul_mem J.1 _ (h zI hzI)

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

Goal state before:
pp: ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
⊢ ∀ (y : M i), ((smulAddMonoidHom A M) 1) ((of M i) y) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) y)

Tactic:
xi

Goal state after:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst✝⁷ : AddMonoid ιA
inst✝⁶ : VAdd ιA ιB
inst✝⁵ : (i : ιA) → AddCommMonoid (A i)
inst✝⁴ : (i : ιB) → AddCommMonoid (M i)
inst✝³ : DecidableEq ιA
inst✝² : DecidableEq ιB
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ ((smulAddMonoidHom A M) 1) ((of M i) xi) = (AddMonoidHom.id (⨁ (i : ιB), M i)) ((of M i) xi)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDedekindDomain A
I J : Ideal A
this : NormalizedGCDMonoid (Ideal A) := UniqueFactorizationMonoid.toNormalizedGCDMonoid (Ideal A)
hgcd : gcd I J = I ⊔ J
⊢ I ∣ lcm I J ∧ J ∣ lcm I J

Tactic:
exact ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩

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
inst✝⁵ : CommRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ (u - v).ker.CoFG

Tactic:
ker_coFG_iff_hasFiniteRange,

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst✝⁵ : CommRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : IsNoetherianRing K
u v : V →ₗ[K] V₂
⊢ u ≈ v ↔ (u - v).HasFiniteRange
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
σ : ↥⋯.toFinset → Free.ChooseBasisIndex R M
hσ : ∀ (b_1 : ↥⋯.toFinset), π (σ b_1) = b_1
hπ : Subtype.val ∘ π = ⇑l ∘ ⇑b
hσ₁ : π ∘ σ = id
hσ₂ : ⇑l ∘ ⇑b ∘ σ = Subtype.val
f : M →ₗ[R] ↥⋯.toFinset →₀ R := lmapDomain R R π ∘ₗ ↑b.repr
y : M
hy : l y = 0
⊢ (linearCombination R Subtype.val) (f y) = 0

Tactic:
simp [f, hπ, ← Finsupp.apply_linearCombination, hy]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : FinitePresentation R N
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
inst✝ : FinitePresentation R ↥l.ker
s : Finset M
hs : Submodule.span R ↑s = ⊤
π : (↥s →₀ R) →ₗ[R] M := ⋯
H : Function.Surjective ⇑π
inst : Module.Finite R ↥(l ∘ₗ π).ker
f : ↥(l ∘ₗ π).ker →ₗ[R] ↥l.ker := ⋯
e : π ∘ₗ (l ∘ₗ π).ker.subtype = l.ker.subtype ∘ₗ f
⊢ Submodule.map l.ker.subtype f.range = Submodule.map l.ker.subtype ⊤

Tactic:
rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
      Submodule.map_comap_eq_of_surjective H]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
A : Type u_4
inst✝⁷ : CommRing A
inst✝⁶ : IsDomain A
inst✝⁵ : IsLocalRing A
inst✝⁴ : IsDedekindDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Module.Finite R A
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
⊢ IsDedekindDomain.primesOverFinset p A = {maximalIdeal A}

Tactic:
by
  have : IsDomain R := .of_faithfulSMul R A
  rw [← Finset.coe_eq_singleton, IsDedekindDomain.coe_primesOverFinset hp0,
    IsLocalRing.primesOver_eq A hp0]

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : IsDomain A
inst✝³ : Algebra R A
inst✝² : FaithfulSMul R A
inst✝¹ : Algebra.IsIntegral R A
inst✝ : Nontrivial (HeightOneSpectrum R)
⊢ Nontrivial (HeightOneSpectrum A)

Tactic:
have := (FaithfulSMul.algebraMap_injective R A).isDomain
  let f (p : HeightOneSpectrum A) : HeightOneSpectrum R := p.under R
  have : Function.Surjective f := fun ⟨p, _, hp⟩ ↦ by
    obtain ⟨P, hP, rfl⟩ := p.exists_ideal_over_prime_of_isIntegral_of_isDomain (S := A) (by simp)
    exact ⟨⟨P, hP, by aesop⟩, rfl⟩
  exact this.nontrivial

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
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
⊢ DirectSum.IsInternal fun p ↦ torsionBy R M (IsPrincipal.generator ↑p ^ Multiset.count (↑p) (factors ⊤.annihilator))

Tactic:
convert! isInternal_prime_power_torsion hM

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
inst✝ : Module.Finite R M
hM : Module.IsTorsion R M
x✝ : ↥(factors ⊤.annihilator).toFinset
⊢ torsionBy R M (IsPrincipal.generator ↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator)) =
    torsionBySet R M ↑(↑x✝ ^ Multiset.count (↑x✝) (factors ⊤.annihilator))
Module: Mathlib.RingTheory.Extension.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.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
⊢ (r • s) • m = r • s • m

Tactic:
change algebraMap R₂ S (r • s) • m = (algebraMap _ S r) • (algebraMap _ S s) • m

Goal state after:
R : Type u
S : Type v
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
R₁ : Type u_1
R₂ : Type u_2
inst✝⁵ : CommRing R₁
inst✝⁴ : CommRing R₂
inst✝³ : Algebra R₁ S
inst✝² : Algebra R₂ S
inst✝¹ : Algebra R₁ R₂
inst✝ : IsScalarTower R₁ R₂ S
r : R₁
s : R₂
m : P.Cotangent
⊢ (algebraMap R₂ S) (r • s) • m = (algebraMap R₁ S) r • (algebraMap R₂ S) s • m
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case a
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 (ι' →₀ ℕ)
⊢ P.ker ≤ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)

Tactic:
rintro x (hx : algebraMap P.Ring S x = 0)

Goal state after:
case a
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 (ι' →₀ ℕ)
x : P.Ring
hx : (algebraMap P.Ring S) x = 0
⊢ x ∈ Ideal.comap (Q.toComp P).toAlgHom (RingHom.ker (Q.ofComp P).toAlgHom)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
m : M
hm : (R ∙ m).annihilator ≤ x.asIdeal
⊢ f ∈ ↑x.asIdeal

Tactic:
obtain ⟨_, ⟨n, rfl⟩, e⟩ := H m

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : PrimeSpectrum R
hx' : x ∈ Module.support R M
f : R
H : ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0
m : M
hm : (R ∙ m).annihilator ≤ x.asIdeal
n : ℕ
e : (fun x ↦ f ^ x) n • m = 0
⊢ f ∈ ↑x.asIdeal
Module: Mathlib.Algebra.Module.StablyFree.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Ring R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type w
inst✝² : AddCommGroup N
inst✝¹ : Module R N
e : M ≃ₗ[R] N
inst✝ : IsStablyFree R M
⊢ IsStablyFree R N

Tactic:
obtain ⟨P, hPc, hPm, hPfin, hPfree, _⟩ := IsStablyFree.exist_free_prod R M
  exact ⟨P, hPc, hPm, hPfin, hPfree, Free.of_equiv (e.prodCongr (LinearEquiv.refl R P))⟩

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Submodule R M
R' : Type u_1
inst✝⁷ : CommSemiring R'
inst✝⁶ : Algebra R R'
M' : Type u_2
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Module R' M'
inst✝² : IsScalarTower R R' M'
S : Submonoid R
inst✝¹ : IsLocalization S R'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
h : N.FG
⊢ (localized' R' S f N).FG

Tactic:
rw [fg_def] at h ⊢
  rcases h with ⟨s, hfin, hspan⟩
  exact ⟨f '' s, hfin.image f, by rw [← hspan, localized'_span]⟩

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
M N : Submodule R S
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N).range = N

Tactic:
rw [Algebra.toSubmodule_bot, mulMap_range, one_mul]

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

Goal state before:
pp: case insert
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 ∉ 𝔪 • ⊤
⊢ f i = 0

Tactic:
set n : ↥(insert n s) := ⟨n, Finset.mem_insert_self ..⟩ with n_def

Goal state after:
case insert
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✝, ⋯⟩
⊢ f i = 0
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
inst✝² : Semiring R₁
inst✝¹ : Module R₁ R
inst✝ : SMulCommClass R₁ R R
r r' : R₁
x✝ x y : ⨂[R] (i : ι), s i
ihx : (r + r') • x = r • x + r' • x
ihy : (r + r') • y = r • y + r' • y
⊢ (r + r') • (x + y) = r • (x + y) + r' • (x + y)

Tactic:
simp_rw [PiTensorProduct.smul_add, ihx, ihy, add_add_add_comm]

Goal state after:
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
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = tprodCoeff R 1 (update (update f i x) i (r • update f i x i))

Tactic:
update_idem,

Goal state after:
ι : 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
x✝ : DecidableEq ι
f : (i : ι) → s i
i : ι
r : R
x : s i
⊢ tprodCoeff R 1 (update f i (r • x)) = tprodCoeff R 1 (update f i (r • update f i x i))
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
N' : Submodule R S
h : N' ≤ N
inst✝ : Flat R ↥M
⊢ M.LinearDisjoint N'

Tactic:
by
  let i := mulMap M N ∘ₗ (inclusion h).lTensor M
  have hi : Function.Injective i := H.injective.comp <|
    Module.Flat.lTensor_preserves_injective_linearMap _ <| inclusion_injective h
  have : i = mulMap M N' := by ext; simp [i]
  exact ⟨this ▸ hi⟩

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 : ℕ
r : R
a : ⨂[R]^n M
⊢ (cast R M ⋯) ((((TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M)).compr₂ ↑mulEquiv) (r • GradedMonoid.GOne.one)) a) = r • a

Tactic:
LinearMap.map_smul₂,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
r : R
a : ⨂[R]^n M
⊢ (cast R M ⋯) (r • (((TensorProduct.mk R (⨂[R]^0 M) (⨂[R]^n M)).compr₂ ↑mulEquiv) GradedMonoid.GOne.one) a) = r • a
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 : ℕ
hn : n = 0
⊢ ¬ann.radical ^ n ≤ ann

Tactic:
simpa [hn, ann]

Goal state after:
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
⊢ ∀ (r : R) (f : (i : ι) → s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (r • (tprod R) f)) = r • (tprod R) f

pp: case refine_2
ι : 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 y : ⨂[R] (i : ι), s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) x) = x →
      (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) y) = y →
        (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (x + y)) = x + y

Tactic:
· intro x y
      simp only [map_smulₛₗ, RingHom.id_apply, lift.tprod, constOfIsEmpty_apply, const_apply,
        smul_eq_mul, mul_one]
      congr
      aesop

Goal state after:
case refine_2
ι : 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 y : ⨂[R] (i : ι), s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) x) = x →
      (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) y) = y →
        (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (x + y)) = x + y
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mp
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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom x = I) →
    ∃ x, spanSingleton R⁰ x = ↑I

pp: case mpr
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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) →
    ∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom x = I

Tactic:
· rintro ⟨I, ⟨x, hx⟩, rfl⟩
      refine ⟨FractionRing.algEquiv R K x, ?_⟩
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
      rfl

Goal state after:
case mpr
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
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) →
    ∃ x,
      (∃ x_1, spanSingleton R⁰ x_1 = ↑x) ∧
        (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom x = I
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hden0 : (algebraMap R (FractionRing R)) ↑I.den ≠ 0
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R)) ↑I.den) hden0
c : (FractionalIdeal R⁰ (FractionRing R))ˣ
hc : ↑c = spanSingleton R⁰ ((algebraMap R (FractionRing R)) ↑I.den)
⊢ IsUnit (spanSingleton R⁰ ((algebraMap R (FractionRing R)) ↑I.den) * I) ↔ IsUnit I

Tactic:
← hc,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : FractionalIdeal R⁰ (FractionRing R)
hden0 : (algebraMap R (FractionRing R)) ↑I.den ≠ 0
u : (FractionRing R)ˣ := Units.mk0 ((algebraMap R (FractionRing R)) ↑I.den) hden0
c : (FractionalIdeal R⁰ (FractionRing R))ˣ
hc : ↑c = spanSingleton R⁰ ((algebraMap R (FractionRing R)) ↑I.den)
⊢ IsUnit (↑c * I) ↔ IsUnit I
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case refine_1
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
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
hx' : ↑I = spanSingleton R⁰ x
⊢ x ≠ 0

Tactic:
intro x_eq; apply Units.ne_zero I; simp [hx', x_eq]

Goal state after:
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = ⊥

Tactic:
← hn

Goal state after:
case h
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n) = ⊥
⊢ map H.subtype (derivedSeries (↥H) (n + 1)) = map ⁅H, H⁆.subtype (derivedSeries (↥⁅H, H⁆) n)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ ⊥

Tactic:
← hn

Goal state after:
case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ derivedSeries G 0