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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasColimit (walkingCospanOpEquiv.inverse ⋙ (cospan f g).leftOp) ↔ HasPullback f g

Tactic:
hasColimit_inverse_equivalence_comp_iff,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasColimit (cospan f g).leftOp ↔ HasPullback f g
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
x : TensorAlgebra R M
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι R))

Tactic:
induction x using induction with
  | algebraMap => exact algebraMap_mem _ _
  | add x y hx hy => exact add_mem hx hy
  | mul x y hx hy => exact mul_mem hx hy
  | ι x => exact Algebra.subset_adjoin (Set.mem_range_self _)

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

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

Tactic:
one_smul,

Goal state after:
R : Type u
M : Type v
inst✝³ : Monoid R
inst✝² : AddMonoid M
inst✝¹ : DistribMulAction R M
inst✝ : DistribMulAction Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ x.2 + 0 <• x.1 = x.2
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ x.fst ^ (n.pred - i) •> x.fst ^ i •> x.snd) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd

Tactic:
smul_smul,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ (List.map (fun i ↦ (x.fst ^ (n.pred - i) * x.fst ^ i) •> x.snd) (List.range n)).sum = n •> x.fst ^ n.pred •> x.snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• x.fst ^ i.succ)) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (x.snd <• x.fst ^ x_1 <• x.fst)) (List.range (n✝ + 1))).sum

Tactic:
smul_smul,

Goal state after:
case succ
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
n✝ : ℕ
⊢ x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun i ↦ x.fst ^ (n✝ - i) •> (x.snd <• x.fst ^ i.succ)) (List.range (n✝ + 1))).sum =
    x.fst ^ (n✝ + 1) •> x.snd +
      (List.map (fun x_1 ↦ x.fst ^ (n✝ - x_1) •> (op x.fst * op (x.fst ^ x_1)) •> x.snd) (List.range (n✝ + 1))).sum
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.fst •> xs.prod.snd + x.snd <• xs.prod.fst =
    (1 •> x.snd <• (List.drop (Nat.succ 0) (x.fst :: List.map fst xs)).prod ::
        List.map
          (fun x_1 ↦
            (x.fst * (List.take x_1.2 (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:
one_smul,

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.fst •> xs.prod.snd + x.snd <• xs.prod.fst =
    (x.snd <• (List.drop (Nat.succ 0) (x.fst :: List.map fst xs)).prod ::
        List.map
          (fun x_1 ↦
            (x.fst * (List.take x_1.2 (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 •> x.snd + -(1 •> r •> x.snd) = 0

Tactic:
one_smul,

Goal state after:
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 •> x.snd + -(r •> x.snd) = 0
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
x : tsze R M
r : R
h : x.fst * r = 1
⊢ -(x.fst •> r •> (x.snd <• r)) + x.snd <• r = 0

Tactic:
smul_smul,

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

Tactic:
one_smul,

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

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹) •> a.fst •> b.snd <• (b.fst⁻¹ * a.fst⁻¹) +
        (b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) =
    -(b.fst⁻¹ •> a.fst⁻¹ •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))

Tactic:
smul_smul,

Goal state after:
case h2
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
a b : tsze R M
⊢ -((b.fst⁻¹ * a.fst⁻¹ * a.fst) •> b.snd <• (b.fst⁻¹ * a.fst⁻¹) +
        (b.fst⁻¹ * a.fst⁻¹) •> a.snd <• (b.fst * (b.fst⁻¹ * a.fst⁻¹))) =
    -((b.fst⁻¹ * a.fst⁻¹) •> a.snd <• a.fst⁻¹) + -(b.fst⁻¹ •> b.snd <• (b.fst⁻¹ * a.fst⁻¹))
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹³ : CommSemiring S
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring 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
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s •> 1 •> x.snd = (s •> 1) •> x.snd

Tactic:
one_smul,

Goal state after:
S : Type u_1
R R' : Type u
M : Type v
inst✝¹³ : CommSemiring S
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring 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
inst✝² : Module R' M
inst✝¹ : Module R'ᵐᵒᵖ M
inst✝ : IsCentralScalar R' M
s : S
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ s •> x.snd = (s •> 1) •> x.snd
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
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x : S
⊢ (0 • g) x = 0 x

Tactic:
simp [map_zero]

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

Goal state before:
pp: case e'_2.tmul.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
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₁ • counit x₁ • x₂ ⊗ₜ[R] y₂ = 1 • counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂

Tactic:
one_smul,

Goal state after:
case e'_2.tmul.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
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₁ • counit x₁ • x₂ ⊗ₜ[R] y₂ = counit y₁ • (counit x₁ • x₂) ⊗ₜ[R] y₂
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.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
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₂ • counit x₂ • x₁ ⊗ₜ[R] y₁ = 1 • counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁

Tactic:
one_smul,

Goal state after:
case e'_2.tmul.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
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
x₁ x₂ : A
y₁ y₂ : B
⊢ counit y₂ • counit x₂ • x₁ ⊗ₜ[R] y₁ = counit y₂ • (counit x₂ • x₁) ⊗ₜ[R] y₁
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
⊢ _root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P) ∘ₗ comul =
    comul ∘ₗ ↑(_root_.TensorProduct.lid R P)

Tactic:
by
      ext x
      dsimp
      simp only [one_smul]
      hopf_tensor_induction comul (R := R) x with x₁ x₂
      simp

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

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

Tactic:
rw [mul_self]

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:
rw [mul_self]

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

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

Tactic:
rw [mul_self]

Goal state after:
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✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f g : HeytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
g : HeytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_bot'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊥ = ⊥
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝,
        map_himp' := map_himp'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_bot' := map_bot'✝, map_himp' := map_himp'✝ } = g
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✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f g : CoheytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
g : CoheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_top'✝ : { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun ⊤ = ⊤
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_top' := map_top'✝, map_sdiff' := map_sdiff'✝ } =
    g
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✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f g : BiheytingHom α β
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
g : BiheytingHom α β
toFun✝ : α → β
map_sup'✝ : ∀ (a b : α), toFun✝ (a ⊔ b) = toFun✝ a ⊔ toFun✝ b
map_inf'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun (a ⊓ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun a ⊓ { toFun := toFun✝, map_sup' := map_sup'✝ }.toFun b
map_himp'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a ⇨ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a ⇨
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
map_sdiff'✝ :
  ∀ (a b : α),
    { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun (a \ b) =
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun a \
        { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝ }.toFun b
h :
  (fun f ↦ f.toFun)
      { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
        map_sdiff' := map_sdiff'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_sup' := map_sup'✝, map_inf' := map_inf'✝, map_himp' := map_himp'✝,
      map_sdiff' := map_sdiff'✝ } =
    g
Module: Mathlib.CategoryTheory.Monoidal.Comon_

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
M N O : C
inst✝² : ComonObj M
inst✝¹ : ComonObj N
inst✝ : ComonObj O
X✝ Y✝ : (Mon Cᵒᵖ)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ f.unop.hom.unop ≫ Δ = Δ ≫ (f.unop.hom.unop ⊗ₘ f.unop.hom.unop)

Tactic:
by apply Quiver.Hom.op_inj; simp [op_tensorHom]

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

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

Tactic:
refine .inr <| ⟨x * r' * y, ⟨x * r', mem_univ _, y, hy, ?_⟩, ⟨r, mem_univ _, ?_⟩⟩

Goal state after:
case refine_1.inr.refine_1
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) (x * r') y = x * r' * y

case refine_1.inr.refine_2
R : Type u_1
inst✝ : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun x1 x2 ↦ x1 * x2) (x * r' * y) r = x * (fun x1 x2 ↦ x1 * x2) ((fun x1 x2 ↦ x1 * x2) r' y) r
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I✝ I J : TwoSidedIdeal R
h : I ≤ J
x : Rᵐᵒᵖ
h' : x ∈ (fun I ↦ asIdeal { ringCon := I.ringCon.op }) I
⊢ x ∈ (fun I ↦ asIdeal { ringCon := I.ringCon.op }) J

Tactic:
simp only [mem_asIdeal, mem_iff, RingCon.op_iff, MulOpposite.unop_zero] at h' ⊢
    exact J.rel_iff _ _ |>.2 <| h <| I.rel_iff 0 x.unop |>.1 h'

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
fg : N.FG
le : N ≠ ⊥
⊢ ¬N ≤ Ring.jacobson R • N

Tactic:
exact (jacobson_smul_lt le fg).not_ge

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

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a b : R
h : a ∣ b
H : Function.Injective ⇑(awayMap f a)
⊢ Function.Injective ⇑(awayMap f b)

Tactic:
by
  simp only [awayMap_injective_iff] at H ⊢
  obtain ⟨b, rfl⟩ := h
  refine fun x hx ↦ ?_
  obtain ⟨n, hn⟩ := H x hx
  exact ⟨n, by simp [mul_pow, mul_assoc, mul_left_comm (a ^ n), hn]⟩

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

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
⊢ ⊥.jacobson = ⊥ → I.jacobson = I

Tactic:
intro h
    replace h := congr_arg (comap (Ideal.Quotient.mk I)) h
    rw [comap_jacobson_of_surjective hf, ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at h
    simpa using h

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson

Tactic:
by
  have hf : Function.Surjective (Ideal.Quotient.mk I) := Submodule.Quotient.mk_surjective I
  constructor
  · intro h
    have := congr_arg (map (Ideal.Quotient.mk I)) h
    rw [map_radical_of_surjective hf (le_of_eq mk_ker),
      map_jacobson_of_surjective hf (le_of_eq mk_ker)] at this
    simpa using this
  · intro h
    have := congr_arg (comap (Ideal.Quotient.mk I)) h
    rw [comap_radical, comap_jacobson_of_surjective hf,
      ← RingHom.ker_eq_comap_bot (Ideal.Quotient.mk I)] at this
    simpa using this

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

Goal state before:
pp: 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
⊢ n + m = ↑m.natAbs - ↑n.natAbs

Tactic:
rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
A : Type u_2
Aₛ : Type u_3
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring Aₛ
inst✝² : Algebra A Aₛ
inst✝¹ : Algebra R Aₛ
inst✝ : IsScalarTower R A Aₛ
x✝ : Aₛ
⊢ (∃ a a_1, ∃ (b : a_1 ∈ S), ⟨a_1, b⟩ • x✝ = (IsScalarTower.toAlgHom R A Aₛ).toLinearMap a) ↔
    ∃ a a_1, ∃ (_ : a_1 ∈ Submonoid.map (algebraMap R A) S), x✝ * (algebraMap A Aₛ) a_1 = (algebraMap A Aₛ) a

Tactic:
simp [← IsScalarTower.algebraMap_apply, Submonoid.mk_smul, Algebra.smul_def, mul_comm]

Goal state after:
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:
rw [IsLocalizedModule.mk_eq_mk', IsLocalizedModule.mk_eq_mk']

Goal state after:
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) (IsLocalizedModule.mk' (mkLinearMap S M) x y) = IsLocalizedModule.mk' (mkLinearMap S N) (f x) y
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) (IsLocalizedModule.mk' (mkLinearMap S M) x y) = IsLocalizedModule.mk' (mkLinearMap S N) (f x) y

Tactic:
exact IsLocalizedModule.map_mk' _ _ _ _ _ _

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
s₁ s₂ : ↥S
⊢ mk a₁ s₁ * mk a₂ s₂ = mk (a₁ * a₂) (s₁ * s₂)

Tactic:
by rw [mk_mul_mk', mul_comm s₁ s₂]

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'
t : T
t' : T'
p : LocalizedModule S M
⊢ t • t' • p = t' • t • p

Tactic:
induction p with | _ m s

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'
t : T
t' : T'
m : M
s : ↥S
⊢ t • t' • mk m s = t' • t • mk m s