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

Goal state before:
pp: case pos
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (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
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : i' = i
⊢ A i' j' = A i j' + 0 * B.updateRow i (A i) k j'

pp: case neg
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (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
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : ¬i' = i
⊢ A i' j' = B i' j' + c i' * B.updateRow i (A i) k j'

Tactic:
· simp [hi'i]

Goal state after:
case neg
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (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
B : Matrix n n R
c : n → R
hs : ∀ i_1 ∉ insert i s, c i_1 = 0
k : n
hk : k ∉ insert i s
A_eq : ∀ (i j : n), A i j = B i j + c i * B k j
hAi : A i = B i + c i • B k
i' j' : n
hi'i : ¬i' = i
⊢ A i' j' = B i' j' + c i' * B.updateRow i (A i) k j'
Module: Mathlib.CategoryTheory.Limits.Preserves.Filtered

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : PreservesCofilteredLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsCofiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ PreservesLimitsOfShape J F

Tactic:
exact preservesLimitsOfShape_of_equiv e F

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

Goal state before:
pp: case fst
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := ⋯
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
k : o
x : n
⊢ ((σ (x, k)).1, k).1 = (σ (x, k)).1

pp: case snd
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := ⋯
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
k : o
x : n
⊢ ((σ (x, k)).1, k).2 = (σ (x, k)).2

Tactic:
· simp only

Goal state after:
case snd
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
R : Type v
inst✝² : CommRing R
o : Type u_3
inst✝¹ : Fintype o
inst✝ : DecidableEq o
M : o → Matrix n n R
preserving_snd : Finset (Perm (n × o)) := ⋯
mem_preserving_snd : ∀ {σ : Perm (n × o)}, σ ∈ preserving_snd ↔ ∀ (x : n × o), (σ x).2 = x.2
σ : n × o ≃ n × o
hσ : ∀ (x : n × o), (σ x).2 = x.2
hσ' : ∀ (x : n × o), (σ.symm x).2 = x.2
k : o
x : n
⊢ ((σ (x, k)).1, k).2 = (σ (x, k)).2
Module: Mathlib.CategoryTheory.Limits.Creates

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ G.mapCone (liftLimit ((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm t)) ≅ c

Tactic:
refine (IsLimit.mapConeEquiv h ?_).uniqueUpToIso t

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
K : J ⥤ C
F G : C ⥤ D
h : F ≅ G
inst✝ : CreatesLimit K F
c : Cone (K ⋙ G)
t : IsLimit c
⊢ IsLimit (F.mapCone (liftLimit ((IsLimit.postcomposeInvEquiv (K.isoWhiskerLeft h) c).symm t)))
Module: Mathlib.Algebra.Category.Grp.ForgetCorepresentable

Goal state before:
pp: G : Type u
inst✝ : AddCommGroup G
x y : G
⊢ (uliftZMultiplesHom G) (x + y) = (uliftZMultiplesHom G) x + (uliftZMultiplesHom G) y

Tactic:
ext
  simp_all only [uliftZMultiplesHom_apply_apply, smul_add, AddMonoidHom.add_apply]

Goal state after:
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:
by
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): it would be nice to do the next two steps by a single `ext`,
    -- but this will require thinking carefully about the relative priorities of `@[ext]` lemmas.
    refine equalizer.hom_ext ?_
    ext
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ IsIso (h.counit.app X) → L.essImage X

pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ L.essImage X → IsIso (h.counit.app X)

Tactic:
· intro
    exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : L.Faithful
inst✝ : L.Full
X : D
⊢ L.essImage X → IsIso (h.counit.app X)
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z)

Tactic:
by
  rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Finite J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
⊢ g = h

Tactic:
by
  apply (cancel_mono (α_ _ _ _).hom).mp
  ext
  simp [w]

Goal state after:
Module: Mathlib.Tactic.CategoryTheory.Monoidal.Normalize

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
α : f ≅ g
β : f' ≅ g'
η : g' ⟶ h
ηs : h ⟶ i
η₁ : g ⊗ g' ⟶ g ⊗ h
ηs₁ : g ⊗ h ⟶ g ⊗ i
η₂ : g ⊗ g' ⟶ g ⊗ i
η₃ : f ⊗ f' ⟶ g ⊗ i
e_η₁ : g ◁ ((Iso.refl g').hom ≫ η ≫ (Iso.refl h).hom) = η₁
e_ηs₁ : g ◁ ηs = ηs₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (α ⊗ᵢ β).hom ≫ η₂ = η₃
⊢ α.hom ⊗ₘ β.hom ≫ η ≫ ηs = η₃

Tactic:
simp_all [MonoidalCategory.tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : HasPushouts C
⊢ HasPullbacks Cᵒᵖ

Tactic:
by
  have : HasColimitsOfShape WalkingCospanᵒᵖ C :=
    hasColimitsOfShape_of_equivalence walkingCospanOpEquiv.symm
  apply hasLimitsOfShape_op_of_hasColimitsOfShape

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

Goal state before:
pp: case e'_2.e'_6
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦f x⟧ = (c.comapQuotientEquivOfSurj ↑f ⋯ hcd) ↑x

Tactic:
rw [comapQuotientEquivOfSurj_mk, RingEquiv.coe_toRingHom]

Goal state after:
case e'_2.e'_6
M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : N ≃+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ ⟦f x⟧ = ↑(f x)
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 (x_1.2 + 1) (x.fst :: List.map fst xs)).prod •> x_1.1.snd <•
              (List.drop (x_1.2 + 1).succ (x.fst :: List.map fst xs)).prod)
          xs.zipIdx).sum

Tactic:
List.take_zero,

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 =
    ([].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 •> x_1.1.snd <•
              (List.drop (x_1.2 + 1).succ (x.fst :: List.map fst xs)).prod)
          xs.zipIdx).sum
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0

Tactic:
· rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
      add_neg_cancel]

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

Goal state before:
pp: case refine_2
S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
x : tsze R M
⊢ inr x.snd ∈ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr)

Tactic:
· exact le_sup_right (α := Subalgebra S _) <| Algebra.subset_adjoin <| Set.mem_range_self x.snd

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

Goal state before:
pp: case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
x✝ : ↑X
⊢ (s₁ + s₂) • (ConcreteCategory.hom g) x✝ = s₁ • (ConcreteCategory.hom g) x✝ + s₂ • (ConcreteCategory.hom g) x✝

Tactic:
← add_smul

Goal state after:
case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
x✝ : ↑X
⊢ (s₁ + s₂) • (ConcreteCategory.hom g) x✝ = (s₁ + s₂) • (ConcreteCategory.hom g) x✝
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x : P
⊢ (_root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P))
      ((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P) (1 ⊗ₜ[R] 1 ⊗ₜ[R] comul x)) =
    comul x

Tactic:
hopf_tensor_induction comul (R := R) x with x₁ x₂

Goal state after:
case tmul
R✝ : Type u_1
S✝ : Type u_2
A : Type u_3
B : Type u_4
inst✝²⁷ : CommSemiring R✝
inst✝²⁶ : CommSemiring S✝
inst✝²⁵ : AddCommMonoid A
inst✝²⁴ : AddCommMonoid B
inst✝²³ : Algebra R✝ S✝
inst✝²² : Module R✝ A
inst✝²¹ : Module S✝ A
inst✝²⁰ : Module R✝ B
inst✝¹⁹ : IsScalarTower R✝ S✝ A
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x x₁ x₂ : P
⊢ (_root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P))
      ((AlgebraTensorModule.tensorTensorTensorComm R R R R R R P P) (1 ⊗ₜ[R] 1 ⊗ₜ[R] (x₁ ⊗ₜ[R] x₂))) =
    x₁ ⊗ₜ[R] x₂
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (a \ b) ≤ c ↔ f a \ f b ≤ c

Tactic:
simp only [← le_map_inv_iff, sdiff_le_iff]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : CoheytingAlgebra α
x✝ : CoheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (f b ⊔ c)
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ f (a \ b) ≤ c ↔ f a \ f b ≤ c

Tactic:
simp only [← le_map_inv_iff, sdiff_le_iff]

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : EquivLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : OrderIsoClass F α β
f : F
a b : α
c : β
⊢ a ≤ b ⊔ EquivLike.inv f c ↔ a ≤ EquivLike.inv f (f b ⊔ c)
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
x : R
inst✝ : Away x S
a b : R
h : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hx : ↑⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩ * a = ↑⟨(fun x_1 ↦ x ^ x_1) n, ⋯⟩ * b
⊢ ∃ n, x ^ n * a = x ^ n * b

Tactic:
use n

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ ∃ n, (r * ↑u) ^ n * a = (r * ↑u) ^ n * b

Tactic:
use n

Goal state after:
case h
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
u : Rˣ
a b : R
hab : (algebraMap R S) a = (algebraMap R S) b
n : ℕ
hn : r ^ n * a = r ^ n * b
⊢ (r * ↑u) ^ n * a = (r * ↑u) ^ n * b
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
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
n : ℕ
⊢ (fun x ↦ r ^ x) n ∈ Submonoid.comap f (Submonoid.powers (f r))

Tactic:
use n

Goal state after:
case h
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
x : R
inst✝⁴ : Away x S
g : R →+* P
Q : Type u_4
inst✝³ : CommSemiring Q
inst✝² : Algebra P Q
f : R →+* P
r : R
inst✝¹ : Away r S
inst✝ : Away (f r) Q
n : ℕ
⊢ (fun x ↦ f r ^ x) n = f ((fun x ↦ r ^ x) n)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x : R
⊢ x ∈ asIdeal I ↔ x ∈ I

Tactic:
by simp [asIdeal]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
M : C
inst✝ : MonObj M
⊢ (tensorμ (𝟙_ C) M (𝟙_ C) M ≫ ((λ_ (𝟙_ C)).hom ⊗ₘ μ)) ≫ (λ_ M).hom = ((λ_ M).hom ⊗ₘ (λ_ M).hom) ≫ μ

Tactic:
rw [← Category.comp_id (λ_ (𝟙_ C)).hom, ← Category.id_comp μ, ← tensorHom_comp_tensorHom]
  simp only [tensorHom_id, id_tensorHom]
  slice_lhs 3 4 => rw [leftUnitor_naturality]
  slice_lhs 1 3 => rw [← leftUnitor_monoidal]
  simp only [Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ fst' ≫ f' = snd' ≫ g'

Tactic:
by
    rw [← cancel_epi e₁.hom, ← reassoc_of% commfst, ← commf,
      ← reassoc_of% commsnd, ← commg, h.w_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
P' X' Y' Z' : C
fst' : P' ⟶ X'
snd' : P' ⟶ Y'
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
e₁ : P ≅ P'
e₂ : X ≅ X'
e₃ : Y ≅ Y'
e₄ : Z ≅ Z'
commfst : fst ≫ e₂.hom = e₁.hom ≫ fst'
commsnd : snd ≫ e₃.hom = e₁.hom ≫ snd'
commf : f ≫ e₄.hom = e₂.hom ≫ f'
commg : g ≫ e₄.hom = e₃.hom ≫ g'
⊢ h.cone.snd =
    e₁.hom ≫ PullbackCone.snd ((Cone.postcompose (cospanExt e₂ e₃ e₄ ⋯ ⋯).inv).obj (PullbackCone.mk fst' snd' ⋯))

Tactic:
change snd = e₁.hom ≫ snd' ≫ e₃.inv
              rw [← reassoc_of% commsnd, e₃.hom_inv_id, Category.comp_id]

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

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
M : Type u_3
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
M' : Type u_4
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M'
inst✝¹³ : Module A M'
inst✝¹² : IsScalarTower R A M'
f : M →ₗ[R] M'
T : Type u_5
B : Type u_6
inst✝¹¹ : CommSemiring T
inst✝¹⁰ : CommSemiring B
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra T B
inst✝⁷ : Algebra R B
inst✝⁶ : Algebra A B
inst✝⁵ : IsScalarTower R T B
inst✝⁴ : IsScalarTower R A B
S : Submonoid A
N : Type u_7
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
g : M →ₗ[A] M'
h : IsLocalizedModule S g
Aₚ : Type u_2 := Localization S
this✝ : Module Aₚ M' := AddEquiv.module Aₚ (iso S g).symm.toAddEquiv
this : IsScalarTower A Aₚ M'
r : R
x : M'
⊢ (algebraMap R Aₚ) r • x = r • x

Tactic:
simp [IsScalarTower.algebraMap_apply R A Aₚ]

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

Goal state before:
pp: case mk
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'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a : A
s : ↥S
⊢ Quot.mk ⇑(OreLocalization.oreEqv S A) (a, s) * 0 = 0

Tactic:
exact mk_eq.mpr ⟨1, by simp only [mul_zero, smul_zero]⟩

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ (map Subtype.val) ((restriction s) (of p) * (restriction s) n) = of p * n

Tactic:
restriction_of,

Goal state after:
case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
p : α
hps : p ∈ s
n : FreeCommRing α
ih : (map Subtype.val) ((restriction s) n) = n
⊢ (map Subtype.val) ((if H : p ∈ s then of ⟨p, H⟩ else 0) * (restriction s) n) = of p * n
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
x : FreeCommRing α
⊢ ∃ a, ↑a = x

Tactic:
induction x with
  | neg_one => use -1; rfl
  | of b => exact ⟨FreeRing.of b, rfl⟩
  | add _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x + y, (FreeRing.lift _).map_add _ _⟩
  | mul _ _ hx hy =>
    rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
    exact ⟨x * y, (FreeRing.lift _).map_mul _ _⟩

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
x y : T
m : M
s : ↥S
⊢ mk
      ((((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
            (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
          ↑s) •
        m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s) =
    mk
      ((((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1) • m +
        (((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) • m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s))

Tactic:
← add_smul

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
x y : T
m : M
s : ↥S
⊢ mk
      ((((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
            (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
          ↑s) •
        m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s) =
    mk
      ((((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
          ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
        m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s))
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} 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
⊢ (monadToFunctor C).mapIso (MonadIso.mk f f_η f_μ) = f

Tactic:
by
  ext
  rfl

Goal state after: