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

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
i : ι
⊢ { var := s.var, linearCombination_var_relation := ⋯ }.π (data.lift i) = 0

Tactic:
exact s.linearCombination_var_relation (.inr i)

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

Goal state before:
pp: case h.succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ R ∙ p ^ k i)

Tactic:
let s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove

Goal state after:
case h.succ
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
⊢ ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin (d + 1)), R ⧸ R ∙ p ^ k i)
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
i : Fin d
⊢ f (Submodule.Quotient.mk ⋯.choose) =
    (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) ((Ideal.Quotient.mk (R ∙ p ^ k i)) 1)

Tactic:
map_one (Ideal.Quotient.mk _),

Goal state after:
case h.succ.refine_3.refine_2.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this✝ : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
k : Fin d → ℕ
f : (M ⧸ R ∙ s j) ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i
this :
  ∀ (i : Fin d),
    ∃ x, p ^ k i • x = 0 ∧ f (Submodule.Quotient.mk x) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
i : Fin d
⊢ f (Submodule.Quotient.mk ⋯.choose) = (DirectSum.lof R (Fin d) (fun i ↦ R ⧸ R ∙ p ^ k i) i) 1
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case inr
R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p : MvPolynomial σ R
j : σ
eq : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
h : j ≠ i
⊢ (pderiv i) ((map φ) (p * X j)) = (map φ) ((pderiv i) (p * X j))

Tactic:
· simp [eq, h]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Derivation

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ C a • D f = a • D f

Tactic:
by
  have : C a • D f = D (C a * f) := by simp
  rw [this, C_mul', D.map_smul]

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

Goal state before:
pp: case e'_5
R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
this : IsLocalizedModule S LinearMap.id
⊢ (map S f LinearMap.id) f = LinearMap.id

Tactic:
apply IsLocalizedModule.ext S f

Goal state after:
case e'_5.map_unit
R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
this : IsLocalizedModule S LinearMap.id
⊢ ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M')) ↑x)

case e'_5.h
R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
this : IsLocalizedModule S LinearMap.id
⊢ (map S f LinearMap.id) f ∘ₗ f = LinearMap.id ∘ₗ f
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ mk.ker = P.ker • ⊤

Tactic:
ext ⟨x, hx⟩
  simp [LinearMap.mem_ker, mk_eq_zero_iff, Submodule.mem_smul_top_iff, sq]

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

Goal state before:
pp: case mpr
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
ι' : Type u_1
σ' : Type u_2
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra S T
Q : Presentation S T ι' σ'
P : Presentation R S ι σ
x : MvPolynomial ι' S
⊢ x ∈ Set.range Q.relation → x ∈ ⇑(Q.aux P) '' Set.range (Q.compRelationAux P)

Tactic:
rintro ⟨y, rfl⟩
    use Q.compRelationAux P y
    simp only [Set.mem_range, exists_apply_eq_apply, true_and, compRelationAux_map]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: A : Type u
inst✝⁶ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module A M₁
inst✝² : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
h₁ : solution₁.IsPresentation
h₂ : solution₂.IsPresentation
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (relations₁.tensor relations₂).Solution N✝
g₁ : relations₁.G
r₂ : relations₂.R
⊢ (Finsupp.linearCombination A s.var)
      (Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)) =
    0

Tactic:
exact s.linearCombination_var_relation (.inr ⟨g₁, r₂⟩)

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

Goal state before:
pp: case tmul.add
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : S
x✝ y✝ : P.Ring ⊗[R] P.Ring
a✝¹ :
  (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo x✝) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo x✝)
a✝ :
  (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y✝) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y✝)
⊢ (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ + y✝)) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ + y✝))

Tactic:
simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, *]

Goal state after:
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⋯
x' : Fin l → M := ⋯
this : ∑ i, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i, f' i * a' i j = 0
⊢ ∃ y,
    (x = y ∘ₗ linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) ∧
      (linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) f = 0

Tactic:
use Finsupp.linearCombination R y'

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
tfae_1_iff_2 : Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_2 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
tfae_3_iff_4 :
  (∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → VanishesTrivially R f x) ↔
    ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
h₄ : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x
l : ℕ
f : Fin l →₀ R
x : (Fin l →₀ R) →ₗ[R] M
hfx : x f = 0
f' : Fin l → R := ⋯
x' : Fin l → M := ⋯
this : ∑ i, f' i • x' i = 0
k : ℕ
a' : Fin l → Fin k → R
y' : Fin k → M
ha'y' : ∀ (i : Fin l), x' i = ∑ j, a' i j • y' j
ha' : ∀ (j : Fin k), ∑ i, f' i * a' i j = 0
⊢ (x = linearCombination R y' ∘ₗ linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) ∧
    (linearCombination R fun i ↦ equivFunOnFinite.symm (a' i)) f = 0
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case tmul.add
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
x✝ y✝ : P.Ring ⊗[R] P.Ring
a✝¹ :
  (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo x✝) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo x✝)
a✝ :
  (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y✝) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo y✝)
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ + y✝)) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo (x✝ + y✝))

Tactic:
simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Function.comp_apply, *]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
⊢ map f = map g

Tactic:
ext x
  simp only [map_apply_coe]
  rw [← sub_eq_zero, ← Cotangent.val_sub, ← LinearMap.sub_apply, Cotangent.map_sub_map]
  simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.map_coe_ker, map_zero,
    Cotangent.val_zero]

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ zeroLocus ↑(annihilator R (M ⧸ I • ⊤)) ⊆ zeroLocus ↑I

Tactic:
apply PrimeSpectrum.zeroLocus_anti_mono_ideal

Goal state after:
case a.refine_2
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
⊢ I ≤ annihilator R (M ⧸ I • ⊤)
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
t : Set R
Mₚ : ↑t → Type u_1
inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)
inst✝⁴ : (g : ↑t) → Module R (Mₚ g)
Rₚ : ↑t → Type u_2
inst✝³ : (g : ↑t) → CommSemiring (Rₚ g)
inst✝² : (g : ↑t) → Algebra R (Rₚ g)
h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)
inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)
inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↑t) → M →ₗ[R] Mₚ g
h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)
t' : Finset R
hc : ↑t' ⊆ t
ht' : Ideal.span ↑t' = ⊤
⊢ Module.Finite R M

Tactic:
have (g : t') : IsLocalization.Away g.val (Rₚ ⟨g.val, hc g.property⟩) :=
    h₁ ⟨g.val, hc g.property⟩

Goal state after:
R : Type u
inst✝⁸ : CommSemiring R
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
t : Set R
Mₚ : ↑t → Type u_1
inst✝⁵ : (g : ↑t) → AddCommMonoid (Mₚ g)
inst✝⁴ : (g : ↑t) → Module R (Mₚ g)
Rₚ : ↑t → Type u_2
inst✝³ : (g : ↑t) → CommSemiring (Rₚ g)
inst✝² : (g : ↑t) → Algebra R (Rₚ g)
h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)
inst✝¹ : (g : ↑t) → Module (Rₚ g) (Mₚ g)
inst✝ : ∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↑t) → M →ₗ[R] Mₚ g
h₂ : ∀ (g : ↑t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)
t' : Finset R
hc : ↑t' ⊆ t
ht' : Ideal.span ↑t' = ⊤
this : ∀ (g : ↥t'), IsLocalization.Away (↑g) (Rₚ ⟨↑g, ⋯⟩)
⊢ Module.Finite R M
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
hk : Even k
⊢ Odd n ∨ Even ↑k

Tactic:
← Nat.not_even_iff_odd,

Goal state after:
n : ℕ
k : Fin n
hk : Even k
⊢ ¬Even n ∨ Even ↑k
Module: Mathlib.Data.Fin.Parity

Goal state before:
pp: n : ℕ
k : Fin n
inst✝ : NeZero n
hk : Odd k
⊢ Odd n ∨ Odd ↑k

Tactic:
← Nat.not_even_iff_odd,

Goal state after:
n : ℕ
k : Fin n
inst✝ : NeZero n
hk : Odd k
⊢ ¬Even n ∨ Odd ↑k
Module: Mathlib.LinearAlgebra.TensorPower.Pairing

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x✝ : DecidableEq (Fin n)
f : Fin n → Module.Dual R M
φ : Module.Dual R M
j : Fin n
v : Fin n → M
⊢ (Function.update f j φ j) (v j) = Function.update (fun j ↦ (f j) (v j)) j (φ (v j)) j

Tactic:
simp only [Function.update_self]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
⊢ a = b

Tactic:
have hσ' : Monotone σ.symm := fun i j hij ↦ by
    obtain ⟨i, rfl⟩ := σ.surjective i
    obtain ⟨j, rfl⟩ := σ.surjective j
    simp only [Equiv.symm_apply_apply]
    by_contra! h
    obtain rfl : i = j := σ.injective (le_antisymm hij (hσ h.le))
    simp only [lt_self_iff_false] at h

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : LinearOrder ι
x : ι → M
f : ι → Module.Dual R M
h₀ : ∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0
n : ℕ
a b : Fin n ↪o ι
h : a ≠ b
σ : Equiv.Perm (Fin n)
x✝ : σ ∈ Finset.univ
h' : ¬∏ i, (f (a i)) (x (b (σ i))) = 0
this : ⇑a = ⇑b ∘ ⇑σ
hσ : Monotone ⇑σ
hσ' : Monotone ⇑(Equiv.symm σ)
⊢ a = b
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
⊢ Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂ → N₁ = N₂

Tactic:
intro hN

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsLocalRing R
N₁ N₂ : Submodule R M
h : N₁ ≤ N₂
h' : N₂.FG
hN : Submodule.map (𝔪 • N₂).mkQ N₁ = Submodule.map (𝔪 • N₂).mkQ N₂
⊢ N₁ = N₂
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
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map (𝔪 • ⊤).mkQ N = ⊤ ↔ N = ⊤

Tactic:
rw [← map_mkQ_eq (N₁ := N) le_top Module.Finite.fg_top, Submodule.map_top, Submodule.range_mkQ]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
⊢ Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤ → N = ⊤

Tactic:
intro hN

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
N : Submodule R M
inst✝ : Module.Finite R M
hN : Submodule.map ((TensorProduct.mk R k M) 1) N = ⊤
⊢ N = ⊤
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
h1 : Function.Injective ⇑i1
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))

Tactic:
have h2 : Function.Injective i2 := Module.Flat.lTensor_preserves_injective_linearMap _ hn

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
κ : Type u_1
ι : Type u_2
m : κ → ↥M
n : ι → ↥N
hm : Function.Injective ⇑(Finsupp.linearCombination R m)
hn : Function.Injective ⇑(Finsupp.linearCombination R n)
i0 : (κ × ι →₀ R) ≃ₗ[R] (κ →₀ R) ⊗[R] (ι →₀ R) := (finsuppTensorFinsupp' R κ ι).symm
i1 : (κ →₀ R) ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] (ι →₀ R) := LinearMap.rTensor (ι →₀ R) (Finsupp.linearCombination R m)
i2 : ↥M ⊗[R] (ι →₀ R) →ₗ[R] ↥M ⊗[R] ↥N := LinearMap.lTensor (↥M) (Finsupp.linearCombination R n)
i : (κ × ι →₀ R) →ₗ[R] S := M.mulMap N ∘ₗ i2 ∘ₗ i1 ∘ₗ ↑i0
h1 : Function.Injective ⇑i1
h2 : Function.Injective ⇑i2
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ ↑(m i.1) * ↑(n i.2))
Module: Mathlib.RingTheory.LocalRing.Module

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✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝ : Free R (N ⧸ l.range)
this : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
⊢ Surjective ⇑l'

Tactic:
exact Function.HasRightInverse.surjective ⟨_, DFunLike.congr_fun hl'⟩

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

Goal state before:
pp: case inr
R : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ (ClassGroup.mk K) u = 1

Tactic:
← orderOf_eq_one_iff,

Goal state after:
case inr
R : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
u : (FractionalIdeal R⁰ K)ˣ
hI : (↑(↑u ^ n)).IsPrincipal
⊢ orderOf ((ClassGroup.mk K) u) = 1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ ClassGroup.mk0 ⟨I, ⋯⟩ = 1

Tactic:
← orderOf_eq_one_iff,

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ orderOf (ClassGroup.mk0 ⟨I, ⋯⟩) = 1
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ IsPrincipalIdealRing R → Fintype.card (ClassGroup R) = 1

pp: case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R

Tactic:
· intros; convert! card_classGroup_eq_one (R := R)

Goal state after:
case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 → IsPrincipalIdealRing R
Module: Mathlib.GroupTheory.Perm.ViaEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
e : Perm α
ι : α ↪ β
x : β
hx : ¬x ∈ Set.range ⇑ι
⊢ (e.viaEmbedding ι) x = x

Tactic:
classical
  exact extendDomain_apply_not_subtype e (ofInjective ι.1 ι.2) hx

Goal state after: