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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
m p : Associates α
h₁ : m ≠ 0
h₂ : Irreducible p
k : ℕ
⊢ p ^ k ≤ m ↔ k ≤ bcount ⟨p, h₂⟩ m.factors

Tactic:
rcases Associates.exists_non_zero_rep h₁ with ⟨m, hm, rfl⟩

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : DecidableEq (Associates α)
p : Associates α
h₂ : Irreducible p
k : ℕ
m : α
hm : m ≠ 0
h₁ : Associates.mk m ≠ 0
⊢ p ^ k ≤ Associates.mk m ↔ k ≤ bcount ⟨p, h₂⟩ (Associates.mk m).factors
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: case pos
F : Type u_1
inst✝ : DivisionSemiring F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible 0
hf : C x = f
hx : x = 0
⊢ False

Tactic:
exact not_irreducible_zero h

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b c : Associates α
ha : a ≠ 0
hb : b ≠ 0
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, a = d ^ k

Tactic:
nontriviality α
  by_cases hk0 : k = 0
  · use 1
    rw [hk0, pow_zero] at h ⊢
    apply (mul_eq_one.1 h).1
  · refine is_pow_of_dvd_count ha fun p hp ↦ ?_
    apply dvd_count_of_dvd_count_mul hb hp hab
    rw [h]
    apply dvd_count_pow _ hp
    rintro rfl
    rw [zero_pow hk0] at h
    cases mul_eq_zero.mp h <;> contradiction

Goal state after:
Module: Mathlib.Algebra.Central.Basic

Goal state before:
pp: k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
H : (algebraMap K D) x ∈ ↑(Subalgebra.center k D)
⊢ ∃ a, (algebraMap k K) a = x

Tactic:
simp only [center_eq_bot, coe_bot, Set.mem_range] at H

Goal state after:
k : Type u_1
K : Type u_2
D : Type u_3
inst✝⁸ : Field k
inst✝⁷ : Field K
inst✝⁶ : Ring D
inst✝⁵ : Nontrivial D
inst✝⁴ : Algebra k K
inst✝³ : Algebra K D
inst✝² : Algebra k D
inst✝¹ : IsScalarTower k K D
inst✝ : IsCentral k D
this : IsCentral K D
x : K
H : ∃ y, (algebraMap k D) y = (algebraMap K D) x
⊢ ∃ a, (algebraMap k K) a = x
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ g ((aeval a) q) = g 0

Tactic:
change (g : A →+* B) _ = _

Goal state after:
R : Type u
S : Type u_1
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Ring A
inst✝⁶ : Algebra R A
B : Type u_2
inst✝⁵ : Ring B
inst✝⁴ : Algebra S B
FRS : Type u_3
FAB : Type u_4
inst✝³ : FunLike FRS R S
inst✝² : RingHomClass FRS R S
inst✝¹ : FunLike FAB A B
inst✝ : RingHomClass FAB A B
f : FRS
g : FAB
a : A
hf : Function.Surjective ⇑f
hg : Function.Injective ⇑g
h : (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A)
q : R[X]
h1 : map (↑f) q ≠ 0
h2 : (aeval (↑g a)) (map (↑f) q) = 0
⊢ ↑g ((aeval a) q) = g 0
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
p : K[X]
aeval_eq : (aeval x) p = 0
coeff_zero_ne : p.coeff 0 ≠ 0
⊢ x⁻¹ = -((aeval x) p.divX / (algebraMap K L) (p.coeff 0))

Tactic:
convert!
    inv_eq_of_aeval_divX_ne_zero (p := p) (L := L)
      (mt (fun h => (algebraMap K L).injective ?_) coeff_zero_ne) using 1
  · rw [aeval_eq, zero_sub, div_neg]
  rw [RingHom.map_zero]
  convert! aeval_eq
  conv_rhs => rw [← divX_mul_X_add p]
  rw [map_add, map_mul, h, zero_mul, zero_add, aeval_C]

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
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
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)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
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)
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 : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : (i : ι) × F₁ i
w : (i : ι) × F₂ i
j : ι
hzj : z.fst ≤ j
hwj : w.fst ≤ j
k : ι
hzk : z.fst ≤ k
hwk : w.fst ≤ k
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ z.fst j hzj) z.snd)) ((f₂ j i hji) ((f₂ w.fst j hwj) w.snd)) =
    ih k ((f₁ z.fst k hzk) z.snd) ((f₂ w.fst k hwk) w.snd)

Tactic:
compat _ _ hki,

Goal state after:
ι : Type u_1
inst✝⁷ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
F : ι → Type u_4
X : ι → Type u_5
T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6
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)
T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7
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)
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 : Sort u_9
ih : (i : ι) → F₁ i → F₂ i → C
compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)
z : (i : ι) × F₁ i
w : (i : ι) × F₂ i
j : ι
hzj : z.fst ≤ j
hwj : w.fst ≤ j
k : ι
hzk : z.fst ≤ k
hwk : w.fst ≤ k
i : ι
hji : j ≤ i
hki : k ≤ i
⊢ ih i ((f₁ j i hji) ((f₁ z.fst j hzj) z.snd)) ((f₂ j i hji) ((f₂ w.fst j hwj) w.snd)) =
    ih i ((f₁ k i hki) ((f₁ z.fst k hzk) z.snd)) ((f₂ k i hki) ((f₂ w.fst k hwk) w.snd))
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
inst✝ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
i : ι
x : M ⊗[R] G i
⊢ (LinearMap.lTensor M (f i i ⋯)) x = x

Tactic:
by
    convert! LinearMap.lTensor_id_apply M _ x; ext; apply DirectedSystem.map_self'

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
⊢ (lTensor Q g).range = (lTensor Q g.range.subtype).range

Tactic:
have : g = (Submodule.subtype _).comp g.rangeRestrict := rfl
  nth_rewrite 1 [this]
  rw [lTensor_comp]
  apply range_comp_of_range_eq_top
  rw [range_eq_top]
  apply lTensor_surjective
  rw [← range_eq_top, range_rangeRestrict]

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

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(map g g')

Tactic:
← lTensor_comp_rTensor,

Goal state after:
R : Type u_1
inst✝⁸ : CommSemiring R
N : Type u_3
P : Type u_4
inst✝⁷ : AddCommMonoid N
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R N
inst✝⁴ : Module R P
g : N →ₗ[R] P
hg : Function.Surjective ⇑g
N' : Type u_6
P' : Type u_7
inst✝³ : AddCommMonoid N'
inst✝² : AddCommMonoid P'
inst✝¹ : Module R N'
inst✝ : Module R P'
g' : N' →ₗ[R] P'
hg' : Function.Surjective ⇑g'
⊢ Function.Surjective ⇑(lTensor P g' ∘ₗ rTensor N' g)
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
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
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'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ (lTensor P g').ker = (map g f').range

Tactic:
← lTensor_comp_rTensor,

Goal state after:
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
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
M' : Type u_6
N' : Type u_7
P' : Type u_8
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'
hfg' : Exact ⇑f' ⇑g'
hg' : Surjective ⇑g'
⊢ (lTensor P g').ker = (lTensor P f' ∘ₗ rTensor M' g).range
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_2
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)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x : M
y : N
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x ⊗ₜ[R] y) s ⊆ ↑(mapIncl M' N').range

Tactic:
refine ⟨_, _, hM'.sup (fg_span_singleton x),
      hN'.sup (fg_span_singleton y), Set.insert_subset ?_ fun z hz ↦ ?_⟩
    · exact ⟨⟨x, mem_sup_right (mem_span_singleton_self x)⟩ ⊗ₜ
        ⟨y, mem_sup_right (mem_span_singleton_self y)⟩, rfl⟩
    · exact range_mapIncl_mono le_sup_left le_sup_left (h hz)

Goal state after:
Module: Mathlib.RingTheory.Adjoin.FGBaseChange

Goal state before:
pp: case refine_1
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ (Algebra.adjoin R ↑(Finset.image (fun j ↦ j.2) S)).FG

pp: case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ x ∈ Subalgebra.baseChange A (Algebra.adjoin R ↑(Finset.image (fun j ↦ j.2) S))

Tactic:
· exact Subalgebra.fg_adjoin_finset _

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
x : A ⊗[R] B
S : Finset (A × B)
hS : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2
⊢ x ∈ Subalgebra.baseChange A (Algebra.adjoin R ↑(Finset.image (fun j ↦ j.2) S))
Module: Mathlib.RingTheory.Nilpotent.Defs

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

Tactic:
use hr.choose
  rw [← map_pow, hr.choose_spec, map_zero]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ LinearIndependent S fun x ↦ 1 ⊗ₜ[R] v x

Tactic:
rw [LinearIndependent, ← LinearMap.coe_restrictScalars R,
    Finsupp.linearCombination_one_tmul]

Goal state after:
R : Type u
M : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Flat R S
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
⊢ Injective ⇑(lTensor S (Finsupp.linearCombination R v) ∘ₗ ↑(finsuppScalarRight R R S ι).symm)
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P N : Type v'
x✝³ : AddCommMonoid P
x✝² : AddCommMonoid N
x✝¹ : Module R P
x✝ : Module R N
⊢ ∀ (f : P →ₗ[R] N), Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
by
      let := Module.addCommMonoidToAddCommGroup R (M := P)
      let := Module.addCommMonoidToAddCommGroup R (M := N)
      apply h

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✝⁴ : Zero R
inst✝³ : (i : ι) → Zero (G i)
inst✝² : (i : ι) → SMulWithZero R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0 • x✝⟩⟧ = 0

Tactic:
zero_smul,

