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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
p : R[X]
h_deg : p.natDegree < n
i : ℕ
h : n ≤ i
⊢ ((ofFn n) ((toFn n) p)).coeff i = p.coeff i

Tactic:
· have : p.coeff i = 0 := coeff_eq_zero_of_natDegree_lt <| by lia
    simp [*]

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

Goal state before:
pp: case cons
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
⊢ ∃ q r,
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k

Tactic:
obtain ⟨q, r, -, hf⟩ := ih hg.2 hgg.1

Goal state after:
case cons
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Nontrivial R
ι : Type u_2
inst✝ : DecidableEq ι
f : R[X]
g : ι → R[X]
i : ι
s : Finset ι
hi : i ∉ s
ih :
  (∀ i ∈ s, (g i).Monic) →
    ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) →
      ∃ q r, (∀ i ∈ s, (r i).degree < (g i).degree) ∧ f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
hg : (g i).Monic ∧ ∀ x ∈ s, (g x).Monic
hgg : ((↑s).Pairwise fun i j ↦ IsCoprime (g i) (g j)) ∧ ∀ b ∈ ↑s, i ≠ b → IsCoprime (g i) (g b) ∧ IsCoprime (g b) (g i)
q : R[X]
r : ι → R[X]
hf : f = q * ∏ i ∈ s, g i + ∑ i ∈ s, r i * ∏ k ∈ s.erase i, g k
⊢ ∃ q r,
    (∀ i_1 ∈ Finset.cons i s hi, (r i_1).degree < (g i_1).degree) ∧
      f =
        q * ∏ i ∈ Finset.cons i s hi, g i +
          ∑ i_1 ∈ Finset.cons i s hi, r i_1 * ∏ k ∈ (Finset.cons i s hi).erase i_1, g k
Module: Mathlib.Algebra.Polynomial.UnitTrinomial

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).coeff k ≠ 0

Tactic:
rwa [trinomial_trailing_coeff' hkm hmn]

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

Goal state before:
pp: case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 +
      ((trinomial k m n ↑u ↑v ↑w).coeff m ^ 2 + ∑ x ∈ {n}, (trinomial k m n ↑u ↑v ↑w).coeff x ^ 2) =
    3

Tactic:
sum_singleton,

Goal state after:
case refine_1
k m n : ℕ
hkm : k < m
hmn : m < n
u v w : ℤˣ
⊢ (trinomial k m n ↑u ↑v ↑w).coeff k ^ 2 +
      ((trinomial k m n ↑u ↑v ↑w).coeff m ^ 2 + (trinomial k m n ↑u ↑v ↑w).coeff n ^ 2) =
    3
Module: Mathlib.Algebra.Polynomial.RuleOfSigns

Goal state before:
pp: case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : SignType.sign c ≠ 0
⊢ (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
          (match decide ¬False with
          | true =>
            SignType.sign P.leadingCoeff ::
              ((if (decide ¬SignType.sign 0 = 0) = true then
                  List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
                else []) ++
                match decide ¬SignType.sign c = 0 with
                | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
                | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))
          | false =>
            (if (decide ¬SignType.sign 0 = 0) = true then
                List.replicate (P.natDegree - P.eraseLead.degree.succ) (SignType.sign 0)
              else []) ++
              match decide ¬SignType.sign c = 0 with
              | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
              | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter (fun x1 x2 ↦ ¬x1 = x2)
            (match decide ¬SignType.sign c = 0 with
            | true => SignType.sign c :: List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs)
            | false => List.filter (fun x ↦ decide ¬x = 0) (List.map (⇑SignType.sign) cs))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0

Tactic:
simp only [decide_not, sign_zero, List.destutter, Bool.false_eq_true, reduceIte, h₁,
    decide_false, Bool.not_false, List.nil_append, List.destutter', decide_true, Bool.not_true]

Goal state after:
case neg.cons
R : Type u_1
inst✝¹ : Semiring R
inst✝ : LinearOrder R
P : R[X]
h : P ≠ 0
hpz : ¬P = 0
hsl : SignType.sign P.leadingCoeff ≠ 0
c : R
cs : List R
h_eL : P.eraseLead.coeffList = c :: cs
h₁ : SignType.sign c ≠ 0
⊢ (if ¬SignType.sign P.leadingCoeff = SignType.sign c then
          SignType.sign P.leadingCoeff ::
            List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign c)
              (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))
        else
          List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign P.leadingCoeff)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
      1 =
    (List.destutter' (fun x1 x2 ↦ ¬x1 = x2) (SignType.sign c)
            (List.filter (fun x ↦ !decide (x = 0)) (List.map (⇑SignType.sign) cs))).length -
        1 +
      if SignType.sign P.leadingCoeff = -SignType.sign P.eraseLead.leadingCoeff then 1 else 0
Module: Mathlib.Algebra.QuadraticAlgebra.Basic

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
r : R
⊢ norm ((algebraMap R (QuadraticAlgebra R a b)) r) = r ^ 2

Tactic:
by
  simp [norm_def, pow_two]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℕ
⊢ norm ↑n = ↑n ^ 2

Tactic:
by
  simp [norm_def, pow_two]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
n : ℤ
⊢ norm ↑n = ↑n ^ 2

Tactic:
by
  simp [norm_def, pow_two]

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

Goal state before:
pp: R : Type u_2
a b : R
inst✝ : CommRing R
z : QuadraticAlgebra R a b
hz : ∀ (x : QuadraticAlgebra R a b), x * z = 0 → x = 0
w : QuadraticAlgebra R a b
hw : w * star z = 0
⊢ star w * z = 0

Tactic:
rw [← star_involutive z, ← star_mul, mul_comm, hw, star_zero]

Goal state after:
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
⊢ ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      (⟦x⟧)⁻¹ =
    F (⟦x⟧)⁻¹

Tactic:
map_inv,

Goal state after:
case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
⊢ (((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
          ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
        ⟦x⟧)⁻¹ =
    F (⟦x⟧)⁻¹
Module: Mathlib.Algebra.Quandle

Goal state before:
pp: case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
⊢ (((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
          ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
        ⟦x⟧)⁻¹ =
    F (⟦x⟧)⁻¹

Tactic:
map_inv,

Goal state after:
case inv
R : Type u_1
inst✝¹ : Rack R
G : Type u_2
inst✝ : Group G
F : EnvelGroup R →* G
x✝ : EnvelGroup R
x : PreEnvelGroup R
ih_x :
  ((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
        ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
      ⟦x⟧ =
    F ⟦x⟧
hm : ⟦x.inv⟧ = (⟦x⟧)⁻¹
⊢ (((fun f ↦ { toFun := fun x ↦ Quotient.liftOn x (mapAux f) ⋯, map_one' := ⋯, map_mul' := ⋯ })
          ((fun F ↦ (Quandle.Conj.map F).comp (toEnvelGroup R)) F))
        ⟦x⟧)⁻¹ =
    (F ⟦x⟧)⁻¹
Module: Mathlib.Algebra.QuaternionBasis

Goal state before:
pp: case a.refine_2
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₃]
⊢ y.imI • B.i ∈ R[B.i, B.j, B.k]

pp: case a.refine_3
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₃]
⊢ y.imJ • B.j ∈ R[B.i, B.j, B.k]

pp: case a.refine_4
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₃]
⊢ y.imK • B.k ∈ R[B.i, B.j, B.k]

Tactic:
all_goals
      exact Subalgebra.smul_mem _ (Algebra.subset_adjoin <| by simp) _

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✝¹² : 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 α α
f : CentroidHom α
n : ℕ
a b : α
⊢ (↑(f.toEnd ^ n)).toFun (a * b) = (↑(f.toEnd ^ n)).toFun a * b

Tactic:
by
        induction n with
        | zero => rfl
        | succ n ih =>
          rw [pow_succ']
          exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)

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

Goal state before:
pp: α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
⊢ (toEndRingHom α).rangeS = Subsemiring.centralizer (Set.range ⇑L ∪ Set.range ⇑R)

Tactic:
ext T
  refine ⟨?_, fun h ↦ ?_⟩
  · rintro ⟨f, rfl⟩ S (⟨a, rfl⟩ | ⟨b, rfl⟩)
    · exact AddMonoidHom.ext fun b ↦ (map_mul_left f a b).symm
    · exact AddMonoidHom.ext fun a ↦ (map_mul_right f a b).symm
  · rw [Subsemiring.mem_centralizer_iff] at h
    refine ⟨⟨T, fun a b ↦ ?_, fun a b ↦ ?_⟩, rfl⟩
    · exact congr($(h (L a) (.inl ⟨a, rfl⟩)) b).symm
    · exact congr($(h (R b) (.inr ⟨b, rfl⟩)) a).symm

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✝¹⁶ : 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✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [Subsemiring.mem_center_iff]

Goal state after:
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✝ α α
R : Type u_6
inst✝³ : CommSemiring «R»
inst✝² : Module «R» α
inst✝¹ : SMulCommClass «R» α α
inst✝ : IsScalarTower «R» α α
z : ↥(NonUnitalSubsemiring.center α)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝¹ : DecidableEq G'
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.sum g).coeff.support ⊆ f.coeff.support.biUnion fun a ↦ (g a (f.coeff a)).coeff.support

Tactic:
coeff_sum'

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
k' : Type u_3
G' : Type u_4
inst✝¹ : DecidableEq G'
inst✝ : AddCommMonoid k'
f : SkewMonoidAlgebra k G
g : G → k → SkewMonoidAlgebra k' G'
⊢ (f.coeff.sum fun x1 x2 ↦ (g x1 x2).coeff).support ⊆ f.coeff.support.biUnion fun a ↦ (g a (f.coeff a)).coeff.support
Module: Mathlib.Algebra.SkewMonoidAlgebra.Support

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Monoid G
inst✝¹ : Semiring k
inst✝ : MulSemiringAction G k
f : SkewMonoidAlgebra k G
⊢ f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

Tactic:
rw [Fintype.mem_span_image_iff_exists_fun k]
  use Finset.restrict f.support f.coeff
  simp [smul_single, ← sum_def', sum_single]

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

Goal state before:
pp: M : Type u_4
α : Type u_5
inst✝ : AddCommMonoid M
f : SkewMonoidAlgebra M α
a : α
b : M
⊢ (f.update a b).coeff a = b

Tactic:
rw [f.coeff_update_apply, if_pos rfl]

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 → Prop
inst✝¹ : Semiring T
B : Type uR
inst✝ : CommRing B
r : B → B → Prop
⊢ ∀ a ∈ Ideal.ofRel r, (mkRingHom r) a = 0

Tactic:
refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
      · rintro y ⟨a, b, h, su⟩
        symm at su
        rw [← sub_eq_iff_eq_add] at su
        rw [← su, map_sub, mkRingHom_rel h, sub_self]
      · simp
      · intro a b _ _ ha hb
        simp [ha, hb]
      · intro a x _ hx
        simp [hx]

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

Goal state before:
pp: k : Type u_1
G : Type u_2
S : Type u_3
S₁ : Type u_4
S₂ : Type u_5
M : Type u_6
α : Type u_7
inst✝³ : Monoid G
inst✝² : AddCommMonoid M
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid k
g : G
f f' : SkewMonoidAlgebra k G
a✝ : G
⊢ (g • (f + f')).coeff a✝ = (g • f + g • f').coeff a✝

Tactic:
simp [comapSMul_def, map_add]

Goal state after:
Module: Mathlib.Algebra.Vertex.VertexOperator

Goal state before:
pp: R : Type u_1
V : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup V
inst✝ : Module R V
A : VertexOperator R V
n : ℤ
x : V
h : n < ((HahnModule.of R).symm (A x)).order
⊢ (coeff A n) x = 0

Tactic:
rw [coeff_eq_ncoeff, ncoeff_eq_zero_of_lt_order A (-n - 1) x]
  lia

Goal state after:
Module: Mathlib.Algebra.Vertex.HVertexOperator

Goal state before:
pp: Γ : Type u_1
inst✝⁵ : PartialOrder Γ
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
⊢ Function.Injective ⇑coeff

Tactic:
intro _ _ h
  ext v n
  exact congrFun (congrArg DFunLike.coe (congrFun h n)) v

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
F : TopCat.Sheaf A Y
⊢ (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology ↑X) A).obj F ≅
    (sheafPullback A hf).obj F

pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology ↑X) A).map u ≫
      Iso.hom ?refine_1 =
    Iso.hom ?refine_1 ≫ (sheafPullback A hf).map u

Tactic:
· exact (presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso
      (hf.isOpenMap.pullbackIso.app _) ≪≫
      (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology X) A).preimageIso
      (isoSheafify (Opens.grothendieckTopology X)
      (TopCat.Presheaf.isSheaf_of_isOpenEmbedding hf F.2)).symm

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
X Y : TopCat
f✝ : X ⟶ Y
ι : Type w
U : ι → Opens ↑Y
A : Type u_1
inst✝⁷ : Category.{w, u_1} A
f : X ⟶ Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
FA : A → A → Type u_2
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasColimits A
inst✝³ : HasLimits A
inst✝² : PreservesLimits (CategoryTheory.forget A)
inst✝¹ : PreservesFilteredColimits (CategoryTheory.forget A)
inst✝ : (CategoryTheory.forget A).ReflectsIsomorphisms
X✝ Y✝ : TopCat.Sheaf A Y
u : X✝ ⟶ Y✝
⊢ (Sheaf.forget A Y ⋙ Presheaf.pullback A f ⋙ presheafToSheaf (Opens.grothendieckTopology ↑X) A).map u ≫
      ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso (⋯.pullbackIso.app ((Sheaf.forget A Y).obj Y✝)) ≪≫
          (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology ↑X) A).preimageIso
            (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).symm).hom =
    ((presheafToSheaf (Opens.grothendieckTopology ↑X) A).mapIso (⋯.pullbackIso.app ((Sheaf.forget A Y).obj X✝)) ≪≫
          (fullyFaithfulSheafToPresheaf (Opens.grothendieckTopology ↑X) A).preimageIso
            (isoSheafify (Opens.grothendieckTopology ↑X) ⋯).symm).hom ≫
      (sheafPullback A hf).map u
Module: Mathlib.Geometry.RingedSpace.SheafedSpace

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ α.hom = β.hom

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α β : X ⟶ Y
h : α = β
x : ↑↑X
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom β.base) x)

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ X.presheaf.stalk x = X.presheaf.stalk x'

Tactic:
rw [h]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : PresheafedSpace C
α : X ⟶ Y
x x' : ↑↑X
h : x = x'
⊢ Y.presheaf.stalk ((ConcreteCategory.hom α.base) x) = Y.presheaf.stalk ((ConcreteCategory.hom α.base) x')

Tactic:
rw [h]

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

Goal state before:
pp: X✝ X Y Z : LocallyRingedSpace
f : X.Hom Y
g : Y.Hom Z
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (f.toHom ≫ g.toHom) x))

Tactic:
rw [PresheafedSpace.stalkMap.comp]
    apply +allowSynthFailures RingHom.isLocalHom_comp
    all_goals apply isLocalHomValStalkMap

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

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

Tactic:
apply le_antisymm
  · rw [X.basicOpen_res i f]; exact inf_le_right
  · have := X.basicOpen_res (inv i) (X.presheaf.map i f)
    rw [← CommRingCat.comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id,
        CommRingCat.id_apply] at this
    rw [this]
    exact inf_le_right

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
by
  simp only [invApp, ← Category.assoc]
  rw [IsIso.comp_inv_eq]
  simp only [Functor.op_obj, op_unop, ← X.presheaf.map_comp, Functor.op_map, Category.assoc,
    NatTrans.naturality, Quiver.Hom.unop_op, IsIso.inv_hom_id_assoc,
    TopCat.Presheaf.pushforward_obj_map]
  congr 1

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
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
← hu.mul_right_eq_zero,

Goal state after:
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
hu : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n) * (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ f ⁻¹ᵁ f ''ᵁ U = U

Tactic:
apply Opens.ext
  simp [Set.preimage_image_eq _ f.isOpenEmbedding.injective]

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

Goal state before:
pp: case refine_2
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F : C ⥤ Type u
X : C
R : Presieve X
h : ∀ (x : F.obj X), ∃ Y f, R f ∧ x ∈ Set.range ⇑(ConcreteCategory.hom (F.map f))
x : F.obj X
Y : C
g : Y ⟶ X
hg : R g
hi : x ∈ Set.range ⇑(ConcreteCategory.hom (F.map g))
⊢ ∃ Y g, map F R g ∧ x ∈ Set.range ⇑(ConcreteCategory.hom g)

Tactic:
exact ⟨_, _, ⟨hg⟩, hi⟩

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

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

Tactic:
have : HasLimit (cospan ((cospan f g ⋙ forget).map Hom.inl)
      ((cospan f g ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map f) ((forget).map g))
    infer_instance
  apply hasLimit_of_iso (diagramIsoCospan _).symm

Goal state after: