mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ ((↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))).Flat

Tactic:
refine RingHom.Flat.comp ?_ (.of_bijective <| AlgEquiv.bijective _)

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra S A
inst✝⁸ : IsScalarTower R S A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra R B
inst✝⁵ : CommRing C
inst✝⁴ : Algebra R C
inst✝³ : Algebra S C
inst✝² : IsScalarTower R S C
inst✝¹ : CommRing D
inst✝ : Algebra R D
f : A →ₐ[S] C
g : B →ₐ[R] D
hf : f.Flat
hg : g.Flat
heq :
  Algebra.TensorProduct.map f g =
    (Algebra.TensorProduct.map f (AlgHom.id R D)).comp (Algebra.TensorProduct.map (AlgHom.id S A) g)
this :
  AlgHom.restrictScalars R (Algebra.TensorProduct.map f (AlgHom.id R D)) =
    (↑(Algebra.TensorProduct.comm R D C)).comp
      ((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))
⊢ (↑((Algebra.TensorProduct.lTensor D (AlgHom.restrictScalars R f)).comp ↑(Algebra.TensorProduct.comm R A D))).Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.span {x} * Ideal.span {y} ≤ I
⊢ Ideal.span {x} ⊓ Ideal.span {y} ≤ I

Tactic:
rw [← hI.radical_le_iff] at h' ⊢

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : (Ideal.span {x} * Ideal.span {y}).radical ≤ I
⊢ (Ideal.span {x} ⊓ Ideal.span {y}).radical ≤ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
s : Set S
⊢ zeroLocus (⇑(algebraMap R S) '' ↑(Ideal.comap (algebraMap R S) (Ideal.span s))) = zeroLocus s

Tactic:
rw [← zeroLocus_span, ← zeroLocus_span s, ← Ideal.map, IsLocalization.map_under M S]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D✝ D1 D2 : Derivation R A M
r : R
a✝ b✝ : A
D : Derivation R A M
a b : A
⊢ (-↑D) (a * b) = a • (-↑D) b + b • (-↑D) a

Tactic:
simp only [LinearMap.neg_apply, smul_neg, neg_add_rev, leibniz, coeFn_coe, add_comm]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
⊢ g ^ (k % ↑(Nat.find hex)) * g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H

Tactic:
by
            rw [← zpow_add, Int.emod_add_mul_ediv, hk]; exact hx

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
y : R
hy : y ∈ {e | IsIdempotentElem e}
r : R
hx : r * y ∈ {e | IsIdempotentElem e}
eq : basicOpen (r * y) = basicOpen y
ne : r * y ≠ y
ne' : r * y * y ≠ r * y
mem : r * y ∈ Ideal.span {y}
⊢ r * (y * y) = r * y

Tactic:
hy

Goal state after:
R : Type u
inst✝ : CommSemiring R
y : R
hy : y ∈ {e | IsIdempotentElem e}
r : R
hx : r * y ∈ {e | IsIdempotentElem e}
eq : basicOpen (r * y) = basicOpen y
ne : r * y ≠ y
ne' : r * y * y ≠ r * y
mem : r * y ∈ Ideal.span {y}
⊢ r * y = r * y
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ 0 = sSup (Set.range fun g ↦ orderOf g)

Tactic:
Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he

Goal state after:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : exponent G = 0
⊢ 0 = 0
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
hG : Monoid.exponent G = 2
hx : orderOf 1 = 2
⊢ False

Tactic:
norm_num at hx

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
⊢ p ∈ q.asIdeal → X ∉ q.asIdeal

Tactic:
hpq

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = comap (mapRingHom f) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
⊢ X ∉ q.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
⊢ b.coeff 0 = 1

Tactic:
simpa using! congr(($e).coeff 0)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
⊢ ∃ a, comap (algebraMap R S) a = { asIdeal := p, isPrime := hp }

Tactic:
have hinj : Function.Injective (algebraMap R S) := FaithfulSMul.algebraMap_injective _ _

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
p : Ideal R
hp : p.IsPrime
hinj : Function.Injective ⇑(algebraMap R S)
⊢ ∃ a, comap (algebraMap R S) a = { asIdeal := p, isPrime := hp }
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ∃ n, orderOf g = p ^ n

Tactic:
rw [← orderOf_submonoid, ← mem_primaryComponent_iff_orderOf]

Goal state after:
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
g : ↥(primaryComponent G p)
⊢ ↑g ∈ primaryComponent G p
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
⊢ y ∈ H → y ∈ Subgroup.map (normalizer ↑H).subtype (comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))

Tactic:
hy

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ y ∈ Subgroup.map (normalizer ↑H).subtype (comap (mk' (H.subgroupOf (normalizer ↑H))) (zpowers x))
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i✝ : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
i : Fin ((snoc s x₁ hsat₁).length + (RelSeries.singleton {(x, y) | IsMaximal x y} y₁).length)
⊢ Iso
    (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.castSucc,
      ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i.castSucc).castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i.castSucc).succ)

Tactic:
refine Fin.lastCases ?_ (fun i => ?_) i
      · erw [Equiv.swap_apply_right, snoc_castSucc, snoc_castSucc, snoc_castSucc,
          Fin.succ_castSucc, snoc_castSucc, Fin.succ_last, last_snoc', last_snoc', last_snoc']
        exact hr₁
      · erw [Equiv.swap_apply_of_ne_of_ne h2 h1, snoc_castSucc, snoc_castSucc,
          snoc_castSucc, snoc_castSucc, Fin.succ_castSucc, snoc_castSucc,
          Fin.succ_castSucc, snoc_castSucc, snoc_castSucc, snoc_castSucc]
        exact iso_refl

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁ : s₁.length = 0
⊢ s₂.length = 0

Tactic:
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
    s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁ : s₁.length = 0
this : Fin.last s₂.length = 0
⊢ s₂.length = 0
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ Function.Injective ⇑f ∨ f = 0

Tactic:
← ker_eq_bot,

Goal state after:
R : Type u_2
inst✝⁵ : Ring R
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
f : M →ₗ[R] N
⊢ f.ker = ⊥ ∨ f = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0

Tactic:
rw [mem_torsionOf_iff, smul_eq_zero] at hr

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) 1) (I • N)

Tactic:
mem_comap

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
n : M
hn : n ∈ N
⊢ ((LinearMap.lsmul R M) 1) n ∈ I • N
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
x y : PolynomialModule R M
r✝ r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
r : R[X]
n : ℕ
a : R
⊢ (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (r • single R n a))) =
    r * (toFinsuppIso R).symm (AddMonoidAlgebra.coeffAddEquiv.symm (coeffAddEquiv (single R n a)))

Tactic:
| single n a =>

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I) →
    (monomial (n + 1)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
hy

Goal state after:
case succ.refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
x y : R
hx : (monomial (n + 1)) x ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
hy : (monomial (n + 1)) y ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
⊢ (monomial (n + 1)) (x + y) ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • sInf (N '' S) i ≤ sInf (N '' S) (i + 1)

Tactic:
rw [sInf_eq_iInf', iInf_apply, iInf_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
S : Set (I.Filtration M)
i : ℕ
⊢ I • ⨅ i_1, ↑i_1 i ≤ ⨅ i_1, ↑i_1 (i + 1)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • (mk (R ∙ a * b)) x = 0 ↔ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

Tactic:
constructor <;> intro h

Goal state after:
case mp
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • (mk (R ∙ a * b)) x = 0
⊢ ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x

case mpr
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (mk (R ∙ a * b)) b = (mk (R ∙ a * b)) x
⊢ a • (mk (R ∙ a * b)) x = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : Infinite R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
⊢ (Set.range fun r ↦ x + r • y).Infinite ↔ y ≠ 0

Tactic:
refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : IsDomain R
inst✝³ : Infinite R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTorsionFree R M
x y : M
h : y ≠ 0
r s : R
hrs : x + r • y = x + s • y
⊢ r = s
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : IsAddTorsionFree M
x y : M
⊢ (Set.range fun n ↦ x + n • y).Infinite ↔ y ≠ 0

Tactic:
refine ⟨fun h hy ↦ by simp [hy] at h, fun h ↦ Set.infinite_range_of_injective fun r s hrs ↦ ?_⟩

Goal state after:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : x + r • y = x + s • y
⊢ r = s
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i : ℕ
⊢ (↑r • f).coeff i ∈ F.N i

Tactic:
PolynomialModule.smul_apply

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
r : ↥(reesAlgebra I)
f : PolynomialModule R M
hf : f ∈ {f | ∀ (i : ℕ), f.coeff i ∈ F.N i}
i : ℕ
⊢ ∑ x ∈ Finset.antidiagonal i, (↑r).coeff x.1 • f.coeff x.2 ∈ F.N i
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s : Set (M ⧸ I • N)
hN : N.FG
hIjac : I ≤ ⊥.jacobson
hsspan : span R s = map (I • N).mkQ N
⊢ ∃ t, Set.InjOn (⇑(I • N).mkQ) t ∧ ⇑(I • N).mkQ '' t = s ∧ span R t = N

Tactic:
by
  use Quotient.out '' s
  split_ands
  · simp [Set.InjOn]
  · simp [Set.image_image]
  · symm; apply eq_of_map_mkQ_eq_map_mkQ_of_le_jacobson_bot hN hIjac
    simp [← hsspan, map_span, Set.image_image]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Basic

Goal state before:
pp: A B A' B' : CommRingCat
f : A ⟶ B
f' : A' ⟶ B'
g : A ⟶ A'
g' : B ⟶ B'
fac : g ≫ f' = f ≫ g'
b : ↑B
⊢ (ConcreteCategory.hom (map fac)) (d b) = d ((ConcreteCategory.hom g') b)

Tactic:
by
  algebraize [f.hom, f'.hom, g.hom, g'.hom, f'.hom.comp g.hom]
  have := IsScalarTower.of_algebraMap_eq' (congrArg Hom.hom fac)
  exact _root_.KaehlerDifferential.map_D A A' B B' b

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
hx : I.cotangentToQuotientSquare (I.toCotangent x) = 0
⊢ I.toCotangent x = 0

Tactic:
toCotangent_to_quotient_square

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : ↥I
hx : (Submodule.mkQ (I ^ 2)) ↑x = 0
⊢ I.toCotangent x = 0
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ I ^ 2
hx : x ∈ ⊥
⊢ y ∈ ⊥ → x + y ∈ ⊥

Tactic:
hy

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
hx✝ : x✝ ∈ I.cotangentIdeal • I.cotangentIdeal
x y : R ⧸ I ^ 2
hx : x ∈ ⊥
hy : y ∈ ⊥
⊢ x + y ∈ ⊥
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
⊢ N ≤ I • N

Tactic:
have := hk k (le_refl _)

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
k : ℕ
hk :
  ∀ n ≥ k,
    I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N n = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (n + 1)
this : I • (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N (k + 1)
⊢ N ≤ I • N
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
hs_span' : Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤
t : Set ↥(maximalIdeal R)
ht_inj : Set.InjOn (⇑(maximalIdeal R • ⊤).mkQ) t
ht_image : ⇑(maximalIdeal R • ⊤).mkQ '' t = s
ht_span : Submodule.span R t = ⊤
⊢ ⊤.spanRank ≤ Cardinal.mk ↑s

Tactic:
← ht_span,

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
hs_span' : Submodule.span R s = Submodule.map (maximalIdeal R • ⊤).mkQ ⊤
t : Set ↥(maximalIdeal R)
ht_inj : Set.InjOn (⇑(maximalIdeal R • ⊤).mkQ) t
ht_image : ⇑(maximalIdeal R • ⊤).mkQ '' t = s
ht_span : Submodule.span R t = ⊤
⊢ (Submodule.span R t).spanRank ≤ Cardinal.mk ↑s
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : ↥J
hx : x ∈ Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J)
⊢ I.toCotangent ⟨(Algebra.ofId A B) ↑x, ⋯⟩ = 0

Tactic:
convert! map_zero I.toCotangent

Goal state after:
case e'_3
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
surj : Function.Surjective ⇑(algebraMap A B)
I : Ideal B
J : Ideal A
eq : comap (algebraMap A B) I = RingHom.ker (algebraMap A B) ⊔ J
eqmap : I = map (algebraMap A B) J
x : ↥J
hx : x ∈ Submodule.comap (Submodule.subtype J) (RingHom.ker (algebraMap A B) ⊓ J)
⊢ (Algebra.ofId A B) ↑x = ↑0
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ x y : S ⊗[R] S
hx : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) →
    x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
hy

Goal state after:
case a.refine_3
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x✝ x y : S ⊗[R] S
hx : x - (TensorProduct.lmul' R) x ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
hy : y - (TensorProduct.lmul' R) y ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
⊢ x + y - (TensorProduct.lmul' R) (x + y) ⊗ₜ[R] 1 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' = p'

Tactic:
← add_left_inj p,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ n' + m' + p = p' + p