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

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₁ b₁ ↦ (single g a).sum fun a₂ b₂ ↦ single (a₁ * a₂) (b₁ * a₁ • b₂)) = single g a

Tactic:
sum_single_index

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (1 * 1 • b₂)) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single g a).sum fun a₂ b₂ ↦ single (1 * a₂) (0 * 1 • b₂)) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (a * g • b₂)) = single g a

pp: case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0

Tactic:
sum_single_index

Goal state after:
case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 1) = single g a

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ single (g * 1) (a * g • 0) = 0

case single
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Monoid G
inst✝ : MulSemiringAction G k
g : G
a : k
⊢ ((single 1 1).sum fun a₂ b₂ ↦ single (g * a₂) (0 * g • b₂)) = 0
Module: Mathlib.Algebra.Star.UnitaryStarAlgAut

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

Tactic:
simpa using

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✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
⊢ ↑u = y • ↑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✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
⊢ ↑v = star y • ↑u

Tactic:
simpa using

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✝ : ∃ y, y • 1 = star ↑v * ↑u
y : S
h : y • 1 = star ↑v * ↑u
huv : ↑u = y • ↑v
⊢ ↑v = star y • ↑u
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
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
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 : G × G
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢

Goal state after:
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
s : Finset (G × G)
hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x
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 : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ untrop (x + y) = untrop x

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : x ≤ y
⊢ x ≤ y
Module: Mathlib.Algebra.Tropical.Basic

Goal state before:
pp: R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ untrop (x + y) = untrop y

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
h : y ≤ x
⊢ y ≤ x
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 : G × G
hps : p ∈ s
hp : p ∉ {p ∈ s | p.1 ∈ f.support ∧ p.2 ∈ g.support}
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0

Tactic:
simp only [Finset.mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢

Goal state after:
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 : G × G
hps : p ∈ s
hp : p ∈ s → f.coeff p.1 ≠ 0 → g.coeff p.2 = 0
⊢ f.coeff p.1 * p.1 • g.coeff p.2 = 0
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop (sum ⟦a⟧) = (map trop ⟦a⟧).prod

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset R
⊢ ∀ (a : List R), trop a.sum = (List.map trop a).prod
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)), untrop (prod ⟦a⟧) = (map untrop ⟦a⟧).sum

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : AddCommMonoid R
s : Multiset (Tropical R)
⊢ ∀ (a : List (Tropical R)), untrop a.prod = (List.map untrop a).sum
Module: Mathlib.Algebra.Tropical.BigOperators

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = ⨅ i, untrop (f ↑i)

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ ∑ i ∈ s, f i = ∑ i ∈ s.attach, f ↑i
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
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ ((single g r).sum fun a₁ b₁ ↦ x.sum fun a₂ b₂ ↦ if a₁ * a₂ = g' then b₁ * a₁ • b₂ else 0) = 0

Tactic:
sum_single_index

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then r * g • b₂ else 0) = 0

k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : SMulZeroClass G k
r : k
g g' : G
x : SkewMonoidAlgebra k G
h : ¬∃ d, g' = g * d
⊢ (x.sum fun a₂ b₂ ↦ if g * a₂ = g' then 0 * g • b₂ else 0) = 0
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : Nontrivial k
a b : G
h : (single a 1).coeff = (single b 1).coeff
⊢ a = b

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : Semiring k
inst✝² : Monoid G
inst✝¹ : MulSemiringAction G k
inst✝ : Nontrivial k
a b : G
h : (single a 1).coeff = (single b 1).coeff
⊢ a = b
Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
this : (liftNC ↑f ⇑g).comp ((smulAddHom k (SkewMonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
simpa using

Goal state after:
k : Type u_1
G : Type u_2
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : SkewMonoidAlgebra k G
this : (liftNC ↑f ⇑g).comp ((smulAddHom k (SkewMonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
G : Type u_4
inst✝³ : AddCommMonoid G
inst✝² : Module R G
inst✝¹ : StarAddMonoid G
inst✝ : StarModule R G
f : E →ₗ[R] F
g : G →ₗ[R] E
⊢ star (toConv (f ∘ₗ g)) = toConv ((star (toConv f)).ofConv ∘ₗ (star (toConv g)).ofConv)

Tactic:
simpa using

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
G : Type u_4
inst✝³ : AddCommMonoid G
inst✝² : Module R G
inst✝¹ : StarAddMonoid G
inst✝ : StarModule R G
f : E →ₗ[R] F
g : G →ₗ[R] E
⊢ star (toConv (f ∘ₗ g)) = toConv ((star (toConv f)).ofConv ∘ₗ (star (toConv g)).ofConv)
Module: Mathlib.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : TensorProduct R E G
⊢ star ((TensorProduct.map f.ofConv g.ofConv) x) = (TensorProduct.map (star f).ofConv (star g).ofConv) (star x)

Tactic:
simpa using

Goal state after:
R : Type u_5
E : Type u_6
F : Type u_7
G : Type u_8
H : Type u_9
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : StarRing R
inst✝¹⁵ : AddCommMonoid E
inst✝¹⁴ : StarAddMonoid E
inst✝¹³ : Module R E
inst✝¹² : StarModule R E
inst✝¹¹ : AddCommMonoid F
inst✝¹⁰ : StarAddMonoid F
inst✝⁹ : Module R F
inst✝⁸ : StarModule R F
inst✝⁷ : AddCommMonoid G
inst✝⁶ : StarAddMonoid G
inst✝⁵ : Module R G
inst✝⁴ : StarModule R G
inst✝³ : AddCommMonoid H
inst✝² : StarAddMonoid H
inst✝¹ : Module R H
inst✝ : StarModule R H
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] H)
x : TensorProduct R E G
⊢ star ((TensorProduct.map f.ofConv g.ofConv) x) = (TensorProduct.map (star f).ofConv (star g).ofConv) (star x)
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
⊢ ?m.178

Tactic:
simpa using

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
⊢ ?m.178
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
u : (End R E)ˣ
hu : ↑u = f.ofConv
this : IsUnit (star (toConv ↑u)).ofConv
⊢ IsUnit (star f).ofConv

Tactic:
simpa using

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
this : IsUnit (star (toConv ↑u)).ofConv
⊢ IsUnit (star f).ofConv
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ X.presheaf.germ (h.functor.obj V) ((ConcreteCategory.hom f) x) ⋯ ≫ (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx

Tactic:
rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Goal state after:
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)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (ConcreteCategory.hom h) ((ConcreteCategory.hom f.hom.base) ⋯.choose)

Tactic:
simpa using

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
f : X ⟶ Y
h₁ : Function.Surjective ⇑(ConcreteCategory.hom f.hom.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), Mono (PresheafedSpace.Hom.stalkMap f.hom x)
Z : SheafedSpace C
g : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
gc : Z.presheaf ⟶ (pushforward C g).obj Y.presheaf
h : ↑Y.toPresheafedSpace ⟶ ↑Z.toPresheafedSpace
hc : Z.presheaf ⟶ (pushforward C h).obj Y.presheaf
e : (f ≫ { hom := { base := g, c := gc } }).hom = (f ≫ { hom := { base := h, c := hc } }).hom
y : ↑↑Y.toPresheafedSpace
⊢ (ConcreteCategory.hom g) ((ConcreteCategory.hom f.hom.base) ⋯.choose) =
    (ConcreteCategory.hom h) ((ConcreteCategory.hom f.hom.base) ⋯.choose)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case h
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 : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0

Tactic:
simpa using

Goal state after:
case h
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 : Opens ↑↑X.toPresheafedSpace
hv : ↑x ∈ V
i w✝ : V ⟶ U
hv4 : (ConcreteCategory.hom (X.presheaf.map i.op)) f = (ConcreteCategory.hom (X.presheaf.map w✝.op)) 0
⊢ (ConcreteCategory.hom (X.presheaf.map i.op)) f = 0
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f) *
      (ConcreteCategory.hom (X.presheaf.map i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    1
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.map (i₁ ≫ U.infLELeft V).op)) f)

Tactic:
simpa using

Goal state after:
case h
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
h : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
g : ToType (X.presheaf.obj (op V))
W : Opens ↑↑X.toPresheafedSpace := U ⊓ V
hxW : x ∈ W
heq :
  (ConcreteCategory.hom (X.presheaf.germ W x hxW))
      ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f *
        (ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    (ConcreteCategory.hom (X.presheaf.germ W x hxW)) 1
W' : Opens ↑↑X.toPresheafedSpace
hxW' : x ∈ W'
i₁ i₂ : W' ⟶ W
heq' :
  (ConcreteCategory.hom (X.presheaf.map i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLELeft V).op)) f) *
      (ConcreteCategory.hom (X.presheaf.map i₁.op)) ((ConcreteCategory.hom (X.presheaf.map (U.infLERight V).op)) g) =
    1
⊢ IsUnit ((CommRingCat.Hom.hom (X.presheaf.map i₁.op)) ((CommRingCat.Hom.hom (X.presheaf.map (U.infLELeft V).op)) f))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ α.inv.app (op U✝) ≫
      X.presheaf.map (eqToHom ⋯) ≫
        ((Presheaf.pushforward C H.hom).obj X.presheaf).map ((eqToHom ⋯).app (op U✝)) ≫
          α.hom.app (op ((Opens.map (𝟙 ↑Y)).obj U✝)) =
    (𝟙 Y).c.app (op U✝)

Tactic:
simp only [eqToHom_map, eqToHom_app, eqToHom_trans_assoc, eqToHom_refl, id_comp]

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ α.inv.app (op U✝) ≫ α.hom.app (op ((Opens.map (𝟙 ↑Y)).obj U✝)) = (𝟙 Y).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X : LocallyRingedSpace
U : Opens ↑↑X.toPresheafedSpace
⊢ X.toRingedSpace.basicOpen 0 = ⊥

Tactic:
by
  ext x
  simp only [RingedSpace.basicOpen, Opens.coe_mk, Set.mem_ofPred_eq,
    Opens.coe_bot, Set.mem_empty_iff_false,
    iff_false, not_exists]
  intro hx
  rw [map_zero, isUnit_zero_iff]
  change (0 : X.presheaf.stalk x) ≠ (1 : X.presheaf.stalk x)
  exact zero_ne_one

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
h : g₁.c.app (op V) ≫ eqToHom ⋯ = g₂.c.app (op V)
⊢ (g₁.c ≫ whiskerRight (eqToHom ⋯) Z.presheaf).app (op V) = g₂.c.app (op V)

Tactic:
simpa using

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
this✝¹ : Mono f
Z : PresheafedSpace C
g₁ g₂ : Z ⟶ X.restrict hf
eq : g₁ ≫ X.ofRestrict hf = g₂ ≫ X.ofRestrict hf
V : Opens ↑↑(X.restrict hf)
hV : (Opens.map (X.ofRestrict hf).base).obj (hf.functor.obj V) = V
this✝ : IsIso (⋯.adjunction.counit.app (unop (op (hf.functor.obj V))))
this :
  g₁.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) =
    g₂.c.app (op ((Opens.map (X.ofRestrict hf).base).obj (unop (op (hf.functor.obj V))))) ≫ Z.presheaf.map (eqToHom ⋯)
h : g₁.c.app (op V) ≫ eqToHom ⋯ = g₂.c.app (op V)
⊢ g₁.c.app (op V) ≫ eqToHom ⋯ = g₂.c.app (op V)
Module: Mathlib.Topology.Sheaves.LocalPredicate

Goal state before:
pp: X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ContinuousAt (fun x ↦ f (i x)) ⟨↑x, m⟩
⊢ ContinuousAt f x

Tactic:
simpa using

Goal state after:
X : TopCat
T✝ : ↑X → Type u_1
T : Type ?u.10
inst✝ : TopologicalSpace T
U : Opens ↑X
f : ↥U → T
x : ↥U
V : Opens ↑X
m : ↑x ∈ V
i : V ⟶ U
w : ContinuousAt (fun x ↦ f (i x)) ⟨↑x, m⟩
⊢ ContinuousAt f x
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X : RingedSpace
R : CommRingCat
α β : X ⟶ sheafedSpaceObj R
w : α.hom.base = β.hom.base
h :
  ∀ (r : ↑R),
    let U := PrimeSpectrum.basicOpen r;
    (CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ α.hom.c.app (op U)) ≫
        X.presheaf.map (eqToHom ⋯) =
      CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op U))) ≫ β.hom.c.app (op U)
⊢ α = β

Tactic:
ext : 1
  · exact w
  · apply ((TopCat.Sheaf.pushforward _ β.hom.base).obj X.sheaf).hom_ext _
      PrimeSpectrum.isBasis_basic_opens
    intro r
    apply (StructureSheaf.to_basicOpen_epi R r).1
    simpa using! h r

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
f : ι → Set ↑Γ(X, U)
⊢ X.zeroLocus (⋃ i, f i) = ⋂ i, X.zeroLocus (f i)

Tactic:
simpa using

Goal state after:
X : Scheme
U : X.Opens
ι : Type u_1
f : ι → Set ↑Γ(X, U)
⊢ ⋂ f_1, ⋂ i, ⋂ (_ : f_1 ∈ f i), (↑(X.toRingedSpace.basicOpen f_1))ᶜ =
    ⋂ i, ⋂ f_1 ∈ f i, (↑(X.toRingedSpace.basicOpen f_1))ᶜ
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
hx : x ∈ X.basicOpen f
hn : f ^ 0 ∈ I
⊢ f ∈ I

Tactic:
simpa using

Goal state after:
X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
hx : x ∈ X.basicOpen f
hn : f ^ 0 ∈ I
⊢ f ∈ I