mathlib-initiative/mathlib-tactics huggingface dataset:
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, g i ^ n i + (∑ 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:
add_assoc,

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
⊢ q * ∏ i ∈ s, g i ^ n i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k ^ n k =
    q * ∏ i ∈ s, g i ^ n i +
      ((∑ 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)
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz :
  (z * (algebraMap R (QuadraticAlgebra R a b)) r).re = re 0 ∧ (z * (algebraMap R (QuadraticAlgebra R a b)) r).im = im 0
⊢ z = 0

Tactic:
re_zero,

Goal state after:
case mpr
R : Type u_2
a b : R
inst✝ : CommRing R
r : R
h : ∀ (x : R), x * r = 0 → x = 0
z : QuadraticAlgebra R a b
hz : (z * (algebraMap R (QuadraticAlgebra R a b)) r).re = 0 ∧ (z * (algebraMap R (QuadraticAlgebra R a b)) r).im = im 0
⊢ z = 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
a b : K
Hab : Fact (∀ (r : K), r ^ 2 ≠ a + b * r)
z : QuadraticAlgebra K a b
hz : z.re * z.re + b * z.re * z.im - a * z.im * z.im = 0
h : z.im = 0
⊢ z = 0

Tactic:
simp [h] at hz
      aesop

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: R : Type u_2
inst✝ : Rack R
x y z : R
⊢ x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z

Tactic:
by
  rw [self_distrib]
  rw [left_cancel]

Goal state after:
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[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
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev = gi i ^ (↑j + 1) * gi i ^ ↑j.rev * (algebraMap R[X] K) (g i) ^ ↑j.rev

Tactic:
← pow_add,

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
hc : ∀ x ∈ s, (algebraMap R[X] K) (g x ^ n x) * gi x ^ n x = 1
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ n i * (algebraMap R[X] K) (g i) ^ ↑j.rev = gi i ^ (↑j + 1 + ↑j.rev) * (algebraMap R[X] K) (g i) ^ ↑j.rev
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✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
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₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1) * gi i ^ ↑j * (algebraMap R[X] K) (g i) ^ ↑j * (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (g i) ^ ↑j

Tactic:
← pow_add,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R[X] K
inst✝ : FaithfulSMul R[X] K
ι : Type u_3
s : Finset ι
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₁ q₂ : R[X]
r₁ r₂ : (i : ι) → Fin (n i) → R[X]
hr₁ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₁ i j).degree < (g i).degree
hr₂ : ∀ i ∈ s, ∀ (j : Fin (n i)), (r₂ i j).degree < (g i).degree
hf :
  (algebraMap R[X] K) q₁ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₁ i j) * gi i ^ (↑j + 1) =
    (algebraMap R[X] K) q₂ + ∑ i ∈ s, ∑ j, (algebraMap R[X] K) (r₂ i j) * gi i ^ (↑j + 1)
q : R[X]
r : (i : ι) → Fin (n i) → R[X]
i : ι
hi : i ∈ s
j : Fin (n i)
⊢ gi i ^ (↑j.rev + 1 + ↑j) * (algebraMap R[X] K) (g i) ^ ↑j * (algebraMap R[X] K) (g i) ^ n i =
    (algebraMap R[X] K) (g i) ^ ↑j
Module: Mathlib.Algebra.Ring.IsFormallyReal

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : ∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0
x : R
hx : IsSumNonzeroSq x
⊢ x ≠ 0

Tactic:
induction hx with
    | sq ha => exact fun hc ↦ ha (h IsSumSq.zero (by simpa using hc))
    | sq_add ha hs ih => grind [hs.isSumSq]

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

Goal state before:
pp: α : Type u_1
inst✝² : Mul α
inst✝¹ : Add α
inst✝ : RightDistribClass α
a b c : WithZero α
⊢ (a + b) * c = a * c + b * c

Tactic:
cases c; · simp
    cases a <;> cases b <;> try rfl
    exact congr_arg some (right_distrib _ _ _)

Goal state after:
Module: Mathlib.Algebra.RingQuot

Goal state before:
pp: R : Type uR
inst✝³ : Semiring R
S : Type uS
inst✝² : CommSemiring S
T : Type uT
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r✝ r : R → R → Prop
⊢ ∀ (x : RingQuot r), x ^ 0 = 1

Tactic:
by
    rintro ⟨⟨⟩⟩
    simp only [pow_quot, ← one_quot, pow_zero]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n m : ℕ
r s : R
⊢ (monomial n) r * (monomial m) s = (monomial (n + m)) (r * (⇑φ)^[n] s)

Tactic:
rw [φ_iterate_apply]

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : MulSemiringAction (Multiplicative ℕ) R
n m : ℕ
r s : R
⊢ (monomial n) r * (monomial m) s = (monomial (n + m)) (r * ofAdd n • s)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝ : AddMonoid k
p : SkewMonoidAlgebra k G
⊢ p.support = ∅ ↔ p = 0

Tactic:
by
  rcases p
  simp only [support, Finsupp.support_eq_empty, ofCoeff_eq_zero]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
a₂ : G'
⊢ (f.coeff.sum fun x1 x2 ↦ (g x1 x2).coeff) a₂ = f.coeff.sum fun a₁ b ↦ (g a₁ b).coeff a₂

Tactic:
Finsupp.sum_apply

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
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) := this.toFinset
F : G × G → k := fun p ↦ if p.1 * p.2 = x then f.coeff p.1 * p.1 • g.coeff p.2 else 0
⊢ ∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f.coeff p.1 * p.1 • g.coeff p.2 =
    ∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f.coeff p.1 * p.1 • g.coeff p.2

Tactic:
apply Finset.sum_congr_of_eq_on_inter

Goal state after:
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

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

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
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
h : s.Nonempty
⊢ untrop (∑ i ∈ s, f i) = sInf (untrop ∘ f '' ↑s)

Tactic:
· rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, Finset.untrop_sum']

Goal state after:
Module: Mathlib.Algebra.Symmetrized

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

Tactic:
add_assoc,

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

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

Tactic:
add_assoc,

Goal state after:
α : Type u_1
inst✝¹ : Ring α
inst✝ : Invertible 2
a b : αˢʸᵐ
commute_half_left : ∀ (a : α), ⅟2 * a = a * ⅟2
⊢ unsym a * unsym b * unsym a * unsym a +
        (unsym b * unsym a * unsym a * unsym a + unsym a * unsym a * unsym a * unsym b) -
      (unsym a * unsym b * unsym a * unsym a +
        (unsym a * unsym a * unsym a * unsym b + unsym b * unsym a * unsym a * unsym a)) =
    0
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
⊢ ((star (toConv comul)).ofConv ∘ₗ single R B i) x =
    ((toConv (↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ∘ₗ comul)).ofConv ∘ₗ single R B i) x

Tactic:
have := by simpa using congr($(h i) x)

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)
⊢ ((star (toConv comul)).ofConv ∘ₗ single R B i) x =
    ((toConv (↑(TensorProduct.comm R ((i : n) → B i) ((i : n) → B i)) ∘ₗ comul)).ofConv ∘ₗ single R B i) x
Module: Mathlib.Algebra.Tropical.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (untrop '' s)
⊢ BddBelow s

Tactic:
change BddBelow (tropOrderIso.symm '' s) at hs

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Set (Tropical R)
this : Set.range untrop = Set.univ
hs : BddBelow (⇑tropOrderIso.symm '' s)
⊢ BddBelow s
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 : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
⊢ Epi f

Tactic:
by
  constructor
  intro Z ⟨g, gc⟩ ⟨h, hc⟩ e
  apply_fun InducedCategory.Hom.hom at e
  obtain rfl : g = h := ConcreteCategory.hom_ext _ _ fun y ↦ by
    rw [← (h₁ y).choose_spec]
    simpa using congr(($e).base.hom (h₁ y).choose)
  refine SheafedSpace.hom_stalk_ext ⟨g, gc⟩ ⟨g, hc⟩ rfl fun y ↦ ?_
  rw [← (h₁ y).choose_spec, ← cancel_mono (f.hom.stalkMap (h₁ y).choose), stalkCongr_hom,
    stalkSpecializes_refl, Category.id_comp, ← PresheafedSpace.stalkMap.comp f.hom ⟨g, gc⟩,
    ← PresheafedSpace.stalkMap.comp f.hom ⟨g, hc⟩]
  congr 1

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
have h1 : X.presheaf.germ U x.val x.property f = X.presheaf.germ U x.val x.property 0 := by simpa

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↥U
h : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
h1 : (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) 0
⊢ ∃ V i, ∃ (_ : ↑x ∈ V), (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0
Module: Mathlib.Topology.Sheaves.SheafOfFunctions

Goal state before:
pp: case refine_1
X : TopCat
T : ↑X → Type u_1
ι : Type u_2
U : ι → Opens ↑X
sf : (i : ι) → ToType ((X.presheafToTypes T).obj (Opposite.op (U i)))
hsf : (X.presheafToTypes T).IsCompatible U sf
index : ↥(iSup U) → ι
index_spec : ∀ (x : ↥(iSup U)), ↑x ∈ U (index x)
s : (x : ↥(iSup U)) → T ↑x := fun x ↦ sf (index x) ⟨↑x, ⋯⟩
⊢ (fun s ↦ (X.presheafToTypes T).IsGluing U sf s) s

Tactic:
intro i
      funext x
      -- Now we need to verify that this lifted function restricts correctly to each set `U i`.
      -- Of course, the difficulty is that at any given point `x ∈ U i`,
      -- we may have used the axiom of choice to pick a different `j` with `x ∈ U j`
      -- when defining the function.
      -- Thus we'll need to use the fact that the restrictions are compatible.
      exact congr_fun (hsf (index ⟨x, _⟩) i) ⟨x, ⟨index_spec ⟨x.1, _⟩, x.2⟩⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.LocalPredicate

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

Tactic:
exact ⟨V ⊓ V', ⟨x.2, m'⟩, V.infLELeft _, P.res (V.infLERight V') _ p⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: case h
X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
⊢ toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf = toLRSHom'✝.c

Tactic:
exact TopCat.Presheaf.ext (fun U ↦ by simpa using! h_app U)

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
⊢ R ∈ (Precoverage.comap F Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))

Tactic:
rw [Precoverage.mem_comap_iff]
  refine ⟨fun h x ↦ ?_, fun h x ↦ ?_⟩
  · obtain ⟨-, -, ⟨hf⟩, hi⟩ := h x
    exact ⟨_, _, hf, hi⟩
  · obtain ⟨Y, g, hg, hi⟩ := h x
    exact ⟨_, _, ⟨hg⟩, hi⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) → x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥U
hx✝ : x ∈ ↑(f' ⁻¹ᵁ W)
hx : (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base) x ∉ Set.range ⇑iU
⊢ (ConcreteCategory.hom (LocallyRingedSpace.Hom.toShHom (Scheme.Hom.toLRSHom iU)).hom.base) x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: K : Precoverage Scheme
X Y Z : Scheme
𝒰✝ : Cover K X
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
𝒰 : Cover (precoverage P) X
x : ↥X
⊢ ∃ i, x ∈ Set.range ⇑({ I₀ := ↥X, X := fun x ↦ 𝒰.X (𝒰.idx x), f := fun x ↦ 𝒰.f (𝒰.idx x) }.f i)

Tactic:
use x, (𝒰.exists_eq x).choose_spec.choose, (𝒰.exists_eq x).choose_spec.choose_spec

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 V : Opens ↑(PrimeSpectrum.Top R)} (i : U ⟶ V) (f : (x : ↥V) → Localizations M ↑x),
    IsFraction f → IsFraction fun x ↦ f (i x)

Tactic:
rintro V U i f ⟨r, s, w⟩; exact ⟨r, s, fun x => w (i x)⟩

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
X : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ↑((structurePresheafInCommRingCat R ⋙ forget₂ CommRingCat RingCat).obj X)
    ↑((structurePresheafInModuleCat R M ⋙ forget₂ (ModuleCat R) Ab).obj X)

Tactic:
by
    dsimp; infer_instance

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥U
⊢ (U.stalkIso x).inv = Hom.stalkMap U.ι x

Tactic:
rw [← Category.comp_id (U.stalkIso x).inv, Iso.inv_comp_eq]

Goal state after:
X : Scheme
U : X.Opens
x : ↥U
⊢ 𝟙 ((↑U).presheaf.stalk x) = (U.stalkIso x).hom ≫ Hom.stalkMap U.ι x
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F : Presheaf CommRingCat X
G : F.SubmonoidPresheaf
U : (Opens ↑X)ᵒᵖ
⊢ CommRingCat.ofHom (IsLocalization.map (Localization (G.obj U)) (CommRingCat.Hom.hom (F.map (𝟙 U))) ⋯) =
    𝟙 (CommRingCat.of (Localization (G.obj U)))

Tactic:
by
    simp_rw [F.map_id]
    ext x
    exact IsLocalization.map_id x

Goal state after:
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X : TopCat
C : Type u
inst✝ : Category.{v, u} C
F✝ : Presheaf CommRingCat X
G : F✝.SubmonoidPresheaf
F : Sheaf CommRingCat X
⊢ Mono F.presheaf.toTotalQuotientPresheaf

Tactic:
apply +allowSynthFailures NatTrans.mono_of_mono_app
  intro U
  apply ConcreteCategory.mono_of_injective
  dsimp [toTotalQuotientPresheaf]
  -- Porting note: `M` and `S` need to be specified manually, so used a hack to save some typing
  set m := _
  change Function.Injective (algebraMap _ (Localization m))
  refine IsLocalization.injective (M := m) (S := Localization m) ?_
  rw [← nonZeroDivisorsRight_eq_nonZeroDivisors]
  intro s hs t e
  apply section_ext F (unop U)
  intro x hx
  rw [map_zero]
  apply (Submonoid.mem_iInf.mp hs ⟨x, hx⟩).2
  rw [← map_mul, e, map_zero]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
a : M
b : ↥(Submonoid.powers f)
c : M
d : ↥(Submonoid.powers f)
h_eq : (toBasicOpenₗ R M f) (LocalizedModule.mk a b) = (toBasicOpenₗ R M f) (LocalizedModule.mk c d)
this : f ∈ (⊥.colon {d • a - b • c}).radical
⊢ LocalizedModule.mk a b = LocalizedModule.mk c d

Tactic:
by
    rw [LocalizedModule.mk_eq]
    obtain ⟨n, hn⟩ := this
    exact ⟨⟨f ^ n, n, rfl⟩, by simpa [sub_eq_zero, smul_sub] using! Submodule.mem_colon.mp hn _ rfl⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op

Tactic:
rw [IsAffineOpen.fromSpec, Scheme.Hom.comp_app, Scheme.Opens.ι_app, Scheme.Hom.app_eq _ this,
    ← Scheme.Hom.appTop, IsAffineOpen.isoSpec_inv_appTop]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ X.presheaf.map (homOfLE ⋯).op ≫
      (↑U).presheaf.map (eqToHom ⋯).op ≫
        (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Spec Γ(X, U)).presheaf.map (eqToHom ⋯).op =
    X.presheaf.map (homOfLE h).op ≫ (Scheme.ΓSpecIso Γ(X, U)).inv ≫ (Spec Γ(X, U)).presheaf.map (homOfLE ⋯).op