Goal state after:
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✝⁴ : Zero R
inst✝³ : (i : ι) → Zero (G i)
inst✝² : (i : ι) → SMulWithZero R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0⟩⟧ = 0
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✝³ : 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)
x✝¹ : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass (T h) R (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0 • x✝⟩⟧ = 0

Tactic:
zero_smul,

Goal state after:
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✝³ : 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)
x✝¹ : ∀ (i j : ι) (h : i ≤ j), DistribMulActionHomClass (T h) R (G i) (G j)
i : ι
x✝ : G i
⊢ ⟦⟨i, 0⟩⟧ = 0
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (Even (∑ x ∈ s with Even (f x), f x) ↔ Even (∑ x ∈ s with ¬Even (f x), f x)) ↔ Even #({x ∈ s | Odd (f x)})

Tactic:
simp only [Finset.mem_filter, and_imp, imp_self, implies_true, Finset.even_sum, true_iff]

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ Even (∑ x ∈ s with ¬Even (f x), f x) ↔ Even #({x ∈ s | Odd (f x)})
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset | f a = m}) = Nat.card ↑{a | f a = m}

Tactic:
rw [Nat.card_eq_card_finite_toFinset (hb _ (by aesop))]
    suffices {a | f a = m} ⊆ ht.toFinset from
      congr_arg (Finset.card ·) (Finset.ext_iff.mpr fun a ↦ by simpa using fun h ↦ this h)
    intro _ h
    simp_all

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : Fintype α
x : Sym2 α
⊢ x ∈ univ.sym2

Tactic:
mem_sym2_iff

Goal state after:
α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : Fintype α
x : Sym2 α
⊢ ∀ a ∈ x, a ∈ univ
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
M : Type v₁
N : Type v₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : CommSemiring R
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
Q : Type (max v₁ v₂ u_1)
I₁ : AddCommMonoid Q
I₂ I₃ : Module R Q
I₄ : IsScalarTower R R Q
g : M →ₗ[R] Q
r : R
q : Q
⊢ Q

Tactic:
let _ := I₃; exact r • q

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ (f ⁻¹' s).sym2 = Sym2.map f ⁻¹' s.sym2

Tactic:
by
  ext ⟨x, y⟩
  simp

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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
⊢ ∀ (n : S'), f n = g n → f (s • n) = g (s • n)

Tactic:
s'

Goal state after:
case refine_3
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
s' : S'
⊢ f s' = g s' → f (s • s') = g (s • s')
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty C
h : ∀ (i : ι), P (X i)
⊢ ofObj X ≤ P

Tactic:
by rintro _ ⟨i⟩; exact h i

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
X : C
P : ObjectProperty C
⊢ singleton X ≤ P ↔ P X

Tactic:
simp [ofObj_le_iff]

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

Goal state before:
pp: case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : (p.cons q).length = 0 + 1
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1

Tactic:
rw [length_cons, Nat.zero_add, Nat.add_eq_right] at hp

Goal state after:
case cons.zero
V : Type u
inst✝ : Quiver V
a b c d : V
p : Path a c
q : c ⟶ d
h : ∀ {n : ℕ}, p.length = n + 1 → ∃ c_1 f q x, p = f.toPath.comp q
hp : p.length = 0
⊢ ∃ c_1 f q_1 x, p.cons q = f.toPath.comp q_1
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ (eqToHom h).op = eqToHom ⋯

Tactic:
cases h
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
h : X = Y
⊢ (eqToHom h).unop = eqToHom ⋯

Tactic:
cases h
  rfl

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
A B : T
f g : A ⟶ B
h : mk f = mk g
⊢ f = g

Tactic:
cases h
  rfl

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

Goal state before:
pp: case a
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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
⊢ P ≤ ((P.map F).map G).inverseImage (F ⋙ G)

Tactic:
intro X Y f hf

Goal state after:
case a
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
E : Type u_2
inst✝ : Category.{v_2, u_2} E
G : D ⥤ E
X Y : C
f : X ⟶ Y
hf : P f
⊢ ((P.map F).map G).inverseImage (F ⋙ G) f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P.inverseImage E.functor ≤ P.map E.inverse

Tactic:
intro X Y f hf

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : C
f : X ⟶ Y
hf : P.inverseImage E.functor f
⊢ P.map E.inverse f
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
⊢ P ≤ (P.inverseImage E.functor).inverseImage E.inverse

Tactic:
intro X Y f hf

Goal state after:
case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
f : X ⟶ Y
hf : P f
⊢ (P.inverseImage E.functor).inverseImage E.inverse f
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)

Tactic:
simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
t : F.obj X
⊢ uliftYonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) =
    uliftYoneda.{w, v₁, u₁}.map f.unop ≫ uliftYonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := uliftYonedaEquiv.surjective t
  rw [uliftYonedaEquiv_naturality]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (coyonedaEquiv f) = (ConcreteCategory.hom (f.app Y)) g

Tactic:
rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp, Category.comp_id, tX.hom_ext (k ≫ tX.from j') (tX.from j)]

Goal state after: