mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
map_zero

Goal state after:
case a.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
⊢ 0 ∈ ↑(Submodule.restrictScalars R (map includeRight I))
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ IsNilpotent (f r)

Tactic:
use hr.choose

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ f r ^ Exists.choose hr = 0
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ f 0 = 0

Tactic:
map_zero

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : MonoidWithZero R
inst✝² : MonoidWithZero S
r : R
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : MonoidWithZeroHomClass F R S
hr : IsNilpotent r
f : F
⊢ 0 = 0
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = 0

Tactic:
← pow_nilpotencyClass this,

Goal state after:
R : Type u_1
x : R
inst✝ : MonoidWithZero R
hx : nilpotencyClass x = 1
this : IsNilpotent x
⊢ x = x ^ nilpotencyClass x
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
⊢ IsNilpotent x → x = 0

Tactic:
hx

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ x = 0
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = f 0

Tactic:
map_zero

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : MonoidWithZero R
inst✝³ : MonoidWithZero S
F : Type u_3
inst✝² : FunLike F R S
inst✝¹ : MonoidWithZeroHomClass F R S
f : F
hf : Function.Injective ⇑f
inst✝ : IsReduced S
x : R
hx : IsNilpotent x
⊢ f x = 0
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
⊢ x ∈ Subalgebra.map includeLeft (Subalgebra.center K B) → x ∈ Subalgebra.center K (B ⊗[K] C)

Tactic:
hx

Goal state after:
K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
x : B ⊗[K] C
hx : x ∈ Subalgebra.map includeLeft (Subalgebra.center K B)
⊢ x ∈ Subalgebra.center K (B ⊗[K] C)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
eq : (rTensor M f) ((rTensor M N'.subtype) x) = (rTensor M f) ((rTensor M N'.subtype) y)
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y

Tactic:
← rTensor_comp_apply,

Goal state after:
R : Type u
M : Type v
N : Type u_1
P : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : N →ₗ[R] P
h :
  ∀ (N' : Submodule R N) (P' : Submodule R P),
    N'.FG → P'.FG → ∀ (h : N' ≤ comap f P'), Injective ⇑(rTensor M (f.restrict h))
N' : Submodule R N
Nfg : N'.FG
x y : ↥N' ⊗[R] M
sub : {(rTensor M N'.subtype) x, (rTensor M N'.subtype) y} ⊆ ↑(rTensor M N'.subtype).range
eq : (rTensor M (f ∘ₗ N'.subtype)) x = (rTensor M (f ∘ₗ N'.subtype)) y
⊢ (rTensor M N'.subtype) x = (rTensor M N'.subtype) y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
s : Finset ι
t : ι → Set κ
f : κ → β
h : (↑s).PairwiseDisjoint t
x : κ
⊢ (⋃ i ∈ s, t i).mulIndicator f x = ∏ i ∈ s, (t i).mulIndicator f x

Tactic:
rw [mulIndicator_biUnion s t h]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (↑(#s) ^ n)⁻¹ • ∑ p ∈ Fintype.piFinset fun _i ↦ s, ∏ i, f (p i) =
    (↑(#s ^ n))⁻¹ • ∑ i ∈ Fintype.piFinset fun x ↦ s, ∏ i_1, f (i i_1)

Tactic:
Nat.cast_pow

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (↑(#s) ^ n)⁻¹ • ∑ p ∈ Fintype.piFinset fun _i ↦ s, ∏ i, f (p i) =
    (↑(#s) ^ n)⁻¹ • ∑ i ∈ Fintype.piFinset fun x ↦ s, ∏ i_1, f (i i_1)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive ((TensorProduct.lift f) 0)

Tactic:
map_zero

Goal state after:
case zero
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
⊢ TensorProduct.lift f = ↑e

Tactic:
ext x y

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
e : M₁ ⊗[R] M₂ ≃ₗ[R] M
he : ∀ (x : M₁) (y : M₂), e (x ⊗ₜ[R] y) = (f x) y
x : M₁
y : M₂
⊢ ((AlgebraTensorModule.curry (TensorProduct.lift f)) x) y = ((AlgebraTensorModule.curry ↑e) x) y
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ 0 ≤ i ∧ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Tactic:
rintro ⟨hi₀, hia⟩

Goal state after:
case inr.mpr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
j' : ℕ
hj' : j' < k + 1
hjj' : j ≠ j'
hij' : j < j'
hj'₀ : j' - 1 + 1 = j'
this : (F.intervalGapsWithin h a b ↑(j' - 1)).2 ≤ (F.intervalGapsWithin h a b ↑j').1
⊢ ((F.orderEmbOfFin h) ⟨j, ⋯⟩).1 ≤ ((F.orderEmbOfFin h) ⟨j' - 1, ⋯⟩).1

Tactic:
exact Prod.Lex.le_iff'.mp (F.orderEmbOfFin (α := α ×ₗ α) h |>.monotone (by grind)) |>.left

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [MOD n]

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [MOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).prod ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).prod [MOD
    n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [MOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
α : Type u_1
n : ℕ
f g : α → ℕ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [MOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).sum ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).sum [MOD n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_one, cast_prod, apply_ite Nat.cast] at *
  exact Finset.prod_eq_ite _ hf

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).prod ≡ (Multiset.map g s).prod [ZMOD n]

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).prod ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).prod [ZMOD
    n]
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
h : ∀ x ∈ s, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f s).sum ≡ (Multiset.map g s).sum [ZMOD n]

Tactic:
rcases s with ⟨l⟩

Goal state after:
case mk
α : Type u_1
n : ℤ
f g : α → ℤ
s : Multiset α
l : List α
h : ∀ x ∈ Quot.mk (⇑(List.isSetoid α)) l, f x ≡ g x [ZMOD n]
⊢ (Multiset.map f (Quot.mk (⇑(List.isSetoid α)) l)).sum ≡ (Multiset.map g (Quot.mk (⇑(List.isSetoid α)) l)).sum [ZMOD n]
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ 0 = g₂ 0

Tactic:
map_zero

Goal state after:
case refine_1
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid N
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ 0 = 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x✝ x y : S ⊗[R] M
⊢ (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x →
    (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y →
      (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)

Tactic:
hx

Goal state after:
case refine_3
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
f : M →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
r : S
x✝ x y : S ⊗[R] M
hx : (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x
⊢ (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y →
    (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
m m' : Multiset α
h : m ≤ m'
⊢ m.sym2 ≤ m'.sym2

Tactic:
induction m, m' using Quotient.inductionOn₂ with

Goal state after:
case h
α : Type u_1
xs ys : List α
h : ⟦xs⟧ ≤ ⟦ys⟧
⊢ Multiset.sym2 ⟦xs⟧ ≤ Multiset.sym2 ⟦ys⟧
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case zero
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
⊢ s.sym 0 = ∅ ↔ 0 ≠ 0 ∧ s = ∅

Tactic:
exact iff_of_false (singleton_ne_empty _) fun h ↦ (h.1 rfl).elim

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
⊢ x ∈ (↑k).toFinset → x ∈ s

Tactic:
hx

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
hx : x ∈ (↑k).toFinset
⊢ x ∈ s
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ ((AlgebraTensorModule.curry ((↑ULift.moduleEquiv ∘ₗ g) ∘ₗ f'')) 1) x = ((AlgebraTensorModule.curry LinearMap.id) 1) x

Tactic:
change (g <| (1 : S) • f x).down = _

Goal state after:
case refine_2
R : Type u_1
M : Type v₁
N : Type v₂
S : Type v₃
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
h :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), g (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
x : M
⊢ (g (1 • f x)).down = ((AlgebraTensorModule.curry LinearMap.id) 1) x
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
x y : α × α
⊢ Rel α x y → Rel α y x

Tactic:
by aesop (rule_sets := [Sym2])

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : γ → α
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
p : Sym2 γ
⊢ lift f (map g p) = lift ⟨fun c₁ c₂ ↦ ↑f (g c₁) (g c₂), ⋯⟩ p

Tactic:
by
  conv_rhs => rw [← lift_comp_map, comp_apply]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = ∅
⊢ r = ⊥

Tactic:
ext x y

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = ∅
x y : α
⊢ r x y ↔ ⊥ x y
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = Set.univ
⊢ r = ⊤

Tactic:
ext x y

Goal state after:
α : Type u_1
r : α → α → Prop
sym : Std.Symm r
h : fromRel sym = Set.univ
x y : α
⊢ r x y ↔ ⊤ x y
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
a : α
z : Sym2 α
ha : a ∈ z
hb✝ : Mem.other ha ∈ z
hb : Mem.other' ha ∈ z
⊢ Mem.other ha = Mem.other' ha

Tactic:
apply other_eq_other'

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
Y : C
⊢ (∃ i, X i = Y) → ofObj X Y

Tactic:
rintro ⟨i, rfl⟩

Goal state after:
case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
i : ι
⊢ ofObj X (X i)
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case mpr
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
P : ObjectProperty C
Y : D
⊢ P.map F Y → (P.ι ⋙ F).essImage Y

Tactic:
rintro ⟨X, hX, ⟨e⟩⟩
    exact ⟨⟨X, hX⟩, ⟨e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
L : C ⥤ D
inst✝ : L.EssSurj
h : ∀ ⦃X₁ X₂ : C⦄ (φ : F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)), ∃ f, F.map f = φ
X₁ X₂ : D
ψ : F.obj X₁ ⟶ F.obj X₂
f : L.obj (L.objPreimage X₁) ⟶ L.obj (L.objPreimage X₂)
hf : F.map f = F.map (L.objObjPreimageIso X₁).hom ≫ ψ ≫ F.map (L.objObjPreimageIso X₂).inv
⊢ ∃ a, F.map a = ψ

Tactic:
exact ⟨(L.objObjPreimageIso X₁).inv ≫ f ≫ (L.objObjPreimageIso X₂).hom, by simp [hf]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
functor : C ⥤ D
inverse : D ⥤ C
unitIso : 𝟭 C ≅ functor ⋙ inverse
counitIso : inverse ⋙ functor ≅ 𝟭 D
functor_unitIso_comp :
  ∀ (X : C), counitIso.inv.app (functor.obj X) ≫ functor.map (unitIso.inv.app X) = 𝟙 (functor.obj X)
X : C
⊢ functor.map (unitIso.hom.app X) ≫ counitIso.hom.app (functor.obj X) = 𝟙 (functor.obj X)

Tactic:
simpa [functor_unitIso_comp] using Iso.inv_eq_inv
      (functor.mapIso (unitIso.app X) ≪≫ counitIso.app (functor.obj X)) (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C ↔ isomorphisms C = ⊤

Tactic:
constructor
  · rw [eq_top_iff]
    intro _ _
    simp only [isomorphisms.iff, top_apply]
    infer_instance
  · intro h
    exact ⟨of_eq_top h⟩

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

Goal state before:
pp: ⊢ ∀ {a b c d : Cat} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mp.right
C : Type u
inst✝ : Category.{v, u} C
h : EssentiallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
· infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
X : J
hX : IsTerminal X
F : J ⥤ C
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ ∀ ⦃X_1 Y : J⦄ (f : X_1 ⟶ Y),
    ((Functor.const J).obj (F.obj X)).map f ≫ inv (F.map (hX.from Y)) = inv (F.map (hX.from X_1)) ≫ F.map f

Tactic:
by
        intro i j f
        dsimp
        simp only [IsIso.eq_inv_comp, IsIso.comp_inv_eq, Category.id_comp, ← F.map_comp,
          hX.hom_ext (hX.from i) (f ≫ hX.from j)]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
⊢ ∃ a, (post F).map a = f

Tactic:
obtain ⟨a, ha⟩ := F.map_surjective f.left

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Over X
f : (post F).obj A ⟶ (post F).obj B
a : A.left ⟶ B.left
ha : F.map a = Hom.left f
⊢ ∃ a, (post F).map a = f
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ (post F).map (homMk a ⋯) = f

Tactic:
by ext; simpa

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ pushout.inl f g ≫ inv (pushout.inr f g) = inv f ≫ g

Tactic:
by
  rw [IsIso.eq_inv_comp, pushout.condition_assoc, IsIso.hom_inv_id, Category.comp_id]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
h : W₁.comp W₂ = ⊤
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : W₁.comp W₂ f
⊢ Nonempty (W₁.MapFactorizationData W₂ f)

Tactic:
exact ⟨this.some⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
t : PullbackCone f f
ht : IsLimit t
⊢ IsIso t.fst

Tactic:
refine ⟨⟨PullbackCone.IsLimit.lift ht (𝟙 _) (𝟙 _) (by simp), ?_, by simp⟩⟩
  apply PullbackCone.IsLimit.hom_ext ht
  · simp
  · simp [fst_eq_snd_of_mono_eq]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ preComp f g ≫ ι g = ι (f ≫ g)

Tactic:
by
      simp [image.preComp]

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

Goal state before:
pp: case mk
C : Type u
inst✝ : Category.{v, u} C
J : HasZeroMorphisms C
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ { zero := zero✝, comp_zero := comp_zero✝, zero_comp := zero_comp✝ } = J

Tactic:
cases J

Goal state after:
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
zero✝¹ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝¹ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝¹ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
zero✝ : (X Y : C) → Zero (X ⟶ Y)
comp_zero✝ : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ 0 = 0
zero_comp✝ : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), 0 ≫ f = 0
w : ∀ (X Y : C), Zero.zero = Zero.zero
this : zero = zero
⊢ { zero := zero✝¹, comp_zero := comp_zero✝¹, zero_comp := zero_comp✝¹ } =
    { zero := zero✝, comp_zero := comp_zero✝, zero_comp := zero_comp✝ }