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

Goal state before:
pp: case refine_2
K L : Type
inst✝¹⁶ : Field K
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra K L
inst✝¹³ : FiniteDimensional K L
inst✝¹² : IsGalois K L
inst✝¹¹ : IsCyclic Gal(L/K)
g : Gal(L/K)
A : Type u_1
B : Type u_2
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra A L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsScalarTower A K L
inst✝² : IsFractionRing A K
inst✝¹ : IsDomain A
inst✝ : IsIntegralClosure B A L
hg : ∀ (x : Gal(L/K)), x ∈ Subgroup.zpowers g
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝¹ : Module.IsTorsionFree A L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
η' : Lˣ := Units.mk0 ((algebraMap B L) η) ⋯
ε : Lˣ
a : B
b : ↥(Algebra.algebraMapSubmonoid B A⁰)
h : IsLocalization.mk' L a b = ↑ε
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑b
this : t • IsLocalization.mk' L a b = (algebraMap B L) a
hε : (algebraMap B L) η = IsLocalization.mk' L a b / g (IsLocalization.mk' L a b)
⊢ g (IsLocalization.mk' L a b) ≠ 0

Tactic:
intro e
      rw [(map_eq_zero _).mp e, zero_div] at hε
      rw [hε, Algebra.norm_zero] at hη
      exact zero_ne_one hη

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↥(cocycles₁ A)
⊢ cocyclesMk ((ConcreteCategory.hom (cochainsIso₁ A).inv) ⇑x) ⋯ = (ConcreteCategory.hom (isoCocycles₁ A).inv) x

Tactic:
by
  apply_fun (forget₂ _ Ab).map ((inhomogeneousCochains A).iCycles 1) using
    (AddCommGrpCat.mono_iff_injective _).1 <| (forget₂ _ _).map_mono _
  have := (isoCocycles₁_inv_comp_iCocycles_apply _ x).symm
  rw [HomologicalComplex.i_cyclesMk]
  simp only [ModuleCat.forget₂_obj, ModuleCat.forget₂_map, ConcreteCategory.hom_ofHom,
    AddMonoidHom.coe_coe]
  rw [← this]
  rfl

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x = (ConcreteCategory.hom (H1π A)) y ↔ ⇑x - ⇑y ∈ coboundaries₁ A

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x - (ConcreteCategory.hom (H1π A)) y = 0 ↔ ⇑x - ⇑y ∈ coboundaries₁ A
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x = (ConcreteCategory.hom (H2π A)) y ↔ ⇑x - ⇑y ∈ coboundaries₂ A

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cocycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x - (ConcreteCategory.hom (H2π A)) y = 0 ↔ ⇑x - ⇑y ∈ coboundaries₂ A
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝⁴ : CommRing k
inst✝³ : CommGroup G
inst✝² : Fintype G
A : Rep k G
g : G
inst✝¹ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) x =
      (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) y ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝⁴ : CommRing k
inst✝³ : CommGroup G
inst✝² : Fintype G
A : Rep k G
g : G
inst✝¹ : DecidableEq G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
i : ℕ
inst✝ : NeZero i
hi : Even i
x y : ↥(LinearMap.ker A.ρ.norm)
⊢ (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) x -
        (ConcreteCategory.hom (groupHomologyπEven A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ (Hom.hom (A.applyAsHom g - 𝟙 A)).range
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic

Goal state before:
pp: k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x = (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) y ↔
    ↑x - ↑y ∈ LinearMap.range A.ρ.norm

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝³ : CommRing k
inst✝² : CommGroup G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
g : G
hg : ∀ (x : G), x ∈ Subgroup.zpowers g
A : Rep k G
i : ℕ
hi : Odd i
x y : ↥(Hom.hom (A.applyAsHom g - 𝟙 A)).ker
⊢ (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) x - (ConcreteCategory.hom (groupHomologyπOdd A g hg i hi)) y =
      0 ↔
    ↑x - ↑y ∈ LinearMap.range A.ρ.norm
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ M.tateNorm ≫ (inhomogeneousCochains M).d 0 1 = 0

Tactic:
simp [tateNorm, eq_d₀₁_comp_inv M]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

Tactic:
by_cases h : r = 0

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : ℕ
r : R
h : ¬r = 0
⊢ C r ∈ idealOfVars σ R ^ n ↔ r = 0 ∨ n = 0
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 (embDomain e x)) ((rename ⇑e) p) = (coeff x) p

Tactic:
rw [coeff_rename, Finset.sum_eq_single x _ (by simp [← embDomain_eq_mapDomain])]

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
e : σ ↪ τ
p : MvPowerSeries σ R
x : σ →₀ ℕ
⊢ ∀ b ∈ ⋯.toFinset, b ≠ x → (coeff b) p = 0
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: case mpr
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
a : A
⊢ (∃ x, (x.sum fun g z ↦ g • z - z) = a) → IsBoundary₀ G a

Tactic:
rintro ⟨x, hx⟩
    use x.sum (fun g a => single g (-(g • a)))
    simp_all [sum_neg_index, sum_sum_index, neg_add_eq_sub]

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

Goal state before:
pp: case refine_1
σ : Type u_1
τ : Type u_2
f : σ → τ
inst✝¹ : TendstoCofinite f
R : Type u_6
inst✝ : CommRing R
p : MvPowerSeries σ R
n : τ →₀ ℕ
this : ∀ (d : σ →₀ ℕ), (coeff d) p * (coeff n) (d.prod fun s e ↦ X (f s) ^ e) ≠ 0 → mapDomain f d = n
⊢ Set.Finite.toFinset ⋯ ⊆ ⋯.toFinset

Tactic:
exact Set.Finite.toFinset_mono this

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)
⊢ (ConcreteCategory.hom (H1π A)) x = (ConcreteCategory.hom (H1π A)) y ↔ ↑x - ↑y ∈ boundaries₁ A

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₁ A)
⊢ (ConcreteCategory.hom (H1π A)) x - (ConcreteCategory.hom (H1π A)) y = 0 ↔ ↑x - ↑y ∈ boundaries₁ A
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)
⊢ (ConcreteCategory.hom (H2π A)) x = (ConcreteCategory.hom (H2π A)) y ↔ ↑x - ↑y ∈ boundaries₂ A

Tactic:
← sub_eq_zero,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ (ConcreteCategory.hom (H2π A)) x - (ConcreteCategory.hom (H2π A)) y = 0 ↔ ↑x - ↑y ∈ boundaries₂ A
Module: Mathlib.RingTheory.PowerSeries.Ideal

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∈ P
⊢ P.FG

Tactic:
have H := eq_span_insert_X_of_X_mem_of_span_eq hX hS

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R⟦X⟧
inst✝ : P.IsPrime
S : Finset R
hS : span ↑S = Ideal.map constantCoeff P
hX : X ∈ P
H : P = span (insert X (⇑C '' ↑S))
⊢ P.FG
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
x : R
this✝ : TopologicalSpace R := I.adicTopology
this : (Filter.map (fun y ↦ x + y) (𝓝 0)).HasBasis (fun _n ↦ True) fun i ↦ (fun y ↦ x + y) '' ↑(I ^ i)
⊢ (𝓝 x).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ x + y) '' ↑(I ^ n)

Tactic:
rwa [map_add_left_nhds_zero x] at this

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

Goal state before:
pp: case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R))) ((residue R) z) = x

Tactic:
IsLocalRing.ResidueField.map_residue,

Goal state after:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
this : IsLocalRing (AdicCompletion (maximalIdeal R) R)
x : IsLocalRing.ResidueField (AdicCompletion (maximalIdeal R) R)
y : AdicCompletion (maximalIdeal R) R
hy : (residue (AdicCompletion (maximalIdeal R) R)) y = x
z : R
hz : (Ideal.Quotient.mk (maximalIdeal R ^ 1 • ⊤)) z = ↑y 1
⊢ (residue (AdicCompletion (maximalIdeal R) R)) ((algebraMap R (AdicCompletion (maximalIdeal R) R)) z) = x
Module: Mathlib.RingTheory.AdicCompletion.LocalRing

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
⊢ Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (maximalIdeal R) R)))

Tactic:
have := AdicCompletion.isLocalRing_of_fg fg
  refine ⟨RingHom.injective _, fun x ↦ ?_⟩
  rcases residue_surjective x with ⟨y, hy⟩
  rcases Ideal.Quotient.mk_surjective (y.1 1) with ⟨z, hz⟩
  use residue R z
  rw [IsLocalRing.ResidueField.map_residue, ← hy]
  apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr
  rw [maximalIdeal_eq_map_of_fg fg, ← Submodule.restrictScalars_mem R, ← Ideal.smul_top_eq_map]
  have : (algebraMap R (AdicCompletion (maximalIdeal R) R)) z - y ∈
    (maximalIdeal R) ^ 1 • (⊤ : Submodule R (AdicCompletion (maximalIdeal R) R)) := by
    rw [AdicCompletion.algebraMap_apply, pow_smul_top_eq_ker_eval fg]
    simpa [eval, sub_eq_zero] using hz
  simpa

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 i j : ℕ
hij : j + 1 = i
⊢ ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x) ≫
      (inhomogeneousChains B).d i j =
    (inhomogeneousChains A).d i j ≫
      ModuleCat.ofHom (mapRange.linearMap (Hom.hom φ).toLinearMap ∘ₗ lmapDomain (↑A) k fun x ↦ ⇑f ∘ x)

Tactic:
subst hij
    ext
    simp [Fin.comp_contractNth, map_add, inhomogeneousChains.d, Rep.hom_comm_apply φ]
    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 : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n)) = MvPolynomial.coeff x ((truncTotal n) p)

Tactic:
← sub_eq_zero,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Finite σ
x : σ →₀ ℕ
p : MvPowerSeries σ R
n : ℕ
hx : degree x < n
⊢ MvPolynomial.coeff x (Quotient.out (↑((toAdicCompletion σ R) p) n)) - MvPolynomial.coeff x ((truncTotal n) p) = 0
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✝ : ℕ
e : G ≃* H
e' : ↑A ≃ₗ[k] ↑B
he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ map ((↑e.symm).comp ↑e)
      (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ } ≫
        (resFunctor ↑e).map (ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ }))
      n =
    map (MonoidHom.id G) (𝟙 A) n

Tactic:
exact groupHomology.map_congr e.coe_monoidHom_symm_comp_coe_monoidHom e'.symm_comp n

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

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
simpa [SModEq.zero] using hx

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

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
inst✝³ : IsNoetherianRing R
inst✝² : Module.Finite R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
h : I ≠ ⊤
x : M
hx : ∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]
⊢ x ∈ ⨅ i, I ^ i • ⊤

Tactic:
simpa [SModEq.zero] using hx

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

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
hcxa : d = c x
⊢ False

Tactic:
obtain rfl : x = a := by rwa [hcxa, smul_right_inj hcx] at hc

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
s : Finset A
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
hcxa : d = c x
has : x ∉ s
ha : IsGroupLikeElem R x
hc : c x • x = d • x
⊢ False
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
α : (FractionRing A)ˣ
⊢ (toPrincipalIdeal B (FractionRing B)) (Units.mk0 ((IsFractionRing.map ⋯) ↑α) ⋯) =
    (Units.map ↑(FractionalIdeal.extendedHom (FractionRing B) B)) ((toPrincipalIdeal A (FractionRing A)) α)

Tactic:
simpa [coe_toPrincipalIdeal, Units.coe_map, Units.val_mk0] using!
        (FractionalIdeal.extendedHom_spanSingleton (FractionRing B) B _).symm

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✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
I : ↥(Ideal A)⁰
⊢ (extendedHom A B) (mk0 I) = 1 (mk0 I)

Tactic:
extendedHom_mk0,

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra A B
inst✝² : Module.IsTorsionFree A B
inst✝¹ : IsDedekindDomain A
inst✝ : IsDedekindDomain B
h : ∀ (I : Ideal A), Submodule.IsPrincipal (Ideal.map (algebraMap A B) I)
I : ↥(Ideal A)⁰
⊢ mk0 (extendedIdeal A B I) = 1 (mk0 I)
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (∀ x ∈ ↑p.coeffs, x = 0) → p = 0

Tactic:
contrapose!

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ p ≠ 0 → ∃ x ∈ ↑p.coeffs, x ≠ 0
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ((monomial n) r).contentIdeal = span {r}

Tactic:
by_cases h : r = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
h : r = 0
⊢ ((monomial n) r).contentIdeal = span {r}

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
h : ¬r = 0
⊢ ((monomial n) r).contentIdeal = span {r}
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.IsPrimitive → p.contentIdeal = ⊤

Tactic:
contrapose!

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h_prin : Submodule.IsPrincipal p.contentIdeal
⊢ p.contentIdeal ≠ ⊤ → ¬p.IsPrimitive
Module: Mathlib.RingTheory.DedekindDomain.GaussLemma

Goal state before:
pp: case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)) < 1 → ∀ x ∈ p.coeffs, (v.intAdicAbv hb) x < 1

Tactic:
contrapose!

Goal state after:
case neg.mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
b : NNReal
hb : 1 < b
p : R[X]
hp0 : ¬p = 0
hsupp_nonempty : p.support.Nonempty
⊢ (∃ x ∈ p.coeffs, 1 ≤ (v.intAdicAbv hb) x) → 1 ≤ p.support.sup' ⋯ fun x ↦ (v.intAdicAbv hb) (p.coeff x)
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 : Rˣ
⊢ (valuation K v) ↑((Units.map ↑(algebraMap R K)) x) = ↑1

Tactic:
Units.coe_map,

Goal state after:
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 : Rˣ
⊢ (valuation K v) (↑(algebraMap R K) ↑x) = ↑1
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' r s = IsLocalization.mk' R' (↑t * r) (t * s)

Tactic:
← sub_eq_zero,

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : (Ideal.comap (algebraMap R R') p).IsPrime
x : M
hx : Ideal.comap (algebraMap R R') p = (⊥.colon {x}).radical
t✝ : R'
r : R
s : ↥S
hrs : IsLocalization.mk' R' r s = t✝
x✝ : ∃ n s', s' • r ^ n • x = 0
n : ℕ
t : ↥S
ht : t • r ^ n • x = 0
⊢ IsLocalization.mk' R' r s - IsLocalization.mk' R' (↑t * r) (t * s) = 0
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module R M
p : Ideal R
inst✝ : p.IsPrime
ass : p ∈ associatedPrimes R M
⊢ maximalIdeal (Localization.AtPrime p) ∈ associatedPrimes (Localization.AtPrime p) (LocalizedModule.AtPrime p M)

Tactic:
apply mem_associatedPrimes_of_comap_mem_associatedPrimes_of_isLocalizedModule
    p.primeCompl (LocalizedModule.mkLinearMap p.primeCompl M)
  simpa [Localization.AtPrime.under_maximalIdeal] using ass

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

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
n : ℕ
hn : Fact (0 < n)
val✝ inv✝ : R
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ fromUnit.ker →
    { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ (powMonoidHom n).range

Tactic:
intro hx
    rcases (QuotientGroup.eq_one_iff _).mp (Subtype.mk.inj hx) with ⟨⟨v, i, vi, iv⟩, hx⟩
    have hv : ↑(_ ^ n : Kˣ) = algebraMap R K _ := congr_arg Units.val hx
    have hi : ↑(_ ^ n : Kˣ)⁻¹ = algebraMap R K _ := congr_arg Units.inv hx
    rw [Units.val_pow_eq_pow_val] at hv
    rw [← inv_pow, Units.inv_mk, Units.val_pow_eq_pow_val] at hi
    rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := v) hn.out
        (hv.symm ▸ isIntegral_algebraMap) with
      ⟨v', rfl⟩
    rcases IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow (R := R) (x := i) hn.out
        (hi.symm ▸ isIntegral_algebraMap) with
      ⟨i', rfl⟩
    rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at vi
    rw [← map_mul, map_eq_one_iff _ <| FaithfulSMul.algebraMap_injective R K] at iv
    rw [Units.val_mk, ← map_pow] at hv
    exact ⟨⟨v', i', vi, iv⟩, by
      simpa only [Units.ext_iff, powMonoidHom_apply, Units.val_pow_eq_pow_val] using
         FaithfulSMul.algebraMap_injective R K hv⟩

Goal state after: