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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * (x.imK * y.imI)) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)

Tactic:
simp only [← 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₃
x y : ℍ[R,c₁,c₂,c₃]
⊢ (x * y).re • 1 + (x * y).imI • q.i + (x * y).imJ • q.j + (x * y).imK • q.k =
    (x.re * y.re) • 1 + (x.re * y.imI) • q.i + (x.re * y.imJ) • q.j + (x.re * y.imK) • q.k + (x.imI * y.re) • q.i +
                          (x.imI * y.imI) • (c₁ • 1 + c₂ • q.i) +
                        (x.imI * y.imJ) • q.k +
                      (x.imI * y.imK) • (c₁ • q.j + c₂ • q.k) +
                    (x.imJ * y.re) • q.j +
                  (x.imJ * y.imI) • (c₂ • q.j + -q.k) +
                (x.imJ * c₃ * y.imJ) • 1 +
              (x.imJ * y.imK) • ((c₂ * c₃) • 1 + -(c₃ • q.i)) +
            (x.imK * y.re) • q.k +
          -((c₁ * x.imK * y.imI) • q.j) +
        (x.imK * c₃ * y.imJ) • q.i +
      -((c₁ * c₃ * x.imK * y.imK) • 1)
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s a✝ : R
ha✝ : a✝ ≠ 0
⊢ IsSumSq (a✝ * a✝)

Tactic:
aesop

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

Goal state before:
pp: case sq_add
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
s a✝ s✝ : R
ha✝ : a✝ ≠ 0
hs✝ : IsSumNonzeroSq s✝
hs_ih✝ : IsSumSq s✝
⊢ IsSumSq (a✝ * a✝ + s✝)

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x : R
hx : x ∈ {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ x ∈ ↑(sumNonzeroSq R)

Tactic:
aesop

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

Goal state before:
pp: case sq
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ : R
ha : a✝ ≠ 0
⊢ a✝ * a✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

Tactic:
aesop

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

Goal state before:
pp: case sq_add.a
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ a✝ * a✝ ∈ {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

Tactic:
aesop

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

Goal state before:
pp: case sq_add.a
R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
x a✝ s✝ : R
ha : a✝ ≠ 0
hs : IsSumNonzeroSq s✝
ih : s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}
⊢ s✝ ∈ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x}

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : Mul R
⊢ closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x} = sumNonzeroSq R

Tactic:
by
  refine closure_eq_of_le (fun x hx ↦ by aesop) (fun x hx ↦ ?_)
  -- TODO : fix aesop timeout and change to `induction hx <;> aesop`
  induction hx with
  | sq ha => aesop
  | sq_add ha hs ih =>
    -- `aesop` times out
    apply add_mem
    · apply AddSubsemigroup.mem_closure_of_mem
      aesop
    aesop

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocCommSemiring α
a : α
⊢ (L a = L a ∧ ∀ g ∈ Set.range ⇑L, g * L a = L a * g) ↔ ∀ (b : α), Commute (L b) (L a)

Tactic:
aesop

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

Goal state before:
pp: k : Type u_1
G : Type u_2
A : Type u_4
inst✝⁵ : Monoid G
inst✝⁴ : Semiring A
inst✝³ : CommSemiring k
inst✝² : Algebra k A
inst✝¹ : MulSemiringAction G A
inst✝ : SMulCommClass G k A
⊢ ∀ (a : SkewMonoidAlgebra A G), (domCongrAlg k A ⋯) a = AlgEquiv.refl a

Tactic:
aesop

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
⊢ p.support = ∅ ↔ p = 0

Tactic:
by simp [support]

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 : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    (√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₁) + (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₁) - (√2)⁻¹ • (B₀ * (√2)⁻¹ • A₁) +
          ((√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₀) + (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₀) - (√2)⁻¹ • (B₀ * (√2)⁻¹ • A₀)) -
        ((√2)⁻¹ • ((√2)⁻¹ • A₁ * B₀) + (√2)⁻¹ • ((√2)⁻¹ • A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      ((√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₁) - (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₁) + (√2)⁻¹ • (B₁ * (√2)⁻¹ • A₁) -
          ((√2)⁻¹ • ((√2)⁻¹ • A₁ * (√2)⁻¹ • A₀) - (√2)⁻¹ • ((√2)⁻¹ • A₀ * (√2)⁻¹ • A₀) + (√2)⁻¹ • (B₁ * (√2)⁻¹ • A₀)) +
        ((√2)⁻¹ • ((√2)⁻¹ • A₁ * B₁) - (√2)⁻¹ • ((√2)⁻¹ • A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))

Tactic:
simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, ← mul_smul, sqrt_two_inv_mul_self]

Goal state after:
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 : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      (((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))
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 : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • (B₀ * B₀)) +
      (((√2)⁻¹ * 2⁻¹) • (A₁ * A₁) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₀) + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • (B₁ * B₁)))

Tactic:
simp only [← sq, T.A₀_inv, T.A₁_inv, T.B₀_inv, T.B₁_inv]

Goal state after:
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 : ∀ (m : ℤ) (a : ℝ) (x : R), m • a • x = (↑m * a) • x
P : R := (√2)⁻¹ • (A₁ + A₀) - B₀
Q : R := (√2)⁻¹ • (A₁ - A₀) + B₁
⊢ √2 ^ 3 • 1 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁ =
    ((√2)⁻¹ * 2⁻¹) • 1 + ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) - 2⁻¹ • (B₀ * A₁) +
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) + ((√2)⁻¹ * 2⁻¹) • 1 - 2⁻¹ • (B₀ * A₀)) -
        (2⁻¹ • (A₁ * B₀) + 2⁻¹ • (A₀ * B₀) - (√2)⁻¹ • 1) +
      (((√2)⁻¹ * 2⁻¹) • 1 - ((√2)⁻¹ * 2⁻¹) • (A₀ * A₁) + 2⁻¹ • (B₁ * A₁) -
          (((√2)⁻¹ * 2⁻¹) • (A₁ * A₀) - ((√2)⁻¹ * 2⁻¹) • 1 + 2⁻¹ • (B₁ * A₀)) +
        (2⁻¹ • (A₁ * B₁) - 2⁻¹ • (A₀ * B₁) + (√2)⁻¹ • 1))
Module: Mathlib.Algebra.SkewPolynomial.Basic

Goal state before:
pp: case h0
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ motive 0

Tactic:
aesop

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

Goal state before:
pp: case ha
R : Type u_1
inst✝ : Semiring R
motive : SkewPolynomial R → Prop
p : SkewPolynomial R
h0 : motive 0
ha : ∀ (n : ℕ) (r : R) (q : SkewPolynomial R), n ∉ q.support → r ≠ 0 → motive q → motive ((monomial n) r + q)
⊢ ∀ (a : Multiplicative ℕ) (b : R) (f : SkewMonoidAlgebra R (Multiplicative ℕ)),
    a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)

Tactic:
aesop

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:
by
  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.SkewPolynomial.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : SkewPolynomial R
n : ℕ
a : R
⊢ (p.update n a).coeff = Function.update p.coeff n a

Tactic:
ext; simp [coeff, update]; rfl

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
G' : Type u_3
f : G → G'
v : SkewMonoidAlgebra k G
R : Type u_5
inst✝¹ : Monoid R
inst✝ : DistribMulAction R k
b : R
⊢ (mapDomain f) (b • v) = b • (mapDomain f) v

Tactic:
by
  simp_rw [← coeff_inj, coeff_smul, coeff_mapDomain]
  simp [Finsupp.mapDomain_smul]

Goal state after:
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
f g : SkewMonoidAlgebra k G
x : G
⊢ (Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2) ⊆ ↑(f.support.product g.support)

Tactic:
aesop

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

Goal state before:
pp: R : Type u
inst✝² : LinearOrder R
inst✝¹ : OrderTop R
inst✝ : Zero R
n : ℕ
⊢ untrop (if n + 1 = 0 then 0 else 1) = untrop ((if n = 0 then 0 else 1) + 1)

Tactic:
by cases n <;> simp

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

Goal state before:
pp: case h₁
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = 0

Tactic:
aesop

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

Goal state before:
pp: case h₂
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support},
    a ∉ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x} → f.coeff a.1 * a.1 • g.coeff a.2 = 0

Tactic:
aesop

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

Goal state before:
pp: case h
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
f g : SkewMonoidAlgebra k G
x : G
this : ({p | p.1 * p.2 = x} ∩ Function.support fun p ↦ f.coeff p.1 * p.1 • g.coeff p.2).Finite
s : Finset (G × G) := ⋯
F : G × G → k := ⋯
⊢ ∀ a ∈ {p ∈ f.support ×ˢ g.support | p.1 * p.2 = x},
    a ∈ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support} → f.coeff a.1 * a.1 • g.coeff a.2 = f.coeff a.1 * a.1 • g.coeff a.2

Tactic:
aesop

Goal state after:
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)
⊢ 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:
let i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
    homOfLE (Set.image_preimage_subset f _)

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) ≫
      (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
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) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (X.restrict h).presheaf)
            ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)) ≫
          (X.restrictStalkIso h x).hom

Tactic:
erw [colimit.ι_pre ((OpenNhds.inclusion (f x)).op ⋙ X.presheaf)
      (h.functorNhds x).op]

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) =
    (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
            (X.ofRestrict h).c).app
        (op V) ≫
      (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
          (op V) ≫
        colimit.ι ((OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op ⋙ X.presheaf)
          ((h.functorNhds x).op.obj ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V)))
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
f g : X ⟶ Y
h : f.hom.base = g.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap f.hom x = (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g.hom x
⊢ f = g

Tactic:
obtain ⟨f, fc⟩ := f

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : HasColimits C
inst✝³ : HasLimits C
inst✝² : PreservesLimits (CategoryTheory.forget C)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝ : (CategoryTheory.forget C).ReflectsIsomorphisms
X Y : SheafedSpace C
g : X ⟶ Y
f : ↑X.toPresheafedSpace ⟶ ↑Y.toPresheafedSpace
fc : Y.presheaf ⟶ (pushforward C f).obj X.presheaf
h : { hom := { base := f, c := fc } }.hom.base = g.hom.base
h' :
  ∀ (x : ↑↑X.toPresheafedSpace),
    PresheafedSpace.Hom.stalkMap { hom := { base := f, c := fc } }.hom x =
      (Y.presheaf.stalkCongr ⋯).hom ≫ PresheafedSpace.Hom.stalkMap g.hom x
⊢ { hom := { base := f, c := fc } } = g
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y)ᵒᵖ
⊢ α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
by
  subst h
  simp

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

Goal state before:
pp: case mp
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) → x ∈ ↑(unop V ⊓ X.basicOpen f)

Tactic:
rintro ⟨hxV, hx⟩

Goal state after:
case mp
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
hxV : x ∈ unop V
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ (unop V) x hxV)) ((ConcreteCategory.hom (X.presheaf.map i)) f))
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case succ
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
n : ℕ
hn : 0 < n + Nat.succ 0 → X.basicOpen (f ^ (n + Nat.succ 0)) = X.basicOpen f
h : 0 < n + 1 + Nat.succ 0
⊢ X.basicOpen (f ^ (n + 1 + Nat.succ 0)) = X.basicOpen f

Tactic:
rw [pow_add]; simp_all

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

Goal state before:
pp: case a
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
hf : IsUnit f
⊢ X.basicOpen f ≤ U

Tactic:
exact X.basicOpen_le f

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case app
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
⊢ (Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
      ((Opens.map
              (colimit.isoColimitCocone
                      { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
        (op U)) =
    op ((Opens.map (colimit.ι F (unop X)).base).obj U)

Tactic:
simp only [Functor.op_obj, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
      Set.preimage_preimage]

Goal state after:
case app
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X : Jᵒᵖ
⊢ (fun x ↦
        (ConcreteCategory.hom
            (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base)
          ((ConcreteCategory.hom (colimit.ι (F ⋙ forget C) (unop X))) x)) ⁻¹'
      ↑U =
    ⇑(ConcreteCategory.hom (colimit.ι F (unop X)).base) ⁻¹' ↑U
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case naturality
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map
        ((NatIso.op
                  (Opens.mapIso ((F ⋙ forget C).map f.unop ≫ colimit.ι (F ⋙ forget C) (unop X))
                      (colimit.ι (F ⋙ forget C) (unop Y)) ⋯).symm).hom.app
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U)) ≫
          (eqToIso ⋯).hom) =
    (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      ((pushforward C (F.map f.unop).base).obj (F.obj (unop Y)).presheaf).map (eqToIso ⋯).hom ≫
        (F.obj (unop Y)).presheaf.map (eqToHom ⋯)

Tactic:
← (F.obj (unop Y)).presheaf.map_comp

Goal state after:
case naturality
J : Type u'
inst✝⁵ : Category.{v', u'} J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfShape J TopCat
inst✝² : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝¹ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
inst✝ : HasColimit F
U : Opens ↑↑(Limits.colimit F)
X Y : Jᵒᵖ
f : X ⟶ Y
⊢ (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map
        ((NatIso.op
                  (Opens.mapIso ((F ⋙ forget C).map f.unop ≫ colimit.ι (F ⋙ forget C) (unop X))
                      (colimit.ι (F ⋙ forget C) (unop Y)) ⋯).symm).hom.app
            ((Opens.map
                    (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
              (op U)) ≫
          (eqToIso ⋯).hom) =
    (F.map f.unop).c.app
        ((Opens.map (colimit.ι (F ⋙ forget C) (unop X))).op.obj
          ((Opens.map
                  (colimit.isoColimitCocone
                          { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
            (op U))) ≫
      (F.obj (unop Y)).presheaf.map ((Opens.map (F.map f.unop).base).op.map (eqToIso ⋯).hom ≫ eqToHom ⋯)