mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Archimedean

Goal state before:
pp: case mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
z : ArchimedeanClass R
x y : R
h : mk x ≤ mk y
⊢ mk x + z ≤ mk y + z

Tactic:
induction z with | mk z
     =>  _ 

Goal state after:
case mk.mk.mk
R : Type u_1
S : Type u_2
inst✝³ : LinearOrder R
inst✝² : LinearOrder S
inst✝¹ : CommRing R
inst✝ : IsStrictOrderedRing R
x y : R
h : mk x ≤ mk y
z : R
⊢ mk x + mk z ≤ mk y + mk z
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
⊢ (x * y).order = x.order + y.order

Tactic:
have hx : x.leadingCoeff ≠ 0 := by aesop

Goal state after:
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : x.leadingCoeff ≠ 0
⊢ (x * y).order = x.order + y.order
Module: Mathlib.Order.Quotient

Goal state before:
pp: α : Type u_1
s : Setoid α
inst✝ : LE α
x : Quotient s
⊢ x ≤ x

Tactic:
induction x using Quotient.inductionOn with | h x
    exact .single <| .inr (refl x)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst✝⁸ : AddCommMonoid Γ
inst✝⁷ : PartialOrder Γ
inst✝⁶ : IsOrderedCancelAddMonoid Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : AddAction Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
inst✝² : AddCommMonoid V
inst✝¹ : Semiring R
inst✝ : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
⊢ (x * y) • z = x • y • z

Tactic:
by
  ext b
  rw [coeff_smul_left (x.isPWO_support.add y.isPWO_support)
    HahnSeries.support_mul_subset, coeff_smul_right
    (y.isPWO_support.vadd ((of R).symm z).isPWO_support) support_smul_subset_vadd_support]
  simp only [HahnSeries.coeff_mul, coeff_smul, sum_smul, smul_sum, sum_sigma']
  apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l +ᵥ j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
    aesop (add safe [Set.vadd_mem_vadd, Set.add_mem_add]) (add simp [add_vadd, mul_smul])

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V✝ : Type u_5
inst✝¹⁴ : AddCommMonoid Γ✝
inst✝¹³ : PartialOrder Γ✝
inst✝¹² : IsOrderedCancelAddMonoid Γ✝
inst✝¹¹ : PartialOrder Γ'
inst✝¹⁰ : AddAction Γ✝ Γ'
inst✝⁹ : IsOrderedCancelVAdd Γ✝ Γ'
inst✝⁸ : AddCommMonoid V✝
Γ : Type u_6
V : Type u_7
inst✝⁷ : Ring R
inst✝⁶ : IsDomain R
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Module R V
inst✝ : Module.IsTorsionFree R V
x : R⟦Γ⟧
y : HahnModule Γ R V
hxy : x ≠ 0 ∧ y ≠ 0
⊢ ¬((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) =
      ((of R).symm 0).coeff (x.order + ((of R).symm y).order)

Tactic:
by simpa [coeff_smul_order_add_order]

Goal state after:
Module: Mathlib.Algebra.Order.Star.Conjneg

Goal state before:
pp: G : Type u_1
R : Type u_2
inst✝⁴ : AddGroup G
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ 0 ≤ conjneg (-f) ↔ 0 ≤ -f

Tactic:
conjneg_nonneg

Goal state after:
Module: Mathlib.Algebra.Order.Ring.StandardPart

Goal state before:
pp: case mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
z : FiniteResidueField K
x y : FiniteElement K
h : mk x ≤ mk y
⊢ mk x + z ≤ mk y + z

Tactic:
induction z with | mk z
     =>  _ 

Goal state after:
case mk.mk.mk
K : Type u_1
inst✝⁶ : LinearOrder K
inst✝⁵ : Field K
inst✝⁴ : IsOrderedRing K
x✝ y✝ : K
R : Type u_2
inst✝³ : LinearOrder R
inst✝² : CommRing R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
x y : FiniteElement K
h : mk x ≤ mk y
z : FiniteElement K
⊢ mk x + mk z ≤ mk y + mk z
Module: Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
f : R[X]
H : f.IsMonicOfDegree 2
n : ℕ
hn : n < 1
⊢ f.coeff n = (X ^ 2 + C (f.coeff 1) * X + C (f.coeff 0)).coeff n

Tactic:
obtain rfl : n = 0 := Nat.lt_one_iff.mp hn
    simp

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝¹ : Semiring R
inst✝ : CommSemiring K
i : R →+* K
b : R
bi : K
N : ℕ
a : R
bu : bi * i b = 1
⊢ i 0 = i b ^ N * eval (i a * bi) (Polynomial.map i 0)

Tactic:
by
    simp only [eval_zero, map_zero, mul_zero, Polynomial.map_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ((ofFn n) v).natDegree < n

Tactic:
Nat.lt_iff_le_pred h,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
h : 1 ≤ n
v : Fin n → R
⊢ ((ofFn n) v).natDegree ≤ n - 1
Module: Mathlib.Algebra.Polynomial.OfFn

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

Tactic:
as_sum_range' (ofFn n v) n <| ofFn_natDegree_lt (Nat.one_le_iff_ne_zero.mpr h) v

Goal state after:
case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
v : Fin n → R
h : ¬n = 0
⊢ ∑ i ∈ Finset.range n, (monomial i) (((ofFn n) v).coeff i) = ∑ i, (monomial ↑i) (v i)
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : R[X]
hg : g.Monic
n : ℕ
ih :
  ∀ {q₁ q₂ : R[X]} {r₁ r₂ : Fin n → R[X]},
    (∀ (i : Fin n), (r₁ i).degree < g.degree) →
      (∀ (i : Fin n), (r₂ i).degree < g.degree) →
        q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
q₁ q₂ : R[X]
rs₁ : Fin n → R[X]
r₁ : R[X]
hr₁ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₁ r₁ i).degree < g.degree
rs₂ : Fin n → R[X]
r₂ : R[X]
hr₂ : ∀ (i : Fin (n + 1)), (Fin.snoc rs₂ r₂ i).degree < g.degree
hf : (r₁ + g * q₁) * g ^ n + ∑ x, rs₁ x * g ^ ↑x = (r₂ + g * q₂) * g ^ n + ∑ x, rs₂ x * g ^ ↑x
hqr : r₁ + g * q₁ = r₂ + g * q₂
hrs : rs₁ = rs₂
⊢ r₁.degree < g.degree

Tactic:
simpa using hr₁ (Fin.last n)

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

Goal state before:
pp: k✝ k m : ℕ
hkm : k < m
u v w : ℤˣ
hmn : m < k✝
hk : k✝ ∈ (trinomial k m k✝ ↑u ↑v ↑w).support
⊢ ↑w = (trinomial k m k✝ ↑u ↑v ↑w).coeff k✝

Tactic:
by rw [trinomial_leading_coeff' hkm hmn]

Goal state after:
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
p : R[X]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval₂ (RingHom.id A) r (sumIDeriv (map (algebraMap R A) p))

Tactic:
sumIDeriv_map,

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
r : A
⊢ eval₂ (algebraMap R A) r (sumIDeriv p) = eval₂ (RingHom.id A) r (map (algebraMap R A) (sumIDeriv p))
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case e_a.e_a.e_l.e_p
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)
x✝ : R
⊢ ((fun x ↦ decide (x ≠ 0)) ∘ (fun x ↦ -x) ∘ ⇑SignType.sign) x✝ = ((fun x ↦ decide (x ≠ 0)) ∘ ⇑SignType.sign) x✝

Tactic:
simp [SignType.sign]

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

Goal state before:
pp: case neg
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)
p0 : p ≠ 0
c : ℕ → R[X] := fun k ↦ if hk : q ≤ k then ⋯.choose else 0
k : ℕ
h : ¬q ≤ k
⊢ natDegree 0 ≤ p.natDegree - k

Tactic:
rw [natDegree_zero]; exact Nat.zero_le _

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.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

Tactic:
or_comm,

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 = p.mirror ∨ q.mirror = p.mirror
Module: Mathlib.Algebra.PresentedMonoid.Basic

Goal state before:
pp: case h.one
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ (mk rels) 1 ∈ closure (range (of rels))

Tactic:
exact Submonoid.one_mem _

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

Goal state before:
pp: case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : SignType.sign P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations

Tactic:
have h_ηP : 0 < η * coeff P (d + 1) := by grind [leadingCoeff, mul_pos]

Goal state after:
case succ
R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC : SignType
hs_nC : SignType.sign P.nextCoeff = s_nC
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
⊢ P.signVariations + 1 ≤ ((X - C η) * P).signVariations
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: K : Type u_1
R : Type u_2
a b : R
inst✝ : CommRing R
z w : QuadraticAlgebra R a b
⊢ (z * w).re * (z * w).re + b * (z * w).re * (z * w).im - a * (z * w).im * (z * w).im =
    (z.re * z.re + b * z.re * z.im - a * z.im * z.im) * (w.re * w.re + b * w.re * w.im - a * w.im * w.im)

Tactic:
simp only [re_mul, im_mul]; ring

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    (q + ∑ i ∈ s, q' i) * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r' i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
rw [add_mul, add_assoc, add_right_inj, Finset.sum_mul, ← Finset.sum_add_distrib]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
f : R[X]
g : ι → R[X]
hg : ∀ i ∈ s, (g i).Monic
hgg : (↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)
n : ι → ℕ
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k
q' : ι → R[X]
r' : (i : ι) → Fin (n i) → R[X]
hr' : ∀ i ∈ s, ∀ (j : Fin (n i)), (r' i j).degree < (g i).degree
hr : ∀ i ∈ s, r i = q' i * g i ^ n i + ∑ j, r' i j * g i ^ ↑j
⊢ ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    ∑ x ∈ s, (q' x * ∏ i ∈ s, g i ^ n i + ∑ j, r' x j * g x ^ ↑j * ∏ k ∈ s.erase x, g k ^ n k)
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = 1
⊢ P.nextCoeff ≠ 0

Tactic:
simp [← sign_ne_zero, hs_nC]

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
η : R
hη : 0 < η
P : R[X]
hP : P ≠ 0
h_lC : 0 < P.leadingCoeff
h_mul : (X - C η) * P ≠ 0
h_deg_mul : ((X - C η) * P).natDegree = P.natDegree + 1
d : ℕ
ih : ∀ m < d + 1, ∀ {P : R[X]}, P ≠ 0 → P.natDegree = m → P.signVariations + 1 ≤ ((X - C η) * P).signVariations
hd : P.natDegree = d + 1
s_nC_mul : SignType
hs_nC_mul : SignType.sign ((X - C η) * P).nextCoeff = s_nC_mul
h_ih : P.eraseLead.natDegree < d + 1
h_mul_lC : SignType.sign ((X - C η) * P).leadingCoeff = 1
h_ηP : 0 < η * P.coeff (d + 1)
hs_nC : SignType.sign P.nextCoeff = -1
⊢ P.nextCoeff ≠ 0

Tactic:
simp [← sign_ne_zero, hs_nC]

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
inst✝ : NonUnitalNonAssocRing R
M N : AddSubgroup R
x✝ : R
h : x✝ ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier
m : R
hm : m ∈ M.toAddSubmonoid
n : R
hn : n ∈ N.toAddSubmonoid
⊢ -(m * n) ∈ (M.toAddSubmonoid * N.toAddSubmonoid).carrier

Tactic:
rw [← neg_mul]; exact AddSubmonoid.mul_mem_mul (M.neg_mem hm) hn

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ((liftAlgHom S) ⟨f, w⟩) ((mkAlgHom S s) x) = f x

Tactic:
simp_rw [liftAlgHom_def, preLiftAlgHom_def, mkAlgHom_def, mkRingHom_def]

Goal state after:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → f x = f y
x : A
⊢ ({
          toFun := fun f' ↦
            { toFun := fun x ↦ Quot.lift ⇑↑f' ⋯ x.toQuot, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
              commutes' := ⋯ },
          invFun := fun F ↦
            ⟨F.comp
                { toFun := fun x ↦ { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯,
                  map_add' := ⋯, commutes' := ⋯ },
              ⋯⟩,
          left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ({ toFun := fun x ↦ { toQuot := Quot.mk (Rel s) x }, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯,
          commutes' := ⋯ }
        x) =
    f x
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
c : R
h : c ≠ 0
⊢ (C c * X ^ n).support = {n}

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, support_monomial n h]

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

Goal state before:
pp: R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ (TensorProduct.map (star (toConv (single R B i))).ofConv (star (toConv (single R B i))).ofConv)
      ((TensorProduct.comm R (B i) (B i)) (comul x)) =
    (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ((TensorProduct.map (single R B i) (single R B i)) (comul x))

Tactic:
map_comm

Goal state after:
R : Type u_5
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
n : Type u_8
inst✝⁶ : DecidableEq n
B : n → Type u_9
inst✝⁵ : (i : n) → AddCommMonoid (B i)
inst✝⁴ : (i : n) → Module R (B i)
inst✝³ : (i : n) → StarAddMonoid (B i)
inst✝² : ∀ (i : n), StarModule R (B i)
inst✝¹ : Fintype n
inst✝ : (i : n) → CoalgebraStruct R (B i)
h : ∀ (i : n), star (toConv comul) = toConv (↑(TensorProduct.comm R (B i) (B i)) ∘ₗ comul)
i : n
x : B i
this : star (comul (star x)) = (TensorProduct.comm R (B i) (B i)) (comul x)
⊢ (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i))
      ((TensorProduct.map (star (toConv (single R B i))).ofConv (star (toConv (single R B i))).ofConv) (comul x)) =
    (TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ((TensorProduct.map (single R B i) (single R B i)) (comul x))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X : LocallyRingedSpace
f : ∅ ⟶ X
⊢ f = X.emptyTo

Tactic:
by ext ⟨⟩ x; cat_disch

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom e.hom.base) ((ConcreteCategory.hom e.inv.base) y) = y

Tactic:
change (e.inv.base ≫ e.hom.base) y = 𝟙 Y.toPresheafedSpace y

Goal state after:
X Y : LocallyRingedSpace
e : X ≅ Y
y : ↑Y.toTopCat
⊢ (ConcreteCategory.hom (e.inv.base ≫ e.hom.base)) y = (ConcreteCategory.hom (𝟙 Y.toPresheafedSpace).base) y
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (f ≫ g).unop = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop

Tactic:
dsimp; rw [Spec.locallyRingedSpaceMap_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ (s, ⟨r, hpr⟩ ^ n).2 • y = (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1

Tactic:
Submonoid.smul_def,

Goal state after:
R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
r : ↑(CommRingCat.of ↑R)
hpr : p ∈ PrimeSpectrum.basicOpen r
s' :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).obj
      (op (PrimeSpectrum.basicOpen r)))
e :
  (ConcreteCategory.hom
        (((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
              (structureSheaf ↑S).obj).germ
          (PrimeSpectrum.basicOpen r) p hpr))
      s' =
    y
s : ↑S
n : ℕ
hsn :
  s' *
      (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
        ↑(s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).2 =
    (algebraMap ↑S ↑((structureSheaf ↑S).obj.obj (op (PrimeSpectrum.basicOpen ((algebraMap ↑R ↑S) r)))))
      (s, ⟨(fun x ↦ (algebraMap ↑R ↑S) r ^ x) n, ⋯⟩).1
⊢ ↑(s, ⟨r, hpr⟩ ^ n).2 • y = (toPushforwardStalkAlgHom R S p) (s, ⟨r, hpr⟩ ^ n).1
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ appLE (f ≫ g) U V e = app g U ≫ appLE f (g ⁻¹ᵁ U) V e

Tactic:
rw [g.app_eq_appLE, appLE_comp_appLE]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ X.zeroLocus t ⊆ X.zeroLocus s

Tactic:
simp only [Set.subset_def, Scheme.mem_zeroLocus_iff]

Goal state after:
X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ ∀ (x : ↥X), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ X.presheaf.map (eqToHom ⋯) = X.presheaf.map (eqToHom ⋯).op

Tactic:
by rw [eqToHom_op]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ appIso (𝟙 X) U = Functor.mapIso X.presheaf (eqToIso ⋯).op

Tactic:
by
  ext; simp [appIso_hom]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : MorphismProperty C
⊢ P.precoverage.morphismProperty = P

Tactic:
ext X Y f
  exact ⟨fun ⟨R, hR, hf⟩ ↦ hR hf, fun hf ↦ ⟨.singleton f, by simpa⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ IsPullback (lift g f H) (𝟙 X) g f

Tactic:
convert! IsPullback.of_id_snd.paste_horiz (IsKernelPair.id_of_mono g)

Goal state after:
case e'_7
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ lift g f H = ?convert_2 ≫ 𝟙 U

case e'_10
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ f = ?convert_2 ≫ g

case convert_2
X U Y : Scheme
f : X ⟶ Y
g : U ⟶ Y
inst✝ : IsOpenImmersion g
H : Set.range ⇑f ⊆ Set.range ⇑g
⊢ X ⟶ U
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
H : ∀ (i : 𝒰.I₀), CompactSpace ↥(𝒰.X i)
⊢ CompactSpace ↥X

Tactic:
cases nonempty_fintype 𝒰.I₀
  rw [← isCompact_univ_iff, ← 𝒰.iUnion_range]
  apply isCompact_iUnion
  intro i
  rw [isCompact_iff_compactSpace]
  exact
    @Homeomorph.compactSpace _ _ _ _ (H i)
      (TopCat.homeoOfIso
        (asIso
          (IsOpenImmersion.isoOfRangeEq (𝒰.f i)
            (X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
            Subtype.range_coe.symm).hom.base))

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
U : Opens ↑(PrimeSpectrum.Top R)
x y : ↥U
⊢ ∃ (hs : 1 ∉ (↑y).asIdeal), (fun x ↦ 0 ((𝟙 U) x)) y = LocalizedModule.mk 0 ⟨1, hs⟩

Tactic:
by simp [Ideal.IsPrime.one_notMem]

Goal state after: