mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
⊢ Associated (p * q).content (p.content * q.content)

Tactic:
apply h

Goal state after:
case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
⊢ (p * q).degree < ↑?n

case n
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
a✝ : Nontrivial R
h : ∀ (n : ℕ) (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
⊢ ℕ
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ Associated (C p.content * p.primPart * q).content ((C p.content * p.primPart).content * q.content)

Tactic:
q.eq_C_content_mul_primPart

Goal state after:
case neg.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p✝ q✝ : R[X]
a✝ : Nontrivial R
n : ℕ
ih : ∀ (p q : R[X]), (p * q).degree < ↑n → Associated (p * q).content (p.content * q.content)
p q : R[X]
p0 : ¬p = 0
q0 : ¬q = 0
heq : p.primPart.degree + q.primPart.degree = ↑n
⊢ Associated (C p.content * p.primPart * (C q.content * q.primPart)).content
    ((C p.content * p.primPart).content * (C q.content * q.primPart).content)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p % q = p

Tactic:
have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]

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]
h0 : ¬C (p * q).content = 0
| C p.content * p.primPart * q

Tactic:
q.eq_C_content_mul_primPart

Goal state after:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : StrongNormalizedGCDMonoid R
p q : R[X]
h0 : ¬C (p * q).content = 0
| C p.content * p.primPart * (C q.content * q.primPart)
Module: Mathlib.Algebra.Polynomial.FieldDivision

Goal state before:
pp: R : Type u
a : R
inst✝ : Field R
b : R
ha : a ≠ 0
⊢ (C a * X - C b).roots = {a⁻¹ * b}

Tactic:
by
  simp [roots_C_mul_X_sub_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h✝ : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h✝
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ C r.leadingCoeff * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
h :
  r ∣
    C r.leadingCoeff * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r +
      C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
a✝ : Nontrivial R
hC0 : ¬C r.leadingCoeff = 0
⊢ r ∣ s.primPart

Tactic:
sub_add_cancel,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hp : p.IsPrimitive
hq : q.IsPrimitive
h✝ : ∃ n r, r.natDegree = n ∧ r.IsPrimitive ∧ p ∣ r ∧ q ∣ r
r : R[X]
rdeg : r.natDegree = Nat.find h✝
rprim : r.IsPrimitive
pr : p ∣ r
qr : q ∣ r
con : ∃ n s, s.natDegree = n ∧ (p ∣ s ∧ q ∣ s) ∧ ¬r ∣ s
s : R[X]
sdeg : s.natDegree = Nat.find con
rs : ¬r ∣ s
ps : p ∣ s
qs : q ∣ s
s0 : s ≠ 0
hs : r.natDegree ≤ s.natDegree
sC : 0 < s.natDegree
hcancel : (r.cancelLeads s).natDegree < Nat.find con
rcs : r ∣ C r.leadingCoeff * s - C s.leadingCoeff * X ^ (s.natDegree - r.natDegree) * r
h : r ∣ C r.leadingCoeff * s
a✝ : Nontrivial R
hC0 : ¬C r.leadingCoeff = 0
⊢ r ∣ s.primPart
Module: Mathlib.RingTheory.Polynomial.Content

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
⊢ C p.content * p.primPart ∣ q

Tactic:
q.eq_C_content_mul_primPart

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NormalizedGCDMonoid R
p q : R[X]
hq : q ≠ 0
h₁ : p.content ∣ q.content
h₂ : p.primPart ∣ q.primPart
⊢ C p.content * p.primPart ∣ C q.content * q.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
rw [count, dif_pos h₂, prime_pow_le_iff_le_bcount h₁]

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

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
hp : p = 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

pp: case neg
R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q

Tactic:
· simpa [hp] using zero_notMem_normalizedFactors _

Goal state after:
case neg
R : Type u
inst✝¹ : Field R
p q : R[X]
inst✝ : DecidableEq R
hq : q ≠ 0
hp : ¬p = 0
⊢ p ∈ normalizedFactors q ↔ Irreducible p ∧ p.Monic ∧ p ∣ q
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

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

Tactic:
rw [hz]

Goal state after:
case neg.inl
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
a b : Associates α
hb : b ≠ 0
p : Associates α
hp : Irreducible p
hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d
k : ℕ
habk : k ∣ p.count (a * b).factors
ha : ¬a = 0
hz : p.count a.factors = 0
⊢ k ∣ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ a ∣ p ^ ?m.43

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
a p : Associates α
hp : Irreducible p
inst✝ : (n : ℕ) → Decidable (a ∣ p ^ n)
n : ℕ
h : a ∣ p ^ n
⊢ ℕ

Tactic:
exact h

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
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : q - C (q.coeff 0) = X * p
⊢ ∃ t ∈ R[s], ∃ r, r ≠ 0 ∧ s * t = (algebraMap R S) r

Tactic:
refine ⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hRs : IsAlgebraic R s
hs : s ∈ S⁰
q : R[X]
hq0 : q.coeff 0 ≠ 0
hq : (aeval s) q = 0
p : R[X]
hp : q - C (q.coeff 0) = X * p
⊢ s * (aeval s) p = (algebraMap R S) (-q.coeff 0)
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
h : Transcendental R s
⊢ Transcendental R ⟨s, ⋯⟩

Tactic:
rwa [Subalgebra.transcendental_iff_transcendental_val]

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

Goal state before:
pp: case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
⊢ p + C a ≠ 0 → (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A

Tactic:
_ne_zero

Goal state after:
case refine_2
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
a : K
hp : p.coeff 0 = 0
ha : a ≠ 0
_ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p + C a ≠ 0
⊢ (aeval x) (p + C a) = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.RingTheory.Algebraic.Basic

Goal state before:
pp: case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
⊢ p * X ≠ 0 → (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A

Tactic:
_ne_zero

Goal state after:
case refine_3
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
A : Subalgebra K L
x : ↥A
p✝ p : K[X]
hp : p ≠ 0
ih : p ≠ 0 → (aeval x) p = 0 → (↑x)⁻¹ ∈ A
_ne_zero : p * X ≠ 0
⊢ (aeval x) (p * X) = 0 → (↑x)⁻¹ ∈ A
Module: Mathlib.RingTheory.Finiteness.Small

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Small.{u, u_1} R
s : Set M
inst✝ : Small.{u, u_2} ↑s
this : span R s = ⨆ i, R ∙ ↑i
⊢ Small.{u, u_2} ↥(span R s)

Tactic:
rw [this]
    apply small_iSup

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n

Tactic:
rw [restrictDegree, restrictSupport, AddMonoidAlgebra.mem_supported]
  rfl

Goal state after:
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
hg : Surjective ⇑g
h : P → N
hfg : Exact ⇑f ⇑g
hgh : RightInverse h ⇑g
p p' : P
q : Q
⊢ ((TensorProduct.mk R N Q) (h (p + p'))) q -
      (fun x1 x2 ↦ x1 + x2) (((TensorProduct.mk R N Q) (h p)) q) (((TensorProduct.mk R N Q) (h p')) q) ∈
    (rTensor Q f).range

Tactic:
change h (p + p') ⊗ₜ[R] q - (h p ⊗ₜ[R] q + h p' ⊗ₜ[R] q) ∈ range (rTensor Q f)
      rw [← TensorProduct.add_tmul, ← TensorProduct.sub_tmul]
      apply le_comap_range_rTensor f
      rw [exact_iff] at hfg
      simp only [← hfg, mem_ker, map_sub, map_add, hgh _, sub_self]

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

Goal state before:
pp: case a.tmul
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
⊢ a ⊗ₜ[R] ↑b ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
suffices a ⊗ₜ[R] (b : B) = (a ⊗ₜ[R] (1 : B)) * ((1 : A) ⊗ₜ[R] (b : B)) by
          rw [this]
          simp only [Submodule.coe_restrictScalars, SetLike.mem_coe]
          apply Ideal.mul_mem_left
          -- Note: adding `includeRight` as a hint fixes a timeout https://github.com/leanprover-community/mathlib4/pull/8386
          apply Ideal.mem_map_of_mem includeRight
          exact Submodule.coe_mem b

Goal state after:
case a.tmul
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
a : A
b : ↥(Submodule.restrictScalars R I)
⊢ a ⊗ₜ[R] ↑b = a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] ↑b
Module: Mathlib.Algebra.Central.TensorProduct

Goal state before:
pp: K : Type u_1
B : Type u_2
C : Type u_3
inst✝⁴ : CommSemiring K
inst✝³ : Semiring B
inst✝² : Semiring C
inst✝¹ : Algebra K B
inst✝ : Algebra K C
⊢ Subalgebra.map includeLeft (Subalgebra.center K B) ≤ Subalgebra.center K (B ⊗[K] C)

Tactic:
intro x hx
  simp only [Subalgebra.mem_map, Subalgebra.mem_center_iff] at hx ⊢
  obtain ⟨b, hb0, rfl⟩ := hx
  intro bc
  induction bc using TensorProduct.induction_on with
  | zero => simp
  | tmul b' c => simp [hb0]
  | add _ _ _ _ => simp_all [add_mul, mul_add]

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
inst✝ : Small.{v', u} R
h :
  ∀ ⦃N N' : Type v'⦄ [inst : AddCommMonoid N] [inst_1 : AddCommMonoid N'] [inst_2 : Module R N] [inst_3 : Module R N']
    (f : N →ₗ[R] N'), Injective ⇑f → Injective ⇑(rTensor M f)
P : Type u
x✝⁴ : AddCommMonoid P
x✝³ : Module R P
x✝² : Module.Finite R P
x✝¹ : Submodule R P
x✝ : x✝¹.FG
this : Small.{v', u} P
⊢ Injective ⇑(rTensor M (↑(Shrink.linearEquiv R P).symm ∘ₗ x✝¹.subtype).range.subtype)

Tactic:
exact h _ Subtype.val_injective

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

Goal state before:
pp: case mp
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P) (i : ι),
    Injective ⇑(rTensor (M i) N.subtype)
i✝ : ι
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)

Tactic:
apply h

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁴ : CommSemiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
h :
  ∀ (i : ι) ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P),
    Injective ⇑(rTensor (M i) N.subtype)
P✝ : Type u
inst✝¹ : AddCommMonoid P✝
inst✝ : Module R P✝
N✝ : Submodule R P✝
i✝ : ι
⊢ Injective ⇑(rTensor (M i✝) N✝.subtype)

Tactic:
apply h

Goal state after:
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
this✝ : AddCommGroup P := addCommMonoidToAddCommGroup R
this : AddCommGroup N := addCommMonoidToAddCommGroup R
⊢ ∀ (f : P →ₗ[R] N), Injective ⇑f → Injective ⇑(rTensor M f)

Tactic:
apply h

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
s : Finset α
inst✝ : Nonempty α
⊢ s.dens = 1 ↔ s = univ

Tactic:
simp [dens, div_eq_one_iff_eq, card_eq_iff_eq_univ]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s t : Finset α
⊢ (s ∩ t).dens + (s ∪ t).dens = s.dens + t.dens

Tactic:
rw [add_comm, dens_union_add_dens_inter]

Goal state after:
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 : ι
⊢ ((↑(Fintype.card ι))⁻¹ • ∑ x, if i = x then ↑(Fintype.card ι) * f x else 0) = f i

Tactic:
sum_ite_eq,

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 : ι
⊢ ((↑(Fintype.card ι))⁻¹ • if i ∈ univ then ↑(Fintype.card ι) * f i else 0) = f i
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
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 : N
s : S
n : N
e' : g₁ n = g₂ n
⊢ g₁ (s • n) = g₂ (s • n)

Tactic:
g₁.map_smul,

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
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 : N
s : S
n : N
e' : g₁ n = g₂ n
⊢ s • g₁ n = g₂ (s • n)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
hinj : Injective f
⊢ Injective (map f)

Tactic:
intro z z'
  refine Sym2.inductionOn₂ z z' (fun x y x' y' => ?_)
  simp [hinj.eq_iff]

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
X Y : V
f g : X ⟶ Y
h : homOfEq f ⋯ ⋯ = homOfEq g ⋯ ⋯
⊢ f = g

Tactic:
exact h

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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
f : X ⟶ Y
inst✝ : IsIso f
⊢ F.map (inv f) = inv (F.map f)

Tactic:
by
  apply eq_inv_of_hom_inv_id
  simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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

Tactic:
cases h₂ with

Goal state after:
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F G : C ⥤ D
X✝ Y✝ : C
app : (X : C) → F.obj X ≅ G.obj X
naturality : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≫ (app Y).hom = (app X).hom ≫ G.map f
X Y : C
f : X ⟶ Y
h : G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f
⊢ G.map f ≫ (app Y).inv = (app X).inv ≫ F.map f

Tactic:
exact h

Goal state after:
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✝ : C ⥤ D
G : D ⥤ E
inst✝¹ : F✝.EssSurj
F : C ⥤ D
inst✝ : F.Faithful
⊢ F.toEssImage.Faithful

Tactic:
dsimp only [Functor.toEssImage]

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✝ : C ⥤ D
G : D ⥤ E
inst✝¹ : F✝.EssSurj
F : C ⥤ D
inst✝ : F.Faithful
⊢ (F.essImage.lift F ⋯).Faithful
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✝ : C ⥤ D
G : D ⥤ E
inst✝¹ : F✝.EssSurj
F : C ⥤ D
inst✝ : F.Full
⊢ F.toEssImage.Full

Tactic:
dsimp only [Functor.toEssImage]

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✝ : C ⥤ D
G : D ⥤ E
inst✝¹ : F✝.EssSurj
F : C ⥤ D
inst✝ : F.Full
⊢ (F.essImage.lift F ⋯).Full
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
⊢ eqToHom p ≫ eqToHom q = eqToHom ⋯

Tactic:
cases p
  cases q
  simp

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.left (aux φ ≫ sq) = Hom.left (aux ψ ≫ sq)

Tactic:
exact h

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (ConcreteCategory.hom ((forget₂ C D).map (f ≫ g))) x =
    (ConcreteCategory.hom ((forget₂ C D).map g)) ((ConcreteCategory.hom ((forget₂ C D).map f)) x)

Tactic:
rw [Functor.map_comp, CategoryTheory.comp_apply]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
inst✝ : HasForget₂ C D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x : ToType ((forget₂ C D).obj X)
⊢ (hom ((forget₂ C D).map (f ≫ g))) x = (hom ((forget₂ C D).map g)) ((hom ((forget₂ C D).map f)) x)

Tactic:
rw [Functor.map_comp, CategoryTheory.comp_apply]

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

Goal state before:
pp: m : Type u → Type v
inst✝¹ : _root_.Functor m
inst✝ : LawfulFunctor m
α : Type u
X : m α
⊢ (ConcreteCategory.hom (↾_root_.Functor.map ⇑(Hom.hom (𝟙 α)))).toFun X = (ConcreteCategory.hom (𝟙 (m α))).toFun X

Tactic:
apply id_map

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

Tactic:
Z

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
Z

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
⊢ ∀ {Z : C} (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)

Tactic:
Z

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
⊢ ∀ (e : X ≅ Y) (f : Y ⟶ Z), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (e.hom ≫ f)