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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - ((c₁ * c₃) • 1 + c₂ • (q.i * q.j * q.j)) = -((c₁ * c₃) • 1)

Tactic:
mul_assoc,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ c₂ • (q.i * c₃ • 1) - ((c₁ * c₃) • 1 + c₂ • (q.i * (q.j * q.j))) = -((c₁ * c₃) • 1)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False

Tactic:
← isSumNonzeroSq_iff_isSumSq h₂

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : IsFormallyReal R
s₁ s₂ : R
hs₁ : IsSumNonzeroSq s₁
hs₂ : IsSumNonzeroSq s₂
h : s₁ + s₂ = 0
h₁ : s₁ ≠ 0
h₂ : s₂ ≠ 0
⊢ False
Module: Mathlib.Algebra.Ring.CentroidHom

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝¹² : NonUnitalNonAssocSemiring α
inst✝¹¹ : Monoid M
inst✝¹⁰ : Monoid N
inst✝⁹ : Semiring R
inst✝⁸ : DistribMulAction M α
inst✝⁷ : SMulCommClass M α α
inst✝⁶ : IsScalarTower M α α
inst✝⁵ : DistribMulAction N α
inst✝⁴ : SMulCommClass N α α
inst✝³ : IsScalarTower N α α
inst✝² : Module R α
inst✝¹ : SMulCommClass R α α
inst✝ : IsScalarTower R α α
n : M
f : CentroidHom α
a b : α
⊢ (↑(n • ↑f)).toFun (a * b) = a * (↑(n • ↑f)).toFun b

Tactic:
by
        change n • f (a * b) = a * n • f b
        rw [map_mul_left f, ← mul_smul_comm]

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

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ ((f * g) a✝ - (g * f) a✝) * r * ((f * g) a✝ - (g * f) a✝) = 0

Tactic:
mul_assoc,

Goal state after:
F : Type u_1
M : Type u_2
N : Type u_3
R : Type u_4
α : Type u_5
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
f g : CentroidHom α
a✝ r : α
⊢ ((f * g) a✝ - (g * f) a✝) * (r * ((f * g) a✝ - (g * f) a✝)) = 0
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: case mp.rel.mul_right
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
x₁ x₂ x✝ y✝ a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : RingConGen.Rel r b✝ c✝
⊢ RingConGen.Rel r (a✝¹ * b✝) (a✝¹ * c✝)

Tactic:
| mul_right _ h =>

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

Goal state before:
pp: A : Type v
B : Type w
C : Type w'
R : Type v
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : Star R
p q : NonUnitalStarSubsemiring R
h : (fun {s} ↦ s.carrier) = fun {s} ↦ s.carrier
⊢ p = q

Tactic:
cases p; cases q; congr; exact SetLike.coe_injective h

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

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ X ^ n * X * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)

Tactic:
mul_assoc,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ X ^ n * (X * p) = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ((p.sum fun a b ↦ (monomial a) (φ b)).sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n * X =
    (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)

Tactic:
mul_assoc,

Goal state after:
case succ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n : ℕ
ih : ∀ {p : SkewPolynomial R}, X ^ n * p = (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * X ^ n
p : SkewPolynomial R
⊢ ((p.sum fun a b ↦ (monomial a) (φ b)).sum fun a b ↦ (monomial a) ((⇑φ)^[n] b)) * (X ^ n * X) =
    (p.sum fun a b ↦ (monomial a) ((⇑φ)^[n + 1] b)) * X ^ (n + 1)
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ C a * X = (monomial 1) a

Tactic:
← C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
a : R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ C a * X = C a * X ^ 1
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:
rw [C_mul_X_pow_eq_monomial, support_monomial n h]

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : Nontrivial R
n : ℕ
inst✝ : MulSemiringAction (Multiplicative ℕ) R
⊢ (X ^ n).support = {n}

Tactic:
convert support_monomial n (NeZero.out (n := (1 : R)))
  exact X_pow_eq_monomial n

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

Goal state before:
pp: case mul_right
R : Type u
inst✝¹ : Semiring R
r : R → R → Prop
inst✝ : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a✝¹ b✝ c✝ : R
a✝ : Rel r b✝ c✝
h : Rel r (Star.star b✝) (Star.star c✝)
⊢ Rel r (Star.star (a✝¹ * b✝)) (Star.star (a✝¹ * c✝))

Tactic:
| mul_right _ h =>

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
S : Type u_3
inst✝ : AddCommMonoid S
f : G → k → S
⊢ sum 0 f = 0

Tactic:
by simp [sum]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * f (y • b.coeff x) * (g y * g x) = f (a.coeff y) * g y * (f (b.coeff x) * g x)

Tactic:
mul_assoc,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * (f (y • b.coeff x) * (g y * g x)) = f (a.coeff y) * g y * (f (b.coeff x) * g x)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * (g y * f (b.coeff x) * g x) = f (a.coeff y) * g y * (f (b.coeff x) * g x)

Tactic:
mul_assoc,

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁵ : Mul G
R : Type u_3
inst✝⁴ : Semiring R
inst✝³ : NonAssocSemiring k
inst✝² : SMul G k
g_hom : Type u_4
inst✝¹ : FunLike g_hom G R
inst✝ : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm : ∀ {x y : G}, y ∈ a.support → f (y • b.coeff x) * g y = g y * f (b.coeff x)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
⊢ f (a.coeff y) * (g y * (f (b.coeff x) * g x)) = f (a.coeff y) * g y * (f (b.coeff x) * g x)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ↑(toUnits v) * a * ↑(toUnits v)⁻¹ = ↑(toUnits u) * a * ↑(toUnits u)⁻¹) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
mul_assoc,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), ↑(toUnits v) * (a * ↑(toUnits v)⁻¹) = ↑(toUnits u) * (a * ↑(toUnits u)⁻¹)) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

Goal state before:
pp: R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * ↑(toUnits v)⁻¹ * ↑(toUnits u) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)

Tactic:
mul_assoc,

Goal state after:
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : StarMul R
S : Type u_3
inst✝² : CommSemiring S
inst✝¹ : Algebra S R
inst✝ : Algebra.IsCentral S R
u v : ↥(unitary R)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * (↑(toUnits u) * a)) ↔
    ∃ α, ↑(toUnits u) = α • ↑(toUnits v)
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)
⊢ (∀ (a : R), ↑(toUnits v) * a * ↑(toUnits v)⁻¹ = ↑(toUnits u) * a * ↑(toUnits u)⁻¹) ↔ ∃ α, u = α • v

Tactic:
mul_assoc,

Goal state after:
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)
⊢ (∀ (a : R), ↑(toUnits v) * (a * ↑(toUnits v)⁻¹) = ↑(toUnits u) * (a * ↑(toUnits u)⁻¹)) ↔ ∃ α, u = α • v
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)
⊢ (∀ (a : R), a * ↑(toUnits v)⁻¹ * ↑(toUnits u) = ↑(toUnits v)⁻¹ * ↑(toUnits u) * a) ↔ ∃ α, u = α • v

Tactic:
mul_assoc,

Goal state after:
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)
⊢ (∀ (a : R), a * (↑(toUnits v)⁻¹ * ↑(toUnits u)) = ↑(toUnits v)⁻¹ * (↑(toUnits u) * a)) ↔ ∃ α, u = α • v
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✝ : ∃ α, u = α • v
y : ↥(unitary S)
h : u = y • v
⊢ ↑y • 1 = star ↑v * ↑u

Tactic:
simp only [h, coe_smul, mul_smul_comm, SetLike.coe_mem, star_mul_self_of_mem]

Goal state after:
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✝ : ∃ α, u = α • v
y : ↥(unitary S)
h : u = y • v
⊢ ↑y • 1 = y • 1
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ untrop (a + b) = untrop (if a ≤ b then a else b)

Tactic:
simp only [untrop_add, min_def, untrop_le_iff]

Goal state after:
R : Type u
inst✝ : LinearOrder R
a b : Tropical R
⊢ (if a ≤ b then untrop a else untrop b) = untrop (if a ≤ b then a else b)
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (⅟2 * (unsym a * unsym b + unsym b * unsym a) * unsym (a * a) +
          ⅟2 * unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
mul_assoc,

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (⅟2 * ((unsym a * unsym b + unsym b * unsym a) * unsym (a * a)) +
          ⅟2 * unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Algebra.Symmetrized

Goal state before:
pp: case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (⅟2 * ((unsym a * unsym b + unsym b * unsym a) * unsym (a * a)) +
          ⅟2 * unsym (a * a) * (unsym a * unsym b + unsym b * unsym a))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))

Tactic:
mul_assoc,

Goal state after:
case calc_1
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ sym
      (⅟2 *
        (⅟2 * ((unsym a * unsym b + unsym b * unsym a) * unsym (a * a)) +
          ⅟2 * (unsym (a * a) * (unsym a * unsym b + unsym b * unsym a)))) =
    sym
      (⅟2 * ⅟2 *
        (unsym a * unsym b * unsym (a * a) + unsym b * unsym a * unsym (a * a) + unsym (a * a) * unsym a * unsym b +
          unsym (a * a) * unsym b * unsym a))
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
f : WithConv (End R E)
hf : IsUnit f.ofConv
⊢ IsUnit (star f).ofConv

Tactic:
have ⟨u, hu⟩ := hf

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : InvolutiveStar R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : StarAddMonoid E
inst✝ : StarModule R E
f : WithConv (End R E)
hf : IsUnit f.ofConv
u : (End R E)ˣ
hu : ↑u = f.ofConv
⊢ IsUnit (star f).ofConv
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x

Tactic:
Iso.comp_inv_eq,

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    (colimit.ι
          (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
            X.presheaf)
          (op V) ≫
        Hom.stalkMap (X.ofRestrict h) x) ≫
      (X.restrictStalkIso h x).hom
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ ⋯.functor.op ⋙ X.presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
Opens.inclusion'_top_functor X.carrier

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (Opens.map (Opens.inclusionTopIso ↑X).inv).op ⋙ X.presheaf =
    (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ IsIso
    (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)

Tactic:
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.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
this :
  IsIso (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom
⊢ Function.Bijective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
        (algebraMap (↑R) (Localization M)) ⋯)

Tactic:
ConcreteCategory.isIso_iff_bijective

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
this :
  Function.Bijective
    ⇑(ConcreteCategory.hom
        (IsLocalization.localizationLocalizationAtPrimeIsoLocalization M x.asIdeal).toRingEquiv.toCommRingCatIso.hom)
⊢ Function.Bijective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
        (algebraMap (↑R) (Localization M)) ⋯)
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
⊢ IsUnit ((algebraMap (↑R) (Localization.AtPrime x.asIdeal)) f) ↔ f ∉ x.asIdeal

Tactic:
exact IsLocalization.AtPrime.isUnit_to_map_iff _ (PrimeSpectrum.asIdeal x) f

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s ^ n)

Tactic:
exact IsUnit.pow n hx

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
change (e.hom ≫ e.inv) x = 𝟙 X.toPresheafedSpace x
  simp

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

Goal state before:
pp: case property
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst = s.fst ∧
    pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
      ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
        m ≫ (pullbackConeOfLeft f g).fst = s.fst →
          m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s

Tactic:
use pullbackConeOfLeftLift_fst f g s

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
⊢ pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd = s.snd ∧
    ∀ {m : s.pt ⟶ (pullbackConeOfLeft f g).pt},
      m ≫ (pullbackConeOfLeft f g).fst = s.fst →
        m ≫ (pullbackConeOfLeft f g).snd = s.snd → m = pullbackConeOfLeftLift f g s
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (colimit.ι F i).hom.base) y) =
    (ConcreteCategory.hom
        ((preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      ((ConcreteCategory.hom (forgetToPresheafedSpace.map (colimit.ι F j)).base) x)
⊢ False

Tactic:
change
    ((SheafedSpace.forget C).map (colimit.ι F i) ≫ (preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) y =
      ((SheafedSpace.forget C).map (colimit.ι F j) ≫ (preservesColimitIso (forget C) F).hom ≫
          (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
            (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom) x at eq

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
i j : Discrete ι
h : i ≠ j
U : Opens ↑↑(F.obj i).toPresheafedSpace
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
y : ↑↑(F.obj i).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F i) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F j) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False