mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : Y ⟶ Z), 0 • F.map a = 0

Tactic:
intros

Goal state after:
case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
a✝ : Y ⟶ Z
⊢ 0 • F.map a✝ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : Y ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
intros

Goal state after:
case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
a✝ : Y ⟶ Z
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • F.map a✝ = b₁✝ • F.map a✝ + b₂✝ • F.map a✝
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z), 0 • F.map a = 0

Tactic:
intros

Goal state after:
case single.add.h_zero
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
a✝ : X ⟶ Z
⊢ 0 • F.map a✝ = 0
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
⊢ ∀ (a : X ⟶ Z) (b₁ b₂ : R), (b₁ + b₂) • F.map a = b₁ • F.map a + b₂ • F.map a

Tactic:
intros

Goal state after:
case single.add.h_add
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
f' : X ⟶ Y
r : R
f₁ f₂ : (Y ⟶ Z) →₀ R
w₁ :
  (sum (single f' r ≫ f₁) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₁.sum fun f' r ↦ r • F.map f'
w₂ :
  (sum (single f' r ≫ f₂) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ f₂.sum fun f' r ↦ r • F.map f'
a✝ : X ⟶ Z
b₁✝ b₂✝ : R
⊢ (b₁✝ + b₂✝) • F.map a✝ = b₁✝ • F.map a✝ + b₂✝ • F.map a✝
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S S₁ S₂ S₃ x✝ : SnakeInput C
⊢ pullback.map x✝.L₁.g x✝.v₀₁.τ₃ x✝.L₁.g x✝.v₀₁.τ₃ (𝟙 x✝).f₁.τ₂ (𝟙 x✝).f₀.τ₃ (𝟙 x✝).f₁.τ₃ ⋯ ⋯ = 𝟙 x✝.P

Tactic:
dsimp [P]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S S₁ S₂ S₃ x✝ : SnakeInput C
⊢ pullback.map x✝.L₁.g x✝.v₀₁.τ₃ x✝.L₁.g x✝.v₀₁.τ₃ (𝟙 x✝.L₁.X₂) (𝟙 x✝.L₀.X₃) (𝟙 x✝.L₁.X₃) ⋯ ⋯ =
    𝟙 (pullback x✝.L₁.g x✝.v₀₁.τ₃)
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S S₁ S₂ S₃ X✝ Y✝ Z✝ : SnakeInput C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Z✝.L₁.g Z✝.v₀₁.τ₃ (x✝¹ ≫ x✝).f₁.τ₂ (x✝¹ ≫ x✝).f₀.τ₃ (x✝¹ ≫ x✝).f₁.τ₃ ⋯ ⋯ =
    pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Y✝.L₁.g Y✝.v₀₁.τ₃ x✝¹.f₁.τ₂ x✝¹.f₀.τ₃ x✝¹.f₁.τ₃ ⋯ ⋯ ≫
      pullback.map Y✝.L₁.g Y✝.v₀₁.τ₃ Z✝.L₁.g Z✝.v₀₁.τ₃ x✝.f₁.τ₂ x✝.f₀.τ₃ x✝.f₁.τ₃ ⋯ ⋯

Tactic:
dsimp [P]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S S₁ S₂ S₃ X✝ Y✝ Z✝ : SnakeInput C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Z✝.L₁.g Z✝.v₀₁.τ₃ (x✝¹.f₁.τ₂ ≫ x✝.f₁.τ₂) (x✝¹.f₀.τ₃ ≫ x✝.f₀.τ₃) (x✝¹.f₁.τ₃ ≫ x✝.f₁.τ₃)
      ⋯ ⋯ =
    pullback.map X✝.L₁.g X✝.v₀₁.τ₃ Y✝.L₁.g Y✝.v₀₁.τ₃ x✝¹.f₁.τ₂ x✝¹.f₀.τ₃ x✝¹.f₁.τ₃ ⋯ ⋯ ≫
      pullback.map Y✝.L₁.g Y✝.v₀₁.τ₃ Z✝.L₁.g Z✝.v₀₁.τ₃ x✝.f₁.τ₂ x✝.f₀.τ₃ x✝.f₁.τ₃ ⋯ ⋯
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)

Tactic:
by
  have := ((CategoryTheory.Functor.exact_tfae (ModuleCat.restrictScalars.{v} f)).out 1 3).mp
    (ModuleCat.restrictScalars_map_exact f)
  exact this.2

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
⊢ ∀ (i : ℕ) (hi : i < 1),
    (F.map' i (i + 1) ⋯ hi ≫
        match ⟨i + 1, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) =
      (match ⟨i, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) ≫
        G.map' i (i + 1) ⋯ hi

Tactic:
intro i hi
          obtain rfl : i = 0 := by simpa using hi
          exact w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
⊢ ∀ (s : Cocone I.multispan) (m : K.pt ⟶ s.pt), (∀ (j : WalkingMultispan J), K.ι.app j ≫ m = s.ι.app j) → m = desc s

Tactic:
intro S

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
⊢ ∀ (m : K.pt ⟶ S.pt), (∀ (j : WalkingMultispan J), K.ι.app j ≫ m = S.ι.app j) → m = desc S
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], PreservesLimit (parallelPair f g) F

Tactic:
intros

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this : HasEqualizerOfIsCosplitPair F
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
inst✝ : F.IsCosplitPair f✝ g✝
⊢ PreservesLimit (parallelPair f✝ g✝) F
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this✝ : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
⊢ ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], ReflectsLimit (parallelPair f g) F

Tactic:
intros

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : CreatesLimitOfIsCosplitPair F
I : ∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g], HasLimit (parallelPair f g ⋙ F)
this✝ : HasEqualizerOfIsCosplitPair F
this : PreservesLimitOfIsCosplitPair F
A✝ B✝ : C
f✝ g✝ : A✝ ⟶ B✝
inst✝ : F.IsCosplitPair f✝ g✝
⊢ ReflectsLimit (parallelPair f✝ g✝) F
Module: Mathlib.CategoryTheory.Monad.Limits

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
R : D ⥤ C
inst✝ : Coreflective R
K : Discrete PEmpty.{v + 1} ⥤ C
⊢ PreservesColimit K (comonadicRightAdjoint R)

Tactic:
by
    let F := Functor.empty.{v} D
    let : PreservesColimit (F ⋙ R) (comonadicRightAdjoint R) := by
      constructor
      intro c h
      have : HasColimit (F ⋙ R) := ⟨⟨⟨c, h⟩⟩⟩
      have : HasColimit F := hasColimit_of_coreflective F R
      constructor
      apply isColimitChangeEmptyCocone D (colimit.isColimit F)
      apply (asIso ((comonadicAdjunction R).unit.app _)).trans
      apply (comonadicRightAdjoint R).mapIso
      letI := comonadicCreatesColimits.{v, v} R
      let A := CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit F R
      apply (isColimitOfPreserves _ (colimit.isColimit F)).coconePointUniqueUpToIso h
    apply preservesColimit_of_iso_diagram _ (Functor.emptyExt (F ⋙ R) _)

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
⊢ a⁻¹⁻¹ • x ∈ S ↔ a • x ∈ S

Tactic:
inv_inv

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
⊢ a • x ∈ S ↔ a • x ∈ S
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ ↑M'
⊢ f x ∈ localized₀ p f M'

Tactic:
mem_localized₀

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
x : M
hx : x ∈ ↑M'
⊢ ∃ m ∈ M', ∃ s, IsLocalizedModule.mk' f m s = f x
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
ι : Type u_5
g : ι → Submodule R M
⊢ localized' S p f (⨆ i, g i) = ⨆ i, localized' S p f (g i)

Tactic:
by
  exact GaloisConnection.l_iSup (localized'gi S p f).gc

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_1
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ≤ Submodule.comap f p
hnp : IsNilpotent f
⊢ IsNilpotent (p.mapQ p f hp)

Tactic:
by
  obtain ⟨k, hk⟩ := hnp
  use k
  simp [← p.mapQ_pow, hk]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
x : S
r : R
s : ↥M
hJ : mk' S r s ∈ J
hx : mk' S r s = x
⊢ mk' S r s ∈ Ideal.map (algebraMap R S) (Ideal.under R J)

Tactic:
exact
      Ideal.mul_mem_right _ _
        (Ideal.mem_map_of_mem _
          (show (algebraMap R S) r ∈ J from
            mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
⊢ Ideal.under R (Ideal.map (algebraMap R S) I) = I

Tactic:
refine le_antisymm (fun a ha ↦ ?_) Ideal.le_comap_map

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
I : Ideal R
hI : I.IsPrimary
hM : Disjoint ↑M ↑I
key : Disjoint ↑M ↑I.radical
a : R
ha : a ∈ Ideal.under R (Ideal.map (algebraMap R S) I)
⊢ a ∈ I
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
m : M
N : Submodule R M
h : ∀ (P : Ideal R) [inst : P.IsMaximal], (f P) m ∈ localized₀ P.primeCompl (f P) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
x✝ : ∃ M, M.IsMaximal ∧ I ≤ M
P : Ideal R
hP : P.IsMaximal
le : I ≤ P
a : M
ha : a ∈ N
s t : ↥P.primeCompl
ht : (t * s) • m = (t * 1) • a
⊢ ↑(t * s) ∈ I

Tactic:
by apply ht ▸ smul_mem _ _ ha

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
M₁ : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁵ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝³ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
M₁ₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (M₁ₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (M₁ₚ P)
f₁ : (P : Ideal R) → [inst : P.IsMaximal] → M₁ →ₗ[R] M₁ₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f₁ P)
g g' : M →ₗ[R] M₁
h :
  ∀ (P : Ideal R) [inst : P.IsMaximal],
    (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g = (IsLocalizedModule.map P.primeCompl (f P) (f₁ P)) g'
x : M
P : Ideal R
x✝ : P.IsMaximal
⊢ (f₁ P) (g x) = (f₁ P) (g' x)

Tactic:
by
    simpa only [IsLocalizedModule.map_apply] using DFunLike.congr_fun (h P) (f P x)

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
by
    obtain ⟨m, hm⟩ := h' y
    have := IsLocalization.map_units S ⟨_, hm⟩
    rw [map_mul] at this
    exact (IsUnit.mul_iff.mp this).2

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

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
    (∀ (s : Set a), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e ↑r)) → P e) ↔
      ∀ (s : Finset a), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e ↑r)) → P e

Tactic:
intros

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set a✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P (Localization.awayMap e✝ ↑r)) → P e✝) ↔
    ∀ (s : Finset a✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P (Localization.awayMap e✝ ↑r)) → P e✝
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ ∀ (a b : Type u) (c : CommRing a) (d : CommRing b) (e : a →+* b),
    (∀ (s : Set b), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e) ↔
      ∀ (s : Finset b), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b (Localization.Away ↑r)).comp e)) → P e

Tactic:
intros

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
a✝ b✝ : Type u
c✝ : CommRing a✝
d✝ : CommRing b✝
e✝ : a✝ →+* b✝
⊢ (∀ (s : Set b✝), Ideal.span s = ⊤ → (∀ (r : ↑s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝) ↔
    ∀ (s : Finset b✝), Ideal.span ↑s = ⊤ → (∀ (r : ↥s), P ((algebraMap b✝ (Localization.Away ↑r)).comp e✝)) → P e✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ x ∈ p.coeff.support, AddMonoidAlgebra.single x (p.coeff x)).coeff a

Tactic:
simp only [AddMonoidAlgebra.coeff_sum, coeff_single]

Goal state after:
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (C a * T ↑n) → M (C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (C a * T (-↑n)) → M (C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n ∈ s, C (p.coeff n) * T n)
a : ℤ
⊢ p.coeff a = (∑ i ∈ p.coeff.support, Finsupp.single i (p.coeff i)) a
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (x y : n → α), A.cramerMap (x + y) = A.cramerMap x + A.cramerMap y

Tactic:
intros

Goal state after:
case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
x✝ y✝ : n → α
⊢ A.cramerMap (x✝ + y✝) = A.cramerMap x✝ + A.cramerMap y✝
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ ∀ (c : α) (x : n → α), A.cramerMap (c • x) = c • A.cramerMap x

Tactic:
intros

Goal state after:
case map_smul
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
⊢ A.cramerMap (c✝ • x✝) = c✝ • A.cramerMap x✝
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
h : a = 0
⊢ (C a * T n).degree = ⊥

Tactic:
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne,
      not_false_iff]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
h : ¬a = 0
⊢ (C a * T n).degree = ↑n

Tactic:
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne,
      not_false_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a).degree = 0

Tactic:
rw [← mul_one (C a), ← T_zero]

Goal state after:
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ (C a * T 0).degree = 0
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c : R
⊢ (transvection i j c).det = 1

Tactic:
by
  rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ ↑n ≤ Module.rank R R

Tactic:
suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by
    simpa using this.cardinal_lift_le_rank

Goal state after:
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsDomain R
r : R
s : ↥R⁰
h : ∀ (r' : R) (s' : ↥R⁰), ↑s' * r ≠ r' * ↑s
n : ℕ
⊢ LinearIndependent R fun i ↦ r * ↑s ^ ↑i
Module: Mathlib.RingTheory.MatrixAlgebra

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ ∀ (a₁ a₂ : A) (b₁ b₂ : Matrix n n R),
    (toFunLinear n R A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      (toFunLinear n R A) (a₁ ⊗ₜ[R] b₁) * (toFunLinear n R A) (a₂ ⊗ₜ[R] b₂)

Tactic:
intros

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a₁✝ a₂✝ : A
b₁✝ b₂✝ : Matrix n n R
⊢ (toFunLinear n R A) ((a₁✝ * a₂✝) ⊗ₜ[R] (b₁✝ * b₂✝)) =
    (toFunLinear n R A) (a₁✝ ⊗ₜ[R] b₁✝) * (toFunLinear n R A) (a₂✝ ⊗ₜ[R] b₂✝)
Module: Mathlib.LinearAlgebra.Matrix.SchurComplement

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (fromBlocks 1 (-A) B 1).det = (1 + B * A).det

Tactic:
rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]

Goal state after: