mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Central.End

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
⊢ ∃ α, f = α • g

Tactic:
by_cases! Subsingleton M

Goal state after:
case pos
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Subsingleton M
⊢ ∃ α, f = α • g

case neg
R : Type u_1
M : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : Free R M
S : Type u_4
M₂ : Type u_5
inst✝¹² : CommRing S
inst✝¹¹ : IsCancelMulZero S
inst✝¹⁰ : Module S M
inst✝⁹ : SMulCommClass R S M
inst✝⁸ : Algebra S R
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : AddCommGroup M₂
inst✝⁵ : Module R M₂
inst✝⁴ : Module S M₂
inst✝³ : SMulCommClass R S M₂
inst✝² : IsScalarTower S R M₂
inst✝¹ : Algebra.IsCentral S R
inst✝ : IsTorsionFree S M₂
f g : M ≃ₗ[R] M₂
h : conjAlgEquiv S f = conjAlgEquiv S g
h✝ : Nontrivial M
⊢ ∃ α, f = α • g
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : Invertible x
p : R[X]
hp : p ≠ 0
hp' : (aeval x) p = 0
⊢ (aeval ⅟x) p.reverse = 0

Tactic:
rwa [Polynomial.aeval_def, Polynomial.eval₂_reverse_eq_zero_iff, ← Polynomial.aeval_def]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
r : R[X]
ht : (aeval s) r ∈ R[s]
a✝ : ⟨(aeval s) r, ht⟩ ∈ ⊤
⊢ (aeval ⟨s, ⋯⟩).toRingHom r = ⟨(aeval s) r, ht⟩

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
F : ι → Type u_4
T : ⦃i j : ι⦄ → i ≤ j → Sort u_8
f : (i j : ι) → (h : i ≤ j) → T h
inst✝² : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)
inst✝¹ : DirectedSystem F fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝ : IsDirectedOrder ι
C : DirectLimit F f → DirectLimit F f → Prop
ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧
x y : DirectLimit F f
⊢ C x y

Tactic:
by
  obtain ⟨_, _, _, rfl, rfl⟩ := exists_eq_mk₂ f x y; apply ih

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
g : G i
m : M
⊢ (toDirectLimit f M) ((of R ι G f i) g ⊗ₜ[R] m) =
    (of R ι (fun x ↦ G x ⊗[R] M) (fun i j h ↦ LinearMap.rTensor M (f i j h)) i) (g ⊗ₜ[R] m)

Tactic:
rw [toDirectLimit, lift.tmul, lift_of]
  rfl

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ toDirectLimit f M ∘ₗ fromDirectLimit f M = LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.DirectLimit

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
ι : Type u_2
inst✝⁵ : DecidableEq ι
inst✝⁴ : Preorder ι
G : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (G i)
inst✝² : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ fromDirectLimit f M ∘ₗ toDirectLimit f M = LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
⊢ (fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f) = f

Tactic:
ext j

Goal state after:
case fst
ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j✝ : ι✝
h : i✝ ≤ j✝
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
j : ↑(Iio i)
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).1 j = f.1 j

case snd
ι✝ : Type u_1
inst✝² : Preorder ι✝
F₁ : ι✝ → Type u_2
F₂ : ι✝ → Type u_3
F✝ : ι✝ → Type u_4
X✝ : ι✝ → Type u_5
f✝ : ⦃i j : ι✝⦄ → i ≤ j → F✝ j → F✝ i
i✝ j : ι✝
h : i✝ ≤ j
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
i : ι
inst✝¹ : PartialOrder ι
inst✝ : DecidableEq ι
f : piLT X i × X i
⊢ ((fun f ↦ (fun j ↦ f ⟨↑j, ⋯⟩, f ⟨i, ⋯⟩)) ((fun f j ↦ if h : ↑j = i then ⋯ ▸ f.2 else f.1 ⟨↑j, ⋯⟩) f)).2 = f.2
Module: Mathlib.Algebra.Colimit.Module

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
⊢ lift R ι G f (Module.of R ι G f) ⋯ ∘ₗ Module.lift R ι G f (of R ι G f) ⋯ = LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : (i : ι) → AddCommMonoid (G i)
inst✝⁴ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
inst✝³ : DecidableEq ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
⊢ Module.lift R ι G f (of R ι G f) ⋯ ∘ₗ lift R ι G f (Module.of R ι G f) ⋯ = LinearMap.id

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Data.DFinsupp.Small

