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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s : Set (M ⊗[R] N)
hs : s.Finite
⊢ ∃ N', Module.Finite R ↥N' ∧ s ⊆ ↑(LinearMap.lTensor M N'.subtype).range

Tactic:
by
  obtain ⟨_, N', _, hfin, h⟩ := exists_finite_submodule_of_setFinite s hs
  refine ⟨N', hfin, ?_⟩
  rw [mapIncl, ← LinearMap.lTensor_comp_rTensor] at h
  exact h.trans (LinearMap.range_comp_le_range _ _)

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

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective ⇑(TensorProduct.map Q.subtype i)

Tactic:
← rTensor_comp_lTensor,

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective ⇑(rTensor M Q.subtype ∘ₗ lTensor (↥Q) i)
Module: Mathlib.Algebra.BigOperators.Balance

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f g : ι → G
⊢ balance (f + g) = balance f + balance g

Tactic:
simp only [balance, expect_add_distrib, ← const_add, add_sub_add_comm, Pi.add_apply]

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : (i : ι) → FunLike (H i) (G i) C
inst✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
i : ι
x✝² x✝¹ x✝ : G i
⊢ (⟦⟨i, x✝²⟩⟧ + ⟦⟨i, x✝¹⟩⟧) * ⟦⟨i, x✝⟩⟧ = ⟦⟨i, x✝²⟩⟧ * ⟦⟨i, x✝⟩⟧ + ⟦⟨i, x✝¹⟩⟧ * ⟦⟨i, x✝⟩⟧

Tactic:
by
    simp_rw [add_def, mul_def, right_distrib, add_def]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
· have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind))
    have hj₀ : j - 1 + 1 = j := by lia
    simp only [Nat.succ_eq_add_one, hj₀] at this
    grind

Goal state after:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with

Goal state after:
case ih
R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
g₁ g₂ : DirectLimit G f →ₗ[R] P
h : ∀ (i : ι), g₁ ∘ₗ of R ι G f i = g₂ ∘ₗ of R ι G f i
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with

Goal state after:
case ih
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonUnitalNonAssocSemiring P
g₁ g₂ : DirectLimit G f →ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with

Goal state after:
case ih
ι : Type u_2
inst✝⁷ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁶ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁵ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁴ : IsDirectedOrder ι
inst✝³ : (i : ι) → NonAssocSemiring (G i)
inst✝² : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)
inst✝¹ : Nonempty ι
P : Type u_7
inst✝ : NonAssocSemiring P
g₁ g₂ : DirectLimit G f →+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with

Goal state after:
case ih
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁵ : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)
inst✝⁴ : (i : ι) → StarRing (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : StarRing P
g₁ g₂ : DirectLimit G f →⋆ₙ+* P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with

Goal state after:
case ih
R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g₁ g₂ : DirectLimit G f →ₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with

Goal state after:
case ih
R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁹ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: m n : ℕ
⊢ Ioc (-(↑m + 1)) (↑n + 1) = Ioc (-↑m) ↑n ∪ {-↑m, ↑n + 1}

Tactic:
ext
  simp only [mem_Ioc, union_insert, union_singleton, mem_insert]
  lia

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

Goal state before:
pp: case cons.inr.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : s(a, b) = s(x, c)
⊢ a = x ∨ a ∈ xs

pp: case cons.inr.inr
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs

Tactic:
· rw [Sym2.eq_iff] at h
      obtain (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) := h <;> simp [hc]

Goal state after:
case cons.inr.inr
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
d' : β
b : Sym α n
hd : ∃ a ∈ b, g a = d'
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
⊢ ∃ a ∈ s, g a = d'

Tactic:
obtain ⟨a, ha, rfl⟩ := hd

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
n : ℕ
g : α ↪ β
s : Finset α
d : Sym β n
x✝ : ∃ a, (∀ a_1 ∈ a, a_1 ∈ s) ∧ Sym.map (⇑g) a = d
b : Sym α n
hb : ∀ a ∈ b, a ∈ s
hd' : Sym.map (⇑g) b = d
a : α
ha : a ∈ b
⊢ ∃ a_1 ∈ s, g a_1 = g a
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ Set.range diag = diagSet

Tactic:
ext ⟨a, b⟩; simp [diag, eq_comm]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
T : Type u_4
O : Type u_5
inst✝¹⁰ : CommSemiring T
inst✝⁹ : Algebra R T
inst✝⁸ : Algebra S T
inst✝⁷ : IsScalarTower R S T
inst✝⁶ : AddCommMonoid O
inst✝⁵ : Module R O
inst✝⁴ : Module S O
inst✝³ : Module T O
inst✝² : IsScalarTower S T O
inst✝¹ : IsScalarTower R S O
inst✝ : IsScalarTower R T O
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
⊢ IsBaseChange T h

Tactic:
by
  apply IsBaseChange.of_lift_unique
  intro Q _ _ _ _ r
  let : Module R Q := .restrictScalars R S Q
  have : IsScalarTower R S Q := .restrictScalars R S Q
  have : IsScalarTower R T Q := IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp [IsScalarTower.algebraMap_apply R S T]
  let r' : M →ₗ[R] Q := r ∘ₗ f
  let q : O →ₗ[T] Q := hc.lift r'
  refine ⟨q, ?_, ?_⟩
  · apply hf.algHom_ext'
    simp [r', q, LinearMap.comp_assoc, hc.lift_comp]
  · intro q' hq'
    apply hc.algHom_ext'
    apply_fun LinearMap.restrictScalars R at hq'
    rw [← LinearMap.comp_assoc]
    rw [show q'.restrictScalars R ∘ₗ h.restrictScalars R = _ from hq', hc.lift_comp]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_4
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring 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 R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x : S'
⊢ ∀ (n₁ n₂ : S'), f n₁ = g n₁ → f n₂ = g n₂ → f (n₁ + n₂) = g (n₁ + n₂)

Tactic:
intro s₁ s₂ e₁ e₂

Goal state after:
case refine_4
R : Type u_1
S : Type v₃
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁹ : CommSemiring R'
inst✝⁸ : CommSemiring 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 R S R' S'
A : Type u_8
inst✝¹ : Semiring A
inst✝ : Algebra R A
f g : S' →ₐ[R] A
h₁ : f.comp (toAlgHom R R' S') = g.comp (toAlgHom R R' S')
h₂ : f.comp (toAlgHom R S S') = g.comp (toAlgHom R S S')
x s₁ s₂ : S'
e₁ : f s₁ = g s₁
e₂ : f s₂ = g s₂
⊢ f (s₁ + s₂) = g (s₁ + s₂)
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ 𝟙 Y = inv g ≫ g

Tactic:
inv_hom_id

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ 𝟙 Y = 𝟙 Y
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: case mk.mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X✝ Y✝ : C
F : C ⥤ D
X Y Z : C
hF : F.FullyFaithful
this : F.Faithful
f₁ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₁ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₁ f) = f
preimage_map✝¹ : ∀ {X Y : C} (f : X ⟶ Y), f₁ (F.map f) = f
f₂ : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
hf₂ : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (f₂ f) = f
preimage_map✝ : ∀ {X Y : C} (f : X ⟶ Y), f₂ (F.map f) = f
x✝² x✝¹ : C
x✝ : F.obj x✝² ⟶ F.obj x✝¹
⊢ F.map (f₁ x✝) = F.map (f₂ x✝)

Tactic:
rw [hf₁, hf₂]

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D} (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.map f)

Tactic:
intro F₁ F₂ e hf

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
hf : IsIso (F₁.map f)
⊢ IsIso (F₂.map f)
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
inst✝ : ∀ (a b : V), Subsingleton (a ⟶ b)
a x✝ c : V
p : Path a c
f : c ⟶ x✝
C : Path a c
D : c ⟶ x✝
hAC : p.toList = C.toList
⊢ p.cons f = C.cons D

Tactic:
simp [toList_injective _ _ hAC, eq_iff_true_of_subsingleton]

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
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
        (((𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
                (e.inverse.mapIso
                    (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv) ≫
              e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
rw [id_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
        (((e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv ≫
              e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
            e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
          e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫
          𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
rw [id_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
        e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)

Tactic:
have := ε.hom.naturality (ε.inv.app <| F.obj X)

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
this :
  (G ⋙ F).map (ε.inv.app (F.obj X)) ≫ ε.hom.app ((G ⋙ F).obj (F.obj X)) =
    ε.hom.app ((𝟭 D).obj (F.obj X)) ≫ (𝟭 D).map (ε.inv.app (F.obj X))
⊢ F.map (η.hom.app X) ≫
      (F.map (G.map (ε.inv.app (F.obj X))) ≫ ε.hom.app (F.obj (G.obj (F.obj X)))) ≫ F.map (η.inv.app X) =
    𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ 𝟙 (F.obj (G.obj (F.obj X))) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)

Tactic:
rw [id_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map (η.hom.app X) ≫ F.map (η.inv.app X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.strictMap (𝟭 C) = P

Tactic:
by
  ext
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ 𝟙 W ≫ ↑p j' = ↑p j ≫ F.map f

Tactic:
rw [id_comp]

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
t : Cone F
h : IsLimit t
W : C
p : { p // ∀ {j j' : J} (f : j ⟶ j'), p j ≫ F.map f = p j' }
j j' : J
f : j ⟶ j'
⊢ ↑p j' = ↑p j ≫ F.map f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type w
X Y : C
R : F.RepresentableBy X
e : Y ≅ X
⊢ ∀ {X_1 X' : C} (f : X_1 ⟶ X') (g : X' ⟶ Y),
    (e.homToEquiv.trans R.homEquiv) (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) ((e.homToEquiv.trans R.homEquiv) g)

Tactic:
by simp [R.homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type w
X Y : C
R : F.CorepresentableBy X
e : Y ≅ X
⊢ ∀ {Y_1 Y' : C} (g : Y_1 ⟶ Y') (f : Y ⟶ Y_1),
    (e.homFromEquiv.trans R.homEquiv) (f ≫ g) = (ConcreteCategory.hom (F.map g)) ((e.homFromEquiv.trans R.homEquiv) f)

Tactic:
by simp [R.homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
X : C
R : F.RepresentableBy X
X✝ X'✝ : C
f : X✝ ⟶ X'✝
g : X'✝ ⟶ X
⊢ (R.homEquiv.trans Equiv.ulift.symm) (f ≫ g) =
    (ConcreteCategory.hom ((F ⋙ uliftFunctor.{w, v}).map f.op)) ((R.homEquiv.trans Equiv.ulift.symm) g)

Tactic:
by simp [R.homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
R : F.CorepresentableBy X
Y✝ Y'✝ : C
f : Y✝ ⟶ Y'✝
g : X ⟶ Y✝
⊢ (R.homEquiv.trans Equiv.ulift.symm) (g ≫ f) =
    (ConcreteCategory.hom ((F ⋙ uliftFunctor.{w, v}).map f)) ((R.homEquiv.trans Equiv.ulift.symm) g)

Tactic:
by simp [R.homEquiv_comp]

Goal state after: