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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ x ∈ Finset.antidiagonal (p.natDegree + p.natTrailingDegree), p.coeff x.1 * p.mirror.coeff x.2 =
    p.sum fun x x_1 ↦ x_1 ^ 2

Tactic:
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ ∑ k ∈ Finset.range (p.natDegree + p.natTrailingDegree).succ,
      p.coeff (k, p.natDegree + p.natTrailingDegree - k).1 *
        p.mirror.coeff (k, p.natDegree + p.natTrailingDegree - k).2 =
    p.sum fun x x_1 ↦ x_1 ^ 2
Module: Mathlib.Algebra.Polynomial.OfFn

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
v : Fin 0 → R
⊢ (ofFn 0) v = ∑ i, (monomial ↑i) (v i)

Tactic:
simp [ofFn]

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

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : i < n
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

Tactic:
simp [h, toFn]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : n < m
r : R
⊢ ((monomial m) r).homogenize n = 0

Tactic:
rw [homogenize]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
h : n < m
r : R
⊢ ∑ kl ∈ antidiagonal n, (MvPolynomial.monomial fun₀ | 0 => kl.1 | 1 => kl.2) (((monomial m) r).coeff kl.1) = 0
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff ((2 * p.natDegree + (p * p.mirror).natTrailingDegree) / 2) = 3

Tactic:
natTrailingDegree_mul_mirror,

Goal state after:
p : ℤ[X]
⊢ p.IsUnitTrinomial ↔ (p * p.mirror).coeff ((2 * p.natDegree + 2 * p.natTrailingDegree) / 2) = 3
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (fun x ↦ -x)
            (List.map (⇑SignType.sign)
              (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1

Tactic:
← h_neg_destutter,

Goal state after:
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
P : R[X]
hsc : (⇑SignType.sign ∘ fun x ↦ -x) = (fun x ↦ -x) ∘ ⇑SignType.sign
h_neg_destutter :
  ∀ (l : List SignType),
    List.map (fun x ↦ -x) (List.destutter (fun x1 x2 ↦ ¬x1 = x2) l) =
      List.destutter (fun x1 x2 ↦ ¬x1 = x2) (List.map (fun x ↦ -x) l)
⊢ (List.map (fun x ↦ -x)
          (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (List.map (⇑SignType.sign)
              (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) P.coeffList)))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ x1 ≠ x2)
          (List.map (⇑SignType.sign) (List.filter ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) P.coeffList))).length -
      1
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case h
p : ℤ[X]
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
key : n - m + k < n
⊢ m + n ∈ Set.Ioo (k + n) (n + n)

Tactic:
constructor <;> gcongr

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
P : R[X]
η : R
h₁ : 0 < P.leadingCoeff
h₃ : P ≠ 0
h₄ : P.eraseLead.natDegree + 1 = P.natDegree
h₅ : X - C η ≠ 0
h₆ : P.eraseLead ≠ 0
d : ℕ
hd : P.natDegree = 0 + d + 1
h₂ : P.eraseLead.leadingCoeff = P.nextCoeff
n : ℕ
h_cons :
  ((X - C η) * P.eraseLead).coeffList =
    ((X - C η) * P.eraseLead).leadingCoeff :: (List.replicate n 0 ++ ((X - C η) * P.eraseLead).eraseLead.coeffList)
h₇ : ((X - C η) * P).natDegree = P.natDegree + 1
h₈ : ((X - C η) * P.eraseLead).eraseLead = (X - C η) * P.eraseLead - (monomial P.natDegree) P.nextCoeff
this : P.eraseLead.natDegree + 2 = ((X - C η) * P.eraseLead).coeffList.length
⊢ P.natDegree + 2 = ((X - C η) * P).coeffList.length

Tactic:
simp [X_sub_C_ne_zero, h₃, h₇]

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

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q = trinomial k m' n ↑w ↑v ↑u
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
← mirror_inj,

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q * q.mirror
hq : q.mirror = (trinomial k m' n ↑w ↑v ↑u).mirror
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q = p ∨ q = p.mirror

Tactic:
← mirror_inj,

Goal state after:
case inr
p q : ℤ[X]
k m m' n : ℕ
hkm : k < m
hmn : m < n
hkm' : k < m'
hmn' : m' < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
h : p * p.mirror = q.mirror * q.mirror.mirror
hq : q.mirror = trinomial k (n - m' + k) n ↑u ↑v ↑w
hmul : ↑w * ↑u = ↑u * ↑w
⊢ q.mirror = p.mirror ∨ q = p.mirror
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ (q * q.mirror).natTrailingDegree = 2 * k'

Tactic:
natTrailingDegree_mul_mirror,

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ 2 * q.natTrailingDegree = 2 * k'
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ 2 * (trinomial k' m' n' ↑x ↑y ↑z).natTrailingDegree = 2 * k'

Tactic:
trinomial_natTrailingDegree hkm' hmn' x.ne_zero

Goal state after:
p : ℤ[X]
h : IsRelPrime p p.mirror
q : ℤ[X]
hpq : p * p.mirror = q * q.mirror
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
hp : p = trinomial k m n ↑u ↑v ↑w
k' m' n' : ℕ
hkm' : k' < m'
hmn' : m' < n'
x y z : ℤˣ
hq : q = trinomial k' m' n' ↑x ↑y ↑z
⊢ 2 * k' = 2 * k'
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Nontrivial A
inst✝ : NoZeroDivisors A
p : R[X]
q : ℕ
hq : 0 < q
inj_amap : Function.Injective ⇑(algebraMap R A)
⊢ ∃ gp,
    gp.natDegree ≤ p.natDegree - q ∧
      ∀ (r : A) {p' : A[X]},
        map (algebraMap R A) p = (X - C r) ^ (q - 1) * p' →
          (aeval r) (sumIDeriv p) = (q - 1)! • eval r p' + q ! • (aeval r) gp

Tactic:
by
  rcases eq_or_ne p 0 with (rfl | p0)
  · use 0
    rw [natDegree_zero]
    use Nat.zero_le _
    intro r p' hp
    rw [map_zero, map_zero, smul_zero, add_zero]
    rw [Polynomial.map_zero] at hp
    replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
    · rw [hp, eval_zero, smul_zero]
    exact fun h => X_sub_C_ne_zero r (eq_zero_of_pow_eq_zero h)
  let c k := if hk : q ≤ k then (aeval_iterate_derivative_of_ge A p q hk).choose else 0
  have c_le (k) : (c k).natDegree ≤ p.natDegree - k := by
    dsimp only [c]
    split_ifs with h
    · exact (aeval_iterate_derivative_of_ge A p q h).choose_spec.1
    · rw [natDegree_zero]; exact Nat.zero_le _
  have hc (k) (hk : q ≤ k) : ∀ (r : A), aeval r (derivative^[k] p) = q ! • aeval r (c k) := by
    simp_rw [c, dif_pos hk]
    exact (aeval_iterate_derivative_of_ge A p q hk).choose_spec.2
  refine ⟨∑ x ∈ Ico q (p.natDegree + 1), c x, ?_, ?_⟩
  · refine (natDegree_sum_le _ _).trans ?_
    rw [fold_max_le]
    exact ⟨Nat.zero_le _, fun i hi => (c_le i).trans (tsub_le_tsub_left (mem_Ico.mp hi).1 _)⟩
  intro r p' hp
  have : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1) := by
    rw [range_eq_Ico, range_eq_Ico, Ico_union_Ico_eq_Ico hq.le]
    rw [← tsub_le_iff_right]
    calc
      q - 1 ≤ q - 1 + p'.natDegree := le_self_add
      _ = (p.map <| algebraMap R A).natDegree := by
        rw [hp, natDegree_mul, natDegree_pow, natDegree_X_sub_C, mul_one,
          ← Nat.sub_add_comm (Nat.one_le_of_lt hq)]
        · exact pow_ne_zero _ (X_sub_C_ne_zero r)
        · rintro rfl
          rw [mul_zero, Polynomial.map_eq_zero_iff inj_amap] at hp
          exact p0 hp
      _ ≤ p.natDegree := natDegree_map_le
  rw [← zero_add ((q - 1)! • p'.eval r)]
  rw [sumIDeriv_apply, map_sum, map_sum, this]
  have : range q = range (q - 1 + 1) := by rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]
  rw [sum_union, this, sum_range_succ]
  · congr 2
    · apply sum_eq_zero
      exact fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)
    · rw [← aeval_iterate_derivative_self _ _ _ hp]
    · rw [smul_sum, sum_congr rfl]
      intro k hk
      exact hc k (mem_Ico.mp hk).1 r
  · rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_notMem]
    intro x hx
    rw [mem_inter, mem_Ico, mem_Ico] at hx
    exact hx.1.2.not_ge hx.2.1

Goal state after:
Module: Mathlib.Algebra.Ring.Ext

Goal state before:
pp: case negSucc
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ IntCast.intCast (Int.negSucc n) = IntCast.intCast (Int.negSucc n)

Tactic:
inst₁.intCast_negSucc,

Goal state after:
case negSucc
R : Type u
inst₁ inst₂ : AddGroupWithOne R
h_add : HAdd.hAdd = HAdd.hAdd
h_one : One.one = One.one
this✝ : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne
this : inst₁.toNatCast = inst₂.toNatCast
toAddMonoid_eq✝ : inst₁.toAddMonoid = inst₂.toAddMonoid
toNeg_eq✝ : inst₁.toNeg = inst₂.toNeg
toSub_eq✝ : inst₁.toSub = inst₂.toSub
toZSMul_eq✝ : inst₁.toZSMul = inst₂.toZSMul
n : ℕ
⊢ -↑(n + 1) = IntCast.intCast (Int.negSucc n)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * ∏ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ ^ 1 =
    (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * ((algebraMap R[X] K) (g i))⁻¹ ^ (↑j + 1)
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)

Tactic:
simp_rw [Fin.sum_univ_one, Fin.val_zero, zero_add, pow_one, Finset.prod_inv_distrib] at hf

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
f : R[X]
ι : Type u_3
g : ι → R[X]
s : Finset ι
hg : ∀ i ∈ s, (g i).Monic
hcop : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
this : Nontrivial R
hgi : ∀ i ∈ s, ((algebraMap R[X] K) (g i))⁻¹ * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : ι → Fin 1 → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin 1), (r i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) f * (∏ x ∈ s, (algebraMap R[X] K) (g x))⁻¹ =
    (algebraMap R[X] K) q + ∑ x ∈ s, (algebraMap R[X] K) (r x 0) * ((algebraMap R[X] K) (g x))⁻¹
⊢ ↑f / ∏ i ∈ s, ↑(g i) = ↑q + ∑ i ∈ s, ↑((fun i ↦ r i 0) i) / ↑(g i)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ ((erase a) f).support

Tactic:
support_erase,

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ a ∉ f.support.erase a
Module: Mathlib.Algebra.SkewMonoidAlgebra.Single

Goal state before:
pp: case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ ((erase a) f).support = s

Tactic:
support_erase,

Goal state after:
case a
M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
p : SkewMonoidAlgebra M α → Prop
f✝ : SkewMonoidAlgebra M α
h0 : p 0
ha : ∀ (a : α) (b : M) (f : SkewMonoidAlgebra M α), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)
s✝ : Finset α
a : α
s : Finset α
has : a ∉ s
ih : ∀ (f : SkewMonoidAlgebra M α), f.support = s → p f
f : SkewMonoidAlgebra M α
hf : f.support = Finset.cons a s has
⊢ f.support.erase a = s
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝⁴ : Semiring R
S : Type uS
inst✝³ : CommSemiring S
T : Type uT
A : Type uA
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
inst✝ : Algebra S R
r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) ((algebraMap S R) 1) } = 1

Tactic:
by simp [← one_quot]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) 1 } = 1

Tactic:
by simp [← one_quot]

Goal state after:
Module: Mathlib.Algebra.Star.CHSH

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : Algebra ℝ R
inst✝¹ : IsOrderedModule ℝ R
inst✝ : StarModule ℝ R
A₀ A₁ B₀ B₁ : R
T : IsCHSHTuple A₀ A₁ B₀ B₁
m : ℤ
a : ℝ
x : R
⊢ m • a • x = (↑m * a) • x

Tactic:
rw [← Int.cast_smul_eq_zsmul ℝ, ← mul_smul]

Goal state after:
Module: Mathlib.Algebra.Star.CentroidHom

Goal state before:
pp: α : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (↑z * star a) = star (star a) * ↑(star z)

Tactic:
simp only [star_mul, star_star, StarMemClass.coe_star]

Goal state after:
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ := (lift R) (MulOpposite.op ∘ ι R)
⊢ ∀ (x : X), MulOpposite.unop (y (MulOpposite.unop (y (ι R x)))) = ι R x

Tactic:
intros
      simp only [y, lift_ι_apply, Function.comp_apply, MulOpposite.unop_op]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.sum g).sum h = f.sum fun a b ↦ (g a b).sum h

Tactic:
rw [sum_def, coeff_sum' f g, Finsupp.sum_sum_index h_zero h_add]

Goal state after:
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid N
inst✝ : AddCommMonoid P
f : SkewMonoidAlgebra M α
g : α → M → SkewMonoidAlgebra N β
h : β → N → P
h_zero : ∀ (a : β), h a 0 = 0
h_add : ∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂
⊢ (f.coeff.sum fun a b ↦ (g a b).coeff.sum h) = f.sum fun a b ↦ (g a b).sum h
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
f : k →+ R
g : G → R
l : SkewMonoidAlgebra k G →+ R
h : ∀ (a : G) (b : k), l (single a b) = f b * g a
⊢ l = liftNC f g

Tactic:
ext a b

Goal state after:
k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
R : Type u_5
inst✝ : NonUnitalNonAssocSemiring R
f : k →+ R
g : G → R
l : SkewMonoidAlgebra k G →+ R
h : ∀ (a : G) (b : k), l (single a b) = f b * g a
a : G
b : k
⊢ l (single a b) = (liftNC f g) (single a b)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f * g).coeff x = f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0

Tactic:
rw [mul_def, coeff_sum]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Mul G
inst✝¹ : SMulZeroClass G k
inst✝ : DecidableEq G
f g : SkewMonoidAlgebra k G
x : G
⊢ (f.sum fun a₁ b ↦ (g.sum fun a₂ b₂ ↦ single (a₁ * a₂) (b * a₁ • b₂)).coeff x) =
    f.sum fun a₁ b₁ ↦ g.sum fun a₂ b₂ ↦ if a₁ * a₂ = x then b₁ * a₁ • b₂ else 0
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ (X.restrict h).presheaf.germ V x ?hx ≫ 𝟙 ((X.restrict h).presheaf.stalk x) = (X.restrict h).presheaf.germ V x hx

pp: case hx
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ x ∈ V

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ (X.restrict h).presheaf.germ V x ?hx = (X.restrict h).presheaf.germ V x hx

case hx
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ x ∈ V
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Hom.stalkMap α x = Hom.stalkMap α x ≫ 𝟙 (X.presheaf.stalk x)

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Hom.stalkMap α x = Hom.stalkMap α x
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
⊢ ∀ i ∈ s, IsClosed (↑(X.basicOpen i))ᶜ

Tactic:
intro i _

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
s : Set ↑(X.presheaf.obj (op U))
i : ↑(X.presheaf.obj (op U))
a✝ : i ∈ s
⊢ IsClosed (↑(X.basicOpen i))ᶜ
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
x : ↥U
w : ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)

Tactic:
rcases w with ⟨V, m, i, p⟩

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : ↑X → Type u_2
P : PrelocalPredicate T
U : Opens ↑X
f : (x : ↥U) → T ↑x
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
p : ∀ (x : ↥V), ∃ V_1, ∃ (_ : ↑x ∈ V_1), ∃ i_1, P.pred fun x ↦ (fun x ↦ f (i x)) (i_1 x)
⊢ ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, P.pred fun x ↦ f (i x)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))).hom x)

Tactic:
rw [← localRingHom_comp_stalkIso, ConcreteCategory.isIso_iff_bijective]

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        (CommRingCat.ofHom
            (stalkIso (↑(CommRingCat.of ↑R))
                    (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                      x)).symm.toRingEquiv.toRingHom ≫
          CommRingCat.ofHom
              (Localization.localRingHom
                (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                    x).asIdeal
                x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
            CommRingCat.ofHom (stalkIso (↑(CommRingCat.of (Localization M))) x).toRingEquiv.toRingHom))
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ X.presheaf.map (eqToHom ⋯) ≫ 𝟙 (X.presheaf.obj ((Opens.map f.base).op.obj (op ((opensFunctor f).obj U)))) =
    X.presheaf.map (eqToHom ⋯)

Tactic:
Category.comp_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
ι : Sort u_1
s : ι → X.Opens
⊢ ↑(f ''ᵁ ⨆ i, s i) = ↑(⨆ i, f ''ᵁ s i)

Tactic:
simp [Set.image_iUnion]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X : PresheafedSpace CommRingCat
Y : Scheme
f : X ⟶ Y.toPresheafedSpace
H : IsOpenImmersion f
x : ↑(toLocallyRingedSpace Y.toLocallyRingedSpace f).toTopCat
R : CommRingCat
i : Spec R ⟶ Y
left✝ : AlgebraicGeometry.IsOpenImmersion i
h₁ : (ConcreteCategory.hom f.base) x ∈ Set.range ⇑i
h₂ : Set.range ⇑i ⊆ ↑{ carrier := Set.range ⇑(ConcreteCategory.hom f.base), is_open' := ⋯ }
⊢ LocallyRingedSpace.IsOpenImmersion
    (LocallyRingedSpace.IsOpenImmersion.lift (toLocallyRingedSpaceHom Y.toLocallyRingedSpace f) i.toLRSHom' h₂)

Tactic:
· delta LocallyRingedSpace.IsOpenImmersion.lift; infer_instance

Goal state after: