mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mp.refine_1
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ 0 < (hu.unit⁻¹ • q).degree

pp: case mp.refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ (hu.unit⁻¹ • q).degree ≤ ↑(p.natDegree / 2)

pp: case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q

Tactic:
· rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]

Goal state after:
case mp.refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ (hu.unit⁻¹ • q).degree ≤ ↑(p.natDegree / 2)

case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: case mp.refine_2
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ (hu.unit⁻¹ • q).degree ≤ ↑(p.natDegree / 2)

pp: case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q

Tactic:
· rwa [degree_smul_of_smul_regular _ (isSMulRegular_of_group _)]

Goal state after:
case mp.refine_3
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
p_monic : p.Monic
p_1 : p ≠ 1
h : ∀ (q : R[X]), q.Monic → 0 < q.degree → q.degree ≤ ↑(p.natDegree / 2) → ¬q ∣ p
q : R[X]
deg_le : q.degree ≤ ↑(p.natDegree / 2)
dvd : q ∣ p
q_unit : ¬IsUnit q
this : 0 < q.degree
hu : IsUnit q.leadingCoeff
⊢ hu.unit⁻¹ • q ∣ q
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
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
⊢ (p.primPart.eraseLead * q.primPart).degree < ↑n

Tactic:
← heq,

Goal state after:
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
⊢ (p.primPart.eraseLead * q.primPart).degree < p.primPart.degree + q.primPart.degree
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
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
⊢ (p.primPart * q.primPart.eraseLead).degree < ↑n

Tactic:
← heq,

Goal state after:
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
⊢ (p.primPart * q.primPart.eraseLead).degree < p.primPart.degree + q.primPart.degree
Module: Mathlib.Algebra.Polynomial.Roots

Goal state before:
pp: 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
⊢ ↑(map f p).roots.card ≤ p.degree

Tactic:
by_cases hpm0 : p.map f = 0
  · simp [hp0, hpm0, zero_le_degree_iff]
  exact card_roots hpm0 |>.trans degree_map_le

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
inst✝ : WfDvdMonoid R
f : R[X]
⊢ WellFounded DvdNotUnit

Tactic:
refine
        RelHomClass.wellFounded
          (⟨fun p : R[X] =>
              ((if p = 0 then ⊤ else ↑p.degree : WithTop (WithBot ℕ)), p.leadingCoeff), ?_⟩ :
            DvdNotUnit →r Prod.Lex (· < ·) DvdNotUnit)
          (wellFounded_lt.prod_lex ‹WfDvdMonoid R›.wf)
      rintro a b ⟨ane0, ⟨c, ⟨not_unit_c, rfl⟩⟩⟩
      rw [Polynomial.degree_mul, if_neg ane0]
      split_ifs with hac
      · rw [hac, Polynomial.leadingCoeff_zero]
        apply Prod.Lex.left
        exact WithTop.coe_lt_top _
      have cne0 : c ≠ 0 := right_ne_zero_of_mul hac
      simp only [Polynomial.leadingCoeff_mul]
      by_cases hdeg : c.degree = (0 : ℕ)
      · simp only [hdeg, Nat.cast_zero, add_zero]
        refine Prod.Lex.right _ ⟨?_, ⟨c.leadingCoeff, fun unit_c => not_unit_c ?_, rfl⟩⟩
        · rwa [Ne, Polynomial.leadingCoeff_eq_zero]
        rw [Polynomial.isUnit_iff, Polynomial.eq_C_of_degree_eq_zero hdeg]
        use c.leadingCoeff, unit_c
        rw [Polynomial.leadingCoeff, Polynomial.natDegree_eq_of_degree_eq_some hdeg]
      · apply Prod.Lex.left
        rw [Polynomial.degree_eq_natDegree cne0] at *
        simp only [Nat.cast_inj] at hdeg
        rw [WithTop.coe_lt_coe, Polynomial.degree_eq_natDegree ane0, ← Nat.cast_add, Nat.cast_lt]
        exact lt_add_of_pos_right _ (Nat.pos_of_ne_zero hdeg)

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

Goal state before:
pp: σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
⊢ ∀ (a : MvPolynomial σ D), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a

Tactic:
intro a ha

Goal state after:
σ : Type v
D : Type u
inst✝¹ : CommRing D
inst✝ : UniqueFactorizationMonoid D
d : ℕ
a : MvPolynomial σ D
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod a
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).primPart
a✝ : Nontrivial R
hC0 : ¬C r.leadingCoeff = 0
⊢ r ∣ s.primPart

Tactic:
refine h.trans (Associated.dvd ?_)

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).primPart
a✝ : Nontrivial R
hC0 : ¬C r.leadingCoeff = 0
⊢ Associated (C r.leadingCoeff * s).primPart s.primPart
Module: Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet

Goal state before:
pp: case e'_4
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : DecidableEq (Associates α)
inst✝ : (p : Associates α) → Decidable (Irreducible p)
p a : Associates α
hp : Irreducible p
n : ℕ
h : a ∣ p ^ n
a✝ : Nontrivial α
hph : p ^ n ≠ 0
ha : a ≠ 0
q : Associates α
hq : Irreducible q
h' : q ≠ p
⊢ q.count (p ^ n).factors = 0

Tactic:
rw [count_pow hp.ne_zero hq, count_eq_zero_of_ne hq hp h', mul_zero]

Goal state after:
Module: Mathlib.Order.DirectedInverseSystem

Goal state before:
pp: ι : Type u_1
inst✝⁵ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
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)
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)
i : ι
x : F₁ i
y : F₂ i
⊢ DirectLimit.lift₂ f₁ f₂ ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ih i x y

Tactic:
lift₂_def₂ _ _ _ _ _ _ i le_rfl le_rfl,

Goal state after:
ι : Type u_1
inst✝⁵ : Preorder ι
F₁ : ι → Type u_2
F₂ : ι → Type u_3
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)
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)
i : ι
x : F₁ i
y : F₂ i
⊢ ih i ((f₁ ⟨i, x⟩.fst i ⋯) ⟨i, x⟩.snd) ((f₂ ⟨i, y⟩.fst i ⋯) ⟨i, y⟩.snd) = ih i x y
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:
convert! LinearMap.lTensor_id_apply M _ x; ext; apply DirectedSystem.map_self'

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

Goal state before:
pp: R : Type u_1
M : Type u_2
P : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
N : Submodule R P
hN : N.FG
x y : ↥N ⊗[R] M
eq : (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y
⊢ ∃ N', N'.FG ∧ ∃ (h : N ≤ N'), (LinearMap.rTensor M (inclusion h)) x = (LinearMap.rTensor M (inclusion h)) y

Tactic:
lift N to {N : Submodule R P // N.FG} using hN
  apply_fun (Module.fgSystem.equiv R P).symm.toLinearMap.rTensor M at eq
  apply_fun directLimitLeft _ _ at eq
  simp_rw [← LinearMap.rTensor_comp_apply, ← (LinearEquiv.eq_toLinearMap_symm_comp _ _).mpr
    (Module.fgSystem.equiv_comp_of N), directLimitLeft_rTensor_of] at eq
  have ⟨N', le, eq⟩ := Module.DirectLimit.exists_eq_of_of_eq eq
  exact ⟨_, N'.2, le, eq⟩

Goal state after:
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
⊢ span R s = ⨆ i, R ∙ ↑i

Tactic:
simp [← Submodule.span_iUnion]

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

Tactic:
exact Subalgebra.fg_adjoin_finset _

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
ι : Type v
M : ι → Type w
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
⊢ Flat R (⨁ (i : ι), M i) ↔ ∀ (i : ι), Flat R (M i)

Tactic:
simp_rw [iff_rTensor_injectiveₛ, ← EquivLike.comp_injective _ (directSumRight R R _ _),
    ← LinearEquiv.coe_coe, ← coe_comp, directSumRight_comp_rTensor, coe_comp, LinearEquiv.coe_coe,
    EquivLike.injective_comp, lmap_injective]
  constructor <;> (intro h; intros; 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
⊢ Flat R M ↔
    ∀ ⦃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 ⇑(lTensor M f)

Tactic:
simp_rw [iff_rTensor_preserves_injective_linearMap', LinearMap.lTensor_inj_iff_rTensor_inj]

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

Goal state before:
pp: ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
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✝⁴ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
inst✝¹ : (i : ι) → One (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), OneHomClass (T h) (G i) (G j)
x : (i : ι) × G i
⊢ ⟦x⟧ = 1 ↔ ∃ i, ∃ (h : x.fst ≤ i), (f x.fst i h) x.snd = 1

Tactic:
by
  rw [one_def x.1, Quotient.eq]
  exact ⟨fun ⟨i, h, _, eq⟩ ↦ ⟨i, h, eq.trans (map_one _)⟩,
    fun ⟨i, h, eq⟩ ↦ ⟨i, h, h, eq.trans (map_one _).symm⟩⟩

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✝⁵ : Star R
inst✝⁴ : (i : ι) → Star (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)
inst✝² : (i : ι) → SMul R (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
inst✝ : ∀ (i : ι), StarModule R (G i)
r : R
i : ι
x : G i
⊢ star ⟦⟨i, r • x⟩⟧ = ⟦⟨i, star (r • x)⟩⟧

Tactic:
star_def

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:
| cons i s hi ih =>

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✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
i : ι
x : G i
ne : ⟦⟨i, x⟩⟧ ≠ 0
this : x ≠ 0
⊢ ⟦⟨i, x⟩⟧ * map f f (fun x x_1 ↦ x_1⁻¹) ⋯ ⟦⟨i, x⟩⟧ = 1

Tactic:
simp_rw [map_def, mul_def, mul_inv_cancel₀ this, one_def i]

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✝¹ : (i : ι) → AddMonoidWithOne (G i)
inst✝ : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)
n : ℕ
⊢ ⟦⟨Classical.arbitrary ι, (fun x ↦ ↑(n + 1)) (Classical.arbitrary ι)⟩⟧ =
    ⟦⟨Classical.arbitrary ι, (fun x ↦ ↑n) (Classical.arbitrary ι)⟩⟧ +
      ⟦⟨Classical.arbitrary ι, (fun x ↦ 1) (Classical.arbitrary ι)⟩⟧

Tactic:
simp_rw [Nat.cast_succ, add_def]

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✝⁴ : (i : ι) → Mul (G i)
inst✝³ : (i : ι) → SMul R (G i)
inst✝² : ∀ (i : ι), IsScalarTower R (G i) (G i)
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)
inst✝ : ∀ (i j : ι) (h : i ≤ j), MulActionHomClass (T h) R (G i) (G j)
r : R
i : ι
x✝¹ x✝ : G i
⊢ ⟦⟨i, r • x✝¹ * x✝⟩⟧ = ⟦⟨i, r • (x✝¹ * x✝)⟩⟧

Tactic:
smul_mul_assoc

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ {i ∈ s | p i} = {i ∈ t | q i}

Tactic:
hst,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module ℚ≥0 M
s t : Finset ι
f g : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hst : s = t
hpq : ∀ i ∈ t, p i ↔ q i
h : ∀ i ∈ t, q i → f i = g i
⊢ {i ∈ t | p i} = {i ∈ t | q i}
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
t : Finset κ
f : ι → κ → M
⊢ 𝔼 i ∈ s, ∑ j ∈ t, f i j = ∑ j ∈ t, 𝔼 i ∈ s, f i j

Tactic:
simpa only [expect, smul_sum] using sum_comm

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
by
  simp_rw [expect, card_bij' i j hi hj left_inv right_inv, sum_bij' i j hi hj left_inv right_inv h]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j ∈ Iio k
⊢ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j ∈ ↑F

Tactic:
rw [mem_Iio] at hj

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) j ∈ ↑F
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
⊢ (fun y ↦ s(x, y)) x ∉ map (fun y ↦ s(x, y)) xs

Tactic:
intro h'

Goal state after:
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
h' : (fun y ↦ s(x, y)) x ∈ map (fun y ↦ s(x, y)) xs
⊢ False
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange T (toAlgHom R R' T').toLinearMap ↔ IsBaseChange T (toAlgHom S S' T').toLinearMap

Tactic:
← heq,

Goal state after:
R : Type u_1
S : Type v₃
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
T : Type u_4
inst✝²⁴ : CommSemiring T
inst✝²³ : Algebra R T
inst✝²² : Algebra S T
inst✝²¹ : IsScalarTower R S T
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'
T' : Type u_8
inst✝¹² : CommSemiring T'
inst✝¹¹ : Algebra R T'
inst✝¹⁰ : Algebra S' T'
inst✝⁹ : Algebra S T'
inst✝⁸ : Algebra T T'
inst✝⁷ : Algebra R' T'
inst✝⁶ : IsScalarTower R T T'
inst✝⁵ : IsScalarTower S T T'
inst✝⁴ : IsScalarTower S S' T'
inst✝³ : IsScalarTower R R' T'
inst✝² : IsScalarTower R S' T'
inst✝¹ : IsScalarTower R' S' T'
inst✝ : IsPushout R S R' S'
f : R' →ₗ[R] S' := (toAlgHom R R' S').toLinearMap
this : IsScalarTower R S T'
heq : ↑R (toAlgHom S S' T').toLinearMap ∘ₗ f = (toAlgHom R R' T').toLinearMap
⊢ IsBaseChange T (↑R (toAlgHom S S' T').toLinearMap ∘ₗ f) ↔ IsBaseChange T (toAlgHom S S' T').toLinearMap
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ 𝟙 Y = inv f ≫ g

Tactic:
p,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : IsIso g
p : inv f = inv g
⊢ 𝟙 Y = inv g ≫ g
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso f

Tactic:
rw [(hom_comp_eq_id _).mp h]
  infer_instance

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

Goal state before:
pp: case h_map
V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))

Tactic:
rintro _ _ ⟨⟩
    subst_vars
    simp only [Prefunctor.comp_map]
    rfl

Goal state after: