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

Goal state before:
pp: case inr
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
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror

Tactic:
trinomial_def

Goal state after:
case inr
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 = C ↑u * X ^ k + C ↑v * X ^ m + C ↑w * X ^ n
m' : ℕ
x y z : ℤˣ
hkm' : k < m'
hmn' : m' < n
hq : q = trinomial k m' n (↑x) (-↑v) ↑z
h1 : ↑y = -↑v
⊢ q = p ∨ q = -p ∨ q = p.mirror ∨ q = -p.mirror
Module: Mathlib.Algebra.Polynomial.SumIteratedDerivative

Goal state before:
pp: case inr.refine_2
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
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : x ∈ Ico 0 q ∩ Ico q (p.natDegree + 1)
⊢ False

Tactic:
rw [mem_inter, mem_Ico, mem_Ico] at hx

Goal state after:
case inr.refine_2
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
c_le : ∀ (k : ℕ), (c k).natDegree ≤ p.natDegree - k
hc : ∀ (k : ℕ), q ≤ k → ∀ (r : A), (aeval r) ((⇑derivative)^[k] p) = q ! • (aeval r) (c k)
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ (q - 1) * p'
this✝ : range (p.natDegree + 1) = range q ∪ Ico q (p.natDegree + 1)
this : range q = range (q - 1 + 1)
x : ℕ
hx : (0 ≤ x ∧ x < q) ∧ q ≤ x ∧ x < p.natDegree + 1
⊢ False
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,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k

Tactic:
have hc (i : ι) : ∃ (q' : R[X]) (r' : Fin (n i) → R[X]), i ∈ s →
      (∀ j, (r' j).degree < (g i).degree) ∧
      r i = q' * g i ^ (n i) + ∑ j, r' j * g i ^ j.1 :=
    if hi : i ∈ s then
      (eq_quo_mul_pow_add_sum_rem_mul_pow (r i) (hg i hi) (n i)).elim
        fun q' h => h.elim fun r' h => ⟨q', r', fun _ => h⟩
    else
      ⟨0, fun _ => 0, hi.elim⟩

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
hc :
  ∀ (i : ι),
    ∃ q' r', i ∈ s → (∀ (j : Fin (n i)), (r' j).degree < (g i).degree) ∧ r i = q' * g i ^ n i + ∑ j, r' j * g i ^ ↑j
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : star z ∈ (QuadraticAlgebra R a b)⁰
⊢ z ∈ (QuadraticAlgebra R a b)⁰

Tactic:
← star_involutive z

Goal state after:
R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
h : star z ∈ (QuadraticAlgebra R a b)⁰
⊢ star (star z) ∈ (QuadraticAlgebra R a b)⁰
Module: Mathlib.Algebra.Polynomial.PartialFractions

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
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 : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      (algebraMap R[X] K) f * ∏ i ∈ s, gi i ^ n i =
        (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)

Tactic:
obtain ⟨q, r, hr, hf⟩ := eq_quo_mul_prod_pow_add_sum_rem_mul_prod_pow f hg hgg n

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : Nontrivial R
ι : Type u_3
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 : ι → ℕ
gi : ι → K
hgi : ∀ i ∈ s, gi i * (algebraMap R[X] K) (g i) = 1
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
hr : ∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree
hf : f = q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, ∑ j, r i j * g i ^ ↑j * ∏ k ∈ s.erase i, g k ^ n k
⊢ ∃ q r,
    (∀ i ∈ s, ∀ (j : Fin (n i)), (r i j).degree < (g i).degree) ∧
      (algebraMap R[X] K) f * ∏ i ∈ s, gi i ^ n i =
        (algebraMap R[X] K) q + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r i j) * gi i ^ (↑j + 1)
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x = F ⟦x⟧
ih_y : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y = F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
this : ∀ (x y : EnvelGroup R), F (Mul.mul x y) = F x * F y
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) =
    mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x * F ⟦y⟧

Tactic:
← ih_y,

Goal state after:
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x y : PreEnvelGroup R
ih_x : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x = F ⟦x⟧
ih_y : mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y = F ⟦y⟧
hm : ⟦x.mul y⟧ = Mul.mul ⟦x⟧ ⟦y⟧
this : ∀ (x y : EnvelGroup R), F (Mul.mul x y) = F x * F y
⊢ mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) (x.mul y) =
    mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) x * mapAux ((Quandle.Conj.map F).comp (toEnvelGroup R)) y
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a.refine_1
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
B : Basis A c₁ c₂ c₃
y : ℍ[R,c₁,c₂,c₃]
⊢ (algebraMap R A) y.re ∈ R[B.i, B.j, B.k]

Tactic:
exact algebraMap_mem _ _

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)

Tactic:
simp only [Function.comp_apply]
  rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]

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

Goal state before:
pp: case comm
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: case left_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: case right_assoc
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonAssocSemiring α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
a : G
b : k
⊢ ↑(algebraMap k A) b * F a = (algebraMap k A) b * F a

Tactic:
AddMonoidHom.coe_coe

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
A : Type u_4
inst✝³ : Semiring A
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G k
inst✝ : SMulCommClass G k k
F : G →* A
a : G
b : k
⊢ (algebraMap k A) b * F a = (algebraMap k A) b * F a
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
R : Type uR
inst✝ : Ring R
r : R → R → Prop
⊢ ∀ (a b : RingQuot r), a - b = a + -b

Tactic:
rintro ⟨⟨⟩⟩ ⟨⟨⟩⟩
    simp [neg_quot, sub_quot, add_quot, sub_eq_add_neg]

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: B : Type uR
inst✝ : CommRing B
r : B → B → Prop
x : B
⊢ (ringQuotToIdealQuotient r) ((mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x

Tactic:
by
  simp_rw [ringQuotToIdealQuotient, lift_def, preLift_def, mkRingHom_def]
  rfl

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
⊢ ({ toFun := fun f' ↦ preLiftAlgHom S ⋯, invFun := fun F ↦ ⟨F.comp (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ((mkAlgHom S s) x) =
    f x

Tactic:
preLiftAlgHom_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 (mkAlgHom S s), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
        ⟨f, w⟩)
      ((mkAlgHom S s) x) =
    f x
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ p.sum f = ∑ n ∈ p.support, f n (p.coeff n)

Tactic:
simp only [sum_def', SkewMonoidAlgebra.sum_def, Finsupp.sum]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
S : Type u_5
inst✝ : AddCommMonoid S
p : SkewPolynomial R
f : ℕ → R → S
⊢ ∑ x ∈ p.coeff.support, f (toAdd x) (p.coeff x) = ∑ n ∈ p.support, f n (p.coeff n)
Module: Mathlib.Algebra.Star.Free

Goal state before:
pp: case refine_1
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)
⊢ ∀ (r : R),
    MulOpposite.unop (y (MulOpposite.unop (y ((algebraMap R (FreeAlgebra R X)) r)))) =
      (algebraMap R (FreeAlgebra R X)) r

Tactic:
intros
      simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]

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

Goal state before:
pp: case comm
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a : α), Commute (T 1) a

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: case left_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (b c : α), T 1 * (b * c) = T 1 * b * c

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: case right_assoc
α : Type u_1
inst✝¹ : NonAssocSemiring α
inst✝ : StarRing α
T : CentroidHom α
⊢ ∀ (a b : α), a * b * T 1 = a * (b * T 1)

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ a • X ^ n = (monomial n) a

Tactic:
rw [eq_comm]
  calc monomial n a = monomial n (a * 1) := by simp only [mul_one]
    _ = monomial n (a • 1) := by simp [mul_one, smul_eq_mul]
    _ = a • monomial n 1 := (SkewMonoidAlgebra.smul_single _ _ _).symm
    _ = a • X ^ n  := by rw [X_pow_eq_monomial]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
a b : G →₀ k
⊢ { coeff := a + b } = { coeff := a }.add { coeff := b }

Tactic:
rw [add]

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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g h : SkewMonoidAlgebra k G
x : G
a : k
⊢ single x a * g * h = single x a * (g * h)

Tactic:
induction g with
      | single y b => induction h with
        | single z c => simp [mul_assoc, mul_smul, mul_def]
        | add => simp_all [mul_add]
      | add => simp_all [add_mul, mul_add]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
hvy : star y * y = 1 ∨ ↑v = 0
⊢ ∃ α, u = α • v

Tactic:
obtain (this | this) := hvy

Goal state after:
case inl
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : star y * y = 1
⊢ ∃ α, u = α • v

case inr
R : Type u_3
S : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : StarMul R
inst✝⁶ : CommRing S
inst✝⁵ : StarMul S
inst✝⁴ : Algebra S R
inst✝³ : StarModule S R
inst✝² : Algebra.IsCentral S R
inst✝¹ : IsCancelMulZero S
inst✝ : Module.IsTorsionFree S R
u v : ↥(unitary R)
x✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
hvu : ↑v = star y • ↑u
this : ↑v = 0
⊢ ∃ α, u = α • v
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrderedAddCommMonoidWithTop R
x✝ : Tropical R
⊢ untrop (x✝ * 0) = untrop 0

Tactic:
by simp [add_top]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
this : ∀ {a : G} {b₁ b₂ : k}, single 1 b₁ * single a b₂ = single a (b₁ * b₂)
a : G
b : k
⊢ ((fun f ↦ ↑f) f) (single a (b * 1)) = ((fun f ↦ ↑f) g) (single a (b * 1))

Tactic:
← this,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ : ∀ (b : k), f (single 1 b) = g (single 1 b)
h_of : ∀ (a : G), f (single a 1) = g (single a 1)
this : ∀ {a : G} {b₁ b₂ : k}, single 1 b₁ * single a b₂ = single a (b₁ * b₂)
a : G
b : k
⊢ ((fun f ↦ ↑f) f) (single 1 b * single a 1) = ((fun f ↦ ↑f) g) (single 1 b * single a 1)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ single g (r • 1) = single g r

Tactic:
smul_eq_mul,

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
r : k
⊢ single g (r * 1) = single g r
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ (t • a) • b = t • a • b

Tactic:
simp only [smul_eq_mul]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : IsScalarTower k k k
t : k
a b : SkewMonoidAlgebra k G
⊢ t • a * b = t • (a * b)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ IsUnit (x • 1 - (star f).ofConv) ↔ IsUnit (star x • 1 - f.ofConv)

Tactic:
rw [← isUnit_intrinsicStar_iff]

Goal state after:
R : Type u_4
V : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommGroup V
inst✝² : StarAddMonoid V
inst✝¹ : Module R V
inst✝ : StarModule R V
f : WithConv (End R V)
x : R
⊢ IsUnit (star (toConv (x • 1 - (star f).ofConv))).ofConv ↔ IsUnit (star x • 1 - f.ofConv)
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ Hom.stalkMap α x ≫ eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x) =
    𝟙 (Y.presheaf.stalk ((ConcreteCategory.hom α.base) x))

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ (eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x)) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)

Tactic:
· rw [← Category.assoc, congr_point α x ((α ≫ β).base x) h_eq.symm, Category.assoc]
      erw [← stalkMap.comp β α (α.base x)]
      rw [congr_hom _ _ (IsIso.inv_hom_id α), stalkMap.id, eqToHom_trans_assoc, eqToHom_refl,
        Category.id_comp]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
inst✝ : IsIso α
x : ↑↑X
β : Y ⟶ X := CategoryTheory.inv α
h_eq : (ConcreteCategory.hom (α ≫ β).base) x = x
⊢ (eqToHom ⋯ ≫ Hom.stalkMap β ((ConcreteCategory.hom α.base) x)) ≫ Hom.stalkMap α x = 𝟙 (X.presheaf.stalk x)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f) ≤ X.basicOpen f

pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
· rw [X.basicOpen_res i f]; exact inf_le_right

Goal state after:
case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: 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

Tactic:
exact fun x H f hf hxf ↦ H f (h hf) hxf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Tactic:
have : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 _ := by
    rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
  cases h
  refine (Scheme.Hom.congr_app this _).trans ?_
  simp [eqToHom_map]

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

Goal state before:
pp: case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ invApp f x ≫
      g.c.app (op (⋯.functor.obj x)) ≫
        s.snd.c.app ((Opens.map g.base).op.obj (op (⋯.functor.obj x))) ≫
          ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
            s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)

Tactic:
← this,

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
x : Opens ↑↑X
this :
  ∀ {Z_1 : C}
    (h : ((TopCat.Presheaf.pushforward C (s.snd ≫ g).base).obj s.pt.presheaf).obj (op ((opensFunctor f).obj x)) ⟶ Z_1),
    f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫ inv (s.pt.presheaf.map (eqToHom ⋯)) ≫ h =
      g.c.app (op ((opensFunctor f).obj x)) ≫ s.snd.c.app (op ((Opens.map g.base).obj ((opensFunctor f).obj x))) ≫ h
⊢ invApp f x ≫
      f.c.app (op ((opensFunctor f).obj x)) ≫
        s.fst.c.app (op ((Opens.map f.base).obj ((opensFunctor f).obj x))) ≫
          inv (s.pt.presheaf.map (eqToHom ⋯)) ≫
            ((TopCat.Presheaf.pushforward C s.snd.base).obj s.pt.presheaf).map (eqToHom ⋯) ≫
              s.pt.presheaf.map (eqToHom ⋯ ≫ (eqToHom ⋯).app (op x)) =
    s.fst.c.app (op x)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g) Scheme.forget

Tactic:
delta Scheme.forget

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g) (Scheme.forgetToTop ⋙ «forget» TopCat)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan g f) Scheme.forget

Tactic:
delta Scheme.forget

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan g f) (Scheme.forgetToTop ⋙ «forget» TopCat)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
x : ↥X
⊢ x ∈ ⋃ i, Set.range ⇑(𝒰.f i)

Tactic:
rw [Set.mem_iUnion]

Goal state after:
K : Precoverage Scheme
inst✝ : JointlySurjective K
X : Scheme
𝒰 : Cover K X
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑(𝒰.f i)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)

Tactic:
← f.image_preimage_eq_opensRange_inf,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ f ⁻¹ᵁ U