mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Goal state before:
pp: case inr
α : Type u_1
inst✝⁷ : CommMonoidWithZero α
inst✝⁶ : NormalizationMonoid α
inst✝⁵ : UniqueFactorizationMonoid α
β : Type u_2
inst✝⁴ : CommMonoidWithZero β
inst✝³ : NormalizationMonoid β
inst✝² : UniqueFactorizationMonoid β
F : Type u_3
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
he : ∀ (x : α), normalize (f x) = f (normalize x)
a x : α
ha : a ≠ 0
⊢ x ∈ normalizedFactors a ↔ ↑f x ∈ normalizedFactors (f a)

Tactic:
· simp [mem_normalizedFactors_iff' ha,
        mem_normalizedFactors_iff' (EmbeddingLike.map_ne_zero_iff.mpr ha), map_dvd_iff_dvd_symm,
        MulEquiv.irreducible_iff, he]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p : R[X]
n : ℕ
⊢ p.content ∣ p.coeff n

Tactic:
by
  by_cases h : n ∈ p.support
  · apply Finset.gcd_dvd h
  rw [mem_support_iff, Classical.not_not] at h
  rw [h]
  apply dvd_zero

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
a : S
⊢ a ∈ p.aroots S ↔ map (algebraMap T S) p ≠ 0 ∧ (aeval a) p = 0

Tactic:
rw [mem_roots', IsRoot.def, ← eval₂_eq_eval_map, aeval_def]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ C (↑(normUnit r)⁻¹ * ↑(normUnit r)) = 1

Tactic:
Units.inv_mul,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ C 1 = 1
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ∃ u, ↑u = (C r).primPart

Tactic:
refine
    ⟨⟨C ↑(normUnit r)⁻¹, C ↑(normUnit r), by rw [← map_mul, Units.inv_mul, C_1], by
        rw [← map_mul, Units.mul_inv, C_1]⟩,
      ?_⟩

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
r : R
h0 : ¬r = 0
⊢ ↑{ val := C ↑(normUnit r)⁻¹, inv := C ↑(normUnit r), val_inv := ⋯, inv_val := ⋯ } = (C r).primPart
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ C (↑(normUnit p.leadingCoeff)⁻¹ * ↑(normUnit p.leadingCoeff)) = 1

Tactic:
Units.inv_mul,

Goal state after:
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : NormalizationMonoid R
p : R[X]
⊢ C 1 = 1
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
p : A[X]
f : A →+* B
hmap : map f p ≠ 0
a : A
⊢ rootMultiplicity a p ≤ rootMultiplicity (f a) (map f p)

Tactic:
by
  rw [le_rootMultiplicity_iff hmap]
  refine _root_.trans ?_ (_root_.map_dvd (mapRingHom f) (pow_rootMultiplicity_dvd p a))
  rw [map_pow, map_sub, coe_mapRingHom, map_X, map_C]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ Multiset.map (⇑f) p.roots ≤ (map f p).roots

Tactic:
exact Multiset.le_iff_count.2 fun b => by
    rw [count_roots]
    apply count_map_roots h

Goal state after:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case pos
A : Type u_3
B : Type u_4
inst✝² : Semiring A
inst✝¹ : CommRing B
inst✝ : IsDomain B
f : A →+* B
p : A[X]
hp0 : p ≠ 0
hpm0 : map f p = 0
⊢ ↑(map f p).roots.card ≤ p.degree

Tactic:
simp [hp0, hpm0, zero_le_degree_iff]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
⊢ normalize (p.content * q.content) = p.content * q.content

Tactic:
simp [normalize_content]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
ha : ¬a = 0
hb : b = 0
⊢ p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors

Tactic:
simp [hb]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsAlgebraic R a
⊢ Nontrivial R

Tactic:
by
  contrapose! h
  apply is_transcendental_of_subsingleton

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : A
n : ℕ
hn : 0 < n
ht : IsAlgebraic R (r ^ n)
p : R[X]
p_nonzero : p ≠ 0
hp : (aeval (r ^ n)) p = 0
⊢ ?m.40 p p_nonzero hp ≠ 0

Tactic:
by rwa [expand_ne_zero hn]

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
s : Set S
inst✝ : Small.{u, u_2} ↑s
⊢ Small.{u, u_2} ↥(adjoin R s)

Tactic:
rw [Algebra.adjoin_eq_range]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Small.{u, u_1} R
s : Set S
inst✝ : Small.{u, u_2} ↑s
⊢ Small.{u, u_2} ↥(aeval Subtype.val).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg hgh) ((rTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
by
  simp only [← LinearMap.comp_apply, ← Submodule.mkQ_apply]
  rw [exact_iff] at hfg
  apply LinearMap.congr_fun
  apply TensorProduct.ext'
  intro n q
  suffices Submodule.Quotient.mk (h (g n) ⊗ₜ[R] q) = Submodule.Quotient.mk (n ⊗ₜ[R] q) by simpa
  rw [Submodule.Quotient.eq, ← TensorProduct.sub_tmul]
  apply le_comap_range_rTensor f
  rw [← hfg, mem_ker, map_sub, sub_eq_zero, hgh]

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Defs

Goal state before:
pp: R : Type u_1
x : R
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
⊢ 0 < nilpotencyClass x ↔ IsNilpotent x

Tactic:
by
  refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩
  replace hx := pow_nilpotencyClass hx
  rw [hx', pow_zero] at hx
  exact one_ne_zero hx

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
Q : Type u_3
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✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝⁴ : Type u
x✝³ : AddCommMonoid x✝⁴
x✝² : Module R x✝⁴
x✝¹ : Module.Finite R x✝⁴
I : Submodule R x✝⁴
x✝ : I.FG
⊢ Injective ⇑(rTensor R I.subtype)

Tactic:
by
    rw [← (TensorProduct.rid R I).symm.injective_comp, ← (TensorProduct.rid R _).comp_injective]
    convert! Subtype.coe_injective using 1
    ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ LinearIndependent R fun i ↦ v i.1 ⊗ₜ[R] w i.2

Tactic:
LinearIndependent

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
ι : Type u_6
κ : Type u_7
v : ι → M
w : κ → N
inst✝ : Module.Flat R M
hv : LinearIndependent R v
hw : LinearIndependent R w
⊢ Function.Injective ⇑(Finsupp.linearCombination R fun i ↦ v i.1 ⊗ₜ[R] w i.2)
Module: Mathlib.Data.Finset.Density

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ (↑(#s) + ↑(#t)) / ↑(Fintype.card α) = ↑(#s) / ↑(Fintype.card α) + ↑(#t) / ↑(Fintype.card α)

Tactic:
add_div

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
inst✝⁶ : Module.Flat R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
reg : IsSMulRegular M x
⊢ IsSMulRegular N ((algebraMap R S) x)

Tactic:
have h := hf.map_id_injective_of_flat_left hf (LinearMap.lsmul R M x) reg

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
inst✝⁶ : Module.Flat R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
x : R
reg : IsSMulRegular M x
h : Function.Injective ⇑(IsTensorProduct.map hf hf LinearMap.id ((LinearMap.lsmul R M) x))
⊢ IsSMulRegular N ((algebraMap R S) x)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
⊢ IsReduced (C ⊗[R] A)

Tactic:
by_contra h_contra

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
⊢ False
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
⊢ ¬∀ (x : C ⊗[R] ↥D), IsNilpotent x → x = 0

Tactic:
not_forall

Goal state after:
R : Type u_1
C : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring C
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Module.Flat R C
h : ∀ (B : Subalgebra R A), B.FG → IsReduced (C ⊗[R] ↥B)
h_contra : ¬IsReduced (C ⊗[R] A)
D : Subalgebra R A
h_inj : Function.Injective ⇑(Algebra.TensorProduct.map (AlgHom.id C C) D.val)
z : C ⊗[R] ↥D
hx :
  (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ≠ 0 ∧
    IsNilpotent ((Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z)
hD : D.FG ∧ (Algebra.TensorProduct.map (AlgHom.id C C) D.val).toRingHom z ∈ Subalgebra.baseChange C D
⊢ ∃ x, ∃ (_ : IsNilpotent x), ¬x = 0
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ i ∈ image (fun x ↦ x % a) (Ico n (n + a)) ↔ i ∈ Ico 0 a

Tactic:
simp only [mem_image, mem_Ico]

Goal state after:
case inr
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
⊢ (∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i) ↔ 0 ≤ i ∧ i < a
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : Sym2.Mem x (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x (Quot.mk (Rel α) (x', y'))
hy : Sym2.Mem y (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y (Quot.mk (Rel α) (x', y'))
hx' : Sym2.Mem x' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x' (Quot.mk (Rel α) (x', y'))
hy' : Sym2.Mem y' (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem y' (Quot.mk (Rel α) (x', y'))
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')

Tactic:
simp only [mem_iff'] at hx hy hx' hy'

Goal state after:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
z z' : Sym2 α
x y x' y' : α
h : ∀ (x_1 : α), Sym2.Mem x_1 (Quot.mk (Rel α) (x, y)) ↔ Sym2.Mem x_1 (Quot.mk (Rel α) (x', y'))
hx : True ∨ x = y ↔ x = x' ∨ x = y'
hy : y = x ∨ True ↔ y = x' ∨ y = y'
hx' : x' = x ∨ x' = y ↔ True ∨ x' = y'
hy' : y' = x ∨ y' = y ↔ y' = x' ∨ True
⊢ Quot.mk (Rel α) (x, y) = Quot.mk (Rel α) (x', y')
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ (α ≪≫ β) ≪≫ γ = α ≪≫ β ≪≫ γ

Tactic:
ext; simp only [trans_hom, Category.assoc]

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.length ≠ 0 ↔ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1

case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c e p', p = e.toPath.comp p' ∧ p.length = p'.length + 1) → p.length ≠ 0
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.length ≠ 0 ↔ ∃ c p' e, p = p'.cons e

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Goal state after:
case refine_1
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.length ≠ 0
⊢ ∃ c p' e, p = p'.cons e

case refine_2
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ (∃ c p' e, p = p'.cons e) → p.length ≠ 0
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ (P.strictMap F).isoClosure = P.map F

Tactic:
refine le_antisymm ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ (P.strictMap F).isoClosure ≤ P.map F

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
⊢ P.map F ≤ (P.strictMap F).isoClosure
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
⊢ Function.Surjective F.map

Tactic:
ψ

Goal state after:
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₂
⊢ ∃ a, F.map a = ψ
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.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 [← Iso.hom_inv_id_assoc (e.unitIso.app _) (e.inverse.map (e.functor.map _)), Iso.app_hom,
    Iso.app_inv]

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.unitIso.hom.app (e.inverse.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
            e.unitIso.inv.app (e.inverse.1 (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.functor.map (e.unit.app (e.inverse.obj Y)))) ≫
            e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.unitIso.inv.app (e.inverse.1 (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:
slice_lhs 4 4 =>
    rw [← Iso.hom_inv_id_assoc (e.inverse.mapIso (e.counitIso.app _)) (e.unitInv.app _)]

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.map (e.functor.map (e.inverse.map (e.counitInv.app (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)))))).hom ≫
                (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: case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
    e.inverse.map (e.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv

pp: case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
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)

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))

Tactic:
rw [← map_comp e.inverse]

Goal state after:
case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map
    (e.functor.map (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y)))) ≫
      e.counitIso.hom.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| (e.inverse.mapIso (e.counitIso.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))).inv

case a.a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
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)

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y)))
Module: Mathlib.CategoryTheory.Equivalence

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| 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

pp: case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

pp: case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

pp: case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

pp: case a
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)

Tactic:
dsimp only [Functor.mapIso_inv, Iso.app_inv]

Goal state after:
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unit.app (e.inverse.obj Y))) ≫
    e.inverse.map (e.counitIso.inv.app (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.unitInv.app (e.inverse.obj (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))

case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))

case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
| e.inverse.map (e.counit.app Y)

case a
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)
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 : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ η ≫ (unop G).rightOpLeftOpIso.hom.op =
    (unop F).rightOpLeftOpIso.hom.op ≫ (NatTrans.leftOp (NatTrans.rightOp η.unop)).op

Tactic:
rw [show η = η.unop.op by simp, ← op_comp, ← op_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : (Cᵒᵖ ⥤ D)ᵒᵖ
η : F ⟶ G
⊢ ((unop G).rightOpLeftOpIso.hom ≫ η.unop).op =
    (NatTrans.leftOp (NatTrans.rightOp η.unop.op.unop) ≫ (unop F).rightOpLeftOpIso.hom).op
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
X Y : C
α : X ≅ Y
f : Aut X
⊢ F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)

Tactic:
ext; simp only [mapIso_hom, Iso.conjAut_hom, F.map_conj]

Goal state after: