mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (x✝¹ ≫ x✝) n =
    HomologicalComplex.homologyMap (cochainsMap (MonoidHom.id G) x✝¹ ≫ cochainsMap (MonoidHom.id G) x✝) n

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ✝ : res f A ⟶ B
n✝ n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ HomologicalComplex.cyclesMap (cochainsMap ((MonoidHom.id H).comp f) (resMap f φ)) n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (res f Y)) n =
    HomologicalComplex.cyclesMap
        (cochainsMap (f.comp (MonoidHom.id G)) (resMap (MonoidHom.id G) (𝟙 (res f X)) ≫ resMap f φ)) n ≫
      HomologicalComplex.homologyπ (inhomogeneousCochains (of (MonoidHom.comp Y.ρ f))) n

Tactic:
rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : MvPolynomial σ R
s : Set (σ →₀ ℕ)
⊢ (∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = m' + d) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, ∃ c, xi = si + c

Tactic:
rfl

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

Tactic:
by_cases h : 0 ∈ B

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∈ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
m : MonomialOrder σ
B : Set (MvPolynomial σ R)
h : 0 ∉ B
⊢ span (m.leadingTerm '' insert 0 B) = span (m.leadingTerm '' B)
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq σ
x : τ →₀ ℕ
a✝ : (σ →₀ ℕ) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ mapDomain f a✝.1 = x → a✝.2.1 + a✝.2.2 = a✝.1 → ∃ a b, mapDomain f (a + b) = x ∧ (a + b, a, b) = a✝

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: case ht
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : DecidableEq τ
x : τ →₀ ℕ
a✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ a✝.1.1 + a✝.1.2 = x →
    mapDomain f a✝.2.1 = a✝.1.1 →
      mapDomain f a✝.2.2 = a✝.1.2 →
        ∃ a b, mapDomain f a + mapDomain f b = x ∧ ((mapDomain f a, mapDomain f b), a, b) = a✝

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : Semiring R
p q : MvPowerSeries σ R
x : τ →₀ ℕ
x✝ : ((τ →₀ ℕ) × (τ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ x✝.1.1 + x✝.1.2 = x →
    mapDomain f x✝.2.1 = x✝.1.1 →
      mapDomain f x✝.2.2 = x✝.1.2 →
        ∀ (a b : τ →₀ ℕ) (a_1 b_1 : σ →₀ ℕ),
          a + b = x →
            mapDomain f a_1 = a →
              mapDomain f b_1 = b → x✝.2.1 + x✝.2.2 = a_1 + b_1 → x✝.2 = (a_1, b_1) → x✝ = ((a, b), a_1, b_1)

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
f : σ → τ
inst✝¹ : TendstoCofinite f
inst✝ : CommSemiring R
p : MvPowerSeries σ R
x : τ →₀ ℕ
⊢ (coeff x) ((rename f) p) = ∑ x ∈ ⋯.toFinset, (coeff x) p

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
x : τ →₀ ℕ
r : R
h : x ∉ Set.range (embDomain e)
n✝ : σ →₀ ℕ
⊢ embDomain e n✝ = x → r = 0

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries τ R
x : σ →₀ ℕ
⊢ (coeff x) ((killCompl e) p) = (coeff (embDomain e x)) p

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑(ModuleCat.of k (G →₀ ↑A))
⊢ (ConcreteCategory.hom (shortComplexH0 A).f) x = (ModuleCat.Hom.hom (d₁₀ A)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a : R
ha : a ≠ 0
ha₂ : ¬↑(span {a}) ∩ ↑(closure {r | Prime r}).toSubsemigroup = ∅
x : R
hx : x ∈ ↑(span {a})
b : R
hx₂ : a * b ∈ ↑(closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ {r | Prime r} ⊆ {r | IsUnit r ∨ Prime r}

Tactic:
grind

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (chainsIso₁ A).inv) ↑x =
    (ConcreteCategory.hom ((shortComplexH1 A).moduleCatLeftHomologyData.i ≫ (chainsIso₁ A).inv)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → ∃ x ∈ I, Prime x
a x b : R
hsubset : closure {r | Prime r} ≤ closure {r | IsUnit r ∨ Prime r}
z₁ z₂ : R
hz₁ : z₁ ∈ closure {r | IsUnit r ∨ Prime r}
hz₂ : z₂ ∈ closure {r | IsUnit r ∨ Prime r}
S₁ : Multiset R
hS₁pri : ∀ b ∈ S₁, Prime b
hS₁ : Associated S₁.prod z₁
S₂ : Multiset R
hS₂pri : ∀ b ∈ S₂, Prime b
hS₂ : Associated S₂.prod z₂
⊢ ∀ b ∈ S₁ + S₂, Prime b

Tactic:
grind

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (chainsIso₂ A).inv) ↑x =
    (ConcreteCategory.hom ((shortComplexH2 A).moduleCatLeftHomologyData.i ≫ (chainsIso₂ A).inv)) x

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ ↑(x - y) ∈ boundaries₁ A ↔ ↑x - ↑y ∈ boundaries₁ A

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
g : G
a : ↑A
⊢ (H1AddEquivOfIsTrivial A).symm (Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a) =
    (ConcreteCategory.hom (H1π A)) ((ConcreteCategory.hom (cycles₁IsoOfIsTrivial A).inv) (single g a))

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ ↑(x - y) ∈ boundaries₂ A ↔ ↑x - ↑y ∈ boundaries₂ A

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
i : ℕ
a : R
a_in : a ∈ ↑(I ^ i • ⊤)
⊢ a ∈ (fun x ↦ x • m) ⁻¹' ↑(I ^ i • ⊤)

Tactic:
by
        replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
        exact smul_mem_smul a_in mem_top

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsAdic I

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
e : R ≃+* S
this✝ : WithIdeal R := { i := I }
this : WithIdeal S := { i := Ideal.map e I }
⊢ IsAdic (Ideal.map e I)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : WithIdeal R
a : R
ha : a ∈ i
⊢ ∀ (m : ℕ), ∃ n₀, ∀ (n : ℕ), n₀ ≤ n → a ^ n ∈ i ^ m

Tactic:
exact fun m ↦ ⟨m, fun n hn ↦ Ideal.pow_le_pow_right hn (Ideal.pow_mem_pow ha _)⟩

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (optionElim 0 (single i 1)) none = (single (Option.some i) 1) none

Tactic:
simp [single_apply]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: case some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i val✝ : σ
⊢ (optionElim 0 (single i 1)) (Option.some val✝) = (single (Option.some i) 1) (Option.some val✝)

Tactic:
simp [single_apply]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n))
      ((truncTotal n) ((algebraMap (MvPolynomial σ R) (MvPowerSeries σ R)) p)) =
    (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⧸ MvPolynomial.idealOfVars σ R ^ n)) p

Tactic:
change (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) (truncTotal n p) =
      (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) p

Goal state after:
σ✝ : Type u_1
R✝ : Type u_2
n✝ : ℕ
inst✝³ : CommRing R✝
inst✝² : Finite σ✝
σ : Type u_3
R : Type u_4
inst✝¹ : Finite σ
inst✝ : CommRing R
n : ℕ
p : MvPolynomial σ R
⊢ (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) ((truncTotal n) ↑p) =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n)) p
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f₁ : G →* H
φ : A ⟶ res f₁ B
T : Type u_1
F : (f : G →* H) → (A ⟶ res f B) → T
⊢ F f₁ φ = F f₁ (⋯ ▸ φ)

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n j : ℕ
g✝ : Fin (j + 1) → G
x✝ : ↑(ModuleCat.of k ↑A)
a✝ : Fin j → H
⊢ (single (fun i ↦ f (g✝ i.succ)) ((B.ρ (f (g✝ 0))⁻¹) ((Hom.hom φ) x✝))) a✝ =
    (single (⇑f ∘ fun i ↦ g✝ i.succ) ((B.ρ (f (g✝ 0))⁻¹) ((Hom.hom φ) x✝))) a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
n : ℕ
p : MvPowerSeries σ R
⊢ ↑((toAdicCompletion σ R) p) n = (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((truncTotal n) p)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
x : σ →₀ ℕ
f : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (coeff x) (toAdicCompletionInv σ R f) = MvPolynomial.coeff x (Quotient.out (↑f (degree x + 1)))

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
p : MvPowerSeries σ R
⊢ (toAdicCompletionAlgEquiv σ R) p = (toAdicCompletion σ R) p

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : AdicCompletion (MvPolynomial.idealOfVars σ R) (MvPolynomial σ R)
⊢ (toAdicCompletionAlgEquiv σ R).symm x = toAdicCompletionInv σ R x

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ denominator R x = Submodule.IsPrincipal.generator ((Subalgebra.toSubmodule (integralClosure R S)).colon {x})

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
x : S
⊢ natDenominator x = (denominator ℤ x).natAbs

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
y : AdicCompletion I ↥(I ^ n • ⊤)
⊢ n ≤ n

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.MonoidAlgebra

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : Semiring A
X : Type u_3
inst✝¹ : Module R A
inst✝ : Coalgebra R A
x : X
a : A
⊢ (TensorProduct.map (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x)
        (↑(coeffLinearEquiv R).symm ∘ₗ Finsupp.lsingle x))
      (comul a) =
    (TensorProduct.map (lsingle x) (lsingle x)) (comul a)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup C
inst✝¹ : Module R C
inst✝ : CoalgebraStruct R C
I : Submodule R C
⊢ I.IsCoideal ↔ (∀ x ∈ I, counit x = 0) ∧ ∀ x ∈ I, comul x ∈ (lTensor C I.subtype).range ⊔ (rTensor C I.subtype).range

Tactic:
by
  simp_rw [isCoideal_iff, ← LinearMap.mem_ker,
    TensorProduct.map_ker (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective
      (LinearMap.exact_subtype_mkQ I) I.mkQ_surjective]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case rTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map LinearMap.id I.mkQ ∘ₗ ↑(TensorProduct.lid R C).symm = (TensorProduct.mk R R (C ⧸ I)) 1 ∘ₗ I.mkQ

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Quotient

Goal state before:
pp: case lTensor_counit_comp_comul
R : Type u_1
C : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup C
inst✝² : Module R C
inst✝¹ : Coalgebra R C
I : Submodule R C
inst✝ : I.IsCoideal
⊢ map I.mkQ LinearMap.id ∘ₗ ↑(TensorProduct.rid R C).symm = (TensorProduct.mk R (C ⧸ I) R).flip 1 ∘ₗ I.mkQ

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map LinearMap.id ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) ∘ₗ
      ↑(TensorProduct.lid R A).symm =
    (↑(Algebra.TensorProduct.lid R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Quotient

Goal state before:
pp: case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Bialgebra R A
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : (Submodule.restrictScalars R I).IsCoideal
⊢ map ((AlgHom.id R (A ⧸ I)).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap) LinearMap.id ∘ₗ
      ↑(TensorProduct.rid R A).symm =
    (↑(Algebra.TensorProduct.rid R R (A ⧸ I)).symm).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
α : (FractionalIdeal A⁰ (FractionRing A))ˣ
⊢ (extendedHom A B) ↑α = ↑((Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) α)

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SInteger

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
S : Set (HeightOneSpectrum R)
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x✝¹ x✝ : ↥(S.unit K)
⊢ ↑↑{ val := ⟨↑↑(x✝¹ * x✝), ⋯⟩, inv := ⟨↑(↑(x✝¹ * x✝))⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } =
    ↑↑({ val := ⟨↑↑x✝¹, ⋯⟩, inv := ⟨↑(↑x✝¹)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ } *
          { val := ⟨↑↑x✝, ⋯⟩, inv := ⟨↑(↑x✝)⁻¹, ⋯⟩, val_inv := ⋯, inv_val := ⋯ })

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
⊢ H2π A ≫ map f φ 2 = mapCycles₂ f φ ≫ H2π B

Tactic:
simp [H2π, Iso.inv_comp_eq, ← cyclesMap_comp_isoCycles₂_hom_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f✝ : G →* H
φ : A ⟶ res f✝ B
n✝ n : ℕ
X✝ Y✝ Z✝ : Rep k G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ map (MonoidHom.id G) (f ≫ g) n =
    HomologicalComplex.homologyMap (chainsMap ((MonoidHom.id G).comp (MonoidHom.id G)) (f ≫ resMap (MonoidHom.id G) g))
      n

Tactic:
rfl

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ✝ : A ⟶ res f B
n✝ n : ℕ
X Y : Rep k H
φ : X ⟶ Y
⊢ HomologicalComplex.cyclesMap
        (chainsMap (f.comp (MonoidHom.id G)) (resMap f φ ≫ resMap (MonoidHom.id G) (𝟙 (res f Y)))) n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains Y) n =
    HomologicalComplex.cyclesMap (chainsMap ((MonoidHom.id H).comp f) (resMap f φ)) n ≫
      HomologicalComplex.homologyπ (inhomogeneousChains Y) n

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (v.intValuation.extendToLocalization ⋯ K) ↑x = ?m.34 * ?m.36

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Kˣ
⊢ v.valuationOfNeZero x • ↑n = Multiplicative.toAdd (v.valuationOfNeZero x) * ↑n

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x y : ↥selmerGroup
⊢ (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x * ((↑v).valuationOfNeZeroMod n) ↑y) =
    (fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑x) * fun v ↦ ((↑v).valuationOfNeZeroMod n) ↑y

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
r : R
h : Function.Injective ⇑(DistribSMul.toLinearMap R M r)
⊢ map ((LinearMap.lsmul R M) r) ⊤ ⊓ N ≤ map ((LinearMap.lsmul R M) r) N ↔ r • ⊤ ⊓ N ≤ r • N

Tactic:
rfl

Goal state after:
Module: Mathlib.RingTheory.Regular.LinearMap

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : IsNoetherianRing R
inst✝¹ : Module.Finite R M
inst✝ : Module.Finite R N
hom0 : Subsingleton (N →ₗ[R] M)
h✝ : Nontrivial M
h : ∀ r ∈ annihilator R N, ¬IsSMulRegular M r
Ia : Ideal R
hIa : Ia ∈ associatedPrimes R M
⊢ ∀ i ∈ associatedPrimes R M, i ≠ Ia → i ≠ Ia → i.IsPrime

Tactic:
· exact fun I hin _ _ ↦ IsAssociatedPrime.isPrime hin

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

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : ℕ → A → A
h₀ : ∀ {n : ℕ} {x : A}, x ∉ I → hI n x = 0
dpow_zero✝¹ : ∀ {x : A}, x ∈ I → hI 0 x = 1
dpow_one✝¹ : ∀ {x : A}, x ∈ I → hI 1 x = x
dpow_mem✝¹ : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI n x ∈ I
dpow_add✝¹ : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI n (x + y) = ∑ k ∈ antidiagonal n, hI k.1 x * hI k.2 y
dpow_mul✝¹ : ∀ {n : ℕ} {a x : A}, x ∈ I → hI n (a * x) = a ^ n * hI n x
mul_dpow✝¹ : ∀ {m n : ℕ} {x : A}, x ∈ I → hI m x * hI n x = ↑((m + n).choose m) * hI (m + n) x
dpow_comp✝¹ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI m (hI n x) = ↑(m.uniformBell n) * hI (m * n) x
hI' : ℕ → A → A
h₀' : ∀ {n : ℕ} {x : A}, x ∉ I → hI' n x = 0
dpow_zero✝ : ∀ {x : A}, x ∈ I → hI' 0 x = 1
dpow_one✝ : ∀ {x : A}, x ∈ I → hI' 1 x = x
dpow_mem✝ : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' n x ∈ I
dpow_add✝ : ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → hI' n (x + y) = ∑ k ∈ antidiagonal n, hI' k.1 x * hI' k.2 y
dpow_mul✝ : ∀ {n : ℕ} {a x : A}, x ∈ I → hI' n (a * x) = a ^ n * hI' n x
mul_dpow✝ : ∀ {m n : ℕ} {x : A}, x ∈ I → hI' m x * hI' n x = ↑((m + n).choose m) * hI' (m + n) x
dpow_comp✝ : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → hI' m (hI' n x) = ↑(m.uniformBell n) * hI' (m * n) x
h_eq :
  ∀ (n : ℕ) {x : A},
    x ∈ I →
      { dpow := hI, dpow_null := h₀, dpow_zero := dpow_zero✝¹, dpow_one := dpow_one✝¹, dpow_mem := dpow_mem✝¹,
              dpow_add := dpow_add✝¹, dpow_mul := dpow_mul✝¹, mul_dpow := mul_dpow✝¹, dpow_comp := dpow_comp✝¹ }.dpow
          n x =
        { dpow := hI', dpow_null := h₀', dpow_zero := dpow_zero✝, dpow_one := dpow_one✝, dpow_mem := dpow_mem✝,
              dpow_add := dpow_add✝, dpow_mul := dpow_mul✝, mul_dpow := mul_dpow✝, dpow_comp := dpow_comp✝ }.dpow
          n x
⊢ hI = hI'

Tactic:
grind

Goal state after:
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: case dp.add
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
⊢ ∑ i ∈ antidiagonal k, x * (dp R i.1 m * dp R i.2 n) ∈
    Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))

Tactic:
apply sum_mem (fun c hc ↦ ?_)

Goal state after:
R : Type u_4
M : Type u_5
ι : Type u_6
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
m✝ m n : M
hm_mem : m ∈ Submodule.span R (Set.range v)
hn_mem : n ∈ Submodule.span R (Set.range v)
hm :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k m ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
hn :
  ∀ (x : DividedPowerAlgebra R M) (k : ℕ),
    x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i)) →
      x * dp R k n ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
x : DividedPowerAlgebra R M
k : ℕ
hx : x ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))
c : ℕ × ℕ
hc : c ∈ antidiagonal k
⊢ x * (dp R c.1 m * dp R c.2 n) ∈ Submodule.span R (Set.range fun n ↦ n.prod fun i k ↦ dp R k (v i))