Goal state before:
pp: ι : Type u
π : ι → Type v
inst✝² : (i : ι) → Zero (π i)
inst✝¹ : Small.{w, u} ι
inst✝ : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq : (fun x j ↦ x j) f = (fun x j ↦ x j) f'
⊢ f = f'

Tactic:
ext j

Goal state after:
ι : Type u
π : ι → Type v
inst✝² : (i : ι) → Zero (π i)
inst✝¹ : Small.{w, u} ι
inst✝ : ∀ (i : ι), Small.{w, v} (π i)
f f' : DFinsupp π
eq : (fun x j ↦ x j) f = (fun x j ↦ x j) f'
j : ι
⊢ f j = f' j
Module: Mathlib.RingTheory.MvPolynomial.Basic

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharZero R
x y : ℕ
hxy : ↑x = ↑y
⊢ x = y

Tactic:
Nat.cast_inj

Goal state after:
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
p m : ℕ
inst✝ : CharZero R
x y : ℕ
hxy : x = y
⊢ x = y
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
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
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ rTensor Q f ∘ₗ ↑(TensorProduct.comm R Q M) = ↑(TensorProduct.comm R Q N) ∘ₗ lTensor Q f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_2
N : Type u_3
P : Type u_4
Q : Type u_5
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
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ rTensor Q g ∘ₗ ↑(TensorProduct.comm R Q N) = ↑(TensorProduct.comm R Q P) ∘ₗ lTensor Q g

Tactic:
by ext; simp

Goal state after:
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✝
inst✝ : Flat R M
f : N✝ →ₗ[R] P✝
hf : Injective ⇑f
N : Submodule R N✝
P : Submodule R P✝
Nfg : Module.Finite R ↥N
Pfg : Module.Finite R ↥P
le : N ≤ comap f P
this✝ : Small.{max u ?u.66, u_2} ↥P
se : ↥P ≃ₗ[R] Shrink.{max u ?u.66, u_2} ↥P := (Shrink.linearEquiv R ↥P).symm
this : Module.Finite R (Shrink.{max u ?u.66, u_2} ↥P)
⊢ Injective ⇑(rTensor M (↑se ∘ₗ f.restrict le).range.subtype)

Tactic:
exact (flat_iff R M).mp ‹_› _ (Finite.iff_fg.mp inferInstance)

Goal state after:
Module: Mathlib.Algebra.Azumaya.Matrix

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝³ : CommSemiring R
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Nonempty n
⊢ ∀ {m₁ m₂ : R}, (∀ (a : Matrix n n R), m₁ • a = m₂ • a) → m₁ = m₂

Tactic:
by nontriviality R; exact eq_of_smul_eq_smul

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Indicator

Goal state before:
pp: case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi)).PairwiseDisjoint t
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f = fun a ↦ ∏ i ∈ cons i s hi, (t i).mulIndicator f a

Tactic:
ext j

Goal state after:
case cons
ι : Type u_1
κ : Type u_2
β : Type u_4
inst✝ : CommMonoid β
t : ι → Set κ
f : κ → β
i : ι
s : Finset ι
hi : i ∉ s
ih : (↑s).PairwiseDisjoint t → (⋃ i ∈ s, t i).mulIndicator f = fun a ↦ ∏ i ∈ s, (t i).mulIndicator f a
hs : (↑(cons i s hi)).PairwiseDisjoint t
j : κ
⊢ (⋃ i_1 ∈ cons i s hi, t i_1).mulIndicator f j = ∏ i ∈ cons i s hi, (t i).mulIndicator f j
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ 𝔼 j, (if j = i then ↑(Fintype.card ι) else 0) * f j = f i

Tactic:
@eq_comm _ _ i,

Goal state after:
ι : Type u_1
K : Type u_3
inst✝⁴ : Semifield K
inst✝³ : CharZero K
inst✝² : Fintype ι
inst✝¹ : Nonempty ι
inst✝ : DecidableEq ι
f : ι → K
i : ι
⊢ 𝔼 i_1, (if i = i_1 then ↑(Fintype.card ι) else 0) * f i_1 = f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Powerset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CommMonoid β
s : Finset α
f : Finset α → β
⊢ ∏ t ∈ s.powerset, f t = ∏ j ∈ range (#s + 1), ∏ t ∈ powersetCard j s, f t

Tactic:
by
  rw [powerset_card_disjiUnion, prod_disjiUnion]

Goal state after:
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
N₁ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommMonoid N₁
inst✝² : AddCommMonoid N₂
inst✝¹ : Module R N₁
inst✝ : Module R N₂
ist : Function.Bijective ⇑(TensorProduct.lift f)
e₁ : N₁ ≃ₗ[R] M₁
e₂ : N₂ ≃ₗ[R] M₂
⊢ Function.Bijective ⇑(TensorProduct.lift f ∘ₗ LinearMap.rTensor M₂ ↑e₁ ∘ₗ LinearMap.lTensor N₁ ↑e₂)

Tactic:
exact ist.comp ((e₁.rTensor M₂).bijective.comp (e₂.lTensor N₁).bijective)

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
f : M →ₗ[R] N
h : IsBaseChange S f
m : M
⊢ h.equiv.symm (f m) = 1 ⊗ₜ[R] m

Tactic:
by
  rw [h.equiv.symm_apply_eq, h.equiv_tmul, one_smul]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 < i.2, p s(i.1, i.2)

Tactic:
Finset.offDiag_filter_lt_eq_filter_le

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : { a // a.IsDiag }
⊢ (fun a ↦ ⟨diag a, ⋯⟩) ((fun x ↦ (↑x).diagElem ⋯) x) = x

Tactic:
by ext; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
⊢ diagSet = Set.univ

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToIso p ≪≫ eqToIso q = eqToIso ⋯

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.hom.app X).unop ≫ (e.inv.app X).unop = 𝟙 (Opposite.unop (G.obj X))

Tactic:
rw [← unop_comp, inv_hom_id_app, unop_id]

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
all_split_mono : ∀ {X Y : C} (f : X ⟶ Y), Trunc (IsSplitMono f)
⊢ Groupoid C

Tactic:
apply Groupoid.ofIsIso
  intro X Y f
  have ⟨a,_⟩ := Trunc.exists_rep <| all_split_mono f
  have ⟨b,_⟩ := Trunc.exists_rep <| all_split_mono <| retraction f
  apply IsIso.of_mono_retraction

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F

Tactic:
rw [map_eq_isoClosure, isoClosure_le_iff, strictMap_le_iff_le_inverseImage]

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
FC : C → C → Type t₁
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
FD : D → D → Type t₂
CD : D → Type w
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝² : ConcreteCategory D FD
inst✝¹ : HasForget₂ C D
inst✝ : (forget C).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f

Tactic:
have i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
      have : IsIso ((forget C).map f) := by
        rwa [← @HasForget₂.forget_comp (C := C) (D := D)]
      apply isIso_of_reflects_iso f (forget C)

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
A' : Type u₄
inst✝⁷ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝⁶ : Category.{v₅, u₅} B'
T' : Type u₆
inst✝⁵ : Category.{v₆, u₆} T'
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F₁.EssSurj
inst✝³ : F₂.EssSurj
inst✝² : F.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X : Comma L' R'
⊢ L'.map (F₁.objObjPreimageIso X.left).hom ≫ X.hom =
    L'.map (F₁.objObjPreimageIso X.left).hom ≫
      X.hom ≫ R'.map (F₂.objObjPreimageIso X.right).inv ≫ R'.map (F₂.objObjPreimageIso X.right).hom

Tactic:
rw [← R'.map_comp, Iso.inv_hom_id, R'.map_id, comp_id]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.inv).comp (MonCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
i : X ≅ Y
⊢ (MonCat.Hom.hom i.hom).comp (MonCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.inv).comp (CommMonCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : CommMonCat
i : X ≅ Y
⊢ (CommMonCat.Hom.hom i.hom).comp (CommMonCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
⊢ g₁ = g₂

Tactic:
have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
inst✝ : Mono f
g₁ g₂ : ↑G
h : (ConcreteCategory.hom f) g₁ = (ConcreteCategory.hom f) g₂
t0 : asHom g₁ ≫ f = asHom g₂ ≫ f
t1 : asHom g₁ = asHom g₂
⊢ g₁ = g₂
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
⊢ (GrpCat.Hom.hom i.inv).comp (GrpCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : GrpCat
i : X ≅ Y
⊢ (GrpCat.Hom.hom i.hom).comp (GrpCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
⊢ (CommGrpCat.Hom.hom i.inv).comp (CommGrpCat.Hom.hom i.hom) = MonoidHom.id ↑X

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Basic

Goal state before:
pp: X Y : CommGrpCat
i : X ≅ Y
⊢ (CommGrpCat.Hom.hom i.hom).comp (CommGrpCat.Hom.hom i.inv) = MonoidHom.id ↑Y

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.hom).comp (SemiRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : SemiRingCat
e : R ≅ S
⊢ (SemiRingCat.Hom.hom e.inv).comp (SemiRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.hom).comp (RingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : RingCat
e : R ≅ S
⊢ (RingCat.Hom.hom e.inv).comp (RingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.hom).comp (CommSemiRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommSemiRingCat
e : R ≅ S
⊢ (CommSemiRingCat.Hom.hom e.inv).comp (CommSemiRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.hom).comp (CommRingCat.Hom.hom e.inv) = RingHom.id ↑S

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Basic

Goal state before:
pp: R S : CommRingCat
e : R ≅ S
⊢ (CommRingCat.Hom.hom e.inv).comp (CommRingCat.Hom.hom e.hom) = RingHom.id ↑R

Tactic:
by ext; simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ F.IsLeftAdjoint

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  let iso : F ≅ (F ⋙ G) ⋙ G.asEquivalence.inverse :=
    (Functor.rightUnitor _).symm ≪≫ Functor.isoWhiskerLeft _ G.asEquivalence.unitIso ≪≫
      (Functor.associator _ _ _).symm
  exact isLeftAdjoint_of_iso iso.symm

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
X : C
f : X ⟶ Y
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
rw [e.homEquiv_eq, e'.homEquiv_eq, h]

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
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
rw [e.homEquiv_eq, e'.homEquiv_eq, h]

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
e : Y ≅ X
x✝ : F.RepresentableBy X
⊢ (fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝) = x✝

Tactic:
by ext; simp

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
e : Y ≅ X
x✝ : F.RepresentableBy Y
⊢ (fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝) = x✝

Tactic:
by ext; simp

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
e : Y ≅ X
x✝ : F.CorepresentableBy X
⊢ (fun R ↦ R.ofIsoObj e.symm) ((fun R ↦ R.ofIsoObj e) x✝) = x✝

Tactic:
by ext; simp

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
e : Y ≅ X
x✝ : F.CorepresentableBy Y
⊢ (fun R ↦ R.ofIsoObj e) ((fun R ↦ R.ofIsoObj e.symm) x✝) = x✝

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type (max w v₁)
X✝ : C
R : F.RepresentableBy X✝
X Y : Cᵒᵖ
f : X ⟶ Y
x : (uliftYoneda.{w, v₁, u₁}.obj X✝).obj X
⊢ (ConcreteCategory.hom
          ((uliftYoneda.{w, v₁, u₁}.obj X✝).map f ≫ (equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom)).toFun
      x =
    (ConcreteCategory.hom ((equivEquivIso (Equiv.ulift.trans R.homEquiv)).hom ≫ F.map f)).toFun x

Tactic:
exact R.homEquiv_comp f.unop _

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

Goal state before:
pp: C D : Cat
F : C ⟶ D
⊢ 𝟙 C ≫ F = F

Tactic:
by cases F; rfl

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

Goal state before:
pp: C D : Cat
F : C ⟶ D
⊢ F ≫ 𝟙 D = F

Tactic:
by cases F; rfl

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p ↔ ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)

Tactic:
constructor
  · intro _ φ
    have sq : CommSq φ.left i p φ.right := CommSq.mk φ.w
    exact ⟨{ l := sq.lift }⟩
  · intro h
    exact ⟨fun {f g} sq ↦ ⟨h (Arrow.homMk f g sq.w)⟩⟩

Goal state after: