harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma coeff_Ψ₃_ne_zero (h : (3 : R) ≠ 0) : W.Ψ₃.coeff 4 ≠ 0

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ W.Ψ₃.coeff 4 ≠ 0

Tactic:
rwa [coeff_Ψ₃]

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
theorem CompClosure.of {a b : C} (m₁ m₂ : a ⟶ b) (h : r m₁ m₂) : CompClosure r m₁ m₂

Proof state:
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
⊢ CompClosure r m₁ m₂

Tactic:
simpa using CompClosure.intro (𝟙 _) m₁ m₂ (𝟙 _) h

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem sub (hm : IsPeriodicPt f m x) (hn : IsPeriodicPt f n x) :
    IsPeriodicPt f (m - n) x

Proof state:
case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x

Tactic:
rw [tsub_eq_zero_iff_le.mpr h]

Result:
case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x

Proof state:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x

Tactic:
rwa [tsub_add_cancel_of_le h]

Result:
no goals

Proof state:
case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f 0 x

Tactic:
apply isPeriodicPt_zero

Result:
no goals

Proof state:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

Tactic:
refine left_of_add ?_ hn

Result:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n + n) x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
⊢ IsPeriodicPt f (m - n) x

Tactic:
rcases le_total n m with h | h

Result:
case inl
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : n ≤ m
⊢ IsPeriodicPt f (m - n) x

case inr
α : Type u_1
f : α → α
x : α
m n : ℕ
hm : IsPeriodicPt f m x
hn : IsPeriodicPt f n x
h : m ≤ n
⊢ IsPeriodicPt f (m - n) x
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem mem_incidenceSet (v w : V) : s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ s(v, w) ∈ G.incidenceSet v ↔ G.Adj v w

Tactic:
simp [incidenceSet]

Result:
no goals
-- Mathlib/Data/DFinsupp/Module.lean
theorem mk_smul {s : Finset ι} (c : γ) (x : ∀ i : (↑s : Set ι), β (i : ι)) :
    mk s (c • x) = c • mk s x :=
  ext fun i => by simp only [smul_apply, mk_apply]; split_ifs <;> [rfl; rw [smul_zero]]

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) ⟨i, H⟩ else 0) = c • if H : i ∈ s then x ⟨i, H⟩ else 0

Tactic:
split_ifs <;> [rfl; rw [smul_zero]]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (mk s (c • x)) i = (c • mk s x) i

Tactic:
simp only [smul_apply, mk_apply]

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) ⟨i, H⟩ else 0) = c • if H : i ∈ s then x ⟨i, H⟩ else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Constraint.lean
theorem combo_sat' (s t : Constraint)
    (a : Int) (x : Coeffs) (b : Int) (y : Coeffs) (v : Coeffs)
    (wx : s.sat' x v) (wy : t.sat' y v) :
    (Constraint.combo a s b t).sat' (Coeffs.combo a x b y) v

Proof state:
s t : Constraint
a : Int
x : Coeffs
b : Int
y v : Coeffs
wx : s.sat' x v = true
wy : t.sat' y v = true
⊢ (Constraint.combo a s b t).sat' (Coeffs.combo a x b y) v = true

Tactic:
rw [Constraint.sat', Coeffs.combo_eq_smul_add_smul, Coeffs.dot_distrib_left,
  Coeffs.dot_smul_left, Coeffs.dot_smul_left]

Result:
s t : Constraint
a : Int
x : Coeffs
b : Int
y v : Coeffs
wx : s.sat' x v = true
wy : t.sat' y v = true
⊢ (Constraint.combo a s b t).sat (a * x.dot v + b * y.dot v) = true

Proof state:
s t : Constraint
a : Int
x : Coeffs
b : Int
y v : Coeffs
wx : s.sat' x v = true
wy : t.sat' y v = true
⊢ (Constraint.combo a s b t).sat (a * x.dot v + b * y.dot v) = true

Tactic:
exact Constraint.combo_sat a wx b wy

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma coyonedaEquiv_symm_map {X Y : C} (f : X ⟶ Y) {F : C ⥤ Type v₁} (t : F.obj X) :
    coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
u : coyoneda.obj (op X) ⟶ F
⊢ coyonedaEquiv.symm (F.map f (coyonedaEquiv u)) = coyoneda.map f.op ≫ coyonedaEquiv.symm (coyonedaEquiv u)

Tactic:
simp [coyonedaEquiv_naturality u f]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
t : F.obj X
⊢ coyonedaEquiv.symm (F.map f t) = coyoneda.map f.op ≫ coyonedaEquiv.symm t

Tactic:
obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
u : coyoneda.obj (op X) ⟶ F
⊢ coyonedaEquiv.symm (F.map f (coyonedaEquiv u)) = coyoneda.map f.op ≫ coyonedaEquiv.symm (coyonedaEquiv u)
-- Mathlib/Order/Basic.lean
theorem lt_of_strongLT [Nonempty ι] (h : a ≺ b) : a < b

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
⊢ a < b

Tactic:
inhabit ι

Result:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst✝ : Nonempty ι
h : a ≺ b
inhabited_h : Inhabited ι
⊢ a < b

Tactic:
exact Pi.lt_def.2 ⟨le_of_strongLT h, default, h _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat) (f' : DefaultFormula n)
    (f_readyForRupAdd : ReadyForRupAdd f) (rupAddSuccess : performRupAdd f c rupHints = (f', true)) :
    f' = insert f c

Proof state:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f' = f.insert c

Tactic:
have fc_assignments_size : (insertRupUnits f (negate c)).1.assignments.size = n := by
  rw [size_assignments_insertRupUnits f (negate c)]
  exact f_readyForRupAdd.2.1

Result:
case isFalse.isFalse.isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
rupHints : Array Nat
f' : DefaultFormula n
f_readyForRupAdd : f.ReadyForRupAdd
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = false
rupAddSuccess :
  ({ clauses := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.clauses,
              rupUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.rupUnits,
              ratUnits := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.ratUnits,
              assignments :=
                restoreAssignments ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
⊢ f' = f.insert c
-- Mathlib/Algebra/Tropical/Basic.lean
theorem add_eq_left_iff {x y : Tropical R} : x + y = x ↔ x ≤ y

Proof state:
R : Type u
inst✝ : LinearOrder R
x y : Tropical R
⊢ x + y = x ↔ x ≤ y

Tactic:
rw [trop_add_def, trop_eq_iff_eq_untrop, ← untrop_le_iff, min_eq_left_iff]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem sup_sdiff_right_self : (a ⊔ b) \ b = a \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊔ b) \ b = a \ b

Tactic:
rw [sup_sdiff, sdiff_self, sup_bot_eq]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem hnot_symmDiff_self : (￢a) ∆ a = ⊤

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a

Tactic:
exact Codisjoint.top_le codisjoint_hnot_left

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤

Tactic:
rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]

Result:
α : Type u_2
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem stronglyMeasurable_const' (hf : ∀ x y, f x = f y) : StronglyMeasurable f

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ f = fun x => ?convert_3

case convert_3
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ β

Tactic:
exact funext fun x => hf x default

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
⊢ StronglyMeasurable f

Tactic:
nontriviality α

Result:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ StronglyMeasurable f

Tactic:
convert stronglyMeasurable_const (β := β) using 1

Result:
case h.e'_5
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ f = fun x => ?convert_3

case convert_3
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ β

Proof state:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
⊢ StronglyMeasurable f

Tactic:
inhabit α

Result:
α : Type u_1
β : Type u_2
x✝ : MeasurableSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : ∀ (x y : α), f x = f y
a✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ StronglyMeasurable f
-- Mathlib/Algebra/GroupWithZero/Action/Defs.lean
theorem smul_sub (r : M) (x y : A) : r • (x - y) = r • x - r • y

Proof state:
M : Type u_1
A : Type u_3
inst✝² : Monoid M
inst✝¹ : AddGroup A
inst✝ : DistribMulAction M A
r : M
x y : A
⊢ r • (x - y) = r • x - r • y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, smul_add, smul_neg]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem lift_cardinalMk_adjoin_le {A : Type v} [Semiring A] [Algebra R A] (s : Set A) :
    lift.{u} #(adjoin R s) ≤ lift.{v} #R ⊔ lift.{u} #s ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
rw [Algebra.adjoin_eq_range_freeAlgebra_lift]

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥((FreeAlgebra.lift R) Subtype.val).range ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H :
  lift.{max u v, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤
    lift.{v, max u v} #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
rw [lift_umax, lift_id'.{v, u}] at H

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ lift.{u, v} #↥(adjoin R s) ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
have H := mk_range_le_lift (f := FreeAlgebra.lift R ((↑) : s → A))

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H :
  lift.{max u v, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤
    lift.{v, max u v} #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥(adjoin R s) ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
H : lift.{u, v} #↑(Set.range ⇑((FreeAlgebra.lift R) Subtype.val)) ≤ #(FreeAlgebra R { x // x ∈ s })
⊢ lift.{u, v} #↥((FreeAlgebra.lift R) Subtype.val).range ≤ lift.{v, u} #R ⊔ lift.{u, v} #↑s ⊔ ℵ₀

Tactic:
exact H.trans (FreeAlgebra.cardinalMk_le_max_lift R s)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem zero_mod (b : Ordinal) : 0 % b = 0

Proof state:
b : Ordinal.{u_4}
⊢ 0 % b = 0

Tactic:
simp only [mod_def, zero_div, mul_zero, sub_self]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem mem_orthogonal_singleton_iff_inner_left {u v : E} : v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪v, u⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
u v : E
⊢ v ∈ (span 𝕜 {u})ᗮ ↔ inner v u = 0

Tactic:
rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma support_vanishingIdeal {Z : Set X} :
    (vanishingIdeal Z).support = closure Z

Proof state:
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ closure Z ∩ Set.range ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec hU).base) ↔ x ∈ closure Z

Tactic:
simp [hxU]

Result:
no goals

Proof state:
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (vanishingIdeal Z).support ↔ x ∈ (vanishingIdeal Z).support ∩ ↑U

Tactic:
simp [hxU]

Result:
no goals

Proof state:
case h.intro.intro.intro.intro.intro
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (vanishingIdeal Z).support ↔ x ∈ closure Z

Tactic:
trans x ∈ (vanishingIdeal Z).support ∩ U

Result:
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (vanishingIdeal Z).support ↔ x ∈ (vanishingIdeal Z).support ∩ ↑U

X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (vanishingIdeal Z).support ∩ ↑U ↔ x ∈ closure Z

Proof state:
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (vanishingIdeal Z).support ∩ ↑U ↔ x ∈ closure Z

Tactic:
rw [(vanishingIdeal Z).support_inter ⟨U, hU⟩, ← hU.fromSpec_image_zeroLocus,
  vanishingIdeal, zeroLocus_vanishingIdeal_eq_closure,
    ← hU.fromSpec.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage
      hU.fromSpec.base.1.2,
    Set.image_preimage_eq_inter_range]

Result:
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ closure Z ∩ Set.range ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec hU).base) ↔ x ∈ closure Z

Proof state:
case h
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ (vanishingIdeal Z).support ↔ x ∈ closure Z

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Result:
case h.intro.intro.intro.intro.intro
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ (vanishingIdeal Z).support ↔ x ∈ closure Z

Proof state:
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
⊢ (vanishingIdeal Z).support = closure Z

Tactic:
ext x

Result:
case h
X : Scheme
Z : Set ↑↑X.toPresheafedSpace
x : ↑↑X.toPresheafedSpace
⊢ x ∈ (vanishingIdeal Z).support ↔ x ∈ closure Z
-- Mathlib/Data/Rat/Defs.lean
@[simp]
lemma divInt_mul_divInt' (n₁ d₁ n₂ d₂ : ℤ) : (n₁ /. d₁) * (n₂ /. d₂) = (n₁ * n₂) /. (d₁ * d₂)

Proof state:
case inr.inl
n₁ d₁ n₂ : ℤ
h₁ : d₁ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. 0) = n₁ * n₂ /. (d₁ * 0)

Tactic:
simp

Result:
no goals

Proof state:
n₁ d₁ n₂ d₂ : ℤ
⊢ n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)

Tactic:
obtain rfl | h₁ := eq_or_ne d₁ 0

Result:
case inl
n₁ n₂ d₂ : ℤ
⊢ n₁ /. 0 * (n₂ /. d₂) = n₁ * n₂ /. (0 * d₂)

case inr
n₁ d₁ n₂ d₂ : ℤ
h₁ : d₁ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)

Proof state:
case inr.inr
n₁ d₁ n₂ d₂ : ℤ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)

Tactic:
exact divInt_mul_divInt _ _ h₁ h₂

Result:
no goals

Proof state:
case inl
n₁ n₂ d₂ : ℤ
⊢ n₁ /. 0 * (n₂ /. d₂) = n₁ * n₂ /. (0 * d₂)

Tactic:
simp

Result:
no goals

Proof state:
case inr
n₁ d₁ n₂ d₂ : ℤ
h₁ : d₁ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)

Tactic:
obtain rfl | h₂ := eq_or_ne d₂ 0

Result:
case inr.inl
n₁ d₁ n₂ : ℤ
h₁ : d₁ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. 0) = n₁ * n₂ /. (d₁ * 0)

case inr.inr
n₁ d₁ n₂ d₂ : ℤ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ n₁ /. d₁ * (n₂ /. d₂) = n₁ * n₂ /. (d₁ * d₂)
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private lemma ofTensorProduct_comp_ofTensorProductInvOfPiFintype :
    ofTensorProduct I (ι → R) ∘ₗ ofTensorProductInvOfPiFintype I ι = LinearMap.id

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) ∘ₗ ↑(AdicCompletion.ofTensorProductInvOfPiFintype I ι) = LinearMap.id

Tactic:
dsimp only [ofTensorProductInvOfPiFintype]

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) ∘ₗ
      ↑((piEquivOfFintype I fun x => R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) =
    LinearMap.id

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piEquivOfFintype I fun x => R).symm ∘ₗ
      (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) ∘ₗ
          ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ
        ↑(piEquivOfFintype I fun x => R) =
    LinearMap.id

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ofTensorProduct I (ι → R) ∘ₗ
      ↑((piEquivOfFintype I fun x => R).trans (piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) =
    LinearMap.id

Tactic:
rw [LinearEquiv.coe_trans, ofTensorProduct_eq, LinearMap.comp_assoc]

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piEquivOfFintype I fun x => R).symm ∘ₗ
      ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) ∘ₗ
        ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ ↑(piEquivOfFintype I fun x => R) =
    LinearMap.id

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piEquivOfFintype I fun x => R).symm ∘ₗ
      ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) ∘ₗ
        ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm ∘ₗ ↑(piEquivOfFintype I fun x => R) =
    LinearMap.id

Tactic:
nth_rw 2 [← LinearMap.comp_assoc]

Result:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
ι : Type u_4
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
⊢ ↑(piEquivOfFintype I fun x => R).symm ∘ₗ
      (↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι) ∘ₗ
          ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι).symm) ∘ₗ
        ↑(piEquivOfFintype I fun x => R) =
    LinearMap.id
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order = φ.order + ψ.order

Tactic:
classical
simp only [order_eq_emultiplicity_X]
exact emultiplicity_mul X_prime

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : R⟦X⟧
⊢ emultiplicity X (φ * ψ) = emultiplicity X φ + emultiplicity X ψ

Tactic:
exact emultiplicity_mul X_prime

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : R⟦X⟧
⊢ (φ * ψ).order = φ.order + ψ.order

Tactic:
simp only [order_eq_emultiplicity_X]

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : R⟦X⟧
⊢ emultiplicity X (φ * ψ) = emultiplicity X φ + emultiplicity X ψ