mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ Mono (homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f

Tactic:
refine ⟨fun h A x₂ hx₂ y₁ fac ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : Mono (homologyMap φ)
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ S₁.g = 0
y₁ : A ⟶ S₂.X₁
fac : x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (homologyMap φ)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
      (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom

Tactic:
rw [← cancel_epi ((μIso R X Y).inv ▷ _), ← cancel_epi (μIso R _ _).inv]

Goal state after:
R : Type u
inst✝ : CommRing R
X Y Z : Type u
⊢ (μIso R (X ⊗ Y) Z).inv ≫
      (μIso R X Y).inv ▷ (free R).obj Z ≫
        (μIso R X Y).hom ▷ (free R).obj Z ≫ (μIso R (X ⊗ Y) Z).hom ≫ (free R).map (α_ X Y Z).hom =
    (μIso R (X ⊗ Y) Z).inv ≫
      (μIso R X Y).inv ▷ (free R).obj Z ≫
        (α_ ((free R).obj X) ((free R).obj Y) ((free R).obj Z)).hom ≫
          (free R).obj X ◁ (μIso R Y Z).hom ≫ (μIso R X (Y ⊗ Z)).hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
c : Fan I.left
hc : IsLimit c
d : Fan I.right
hd : IsLimit d
⊢ Fan.IsLimit.lift hc K.ι ≫ I.fstPiMapOfIsLimit c hd = Fan.IsLimit.lift hc K.ι ≫ I.sndPiMapOfIsLimit c hd

Tactic:
apply Fan.IsLimit.hom_ext hd
  simp

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
⊢ K.ι.app (WalkingMultispan.left a) ≫ desc S = S.ι.app (WalkingMultispan.left a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a),
          Category.assoc]

Goal state after:
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))
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ (Monad.comparison (reflectorAdjunction R)).EssSurj

Tactic:
refine ⟨fun X => ⟨(reflector R).obj X.A, ⟨?_⟩⟩⟩

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : (reflectorAdjunction R).toMonad.Algebra
⊢ (Monad.comparison (reflectorAdjunction R)).obj ((reflector R).obj X.A) ≅ X
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: ⊢ ∀ {W X Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
intro _ _ _ _ f g h; cases f <;> cases g <;> cases h <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map (reflexion ≫ left) = 𝟙 (F.obj zero)

Tactic:
reflexion_comp_left,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
⊢ F.map (𝟙 zero) = 𝟙 (F.obj zero)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C (n + 1)
h₀ : F.obj' 0 ⋯ = G.obj' 0 ⋯
h : F.δ₀ = G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ = eqToHom h₀ ≫ G.map' 0 1 homMk₁._proof_4 ⋯ ≫ eqToHom ⋯
this : ∀ (i : Fin (n + 1 + 1)), F.obj i = G.obj i
⊢ F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' (eqToIso h).hom 0 ⋯ = (eqToIso h₀).hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯

Tactic:
rw [w]
      dsimp [app']
      rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id]

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

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective
    (⇑↑(cancelBaseChange R S S M P) ∘
      ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype)))

Tactic:
LinearEquiv.coe_coe,

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : Module S M
inst✝⁴ : IsScalarTower R S M
inst✝³ : Flat R S
inst✝² : Flat S M
P : Type u
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
⊢ Injective
    (⇑(cancelBaseChange R S S M P) ∘ ⇑((AlgebraTensorModule.lTensor S M) ((AlgebraTensorModule.lTensor S S) N.subtype)))
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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (lambda c t ≫ T.δ.app c.pt) ≫ (T.mapCone (T.mapCone c)).π.app j =
    (lambda c t ≫ T.map (lambda c t)) ≫ (T.mapCone (T.mapCone c)).π.app j

Tactic:
rw [Functor.mapCone_π_app, Functor.mapCone_π_app, assoc,
      ← show _ = _ ≫ T.map (T.map _) from T.δ.naturality _, assoc, ← Functor.map_comp, commuting,
      Functor.map_comp, ← assoc, commuting]

Goal state after:
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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
j : J
⊢ (c.π.app j ≫ (D.obj j).a) ≫ T.δ.app ((D ⋙ T.forget).obj j) = lambda c t ≫ T.map (c.π.app j) ≫ T.map (D.obj j).a
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 : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
m : s.pt ⟶ (liftedCone c t).pt
J : ∀ (j : J✝), m ≫ (liftedCone c t).π.app j = s.π.app j
j : J✝
⊢ m.f ≫ c.π.app j = { f := t.lift (T.forget.mapCone s), h := ⋯ }.f ≫ c.π.app j

Tactic:
simpa using congr_arg Coalgebra.Hom.f (J j)

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

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| comap (↑(RingEquiv.symm ((MulSemiringAction.toRingAut G A) g))) (comap (algebraMap A B) P)

Tactic:
comap_comap

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| comap ((algebraMap A B).comp ↑(RingEquiv.symm ((MulSemiringAction.toRingAut G A) g))) P
Module: Mathlib.RingTheory.Ideal.Over

Goal state before:
pp: A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| comap (algebraMap A B) (comap (↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) g))) P)

Tactic:
comap_comap

Goal state after:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : Semiring B
inst✝⁴ : Algebra A B
P : Ideal B
G : Type u_5
inst✝³ : Group G
inst✝² : MulSemiringAction G B
g : G
inst✝¹ : MulSemiringAction G A
inst✝ : SMulDistribClass G A B
| comap ((↑(RingEquiv.symm ((MulSemiringAction.toRingAut G B) g))).comp (algebraMap A B)) P
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
M' M'' : Submodule R M
s : Set (Submodule R M)
⊢ localized' S p f (sSup s) = sSup (localized' S p f '' s)

Tactic:
rw [sSup_eq_iSup', localized'_iSup, sSup_image']

Goal state after:
Module: Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Goal state before:
pp: case pos
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝ : CommRing S
hI : ⊥ ^ n = ⊥
⊢ ⊥ ^ 2 = ⊥

Tactic:
← Ideal.zero_eq_bot,

Goal state after:
case pos
P : ⦃S : Type u_1⦄ → [inst : CommRing S] → Ideal S → Prop
h₁ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I : Ideal S), I ^ 2 = ⊥ → P I
h₂ : ∀ ⦃S : Type u_1⦄ [inst : CommRing S] (I J : Ideal S), I ≤ J → P I → P (map (Quotient.mk I) J) → P J
n : ℕ
H : ∀ m < n, ∀ {S : Type u_1} [inst : CommRing S] (I : Ideal S), I ^ m = ⊥ → P I
S : Type u_1
inst✝ : CommRing S
hI : ⊥ ^ n = ⊥
⊢ 0 ^ 2 = 0
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬p.coeff k = 0
a : A
⊢ (if ¬p.coeff k = 0 then a * (algebraMap R A) (p.coeff k) else 0) = a * (algebraMap R A) (p.coeff k)

Tactic:
by split_ifs <;> simp [*]

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

Goal state before:
pp: R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ ↑R
      ((IsLocalizedModule.mapExtendScalars M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
          (IsScalarTower.toAlgHom R B Bₚ).toLinearMap Rₚ)
        f.toLinearMap) =
    ↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap

Tactic:
apply IsLocalizedModule.linearMap_ext M
    (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
    ((IsScalarTower.toAlgHom R B Bₚ).toLinearMap)

Goal state after:
R : Type u_5
inst✝²¹ : CommSemiring R
M : Submonoid R
A : Type u_6
inst✝²⁰ : CommSemiring A
inst✝¹⁹ : Algebra R A
B : Type u_7
inst✝¹⁸ : CommSemiring B
inst✝¹⁷ : Algebra R B
Rₚ : Type u_8
inst✝¹⁶ : CommSemiring Rₚ
inst✝¹⁵ : Algebra R Rₚ
inst✝¹⁴ : IsLocalization M Rₚ
Aₚ : Type u_9
inst✝¹³ : CommSemiring Aₚ
inst✝¹² : Algebra R Aₚ
inst✝¹¹ : Algebra A Aₚ
inst✝¹⁰ : IsScalarTower R A Aₚ
inst✝⁹ : IsLocalization (algebraMapSubmonoid A M) Aₚ
Bₚ : Type u_10
inst✝⁸ : CommSemiring Bₚ
inst✝⁷ : Algebra R Bₚ
inst✝⁶ : Algebra B Bₚ
inst✝⁵ : IsScalarTower R B Bₚ
inst✝⁴ : IsLocalization (algebraMapSubmonoid B M) Bₚ
inst✝³ : Algebra Rₚ Aₚ
inst✝² : Algebra Rₚ Bₚ
inst✝¹ : IsScalarTower R Rₚ Aₚ
inst✝ : IsScalarTower R Rₚ Bₚ
f : A →ₐ[R] B
⊢ ↑R
        ((IsLocalizedModule.mapExtendScalars M (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
            (IsScalarTower.toAlgHom R B Bₚ).toLinearMap Rₚ)
          f.toLinearMap) ∘ₗ
      (IsScalarTower.toAlgHom R A Aₚ).toLinearMap =
    ↑R (mapₐ M Rₚ Aₚ Bₚ f).toLinearMap ∘ₗ (IsScalarTower.toAlgHom R A Aₚ).toLinearMap
Module: Mathlib.RingTheory.LocalProperties.Exactness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := f.toAlgebra
this✝³ : (r : ↑s) → Algebra R (Sᵣ r) := fun r ↦ ((algebraMap S (Sᵣ r)).comp f).toAlgebra
this✝² : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
this✝¹ : ∀ (r : ↑s), IsLocalization.Away ((algebraMap R S) ↑r) (Sᵣ r)
this✝ : (r : ↑s) → Algebra (Rᵣ r) (Sᵣ r) := fun r ↦ localizationAlgebra (Submonoid.powers ↑r) S
this : ∀ (r : ↑s), IsScalarTower R (Rᵣ r) (Sᵣ r)
⊢ Function.Surjective ⇑f

Tactic:
apply surjective_of_isLocalized_span s hs Rᵣ (fun r : s ↦ Algebra.linearMap _ _) _
    (fun r : s ↦ ((IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)) (Algebra.linearMap R S)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
s : Set R
hs : Ideal.span s = ⊤
Rᵣ : ↑s → Type u_3
inst✝⁵ : (r : ↑s) → CommSemiring (Rᵣ r)
inst✝⁴ : (r : ↑s) → Algebra R (Rᵣ r)
Sᵣ : ↑s → Type u_4
inst✝³ : (r : ↑s) → CommSemiring (Sᵣ r)
inst✝² : (r : ↑s) → Algebra S (Sᵣ r)
f : R →+* S
inst✝¹ : ∀ (r : ↑s), IsLocalization.Away (↑r) (Rᵣ r)
inst✝ : ∀ (r : ↑s), IsLocalization.Away (f ↑r) (Sᵣ r)
h : ∀ (r : ↑s), Function.Surjective ⇑(IsLocalization.Away.map (Rᵣ r) (Sᵣ r) f ↑r)
algInst✝ : Algebra R S := ⋯
this✝³ : (r : ↑s) → Algebra R (Sᵣ r) := ⋯
this✝² : ∀ (r : ↑s), IsScalarTower R S (Sᵣ r)
this✝¹ : ∀ (r : ↑s), IsLocalization.Away ((algebraMap R S) ↑r) (Sᵣ r)
this✝ : (r : ↑s) → Algebra (Rᵣ r) (Sᵣ r) := ⋯
this : ∀ (r : ↑s), IsScalarTower R (Rᵣ r) (Sᵣ r)
⊢ ∀ (r : ↑s),
    Function.Surjective
      ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (Algebra.linearMap R (Rᵣ r))
            (IsScalarTower.toAlgHom R S (Sᵣ r)).toLinearMap)
          (Algebra.linearMap R S))
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
⊢ False

Tactic:
obtain ⟨z, hxyz⟩ := isUnit_iff_exists_inv.1 hu

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Ideal R
hp : P.IsPrime
inst✝ : IsLocalization.AtPrime S P
this : Nontrivial S := nontrivial S P
x y : S
hx : x ∈ nonunits S
hy : y ∈ nonunits S
hu : IsUnit (x + y)
z : S
hxyz : (x + y) * z = 1
⊢ False
Module: Mathlib.RingTheory.TensorProduct.Quotient

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
I : Ideal A
x y : B ⧸ Ideal.map (algebraMap A B) I
⊢ (quotIdealMapEquivTensorQuotAux B I) (x * y) =
    (quotIdealMapEquivTensorQuotAux B I) x * (quotIdealMapEquivTensorQuotAux B I) y

Tactic:
by
      obtain ⟨u, rfl⟩ := Ideal.Quotient.mk_surjective x
      obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective y
      simp_rw [← map_mul, quotIdealMapEquivTensorQuotAux_mk]
      simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₂ : T ⧸ I
b₁ : T
⊢ ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) ((a₁ * a₂) ⊗ₜ[R] ((Ideal.Quotient.mk I) b₁ * b₂)) =
    ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₁ ⊗ₜ[R] (Ideal.Quotient.mk I) b₁) *
      ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₂ ⊗ₜ[R] b₂)

Tactic:
obtain ⟨b₂, rfl⟩ := Ideal.Quotient.mk_surjective b₂

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
I : Ideal T
g : (A ⊗[R] T ⧸ ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range) ≃ₗ[S]
  A ⊗[R] T ⧸ Submodule.restrictScalars S (Ideal.map includeRight I) :=
  ((AlgebraTensorModule.lTensor S A) (↑R (Submodule.subtype I))).range.quotEquivOfEq
    (Submodule.restrictScalars S (Ideal.map includeRight I)) ⋯
a₁ a₂ : A
b₁ b₂ : T
⊢ ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g)
      ((a₁ * a₂) ⊗ₜ[R] ((Ideal.Quotient.mk I) b₁ * (Ideal.Quotient.mk I) b₂)) =
    ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₁ ⊗ₜ[R] (Ideal.Quotient.mk I) b₁) *
      ↑(AlgebraTensorModule.tensorQuotientEquiv S T A I ≪≫ₗ g) (a₂ ⊗ₜ[R] (Ideal.Quotient.mk I) b₂)
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
by
  constructor
  · introv _ _ hf
    exact hPc _ _ (hPl S r) hf
  · introv _ _ hf
    exact hPc _ _ hf (hPl T s)

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
H : LocalizationPreserves P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
hf : P f
⊢ IsLocalization (Submonoid.map f (Submonoid.powers r)) S'

Tactic:
rw [Submonoid.map_powers]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
H : LocalizationPreserves P
R S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
f : R →+* S
r : R
R' S' : Type u
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
hf : P f
⊢ IsLocalization (Submonoid.powers (f r)) S'
Module: Mathlib.RingTheory.LocalProperties.Basic

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.map f (Ideal.span s) = Ideal.map f ⊤
⊢ P f

Tactic:
Ideal.map_span,

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : OfLocalizationSpanTarget P
hP' : StableUnderCompositionWithLocalizationAwaySource P
R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs' : ∀ (r : ↑s), P (Localization.awayMap f ↑r)
hs : Ideal.span (⇑f '' s) = Ideal.map f ⊤
⊢ P f
Module: Mathlib.LinearAlgebra.Matrix.Symmetric

Goal state before:
pp: α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ Matrix.fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D

Tactic:
hA,

Goal state after:
α : Type u_1
n : Type u_3
m : Type u_4
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsSymm
hBC : Bᵀ = C
hD : D.IsSymm
hCB : Cᵀ = B
⊢ Matrix.fromBlocks A Cᵀ Bᵀ Dᵀ = Matrix.fromBlocks A B C D
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (toLaurent ↑⟨(fun x ↦ X ^ x) n, ⋯⟩)

Tactic:
toLaurent_X_pow

Goal state after:
R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
x✝ : ↥(Submonoid.powers X)
n : ℕ
⊢ IsUnit (T ↑n)
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1

Tactic:
by
  induction L with
  | nil => simp
  | cons t L IH =>
    suffices
      t.toMatrix *
            ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) *
          t.inv.toMatrix = 1
      by simpa [Matrix.mul_assoc]
    simp_rw [IH, Matrix.mul_one, t.mul_inv]

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

Goal state before:
pp: n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ fromBlocks M 0 0 N * (List.map (toMatrix ∘ sumInl p) L).prod = fromBlocks (M * (List.map toMatrix L).prod) 0 0 N

Tactic:
induction L generalizing M N with
  | nil => simp
  | cons t L IH => simp [IH, toMatrix_sumInl, fromBlocks_multiply]

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

Goal state before:
pp: α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]

Goal state after:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * (A.submatrix j.succAbove x.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det