mathlib-initiative/mathlib-tactics huggingface dataset:
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.OplaxMonoidal
X : C
⊢ δ F X (𝟙_ C) ≫ F.obj X ◁ η F ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv, right_unitality, ← Category.assoc,
    ← F.map_comp, Iso.hom_inv_id, F.map_id, id_comp]

Goal state after:
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)
s : Cocone F
r : R
j : J
⊢ AddCommGrpCat.ofHom ↑(Hom.hom (s.ι.app j)) ≫ s.pt.smul r =
    (F.obj j).smul r ≫ AddCommGrpCat.ofHom ↑(Hom.hom (s.ι.app j))

Tactic:
exact smul_naturality (s.ι.app j) r

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ { toFun := fun d ↦ mapGen ⇑c.mk', invFun := fun d ↦ ⟨d.comap c.mk', ⋯⟩, left_inv := ⋯, right_inv := ⋯ } s ≤
      { toFun := fun d ↦ mapGen ⇑c.mk', invFun := fun d ↦ ⟨d.comap c.mk', ⋯⟩, left_inv := ⋯, right_inv := ⋯ } t ↔
    s ≤ t

Tactic:
simp only [Equiv.coe_fn_mk, le_def, c.mk'_surjective.forall, ← Subtype.coe_le_coe]

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d c : RingCon M
s t : ↑(Set.Ici c)
⊢ (∀ (x x_1 : M), (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1) → (mapGen ⇑c.mk') (c.mk' x) (c.mk' x_1)) ↔
    ∀ {x y : M}, ↑s x y → ↑t x y
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
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
⊢ C a

Tactic:
let of : M →ₗ[R] s := (TensorAlgebra.ι R).codRestrict (Subalgebra.toSubmodule s) ι

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
⊢ C a
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    ((List.take 0 (x.fst :: List.map fst xs)).prod •> x.snd <•
          (List.drop (Nat.succ 0) (x.fst :: List.map fst xs)).prod ::
        List.map
          (fun x_1 ↦
            (List.take (Prod.map id (fun x ↦ x + 1) x_1).2 (x.fst :: List.map fst xs)).prod •>
                (Prod.map id (fun x ↦ x + 1) x_1).1.snd <•
              (List.drop (Prod.map id (fun x ↦ x + 1) x_1).2.succ (x.fst :: List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
Prod.map_snd,

Goal state after:
case cons
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddCommMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
xs : List (tsze R M)
ih :
  xs.prod.snd =
    (List.map (fun x ↦ (List.take x.2 (List.map fst xs)).prod •> x.1.snd <• (List.drop x.2.succ (List.map fst xs)).prod)
        xs.zipIdx).sum
⊢ (x :: xs).prod.snd =
    ((List.take 0 (x.fst :: List.map fst xs)).prod •> x.snd <•
          (List.drop (Nat.succ 0) (x.fst :: List.map fst xs)).prod ::
        List.map
          (fun x_1 ↦
            (List.take (x_1.2 + 1) (x.fst :: List.map fst xs)).prod •> (Prod.map id (fun x ↦ x + 1) x_1).1.snd <•
              (List.drop (x_1.2 + 1).succ (x.fst :: List.map fst xs)).prod)
          xs.zipIdx).sum
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : Coalgebra R B
e : A ≃ B
this✝ : AddCommMonoid A := ⋯
this : Module R A := ⋯
x✝ : A
⊢ (TensorProduct.map LinearMap.id ↑(linearEquiv R e)) ((LinearMap.rTensor A counit ∘ₗ comul) x✝) =
    (TensorProduct.map LinearMap.id ↑(linearEquiv R e)) (((TensorProduct.mk R R A) 1) x✝)

Tactic:
simpa +instances [coalgebraStruct, LinearMap.comp_assoc, TensorProduct.map_map,
        LinearMap.rTensor] using! Coalgebra.rTensor_counit_comul _

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
Y Y' : ModuleCat S
g : Y ⟶ Y'
y : ↑Y
s : S
⊢ ((CoextendScalars.equiv f ((restrictScalars f).obj Y')) ((Hom.hom ((𝟭 (ModuleCat S)).map g ≫ ↟(app' f Y'))) y)) s =
    ((CoextendScalars.equiv f ((restrictScalars f).obj Y'))
        ((Hom.hom (↟(app' f Y) ≫ (restrictScalars f ⋙ coextendScalars f).map g)) y))
      s

Tactic:
simp only [Functor.id_map, Functor.id_obj, Functor.comp_map]
      change s • (g y) = g (s • y)
      rw [map_smul]

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

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

Tactic:
by rw [add_mul, mul_add]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
M' : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
g : P →ₗ[R] M ⊗[R] N
⊢ (α⁻¹ ∘ₗ f ⊗ₘ ρ⁻¹) ∘ₗ g = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ ρ⁻¹) ∘ₗ g

Tactic:
← assoc_symm_comp_map_rid_symm

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
M : C
inst✝ : ComonObj M
Z : C
f : M ⟶ Z
⊢ Δ ≫ (f ⊗ₘ ε) = f ≫ (ρ_ Z).inv

Tactic:
by
  rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc]

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

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
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
x : R
e : IsUnit x
inst✝ : Away x S
⊢ Submonoid.powers x ≤ IsUnit.submonoid R

Tactic:
rwa [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]

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

Goal state before:
pp: case refine_2.inl.inr
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun x1 x2 ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩

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 x y : R
hy : y ∈ univ * (s * univ)
⊢ x * y ∈ univ * (s * univ)

Tactic:
obtain ⟨r, -, y, hy, rfl⟩ := hy

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x r y : R
hy : y ∈ s * univ
⊢ x * (fun x1 x2 ↦ x1 * x2) r y ∈ univ * (s * univ)
Module: Mathlib.RingTheory.LocalRing.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
P : Ideal R
hPunique : ∀ (y : Ideal R), (fun P ↦ P ≠ ⊥ ∧ P.IsPrime) y → y = P
hPnonzero : P ≠ ⊥
hPnot_top : P ≠ ⊤
mem_or_mem'✝ : ∀ {x y : R}, x * y ∈ P → x ∈ P ∨ y ∈ P
⊢ ∀ (b : Ideal R), P < b → b = ⊤

Tactic:
refine Ideal.maximal_of_no_maximal fun M hPM hM => ne_of_lt hPM ?_
        exact (hPunique _ ⟨ne_bot_of_gt hPM, Ideal.IsMaximal.isPrime hM⟩).symm

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : Function.Surjective ⇑(awayMap f (a * b))
⊢ Function.Surjective ⇑(awayMap (awayMap f a) ((algebraMap R (Away a)) b))

Tactic:
rw [awayMap_surjective_iff] at H ⊢

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
S : Type u_2
inst✝ : CommSemiring S
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
⊢ ∀ (a_1 : Away (f a)), ∃ b_1 m, (awayMap f a) b_1 = (awayMap f a) ((algebraMap R (Away a)) b) ^ m * a_1
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: 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

Tactic:
rw [selfZPow_of_neg _ _ hn, selfZPow_of_neg _ _ hm, selfZPow_of_neg _ _ (add_neg hn hm),
      Int.natAbs_add_of_nonpos hn.le hm.le, ← mk'_mul, one_mul]
    congr
    ext
    simp [pow_add]

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

Goal state before:
pp: R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZPow x B (↑m - ↑d) * (algebraMap R B) a = b

Tactic:
← mk'_one (M := Submonoid.powers x) B,

Goal state after:
R : Type u_3
inst✝⁵ : CommRing R
x : R
B : Type u_4
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : IsLocalization.Away x B
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
b : B
hb : b ≠ 0
hx : Irreducible x
a₀ : R
y : ↥(Submonoid.powers x)
d : ℕ
hy : x ^ d = ↑y
ha₀ : a₀ ≠ 0
H : b * (algebraMap R B) (x ^ d) = (algebraMap R B) a₀
m : ℕ
a : R
hyp1 : ¬x ∣ a
hyp2 : a₀ = x ^ m * a
⊢ ¬x ∣ a ∧ selfZPow x B (↑m - ↑d) * mk' B a 1 = b
Module: Mathlib.Algebra.Module.LocalizedModule.IsLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
x : R
s : ↥S
⊢ mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s

Tactic:
by
  rw [← IsLocalizedModule.smul_inj (Algebra.linearMap R A) s, IsLocalizedModule.mk'_cancel']
  exact IsLocalization.smul_mk'_self

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X : C
h₁ h₂ : MonObj X
H : μ = μ
⊢ h₁ = h₂

Tactic:
suffices h₁.one = h₂.one by cases h₁; cases h₂; subst H this; rfl
  trans (λ_ _).inv ≫ (h₁.one ⊗ₘ h₂.one) ≫ h₁.mul
  · simp [tensorHom_def, H, ← unitors_equal]
  · simp [tensorHom_def']

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

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq✝ : f (∑ i ∈ t, fg (Sum.inl i) • v i) = f (∑ i ∈ t, fg (Sum.inr i) • v i)
s : ↥S
eq : ∑ x ∈ t, (↑s * fg (Sum.inl x)) • v x = ∑ x ∈ t, (↑s * fg (Sum.inr x)) • v x
⊢ g₁ i = g₂ i

Tactic:
have := congr(algebraMap R Rₛ $(hv t _ _ eq i hi))

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ g₂ : ι → Rₛ
i : ι
hi : i ∈ t
a : ↥S
fg : ι ⊕ ι → R
hfg :
  (∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inl ↑x)) = ↑a • g₁ ↑x) ∧
    ∀ (x : ↥t), (algebraMap R Rₛ) (fg (Sum.inr ↑x)) = ↑a • g₂ ↑x
eq✝ : f (∑ i ∈ t, fg (Sum.inl i) • v i) = f (∑ i ∈ t, fg (Sum.inr i) • v i)
s : ↥S
eq : ∑ x ∈ t, (↑s * fg (Sum.inl x)) • v x = ∑ x ∈ t, (↑s * fg (Sum.inr x)) • v x
this : (algebraMap R Rₛ) (↑s * fg (Sum.inl i)) = (algebraMap R Rₛ) (↑s * fg (Sum.inr i))
⊢ g₁ i = g₂ i
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
x : M
y : ↥S
⊢ ((map S) f) (mk x y) = mk (f x) y

Tactic:
by
  rw [IsLocalizedModule.mk_eq_mk', IsLocalizedModule.mk_eq_mk']
  exact IsLocalizedModule.map_mk' _ _ _ _ _ _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
⊢ s.fst ≫ g₁ = l₂ ≫ i₂

Tactic:
← hl₂,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
⊢ l₂ ≫ t₂.fst = l₂ ≫ i₂
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = C ↑w
this : X.coeff 1 = if 1 = 0 then w else 0
⊢ 1 = 0

Tactic:
if_neg (one_ne_zero : 1 ≠ 0),

Goal state after:
case neg
α : Type u
p : α
s : Set α
hps : (of p).IsSupported s
this✝ : DecidablePred fun x ↦ x ∈ s
h : p ∉ s
w : ℤ
H : X = C ↑w
this : X.coeff 1 = 0
⊢ 1 = 0
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
hr : r ∈ S
m : M
s : ↥S
n : M
t : ↥S
⊢ r • mk m s = mk n t ↔ mk m s = Localization.mk 1 ⟨r, hr⟩ • mk n t

Tactic:
rw [smul'_mk, mk_smul_mk, one_smul, mk_eq, mk_eq]
      simp only [Subtype.exists, Submonoid.mk_smul, exists_prop]
      fconstructor
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [mul_smul, ← eq1, Submonoid.mk_smul, smul_comm r t]
      · rintro ⟨a, ha, eq1⟩
        refine ⟨a, ha, ?_⟩
        rw [← eq1, mul_comm, mul_smul, Submonoid.mk_smul, Submonoid.smul_def, Submonoid.mk_smul]

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

Goal state before:
pp: 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'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
⊢ ∀ (s_1 s' : ↥S),
    (mk m₁ s_1 + mk m₂ s').liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
      (mk m₁ s_1).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m₂ s').liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯

Tactic:
t₁

Goal state after:
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'
s : ↥S
x y : LocalizedModule S M
m₁ m₂ : M
t₁ : ↥S
⊢ ∀ (s' : ↥S),
    (mk m₁ t₁ + mk m₂ s').liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ =
      (mk m₁ t₁).liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯ + (mk m₂ s').liftOn (fun p ↦ mk p.1 (p.2 * s)) ⋯
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
G : Comonad C
M N : Monad C
f : M.toFunctor ≅ N.toFunctor
f_η : ∀ (X : C), M.η.app X ≫ f.hom.app X = N.η.app X
f_μ : ∀ (X : C), M.μ.app X ≫ f.hom.app X = (M.map (f.hom.app X) ≫ f.hom.app (N.obj X)) ≫ N.μ.app X
X : C
⊢ N.η.app X ≫ f.inv.app X = M.η.app X

Tactic:
by simp [← f_η]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
h1 :
  (ConcreteCategory.hom ⋯.isoPushout.hom) ((algebraMap S (R' ⊗[R] S)) s) =
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) s
h4 :
  ∀ (x : S),
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) ≫ h.isoPushout.inv)) x =
      (ConcreteCategory.hom (ofHom (algebraMap S S'))) x
⊢ (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) s = (algebraMap S S') s

Tactic:
dsimp only [hom_comp, RingHom.coe_comp, Function.comp_apply, hom_ofHom] at h4

Goal state after:
R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
h1 :
  (ConcreteCategory.hom ⋯.isoPushout.hom) ((algebraMap S (R' ⊗[R] S)) s) =
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) s
h4 :
  ∀ (x : S),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap S S') x
⊢ (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) s = (algebraMap S S') s
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ X i = unop Z

Tactic:
← hi

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u_1
X : ι → C
Z : Cᵒᵖ
i : ι
hi : op (X i) = Z
⊢ X i = unop (op (X i))
Module: Mathlib.RingTheory.MvPolynomial.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective ⇑(algebraMap A B)
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = 0 ↔ (aeval x) p = 0

Tactic:
by
  rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
r : J → J → Prop
hr : _root_.Equivalence r
h : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂
⊢ ∀ (j₁ j₂ : J), r j₁ j₂

Tactic:
by
  intro j₁ j₂
  have z : ∀ j : J, r j₁ j :=
    induct_on_objects {k | r j₁ k} (hr.1 j₁)
      fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
  exact z j₂

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Equivalence

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : ObjectProperty C
h : P ≤ Q
⊢ (ιOfLE h).IsEquivalence ↔ Q ≤ P.isoClosure

Tactic:
by
  rw [← essSurj_ιOfLE_iff h]
  exact ⟨fun _ ↦ inferInstance, fun _ ↦ { }⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case left
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝¹ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ P ≤ (P' ⊔ Q').isoClosure

pp: case right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝¹ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ Q ≤ (P' ⊔ Q').isoClosure

Tactic:
· exact hP'.trans (monotone_isoClosure le_sup_left)

Goal state after:
case right
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
P' : ObjectProperty C
w✝¹ : ObjectProperty.Small.{w, v, u} P'
hP' : P ≤ P'.isoClosure
Q' : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q'
hQ' : Q ≤ Q'.isoClosure
⊢ Q ≤ (P' ⊔ Q').isoClosure