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

Goal state before:
pp: case zero
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
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin 0),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ x ∈ annihilator R M

Tactic:
← mul_one x,

Goal state after:
case zero
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
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
e : M ≃ₗ[R] (Fin 0 →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
h :
  (∀ (a : Fin 0),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).1
          a =
        0.1 a) ∧
    ∀ (i : ι),
      (x • (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1)).2
          i =
        0.2 i
⊢ x * 1 ∈ annihilator R M
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p✝ : MvPolynomial Unit R
hp : p✝ ∈ Ideal.span {C r * X () - 1}
p : MvPolynomial Unit R
⊢ ∀ (y : MvPolynomial Unit R),
    p ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      y ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
        (aeval fun x ↦ invSelf r) p = 0 → (aeval fun x ↦ invSelf r) y = 0 → (aeval fun x ↦ invSelf r) (p + y) = 0

Tactic:
q

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p✝ : MvPolynomial Unit R
hp : p✝ ∈ Ideal.span {C r * X () - 1}
p q : MvPolynomial Unit R
⊢ p ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
    q ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      (aeval fun x ↦ invSelf r) p = 0 → (aeval fun x ↦ invSelf r) q = 0 → (aeval fun x ↦ invSelf r) (p + q) = 0
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case neg
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : ¬Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
w_chi : ¬Weight.toLinear K (↥H) L χ = 0
h_pos_containment : ⁅x_χ, m_pos⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α)
h_neg_containment : ⁅x_χ, m_neg⁆ ∈ genWeightSpace L ⇑(Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α)
y : ↥H.toLieSubmodule
hy : y ∈ ↑↑(corootSpace ⇑α)
hm_eq : m_αneg + ↑H.toLieSubmodule.incl y = m_α
hm_α_decomp : m_α = m_pos + m_neg + ↑H.toLieSubmodule.incl y
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, ↑H.toLieSubmodule.incl y⁆
h_chi_in_q : Weight.toLinear K (↥H) L χ ∉ q
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
exact chi_not_in_q_aux q hq χ x_χ m_α hx_χ α hαq hα₀ w_plus w_minus w_chi m_pos m_neg y hy
      h_bracket_sum h_pos_containment h_neg_containment h_chi_in_q

Goal state after:
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
P : Presentation R S ι σ
h : Function.Bijective ⇑(algebraMap R S)
⊢ Ideal.span (Set.range PEmpty.elim) = (Generators.ofSurjectiveAlgebraMap ⋯).ker

Tactic:
by
    simp only [Set.range_eq_empty, Ideal.span_empty]
    symm
    rw [← RingHom.injective_iff_ker_eq_bot]
    change Function.Injective (aeval PEmpty.elim)
    rw [aeval_injective_iff_of_isEmpty]
    exact h.injective

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✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
⊢ Generators T (T ⊗[R] S) ι

Tactic:
apply Generators.ofSurjective (fun x ↦ 1 ⊗ₜ[R] P.val x)

Goal state after:
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✝
T : Type ?u.24
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι
⊢ Function.Surjective ⇑(aeval fun x ↦ 1 ⊗ₜ[R] P.val x)
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
σ : Type u_2
I : Ideal (MvPolynomial σ R)
s✝ : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs✝ : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s✝ x) = x
s : MvPolynomial σ R ⧸ I → MvPolynomial σ R
hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x
⊢ algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ I) = ↑(aeval fun i ↦ (Ideal.Quotient.mk I) (X i))

Tactic:
ext x <;> simp [IsScalarTower.algebraMap_apply R (MvPolynomial σ R)]

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

Goal state before:
pp: case refine_1.refine_2
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''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 0

Tactic:
ha'

Goal state after:
case refine_1.refine_2
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''
inst✝¹³ : Algebra R R'
inst✝¹² : Algebra R' R''
inst✝¹¹ : Algebra R' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
a : P.Ring
ha : a ∈ P.ker • P.ker
b : P.Ring
hb : b ∈ P.ker • P.ker
ha' : 1 ⊗ₜ[P.Ring] ⟨a, ⋯⟩ = 0
⊢ 1 ⊗ₜ[P.Ring] ⟨b, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨a + b, ⋯⟩ = 0
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
hf : Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
    Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
rw [map_add, Finsupp.single_add]

Goal state after:
case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
hf : Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
⊢ Finsupp.single r (presB.π (Finsupp.single g a)) + Finsupp.single r (presB.π f) ∈
    Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: case e'_5
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 : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
j : ι →₀ ℕ
this :
  (Q.toComp P).toAlgHom ((monomial j) (coeff (e.symm (i, j)) x)) = (monomial (e.symm (0, j))) (coeff (e.symm (i, j)) x)
⊢ (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x) = (monomial (e.symm (i, 0 + j))) (1 * coeff (e.symm (i, j)) x)

Tactic:
zero_add,

Goal state after:
case e'_5
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 : (Q.comp P).Ring
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
j : ι →₀ ℕ
this :
  (Q.toComp P).toAlgHom ((monomial j) (coeff (e.symm (i, j)) x)) = (monomial (e.symm (0, j))) (coeff (e.symm (i, j)) x)
⊢ (monomial (e.symm (i, j))) (coeff (e.symm (i, j)) x) = (monomial (e.symm (i, j))) (1 * coeff (e.symm (i, j)) x)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn :
  ((finsuppScalarLeft R N ι) en) i =
    ((finsuppScalarLeft R N ι) ((rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2))) i
⊢ n i =
    ∑ j,
      (match j with
        | ⟨(kj, snd), property⟩ => ↑kj i) •
        match j with
        | ⟨(fst, yj), property⟩ => yj

Tactic:
simp only [map_sum, finsuppScalarLeft_apply_tmul, zero_smul, Finsupp.single_zero,
      Finsupp.sum_single_index, one_smul, Finsupp.finsetSum_apply, Finsupp.single_apply,
      Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, rTensor_tmul, coe_subtype, Finsupp.sum_apply,
      Finsupp.sum_ite_eq', Finsupp.mem_support_iff, ne_eq, ite_not, en] at hkn

Goal state after:
case refine_1
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
i : ι
hkn : n i = ∑ x ∈ ma, if ↑x.1 i = 0 then 0 else ↑x.1 i • x.2
⊢ n i =
    ∑ j,
      (match j with
        | ⟨(kj, snd), property⟩ => ↑kj i) •
        match j with
        | ⟨(fst, yj), property⟩ => yj
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 ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
x : ↥Q.ker
⊢ ↥(Q.comp P).ker

Tactic:
refine ⟨(AddMonoidAlgebra.coeff x.1).sum fun n r ↦ ?_, ?_⟩

Goal state after:
case refine_1
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
x : ↥Q.ker
n : ι' →₀ ℕ
r : S
⊢ (Q.comp P).Ring

case refine_2
R : Type u
S : Type v
ι : Type w
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : Algebra R S
P✝ : Generators R S ι
R' : Type u_1
S' : Type u_2
ι' : Type u_3
inst✝¹⁵ : CommRing R'
inst✝¹⁴ : CommRing S'
inst✝¹³ : Algebra R' S'
P' : Generators R' S' ι'
R'' : Type u_4
S'' : Type u_5
ι'' : Type u_6
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Generators R'' S'' ι''
inst✝⁹ : Algebra R R'
inst✝⁸ : Algebra R' R''
inst✝⁷ : Algebra R' S''
inst✝⁶ : Algebra S S'
inst✝⁵ : Algebra S' S''
inst✝⁴ : Algebra S S''
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 ι
x : ↥Q.ker
⊢ ((↑x).coeff.sum fun n r ↦ ?refine_1) ∈ (Q.comp P).ker
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
p : PrimeSpectrum R
s : Set M
hs : Submodule.span R s = ⊤
⊢ p ∈ support R M ↔ ∃ m ∈ s, (R ∙ m).annihilator ≤ p.asIdeal

Tactic:
by
  constructor
  · contrapose
    rw [notMem_support_iff, LocalizedModule.subsingleton_iff_ker_eq_top, ← top_le_iff,
      ← hs, Submodule.span_le, Set.subset_def]
    simp_rw [SetLike.le_def, Submodule.mem_annihilator_span_singleton, SetLike.mem_coe,
      LocalizedModule.mem_ker_mkLinearMap_iff]
    push Not
    simp_rw [and_comm]
    exact id
  · intro ⟨m, _, hm⟩
    exact mem_support_iff_exists_annihilator.mpr ⟨m, hm⟩

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case pos
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 : (R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

pp: case neg
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 : ¬(R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
· rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h
      exact ⟨1, one_mem _, by simpa using h⟩

Goal state after:
case neg
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 : ¬(R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1

Tactic:
rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩

Goal state after:
case insert
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
a : N
s : Finset N
a✝ : a ∉ s
hs : ∀ x ∈ Submodule.span R' ↑s, ∃ t, t • x ∈ Submodule.span R ↑s
y : R'
z : N
hz : z ∈ Submodule.span R' ↑s
y' : R
s' : ↥M
e : y * (algebraMap R R') ↑(y', s').2 = (algebraMap R R') (y', s').1
⊢ ∃ t a_1, ∃ z_1 ∈ Submodule.span R ↑s, t • (y • a + z) = a_1 • a + z_1
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
K : Type u_3
n : ℕ
inst✝² : AddCommGroup K
inst✝¹ : Module R K
inst✝ : Module.Finite R K
f : K →ₗ[R] Fin n →₀ R
x : (Fin n →₀ R) →ₗ[R] M
h : x ∘ₗ f = 0
⊢ ∃ k a y, x = y ∘ₗ a ∧ a ∘ₗ f = 0

Tactic:
by
  have (K' : Submodule R K) (hK' : K'.FG) : ∃ (k : ℕ) (a : (Fin n →₀ R) →ₗ[R] (Fin k →₀ R))
      (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ K' ≤ LinearMap.ker (a ∘ₗ f) := by
    induction K', hK' using Submodule.fg_induction generalizing n with
    | singleton k =>
      have : x (f k) = 0 := by simpa using LinearMap.congr_fun h k
      simpa using exists_factorization_of_apply_eq_zero_of_free this
    | sup K₁ K₂ _ _ ih₁ ih₂ =>
      obtain ⟨k₁, a₁, y₁, rfl, ha₁⟩ := ih₁ h
      have : y₁ ∘ₗ (a₁ ∘ₗ f) = 0 := by rw [← comp_assoc, h]
      obtain ⟨k₂, a₂, y₂, rfl, ha₂⟩ := ih₂ this
      use k₂, a₂ ∘ₗ a₁, y₂
      simp_rw [comp_assoc]
      exact ⟨trivial, sup_le (ha₁.trans (ker_le_ker_comp _ _)) ha₂⟩
  convert! this ⊤ Finite.fg_top
  simp only [top_le_iff, ker_eq_top]

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
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R M
p : Ideal R
inst✝ : p.IsPrime
φ : N →ₗ[R] M
hφ : Function.Surjective ⇑((LocalizedModule.map p.primeCompl) φ)
⊢ ∃ a ∉ p, Function.Surjective ⇑((LocalizedModule.map (Submonoid.powers a)) φ)

Tactic:
simp_rw [φ.localizedMap_surjective_iff_subsingleton_localized_coker] at hφ ⊢

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R M
p : Ideal R
inst✝ : p.IsPrime
φ : N →ₗ[R] M
hφ : Subsingleton (LocalizedModule p.primeCompl (M ⧸ φ.range))
⊢ ∃ a ∉ p, Subsingleton (LocalizedModule (Submonoid.powers a) (M ⧸ φ.range))
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)

Tactic:
have : 1 ≤ (i : ℕ) := (Nat.zero_le j).trans_lt hji

Goal state after:
case inl
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
this : 1 ≤ ↑i
⊢ Even (↑(i.succAbove j) + ↑(j.predAbove i)) ↔ Odd (↑i + ↑j)
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ Odd k ↔ Odd ↑k

Tactic:
rcases hn with ⟨n, rfl⟩
  refine ⟨?_, odd_of_val⟩
  rintro ⟨l, rfl⟩
  rw [val_add, val_mul, coe_ofNat_eq_mod, coe_ofNat_eq_mod]
  simp only [Nat.mod_mul_mod, Nat.add_mod_mod, Nat.mod_add_mod, Nat.odd_iff]
  rw [Nat.mod_mod_of_dvd _ ⟨n, (two_mul n).symm⟩, ← Nat.odd_iff, Nat.odd_add_one,
    Nat.not_odd_iff_even]
  simp

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

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hn : Even n
⊢ ¬Odd ↑k ↔ Even ↑k

Tactic:
exact Nat.not_odd_iff_even

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ (baseChange A N).spanRank ≤ Cardinal.lift.{u_2, u_3} N.spanRank

Tactic:
grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card]

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk ↑s = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk ↑(⇑((TensorProduct.mk R A M) 1) '' s) ≤ Cardinal.lift.{u_2, u_3} (Cardinal.mk ↑s)
Module: Mathlib.LinearAlgebra.TensorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
n : ℕ
this :
  ∀ (x : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
    (Function.update f i φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) i (φ (v i)) j
inst✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
i : Fin n
a : R
φ : Module.Dual R M
⊢ PiTensorProduct.lift ((MultilinearMap.mkPiRing R (Fin n) 1).compLinearMap (Function.update f i (a • φ))) =
    a • PiTensorProduct.lift ((MultilinearMap.mkPiRing R (Fin n) 1).compLinearMap (Function.update f i φ))

Tactic:
ext v
      simp [this, Finset.prod_update_of_mem, Semigroup.mul_assoc]

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
⊢ Function.Surjective ⇑(M.mulMap N).rangeRestrict

Tactic:
LinearMap.surjective_rangeRestrict

Goal state after: