mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ (lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b))) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b) =
    E.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)

Tactic:
congr 1

Goal state after:
case right.e_a
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ lift E ≫ K.π.app (WalkingMulticospan.left (J.fst b)) = E.π.app (WalkingMulticospan.left (J.fst b))
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f

Tactic:
suffices ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
        F.map' i j ≫ app _ = app _ ≫ G.map' i j by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      have hij' := leOfHom hij
      simp only [Fin.mk_le_mk] at hij'
      obtain ⟨k, hk⟩ := Nat.le.dest hij'
      exact this k i j hk (by valid)
    intro k
    induction k with intro i j hj hj'
    | zero =>
      simp only [add_zero] at hj
      obtain rfl := hj
      rw [F.map'_self i, G.map'_self i, id_comp, comp_id]
    | succ k hk =>
      rw [← add_assoc] at hj
      subst hj
      rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]

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

Goal state before:
pp: case left
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
a : J.L
⊢ I.multispan.map (WalkingMultispan.Hom.fst a) ≫ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S =
    I.multispan.map (WalkingMultispan.Hom.fst a) ≫ S.ι.app (WalkingMultispan.right (J.fst a))

Tactic:
congr 1

Goal state after:
case e_a
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
a : J.L
⊢ K.ι.app (WalkingMultispan.right (J.fst a)) ≫ desc S = S.ι.app (WalkingMultispan.right (J.fst a))
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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A) =
    f ≫ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.a

Tactic:
congr 1

Goal state after:
case e_a
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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ adj.unit.app (G.obj A.A) =
    equalizer.ι (G.map A.a) (adj.unit.app (G.1 A.A)) ≫ G.map A.a
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
| one =>

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

Goal state before:
pp: case one
C : Type u
inst✝ : Category.{v, u} C
⊢ IsConnected (StructuredArrow WalkingReflexivePair.one inclusionWalkingReflexivePair)

Tactic:
| one =>

Goal state after:
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✝
J : Type u
inst✝ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
s : Cocone D
j : J
⊢ (D.obj j).a ≫ T.map ((T.forget.mapCocone s).ι.app j) = T.forget.map (s.ι.app j) ≫ s.pt.a

Tactic:
apply (s.ι.app j).h

Goal state after:
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
J : Type u
inst✝³ : Category.{v, u} J
R : D ⥤ C
K : J ⥤ D
inst✝² : ComonadicLeftAdjoint R
inst✝¹ : PreservesLimit (K ⋙ R) (comonadicRightAdjoint R ⋙ R)
inst✝ : PreservesLimit ((K ⋙ R) ⋙ comonadicRightAdjoint R ⋙ R) (comonadicRightAdjoint R ⋙ R)
A : D ⥤ (comonadicAdjunction R).toComonad.Coalgebra := Comonad.comparison (comonadicAdjunction R)
B : (comonadicAdjunction R).toComonad.Coalgebra ⥤ C := (comonadicAdjunction R).toComonad.forget
i : (K ⋙ Comonad.comparison (comonadicAdjunction R)) ⋙ (comonadicAdjunction R).toComonad.forget ≅ K ⋙ R :=
  K.associator (Comonad.comparison (comonadicAdjunction R)) (comonadicAdjunction R).toComonad.forget ≪≫
    K.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction R))
⊢ PreservesLimit ((K ⋙ A) ⋙ (comonadicAdjunction R).toComonad.forget) (comonadicRightAdjoint R ⋙ R)

Tactic:
exact preservesLimit_of_iso_diagram _ i.symm

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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
σ : M
hσ : σ ∈ inertia M P
x : R
⊢ x ∈ σ • P ↔ x ∈ P

Tactic:
Ideal.mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
M : Type u_1
inst✝² : Group M
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
σ : M
hσ : σ ∈ inertia M P
x : R
⊢ σ⁻¹ • x ∈ P ↔ x ∈ P
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
⊢ (inertia (↥(MulAction.stabilizer M P)) P).Normal

Tactic:
refine (Subgroup.normal_subgroupOf_iff (inertia_le_stabilizer P)).mpr fun g s hg hs x ↦ ?_

Goal state after:
M : Type u_1
N : Type u_2
R✝ : Type u_3
inst✝⁴ : Group M
inst✝³ : Semiring R✝
inst✝² : MulSemiringAction M R✝
R : Type u_4
inst✝¹ : Ring R
P : Ideal R
inst✝ : MulSemiringAction M R
g s : M
hg : g ∈ inertia M P
hs : s ∈ MulAction.stabilizer M P
x : R
⊢ (s * g * s⁻¹) • x - x ∈ Submodule.toAddSubgroup P
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))
⊢ comap (algebraMap R S) P = p

Tactic:
ext x
  rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← Quotient.eq_zero_iff_mem, Quotient.mk_algebraMap,
    IsScalarTower.algebraMap_apply R (R ⧸ p) (S ⧸ P), Quotient.algebraMap_eq]
  exact map_eq_zero_iff _ h

Goal state after:
Module: Mathlib.RingTheory.IsPrimary

Goal state before:
pp: case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
⊢ (f a ⊓ s.inf f).IsPrimary

Tactic:
have H ⦃x⦄ (hx : x ∈ s) : ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical := by
      rw [hs' (mem_insert_of_mem hx), hs' (mem_insert_of_mem hy)]

Goal state after:
case insert.inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_3
f : ι → Submodule R M
a : ι
s : Finset ι
ha : a ∉ s
IH :
  ∀ {i : ι},
    i ∈ s →
      (∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) →
        (∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) → (s.inf f).IsPrimary
i : ι
hi : i ∈ insert a s
hs : ∀ ⦃y : ι⦄, y ∈ insert a s → (f y).IsPrimary
hs' : ∀ ⦃y : ι⦄, y ∈ insert a s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical
y : ι
hy : y ∈ s
H : ∀ ⦃x : ι⦄, x ∈ s → ((f x).colon Set.univ).radical = ((f y).colon Set.univ).radical
⊢ (f a ⊓ s.inf f).IsPrimary
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
⊢ (∀ ⦃x : R⦄, x ∈ nilradical R → x ∈ ⊥) ↔ IsReduced R

Tactic:
Submodule.mem_bot,

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
⊢ (∀ ⦃x : R⦄, x ∈ nilradical R → x = 0) ↔ IsReduced R
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_2
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
P : Type u_5
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
Q : Type u_6
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x : N
⊢ (∃ m, g m = 0 ∧ ∃ s, mk' f m s = x) → ((IsLocalizedModule.map p f f') g) x = 0

Tactic:
· rintro ⟨m, hm, a, ha, rfl⟩
    simp [IsLocalizedModule.map_mk', hm]

Goal state after:
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 : ↥P.primeCompl
e : IsLocalizedModule.mk' (f P) a s = (f P) m
⊢ False

Tactic:
rw [← IsLocalizedModule.mk'_one P.primeCompl, IsLocalizedModule.mk'_eq_mk'_iff] at e

Goal state after:
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 : ↥P.primeCompl
e : ∃ s_1, s_1 • s • m = s_1 • 1 • a
⊢ False
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mp.refine_1
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
h : J.IsPrime
⊢ Ideal.under R J ≠ ⊤

Tactic:
refine fun hJ => h.ne_top ?_
      rw [eq_top_iff, ← (orderEmbedding M S).le_iff_le]
      exact le_of_eq hJ.symm

Goal state after:
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
s : Set R
span_eq : span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
x y : M
h : ∀ (r : ↑s), (f r) x = (f r) y
this : eqIdeal R x y = ⊤
⊢ x = y

Tactic:
simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this

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

Goal state before:
pp: case hx
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
y : R
hy : y ∈ ↑I
hny : y ∈ ↑M
⊢ ?x ∈ Ideal.map (algebraMap R S) I

Tactic:
exact Ideal.mem_map_of_mem (algebraMap R _) hy

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

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
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
y : ↥(localizationLocalizationSubmodule M N)
y' : ↥N
z : ↥M
eq : (algebraMap R S) ↑y = ↑y' * (algebraMap R S) ↑z
⊢ IsUnit ((algebraMap S T) ↑y') ∧ IsUnit ((algebraMap S T) ((algebraMap R S) ↑z))

Tactic:
exact ⟨IsLocalization.map_units T y', (IsLocalization.map_units _ z).map (algebraMap S T)⟩

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
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
⊢ ∀ (y : ↥(Submonoid.map (algebraMap R S) N)), IsUnit ((algebraMap S T) ↑y)

Tactic:
rintro ⟨_, ⟨y, hy, rfl⟩⟩

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
M N : Submonoid R
h : M ≤ N
inst✝³ : IsLocalization M S
inst✝² : IsLocalization N T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
y : R
hy : y ∈ ↑N
⊢ IsUnit ((algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩)
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹² : CommRing R
inst✝¹¹ : CommRing A
inst✝¹⁰ : Algebra R A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R B
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module B N
inst✝ : IsScalarTower R B N
n : Submodule B N
m : A
x y : M ⊗[R] (N ⧸ n)
hx :
  (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • x) =
    (RingHom.id A) m • (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) x
hy :
  (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • y) =
    (RingHom.id A) m • (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) y
⊢ (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (m • (x + y)) =
    (RingHom.id A) m • (TensorProduct.tensorQuotientEquiv M (Submodule.restrictScalars R n)) (x + y)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: case mp.refine_3
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y + mk' S 1 z' • y' =
    (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y + (mk' S 1 (z * z') * (algebraMap R S) ↑z) • y'

Tactic:
congr 1

Goal state after:
case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z • y = (mk' S 1 (z * z') * (algebraMap R S) ↑z') • y

case mp.refine_3.e_a
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
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
x : N
a : Set N
h : x ∈ Submodule.span S a
y : N
hy : y ∈ Submodule.span R a
z : ↥M
hx✝ : mk' S 1 z • y ∈ Submodule.span S a
y' : N
hy' : y' ∈ Submodule.span R a
z' : ↥M
hy✝ : mk' S 1 z' • y' ∈ Submodule.span S a
⊢ mk' S 1 z' • y' = (mk' S 1 (z * z') * (algebraMap R S) ↑z) • y'
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
h₁ : EssFiniteType R S
h₂ : EssFiniteType S T
⊢ EssFiniteType R T

Tactic:
rw [essFiniteType_iff] at h₁ h₂ ⊢
  classical
  obtain ⟨s, hs⟩ := h₁
  obtain ⟨t, ht⟩ := h₂
  use s.image (IsScalarTower.toAlgHom R S T) ∪ t
  simp only [Finset.coe_union, Finset.coe_image, Algebra.adjoin_union, Algebra.adjoin_image]
  intro x
  obtain ⟨y, hy₁, hy₂, hy₃⟩ := ht x
  obtain ⟨t₁, h₁, h₂, h₃⟩ := EssFiniteType.aux _ _ _ _ hs _ y hy₁
  obtain ⟨t₂, h₄, h₅, h₆⟩ := EssFiniteType.aux _ _ _ _ hs _ _ hy₃
  refine ⟨t₂ • t₁ • y, ?_, ?_, ?_⟩
  · rw [Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₄, rfl⟩) h₃
  · rw [Algebra.smul_def, Algebra.smul_def]
    exact (h₅.map _).mul ((h₂.map _).mul hy₂)
  · rw [← mul_smul, mul_comm, smul_mul_assoc, mul_comm, mul_comm y, mul_smul, Algebra.smul_def]
    exact mul_mem (Algebra.mem_sup_left ⟨_, h₁, rfl⟩) h₆

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: case h.add
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : CommRing T
inst✝³ : Algebra R S
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Finset S
hσ : ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
x y : T ⊗[R] S
hx :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ x * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
hy :
  ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ y * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)
⊢ ∃ t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ),
    IsUnit t ∧ (x + y) * t ∈ adjoin T ↑(Finset.image (⇑TensorProduct.includeRight) σ)

Tactic:
| add x y hx hy =>

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
h : ∀ (J : Ideal R) (x : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥
P : Ideal R
hP : P.IsMaximal
⊢ Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) ⊥

Tactic:
by simpa using h P hP

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
⊢ A.IsSymm

Tactic:
rw [← neg_neg A]

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : InvolutiveNeg α
A : Matrix n n α
h : (-A).IsSymm
⊢ (- -A).IsSymm
Module: Mathlib.LinearAlgebra.Matrix.MvPolynomial

Goal state before:
pp: m : Type u_1
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing R
s : m × m → R
⊢ ((MvPolynomial.eval s).mapMatrix (mvPolynomialX m m R)).det = (of fun i j ↦ s (i, j)).det

Tactic:
congr 1

Goal state after:
m : Type u_1
R : Type u_3
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing R
s : m × m → R
⊢ (MvPolynomial.eval s).mapMatrix (mvPolynomialX m m R) = of fun i j ↦ s (i, j)
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ↑↑(sign σ) * ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 =
    ↑↑(sign σ) * ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1

Tactic:
congr 1

Goal state after:
case e_a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
σ : Perm n
a✝ : σ ∈ univ
⊢ ∏ i_1, A.updateRow i (Pi.single j 1) (σ i_1) i_1 = ∏ i_1, A.updateCol j (Pi.single i 1) (σ i_1) i_1
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: case e_a.e_a.e_a
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * A))) = V - ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * (U * (C * V)))))

Tactic:
rw [eq_sub_iff_add_eq, ← Matrix.mul_add]

Goal state after:
case e_a.e_a.e_a
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝¹ : Invertible A
inst✝ : Invertible (C + C * V * ⅟A * U * C)
⊢ ⅟(C + C * V * ⅟A * U * C) * (C * (V * (⅟A * A)) + C * (V * (⅟A * (U * (C * V))))) = V
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : n' = i
⊢ (M * (List.take n (listTransvecRow M)).prod *
        transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
      (inr ()) (inl i) =
    if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0

Tactic:
have hni : n = i := by
        cases i
        simp only [n', Fin.mk_eq_mk] at h
        simp only [h]

Goal state after:
case pos
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
n : ℕ
IH : n ≤ r → (M * (List.take n (listTransvecRow M)).prod) (inr ()) (inl i) = if n ≤ ↑i then M (inr ()) (inl i) else 0
hk : n + 1 ≤ r
hnr : n < r
n' : Fin r := ⟨n, hnr⟩
A : (listTransvecRow M)[n]? = some (transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
h : n' = i
hni : n = ↑i
⊢ (M * (List.take n (listTransvecRow M)).prod *
        transvection (inr ()) (inl n') (-M (inr ()) (inl n') / M (inr ()) (inr ())))
      (inr ()) (inl i) =
    if n + 1 ≤ ↑i then M (inr ()) (inl i) else 0
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ B * B⁻¹ = 1

Tactic:
refine mul_nonsing_inv _ ?_

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A B : Matrix n n α
h : A⁻¹ = B⁻¹
h' : IsUnit A.det
⊢ IsUnit B.det