mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Gaps

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ (∏ i ∈ range k, g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i.succ).1 / g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i).2) *
      ((∏ x ∈ range k, g (F.intervalGapsWithin h a b ↑x).2 / g (F.intervalGapsWithin h a b ↑x).1) *
        (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1)) =
    g b / g a

pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

Tactic:
← mul_assoc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ ((∏ i ∈ range k, g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i.succ).1 / g (F.intervalGapsWithin h ?m.56 ?m.57 ↑i).2) *
        ∏ x ∈ range k, g (F.intervalGapsWithin h a b ↑x).2 / g (F.intervalGapsWithin h a b ↑x).1) *
      (g (F.intervalGapsWithin h a b ↑k).2 / g (F.intervalGapsWithin h a b ↑k).1) =
    g b / g a

α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α

α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : CommGroup β
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
g : α → β
⊢ α
Module: Mathlib.Algebra.BigOperators.Group.Finset.Interval

Goal state before:
pp: case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ f (-↑b) / f ↑b * (f (-(↑b + 1)) / f (-(↑b + 1) + 1) * (f ↑b / f (↑b + 1))) = f (-(↑b + 1)) / f (↑b + 1)

Tactic:
← mul_assoc,

Goal state after:
case succ
α : Type u_1
inst✝ : CommGroup α
f : ℤ → α
b : ℕ
ihb : ∏ n ∈ Ico (-↑b) ↑b, f n / f (n + 1) = f (-↑b) / f ↑b
⊢ f (-↑b) / f ↑b * (f (-(↑b + 1)) / f (-(↑b + 1) + 1)) * (f ↑b / f (↑b + 1)) = f (-(↑b + 1)) / f (↑b + 1)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ ∏ x ∈ (insert a s).powerset, f x = (∏ x ∈ s.powerset, f x) * ∏ x ∈ s.powerset.attach, f (insert a ↑x)

Tactic:
prod_powerset_insert ha,

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
a : α
inst✝ : CommMonoid β
ha : a ∉ s
f : Finset α → β
⊢ (∏ t ∈ s.powerset, f t) * ∏ t ∈ s.powerset, f (insert a t) =
    (∏ x ∈ s.powerset, f x) * ∏ x ∈ s.powerset.attach, f (insert a ↑x)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
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
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
x₁ x₂ : N
e₁ : (IsTensorProduct.lift h F) (r • x₁) = r • (IsTensorProduct.lift h F) x₁
e₂ : (IsTensorProduct.lift h F) (r • x₂) = r • (IsTensorProduct.lift h F) x₂
⊢ (IsTensorProduct.lift h F) (r • (x₁ + x₂)) = r • (IsTensorProduct.lift h F) (x₁ + x₂)

Tactic:
map_add,

Goal state after:
case add
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
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
x₁ x₂ : N
e₁ : (IsTensorProduct.lift h F) (r • x₁) = r • (IsTensorProduct.lift h F) x₁
e₂ : (IsTensorProduct.lift h F) (r • x₂) = r • (IsTensorProduct.lift h F) x₂
⊢ (IsTensorProduct.lift h F) (r • (x₁ + x₂)) = r • ((IsTensorProduct.lift h F) x₁ + (IsTensorProduct.lift h F) x₂)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
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
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
x₁ x₂ : N
e₁ : (IsTensorProduct.lift h F) (r • x₁) = r • (IsTensorProduct.lift h F) x₁
e₂ : (IsTensorProduct.lift h F) (r • x₂) = r • (IsTensorProduct.lift h F) x₂
⊢ (IsTensorProduct.lift h F) (r • x₁ + r • x₂) = r • ((IsTensorProduct.lift h F) x₁ + (IsTensorProduct.lift h F) x₂)

Tactic:
map_add,

Goal state after:
case add
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
inst✝¹ : Module R Q
inst✝ : IsScalarTower R S Q
g : M →ₗ[R] Q
r : S
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
x₁ x₂ : N
e₁ : (IsTensorProduct.lift h F) (r • x₁) = r • (IsTensorProduct.lift h F) x₁
e₂ : (IsTensorProduct.lift h F) (r • x₂) = r • (IsTensorProduct.lift h F) x₂
⊢ (IsTensorProduct.lift h F) (r • x₁) + (IsTensorProduct.lift h F) (r • x₂) =
    r • ((IsTensorProduct.lift h F) x₁ + (IsTensorProduct.lift h F) x₂)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_4
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✝ x y : N
e₁ : g₁ x = g₂ x
e₂ : g₁ y = g₂ y
⊢ g₁ (x + y) = g₂ (x + y)

Tactic:
map_add,

Goal state after:
case refine_4
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✝ x y : N
e₁ : g₁ x = g₂ x
e₂ : g₁ y = g₂ y
⊢ g₁ x + g₁ y = g₂ (x + y)
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_4
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✝ x y : N
e₁ : g₁ x = g₂ x
e₂ : g₁ y = g₂ y
⊢ g₁ x + g₁ y = g₂ (x + y)

Tactic:
map_add,

Goal state after:
case refine_4
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✝ x y : N
e₁ : g₁ x = g₂ x
e₂ : g₁ y = g₂ y
⊢ g₁ x + g₁ y = g₂ x + g₂ y
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
hx : (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)

Tactic:
map_add,

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
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ (IsTensorProduct.equiv h) (r • (x + y)) = r • ((IsTensorProduct.equiv h) x + (IsTensorProduct.equiv h) y)
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
hx : (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ (IsTensorProduct.equiv h) (r • x + r • y) = r • ((IsTensorProduct.equiv h) x + (IsTensorProduct.equiv h) y)

Tactic:
map_add,

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
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ (IsTensorProduct.equiv h) (r • x) + (IsTensorProduct.equiv h) (r • y) =
    r • ((IsTensorProduct.equiv h) x + (IsTensorProduct.equiv h) y)
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ x✝¹.sym2.Perm x✝.sym2

Tactic:
exact h.sym2

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

Goal state before:
pp: α : Type u_1
m : Multiset α
z : Sym2 α
xs : List α
⊢ z ∈ Multiset.sym2 ⟦xs⟧ ↔ ∀ y ∈ z, y ∈ ⟦xs⟧

Tactic:
by simp [List.mem_sym2_iff]

Goal state after:
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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ f' (s • x + s • y) = s • f' (x + y)

Tactic:
map_add,

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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ f' (s • x) + f' (s • y) = s • f' (x + y)
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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ f' (s • x) + f' (s • y) = s • f' (x + y)

Tactic:
map_add,

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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x✝ x y : S ⊗[R] M
hx : f' (s • x) = s • f' x
hy : f' (s • y) = s • f' y
⊢ f' (s • x) + f' (s • y) = s • (f' x + f' y)
Module: Mathlib.Algebra.BigOperators.WithTop

Goal state before:
pp: case mp
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ∏ j ∈ s, f j = ⊤ → (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0

pp: case mpr
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → ∏ j ∈ s, f j = ⊤

Tactic:
· exact fun h ↦ ⟨prod_eq_top_ex_top h, fun _ ih ↦ prod_eq_top_ne_zero ih h⟩

Goal state after:
case mpr
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
⊢ ((∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0) → ∏ j ∈ s, f j = ⊤
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
⊢ IsBaseChange B (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)).toLinearMap

Tactic:
convert! isBaseChange_tensorProduct_map (R := R) (P := S) _ (IsBaseChange.linearMap A B)

Goal state after:
case e'_14
R : Type u_8
S : Type u_9
A : Type u_10
B : Type u_11
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra R S
x✝¹ : Algebra (A ⊗[R] S) (B ⊗[R] S)
x✝ : IsScalarTower A (A ⊗[R] S) (B ⊗[R] S)
H : (algebraMap (A ⊗[R] S) (B ⊗[R] S)).comp TensorProduct.includeRight.toRingHom = TensorProduct.includeRight.toRingHom
e_5✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_6✝ : TensorProduct.instCommSemiring.toAddCommMonoid = addCommMonoid
e_10✝ : toModule ≍ leftModule
e_11✝ : toModule ≍ leftModule
⊢ (toAlgHom A (A ⊗[R] S) (B ⊗[R] S)).toLinearMap = AlgebraTensorModule.map (Algebra.linearMap A B) LinearMap.id
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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'
⊢ f 0 = g 0

Tactic:
simp only [map_zero]

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₁ s₂ : S'
e₁ : f s₁ = g s₁
e₂ : f s₂ = g s₂
⊢ f (s₁ + s₂) = g (s₁ + s₂)

Tactic:
map_add,

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₁ + f s₂ = g (s₁ + s₂)
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₁ s₂ : S'
e₁ : f s₁ = g s₁
e₂ : f s₂ = g s₂
⊢ f s₁ + f s₂ = g (s₁ + s₂)

Tactic:
map_add,

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₁ + f s₂ = g s₁ + g s₂
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯ ≫ eqToHom ⋯

Tactic:
eqToHom_trans,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
e : F ≅ G
hobj : ∀ (X : C), F.obj X = G.obj X
happ : ∀ (X : C), e.hom.app X = eqToHom ⋯
X Y : C
f : X ⟶ Y
⊢ eqToHom ⋯ ≫ G.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : Cᵒᵖ ⥤ D
α : F.rightOp ⟶ G.rightOp
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (G.map f ≫ (α.app (unop Y)).unop).op = ((α.app (unop X)).unop ≫ F.map f).op

Tactic:
simpa only [Functor.rightOp_map] using! (α.naturality f.unop).symm

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: case h₂
T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
aux : (Z ⟶ f.left) → (mk (𝟙 Z) ⟶ f) := ⋯
this : ∀ (g : Z ⟶ f.left), Hom.right (aux g) = g ≫ f.hom
⊢ Hom.right (aux φ ≫ sq) = Hom.right (aux ψ ≫ sq)

Tactic:
· simp [this, ← Arrow.w_mk_right, reassoc_of% h]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ (MorphismProperty.isomorphisms C).RespectsIso

Tactic:
by
  apply RespectsIso.mk <;>
    · intro X Y Z e f
      simp only [isomorphisms.iff]
      intro
      exact IsIso.comp_isIso

Goal state after:
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ α.inv ≫ f ≫ β.hom ≫ β.inv = f

Tactic:
β.hom_inv_id,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ α.inv ≫ f ≫ 𝟙 Y = f
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 : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
j : J
⊢ (colimitCocone h).ι.app j ≫ homOfCocone h s = s.ι.app j

Tactic:
have h := cocone_fac h s
    cases s
    injection h with h₁ h₂
    simp only at h₂
    conv_rhs => rw [← h₂]
    rfl

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Tactic:
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Goal state after: