mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ ∃ ι x x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, DirectSum.IsInternal fun i ↦ torsionBy R M (p i ^ e i)

Tactic:
refine ⟨_, ?_, _, _, ?_, _, Submodule.isInternal_prime_power_torsion_of_pid hM⟩
  · exact Finset.fintypeCoeSort _
  · rintro ⟨p, hp⟩
    have hP := prime_of_factor p (Multiset.mem_toFinset.mp hp)
    have := Ideal.isPrime_of_prime hP
    exact (IsPrincipal.prime_generator_of_isPrime p hP.ne_zero).irreducible

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

Goal state before:
pp: σ : 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
g : R →+* MvPolynomial Unit R ⧸ Ideal.span {C r * X () - 1} := (Ideal.Quotient.mk (Ideal.span {C r * X () - 1})).comp C
⊢ IsUnit (g r)

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, g]
    rw [isUnit_iff_exists_inv]
    use (Ideal.Quotient.mk _ <| X ())
    rw [← map_mul, ← map_one (Ideal.Quotient.mk _), Ideal.Quotient.mk_eq_mk_iff_sub_mem]
    exact Ideal.mem_span_singleton_self (C r * X () - 1)

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

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : e.symm x ∈ Ideal.map TensorProduct.includeRight (Ideal.span (Set.range P.relation))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
← Ideal.mem_comap,

Goal state after:
case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : x ∈ Ideal.comap e.symm (Ideal.map TensorProduct.includeRight (Ideal.span (Set.range P.relation)))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: 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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
⊢ ↑(LieSubmodule.restr J H) = ↑(LieSubmodule.restr I H)

Tactic:
h_restr

Goal state after:
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
I : LieIdeal K L
hI : ∀ (α : ↥LieSubalgebra.root), I.rootSpan ∈ End.invtSubmodule ↑((rootSystem H).reflection α)
J : LieIdeal K L := invtSubmoduleToLieIdeal I.rootSpan ⋯
h_eq : ∀ (α : ↥LieSubalgebra.root), α ∈ J.rootSet ↔ α ∈ I.rootSet
h_restr : LieSubmodule.restr J H = LieSubmodule.restr I H
⊢ ↑(LieSubmodule.restr I H) = ↑(LieSubmodule.restr I H)
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : f.toRingHom ↑x ∈ Ideal.map f.toRingHom (P.ker ^ 2)
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

Tactic:
← Ideal.mem_comap,

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : ↑x ∈ Ideal.comap f.toRingHom (Ideal.map f.toRingHom (P.ker ^ 2))
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
r : σ
⊢ ∃ y, φ y = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩

Tactic:
refine ⟨Finsupp.single r 1, ?_⟩

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Extension.Cotangent.mk.range = ⊤
h₂ : Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = ⊤
r : σ
⊢ φ (Finsupp.single r 1) = Extension.Cotangent.mk ⟨pres.relation r, ⋯⟩
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
r : σ
this : ∀ (r : σ), pres.differentialsRelations.map (Finsupp.single r 1) = pres.differentialsRelations.relation r
⊢ pres.toExtension.cotangentComplex ((hom₁ pres) (Finsupp.single r 1)) =
    pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.map (Finsupp.single r 1))

Tactic:
comm₁₂_single,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
r : σ
this : ∀ (r : σ), pres.differentialsRelations.map (Finsupp.single r 1) = pres.differentialsRelations.relation r
⊢ pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.relation r) =
    pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.map (Finsupp.single r 1))
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ f.toRingHom ↑x ∈ Ideal.map f.toRingHom (P.ker ^ 2)

Tactic:
← Ideal.mem_comap,

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
y : P.Ring
y_in : y ∈ RingHom.ker f.toRingHom
y_in' : y ∈ P.ker
hy : y - ↑x ∈ P.ker ^ 2
⊢ ↑x ∈ Ideal.comap f.toRingHom (Ideal.map f.toRingHom (P.ker ^ 2))
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
r : relations.R
⊢ (Finsupp.linearCombination A fun g ↦ Finsupp.single g 1) (relations.relation r) = 0

Tactic:
exfalso

Goal state after:
A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
r : relations.R
⊢ False
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
ι' : 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 ι
⊢ (Q.toComp P).toAlgHom = rename Sum.inr

Tactic:
rename_eq_aeval

Goal state after:
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 ι
⊢ (Q.toComp P).toAlgHom = aeval (X ∘ Sum.inr)
Module: Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
ι : Type u_2
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : ι → Ideal R
hI : Pairwise (IsCoprime on I)
inst✝ : Finite ι
⊢ (LinearMap.pi fun i ↦ (TensorProduct.mk R (R ⧸ I i) M) 1).ker = (⨅ i, I i) • ⊤

Tactic:
have := rTensor_exact M (exact_subtype_ker_map _) (pi_mkQ_surjective hI)
  rw [← (TensorProduct.lid R M).conj_exact_iff_exact, exact_iff] at this
  convert! this
  · classical simp [pi_mkQ_rTensor, LinearMap.comp_assoc]
  refine le_antisymm (Submodule.smul_le.mpr fun r hr m _ ↦ ⟨⟨r, ?_⟩ ⊗ₜ m, rfl⟩) ?_
  · simpa only [ker_pi, Submodule.ker_mkQ]
  rintro _ ⟨x, rfl⟩
  refine x.induction_on (by simp) (fun r m ↦ Submodule.smul_mem_smul ?_ ⟨⟩) fun _ _ ↦ ?_
  · simpa only [← (I _).ker_mkQ, ← ker_pi] using! Subtype.mem _
  · simpa using! add_mem

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ support R A = PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))

Tactic:
ext p

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ p ∈ support R A ↔ p ∈ PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))
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
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ support R M ⊆ support R N

Tactic:
simp_rw [Set.subset_def, mem_support_iff']
  rintro x ⟨m, hm⟩
  exact ⟨f m, fun r hr ↦ by simpa using hf.ne (hm r hr)⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
ι : Type u_5
v : ι → M
hli : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hsp : Submodule.span k (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
bk : Basis ι k (k ⊗[R] M) := Basis.mk hli ⋯
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
i : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R v
x✝ : ι
⊢ 1 ⊗ₜ[R] v x✝ = bk x✝

Tactic:
simp [bk]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

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
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ M' ≤ M, M'.FG → M'.LinearDisjoint N
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
M' : Submodule R S
hM : M' ≤ M
hFG : M'.FG
h : {x, y} ⊆ ↑(LinearMap.rTensor (↥N) (inclusion hM)).range
x' : ↥M' ⊗[R] ↥N
hx' : (LinearMap.rTensor (↥N) (inclusion hM)) x' = x
y' : ↥M' ⊗[R] ↥N
hy' : (LinearMap.rTensor (↥N) (inclusion hM)) y' = y
⊢ x = y
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
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)

Tactic:
let mul : ∀ n m : ℕ, ⨂[R]^n M →ₗ[R] (⨂[R]^m) M →ₗ[R] (⨂[R]^(n + m)) M := fun n m =>
    (TensorProduct.mk R _ _).compr₂ ↑(mulEquiv : _ ≃ₗ[R] (⨂[R]^(n + m)) M)

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
Module: Mathlib.LinearAlgebra.LinearDisjoint

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
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.lTensor (↥M) (inclusion hN)).range
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
⊢ x = y

Tactic:
obtain ⟨y', hy'⟩ := h (show y ∈ {x, y} by simp)

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
H : ∀ N' ≤ N, N'.FG → M.LinearDisjoint N'
x y : ↥M ⊗[R] ↥N
hxy : (M.mulMap N) x = (M.mulMap N) y
N' : Submodule R S
hN : N' ≤ N
hFG : N'.FG
h : {x, y} ⊆ ↑(LinearMap.lTensor (↥M) (inclusion hN)).range
x' : ↥M ⊗[R] ↥N'
hx' : (LinearMap.lTensor (↥M) (inclusion hN)) x' = x
y' : ↥M ⊗[R] ↥N'
hy' : (LinearMap.lTensor (↥M) (inclusion hN)) y' = y
⊢ x = y
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ φ₁ (tprodCoeff R r f) = φ₂ (tprodCoeff R r f)

Tactic:
rw [tprodCoeff_eq_smul_tprod, φ₁.map_smul, φ₂.map_smul]

Goal state after:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ₁ φ₂ : (⨂[R] (i : ι), s i) →ₗ[R] E
H : φ₁.compMultilinearMap (tprod R) = φ₂.compMultilinearMap (tprod R)
z : ⨂[R] (i : ι), s i
r : R
f : (i : ι) → s i
⊢ r • φ₁ ((tprod R) f) = r • φ₂ ((tprod R) f)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
⊢ Submodule.IsPrincipal J

Tactic:
let g : R := T.gcd id

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
⊢ Submodule.IsPrincipal J
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
⊢ freeLocus R M = freeLocus R M'

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
e : M ≃ₗ[R] M'
p : PrimeSpectrum R
⊢ p ∈ freeLocus R M ↔ p ∈ freeLocus R M'
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
⊢ freeLocus (Localization S) (LocalizedModule S M) = comap (algebraMap R (Localization S)) ⁻¹' freeLocus R M

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submonoid R
p : PrimeSpectrum (Localization S)
⊢ p ∈ freeLocus (Localization S) (LocalizedModule S M) ↔ p ∈ comap (algebraMap R (Localization S)) ⁻¹' freeLocus R 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
⊢ (algebraMap R (p.asIdeal.Fiber S)) r ∉ q.asIdeal

Tactic:
← Ideal.mem_comap,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p✝ : Ideal R
inst✝ : p✝.IsPrime
p : PrimeSpectrum R
q : PrimeSpectrum (p.asIdeal.Fiber S)
x : p.asIdeal.Fiber S
r : R
hr : r ∉ p.asIdeal
s : S
e : r • x = 1 ⊗ₜ[R] s
this : ∀ {R : Type (max u_1 u_2)} [inst : CommSemiring R] (self : PrimeSpectrum R), self.asIdeal.IsPrime
⊢ r ∉ Ideal.comap (algebraMap R (p.asIdeal.Fiber S)) q.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ rankAtStalk M = 0

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
p : PrimeSpectrum R
⊢ rankAtStalk M p = 0 p
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ rankAtStalk M = rankAtStalk N

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_1
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
p : PrimeSpectrum R
⊢ rankAtStalk M p = rankAtStalk N p
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
⊢ rankAtStalk M = ↑(finrank R M)

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Free R M
p : PrimeSpectrum R
⊢ rankAtStalk M p = ↑(finrank R M) p
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Flat R N
inst✝ : Module.Finite R N
⊢ rankAtStalk (M × N) = rankAtStalk M + rankAtStalk N

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Flat R N
inst✝ : Module.Finite R N
p : PrimeSpectrum R
⊢ rankAtStalk (M × N) p = (rankAtStalk M + rankAtStalk N) p
Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
⊢ rankAtStalk (M ⊗[R] N) = rankAtStalk M * rankAtStalk N

Tactic:
ext p

Goal state after:
R : Type uR
M : Type uM
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Flat R M
inst✝⁴ : Module.Finite R M
N : Type u_1
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module.Finite R N
inst✝ : Flat R N
p : PrimeSpectrum R
⊢ rankAtStalk (M ⊗[R] N) p = (rankAtStalk M * rankAtStalk N) p
Module: Mathlib.RingTheory.PicardGroup

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Invertible R M
⊢ Free R M ↔ Nonempty (M ≃ₗ[R] R)

Tactic:
refine ⟨fun _ ↦ ?_, fun ⟨e⟩ ↦ .of_equiv e.symm⟩
  nontriviality R
  have e := (Free.chooseBasis R M).repr
  have := card_eq_of_linearEquiv R <|
    (finsuppTensorFinsupp' .. ≪≫ₗ linearEquivFunOnFinite R R _).symm ≪≫ₗ TensorProduct.congr
      (linearEquivFunOnFinite R R _ ≪≫ₗ llift R R R _ ≪≫ₗ e.dualMap)
      e.symm ≪≫ₗ linearEquiv R M ≪≫ₗ (.symm <| .funUnique Unit R R)
  have : Unique (Free.ChooseBasisIndex R M) :=
    (Fintype.card_eq_one_iff_nonempty_unique.mp (by simpa using this)).some
  exact ⟨e ≪≫ₗ uniqueLinearEquiv R R default⟩

Goal state after: