mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A B : Matrix n n R
s : Finset n
⊢ ∀ (c : n → R), (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det

Tactic:
induction s using Finset.induction_on generalizing B with

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

Goal state before:
pp: case intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : IsCofilteredOrEmpty C
I : Type u_1
inst✝ : Finite I
i : C
j : I → C
f : (x : I) → j x ⟶ i
this : IsCofiltered C
val✝ : Fintype I
k : C
fk : {X : C} → X ∈ insert i (Finset.image j Finset.univ) → (k ⟶ X)
hk :
  ∀ {X Y : C} (mX : X ∈ insert i (Finset.image j Finset.univ)) (mY : Y ∈ insert i (Finset.image j Finset.univ))
    {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j x, ⟨i, ⟨⋯, ⟨⋯, f x⟩⟩⟩⟩) Finset.univ → fk mX ≫ f_1 = fk mY
⊢ ∃ k fki g, ∀ (x : I), g x ≫ f x = fki

Tactic:
exact ⟨k, _, _, fun x ↦ hk _ _ (Finset.mem_image_of_mem _ (Finset.mem_univ _))⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
j : J
x : F.obj j
j' : J
y : F.obj j'
⊢ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩ → FilteredColimit.Rel F ⟨j, x⟩ ⟨j', y⟩

Tactic:
· rw [← (FilteredColimit.rel_equiv F).eqvGen_iff]
    exact Relation.EqvGen.mono (rel_of_colimitTypeRel F) _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

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

Tactic:
rw [← det_transpose, det_succ_row _ j]

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
j : Fin n.succ
⊢ ∑ j_1, (-1) ^ (↑j + ↑j_1) * Aᵀ j j_1 * (Aᵀ.submatrix j.succAbove j_1.succAbove).det =
    ∑ i, (-1) ^ (↑i + ↑j) * A i j * (A.submatrix i.succAbove j.succAbove).det
Module: Mathlib.Algebra.Category.Grp.Limits

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom { toFun := fun g ↦ ⟨(ConcreteCategory.hom (kernel.ι f)) g, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ } ≫
      kernel.lift f (ofHom (Hom.hom f).ker.subtype) ⋯ =
    𝟙 (kernel f)

Tactic:
refine equalizer.hom_ext ?_
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z ≫ (α_ (W ⊗ X) Y Z).hom = W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv

Tactic:
rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]
  simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
M N : SemimoduleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f

Tactic:
ext : 1
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
  apply TensorProduct.ext
  ext
  simp [tensorHom, tensorObj, leftUnitor]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y : C
T : D
⊢ δ F X Y ▷ T ≫ μ F X Y ▷ T = 𝟙 (F.obj (X ⊗ Y) ⊗ T)

Tactic:
by
  rw [← MonoidalCategory.comp_whiskerRight, δ_μ, id_whiskerRight]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: case h₂
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F✝ F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.Monoidal
inst✝ : G.Monoidal
x✝¹ x✝ : C
⊢ (μ (F.prod' G) x✝¹ x✝ ≫ δ (F.prod' G) x✝¹ x✝).2 = (𝟙 ((F.prod' G).obj x✝¹ ⊗ (F.prod' G).obj x✝)).2

Tactic:
simp only [CategoryTheory.prod_comp_snd, prod'_μ_snd, prod'_δ_snd, μ_δ,
        prod'_obj, prodMonoidal_tensorObj, prod_id]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : MorphismProperty.bijective C f
hg : MorphismProperty.bijective C g
⊢ MorphismProperty.bijective C (f ≫ g)

Tactic:
delta MorphismProperty.bijective
    rw [hom_comp]
    exact hg.comp hf

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst✝¹ : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst✝ : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
⊢ (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op =
    (pullbackIsoOpPushout g₁.op g₂.op).inv ≫
      pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯ ≫ (pullbackIsoOpPushout f₁.op f₂.op).hom

Tactic:
by
  rw [← Category.assoc, ← Iso.comp_inv_eq]
  ext <;> simp [← op_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.trans e').toAdjunction.IsMonoidal

Tactic:
trans_toAdjunction

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.toAdjunction.comp e'.toAdjunction).IsMonoidal
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.trans e').toAdjunction.IsMonoidal

Tactic:
rw [trans_toAdjunction]

Goal state after:
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
inst✝¹¹ : MonoidalCategory C
D : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D
inst✝⁹ : MonoidalCategory D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
inst✝⁷ : MonoidalCategory E
C' : Type u₁'
inst✝⁶ : Category.{v₁', u₁'} C'
e : C ≌ D
inst✝⁵ : e.functor.Monoidal
inst✝⁴ : e.inverse.Monoidal
inst✝³ : e.IsMonoidal
e' : D ≌ E
inst✝² : e'.functor.Monoidal
inst✝¹ : e'.inverse.Monoidal
inst✝ : e'.IsMonoidal
⊢ (e.toAdjunction.comp e'.toAdjunction).IsMonoidal
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ ((F.obj j).smul r + (F.obj j).smul s) ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } +
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ })

Tactic:
Preadditive.add_comp,

Goal state after:
R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ (F.obj j).smul r ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j +
      (F.obj j).smul s ≫ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } +
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ })
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ((ι (F ⋙ uliftFunctor) j) { down := a }) =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Tactic:
Quot.ι_desc

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)) { down := a } =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((lift R) f) ((ι R) x) = f x

Tactic:
conv_rhs => rw [← ι_comp_lift f]

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((lift R) f) ((ι R) x) = (((lift R) f).toLinearMap ∘ₗ ι R) x
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module Rᵐᵒᵖ M
x₁ x₂ x₃ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (x₁.1 + x₂.1) •> x₃.2 + (x₁.2 + x₂.2) <• x₃.1 = x₁.1 •> x₃.2 + x₁.2 <• x₃.1 + (x₂.1 •> x₃.2 + x₂.2 <• x₃.1)

Tactic:
simp_rw [add_smul, smul_add, add_add_add_comm]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
⊢ (TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A comul) (comul a)) = (LinearMap.rTensor A comul) (comul a)

Tactic:
rw [(TensorProduct.assoc R A A A).symm_apply_eq, coassoc_apply a]

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

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
⊢ ↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ rTensor ((i : n) → A i) comul ∘ₗ comul =
    lTensor ((i : n) → A i) comul ∘ₗ comul

Tactic:
by
    ext : 1
    simp_rw [comp_assoc, comul_comp_single, ← comp_assoc, lTensor_comp_map, comul_comp_single,
      comp_assoc, ← comp_assoc comul, rTensor_comp_map, comul_comp_single, ← map_comp_rTensor,
      ← map_comp_lTensor, comp_assoc, ← coassoc, ← comp_assoc comul, ← comp_assoc,
      map_map_comp_assoc_eq]

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ f : A →ₐc[R] B
f' : A → B
h : f' = ⇑f
⊢ ((↑f).copy f' h).toFun 1 = 1

Tactic:
by simp_all

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * b + b * a = 0

Tactic:
by
  have : a + b = a + b + (a * b + b * a) :=
    calc
      a + b = (a + b) * (a + b) := by rw [mul_self]
      _ = a * a + a * b + (b * a + b * b) := by rw [add_mul, mul_add, mul_add]
      _ = a + a * b + (b * a + b) := by simp only [mul_self]
      _ = a + b + (a * b + b * a) := by abel
  rwa [left_eq_add] at this

Goal state after:
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ (a + b + a * b) * (a + c + a * c) + (a + b * c + a * (b * c)) +
      (a + b + a * b) * (a + c + a * c) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)

Tactic:
le_sup_inf_aux,

Goal state after:
α : Type u_1
inst✝ : BooleanRing α
a b c : α
⊢ a + b * c + a * (b * c) + (a + b * c + a * (b * c)) + (a + b * c + a * (b * c)) * (a + b * c + a * (b * c)) =
    a + b * c + a * (b * c)
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (g (n • x))

Tactic:
rw [g.map_nsmul]

Goal state after:
M : Type u_1
inst✝⁵ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝⁴ : CommMonoid N
P : Type u_3
inst✝³ : CommMonoid P
A : Type u_4
inst✝² : AddCommMonoid A
x : A
B : Type u_5
inst✝¹ : AddCommMonoid B
F : AwayMap x B
C : Type u_6
inst✝ : AddCommMonoid C
g : A →+ C
hg : IsAddUnit (g x)
y : ↥(multiples x)
n : ℕ
hn : (fun i ↦ i • x) n = ↑y
⊢ IsAddUnit (n • g x)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
p : (x : R) → x ∈ span s → Prop
mem : ∀ (x : R) (h : x ∈ s), p x ⋯
zero : p 0 ⋯
add : ∀ (x y : R) (hx : x ∈ span s) (hy : y ∈ span s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : R) (hx : x ∈ span s), p x hx → p (-x) ⋯
left_absorb : ∀ (a x : R) (hx : x ∈ span s), p x hx → p (a * x) ⋯
right_absorb : ∀ (b x : R) (hx : x ∈ span s), p x hx → p (x * b) ⋯
x✝ : R
hx✝ : x✝ ∈ span s
J : TwoSidedIdeal R := mk' {x | ∃ (hx : x ∈ span s), p x hx} ⋯ ⋯ ⋯ ⋯ ⋯
x : R
hx : x ∈ s
⊢ p (x - 0) ⋯

Tactic:
by simp_all

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
x✝ : z ∈ span s
x : R
hx : x ∈ s
⊢ x ∈ univ * s * univ

pp: case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
hz : z ∈ span (univ * s * univ)
⊢ z ∈ span s

Tactic:
· exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩

Goal state after:
case refine_2
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
hz : z ∈ span (univ * s * univ)
⊢ z ∈ span s
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : Ring S
inst✝ : Nontrivial S
f : R →+* S
hf : Function.Surjective ⇑f
⊢ ∀ (a : S), IsUnit a ∨ IsUnit (1 - a)

Tactic:
by
    intro b
    obtain ⟨a, rfl⟩ := hf b
    apply (isUnit_or_isUnit_one_sub_self a).imp <| RingHom.isUnit_map _
    rw [← f.map_one, ← f.map_sub]
    apply f.isUnit_map

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
⊢ ∀ ⦃I_1 : Ideal R⦄, I_1 ∈ {J | I ≤ J ∧ J.IsMaximal} → x * r ∈ I_1

Tactic:
intro 𝔪 𝔪_mem

Goal state after:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Ring S
I✝ I : Ideal R
inst✝ : I.IsTwoSided
x r : R
xJ : x ∈ I.jacobson
𝔪 : Ideal R
𝔪_mem : 𝔪 ∈ {J | I ≤ J ∧ J.IsMaximal}
⊢ x * r ∈ 𝔪
Module: Mathlib.RingTheory.LocalRing.RingHom.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : IsLocalRing S
f : R →+* S
inst✝ : IsLocalHom f
a b : R
h : a + b = 1
⊢ f a + f b = 1

Tactic:
rw [← map_add, h, map_one]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rcases le_or_gt 0 m with hm | hm

Goal state after:
case inl.inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

case inl.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : 0 ≤ n
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

Tactic:
rcases le_or_gt 0 m with hm | hm

Goal state after:
case inr.inl
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : 0 ≤ m
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m

case inr.inr
R : Type u_1
inst✝³ : CommSemiring R
x : R
B : Type u_2
inst✝² : CommSemiring B
inst✝¹ : Algebra R B
inst✝ : IsLocalization.Away x B
n m : ℤ
hn : n < 0
hm : m < 0
⊢ selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
c : BinaryFan X Y
hc : IsLimit c
T : C
hT : IsTerminal T
s :
  PullbackCone (hT.from ((pair X Y).obj { as := WalkingPair.left }))
    (hT.from ((pair X Y).obj { as := WalkingPair.right }))
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
h₁ : m ≫ c.fst = s.fst
h₂ : m ≫ c.snd = s.snd
⊢ m = BinaryFan.IsLimit.lift hc s.fst s.snd

Tactic:
apply BinaryFan.IsLimit.hom_ext hc <;> cat_disch

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ (r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2) • mk m s =
    r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • mk m s

Tactic:
IsLocalization.smul_mk',

Goal state after:
case h
R : Type u
inst✝⁸ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
T : Type u_1
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : IsLocalization S T
T' : Type u_2
inst✝² : CommSemiring T'
inst✝¹ : Algebra R T'
inst✝ : IsLocalization S T'
r : R
x : T
m : M
s : ↥S
⊢ IsLocalization.mk' T (r * (IsLocalization.sec S x).1) (IsLocalization.sec S x).2 • mk m s =
    r • IsLocalization.mk' T (IsLocalization.sec S x).1 (IsLocalization.sec S x).2 • mk m s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : AddCommMonoid M''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x : M'
p : M
s : ↥S
h : (p, s).2 • x = f (p, s).1
⊢ (e.symm p, s).2 • x = (f ∘ₗ ↑e) (e.symm p, s).1

Tactic:
by simpa using h

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
x y : LocalizedModule S M
eq1 : (fromLocalizedModule S f) x = (fromLocalizedModule S f) y
⊢ x = y

Tactic:
induction x with | _ a b
  induction y with | _ a' b'
  simp only [fromLocalizedModule_mk] at eq1
  rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul,
    Module.End.algebraMap_isUnit_inv_apply_eq_iff'] at eq1
  rw [LocalizedModule.mk_eq, ← IsLocalizedModule.eq_iff_exists S f, Submonoid.smul_def,
    Submonoid.smul_def, f.map_smul, f.map_smul, eq1]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case h
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
K : Type u₂
inst✝ : Category.{v₂, u₂} K
hc : IsConnected J
p : Set (ULiftHom (ULift.{u₂, u₁} J))
hj₀ : { down := Classical.choice ⋯ } ∈ p
h : ∀ {j₁ j₂ : ULiftHom (ULift.{u₂, u₁} J)} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
p' : Set J := {j | { down := j } ∈ p}
hj₀' : Classical.choice ⋯ ∈ p'
⊢ { down := j } ∈ p

Tactic:
apply induct_on_objects p' hj₀' fun f => h ((ULiftHomULiftCategory.equiv J).functor.map f)

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsPreconnected J

Tactic:
apply IsPreconnected.of_constant_of_preserves_morphisms
  intro α F hF j j'
  specialize h j j'
  induction h with
  | refl => rfl
  | tail _ hj ih =>
    rw [ih]
    rcases hj with (⟨⟨hj⟩⟩ | ⟨⟨hj⟩⟩)
    exacts [hF hj, (hF hj).symm]

Goal state after: