harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/GlueData.lean
theorem ι_gluedIso_inv (i : D.J) : (D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝² : HasMulticoequalizer D.diagram
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ (D.mapGlueData F).ι i ≫ (D.gluedIso F).inv = F.map (D.ι i)

Tactic:
rw [Iso.comp_inv_eq, ι_gluedIso_hom]

Result:
no goals
-- Mathlib/Analysis/Normed/MulAction.lean
lemma enorm_smul (r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

Tactic:
simp [enorm, nnnorm_smul]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_of_mul_apply_of_mem_zero [AddMonoid ι] [SetLike.GradedMonoid A] (r : A 0)
    (r' : ⨁ i, A i) (j : ι) : ((of (fun i => A i) 0 r * r') j : R) = r * r' j :=
  coe_of_mul_apply_aux _ _ _ fun _x => by rw [zero_add]

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁵ : DecidableEq ι
inst✝⁴ : Semiring R
inst✝³ : SetLike σ R
inst✝² : AddSubmonoidClass σ R
A : ι → σ
inst✝¹ : AddMonoid ι
inst✝ : SetLike.GradedMonoid A
r : ↥(A 0)
r' : ⨁ (i : ι), ↥(A i)
j _x : ι
⊢ 0 + _x = j ↔ _x = j

Tactic:
rw [zero_add]

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem im_T_inv_smul : (T⁻¹ • z).im = z.im

Proof state:
z : ℍ
⊢ (T⁻¹ • z).im = z.im

Tactic:
simpa using im_T_zpow_smul z (-1)

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem map_dualCoannihilator (W : Subspace K (Dual K V)) [FiniteDimensional K V] :
    W.dualCoannihilator.map (Dual.eval K V) = W.dualAnnihilator

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
W : Subspace K (Dual K V)
inst✝ : FiniteDimensional K V
⊢ map (Dual.eval K V) (dualCoannihilator W) = dualAnnihilator W

Tactic:
rw [← dualAnnihilator_dualAnnihilator_eq_map, dualCoannihilator_dualAnnihilator_eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma sqrt_zero : sqrt (0 : A) = 0

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
⊢ sqrt 0 = 0

Tactic:
simp [sqrt]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_preimage_of_injective_subset_range {s : Set β} (H : f.Injective)
    (hs : s ⊆ Set.range f) :
    (f ⁻¹' s).ncard = s.ncard

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ (f ⁻¹' s).ncard = s.ncard

Tactic:
rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bind_bind : (p.bind f).bind g = p.bind fun a => (f a).bind g :=
  PMF.ext fun b => by
    simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm,
      ENNReal.tsum_mul_right.symm, mul_assoc, mul_left_comm, mul_comm] using ENNReal.tsum_comm

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : α → PMF β
g : β → PMF γ
b : γ
⊢ ((p.bind f).bind g) b = (p.bind fun a => (f a).bind g) b

Tactic:
simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm,
  ENNReal.tsum_mul_right.symm, mul_assoc, mul_left_comm, mul_comm] using ENNReal.tsum_comm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_insert_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {v : β} :
    get (m.insert k v) k (mem_insert_self h) = v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
v : β
⊢ get (m.insert k v) k ⋯ = v

Tactic:
simp_to_raw using Raw₀.Const.get_insert_self ⟨m, _⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_X_sub_C [Ring S] (r : S) : (X - C r).leadingCoeff = 1

Proof state:
S : Type v
inst✝ : Ring S
r : S
⊢ (X - C r).leadingCoeff = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_left_max {a b : Nat} : max (b + a) a = b + a

Proof state:
a b : Nat
⊢ max (b + a) a = b + a

Tactic:
rw [Nat.max_comm, max_add_left]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem IsIntegral.of_aeval_monic {x : A} {p : R[X]} (monic : p.Monic)
    (deg : p.natDegree ≠ 0) (hx : IsIntegral R (aeval x p)) : IsIntegral R x :=
  have ⟨p, hmonic, heval⟩ := hx
  ⟨_, hmonic.comp monic deg, by rwa [eval₂_comp, ← aeval_def x]⟩

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A
p✝ : R[X]
monic : p✝.Monic
deg : p✝.natDegree ≠ 0
hx : IsIntegral R ((aeval x) p✝)
p : R[X]
hmonic : p.Monic
heval : eval₂ (algebraMap R A) ((aeval x) p✝) p = 0
⊢ eval₂ (algebraMap R A) x (p.comp p✝) = 0

Tactic:
rwa [eval₂_comp, ← aeval_def x]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSubOfPoint_apply (w : ι → k) (p : ι → P) (b : P) :
    s.weightedVSubOfPoint p b w = ∑ i ∈ s, w i • (p i -ᵥ b)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
w : ι → k
p : ι → P
b : P
⊢ (s.weightedVSubOfPoint p b) w = ∑ i ∈ s, w i • (p i -ᵥ b)

Tactic:
simp [weightedVSubOfPoint, LinearMap.sum_apply]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem eq_of_mem_map_const {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (Function.const α b₂) l) :
    b₁ = b₂ :=
  eq_of_mem_replicate (n := card (l : Multiset α)) <| by rwa [map_const] at h

Proof state:
α : Type u_1
β : Type v
b₁ b₂ : β
l : List α
h : b₁ ∈ map (const α b₂) ↑l
⊢ b₁ ∈ replicate (↑l).card b₂

Tactic:
rwa [map_const] at h

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mem_splitSupport_iff_nonzero (i : ι) : i ∈ splitSupport l ↔ split l i ≠ 0

Proof state:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ l.splitSupport ↔ l.split i ≠ 0

Tactic:
rw [splitSupport, @mem_image _ _ (Classical.decEq _), Ne, ← support_eq_empty, ← Ne, ←
  Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]

Result:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔
    ∃ x,
      x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a => l ⟨i, a⟩, mem_support_toFun := ⋯ }.support

Proof state:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ (∃ a ∈ l.support, a.fst = i) ↔
    ∃ x,
      x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a => l ⟨i, a⟩, mem_support_toFun := ⋯ }.support

Tactic:
simp only [exists_prop, Finset.mem_preimage, exists_and_right, exists_eq_right, mem_support_iff,
  Sigma.exists, Ne]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
theorem binomial_apply_self (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) :
    binomial p h n n = p^n

Proof state:
p : ℝ≥0∞
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) ↑n = p ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/Int.lean
theorem ball_eq_Ioo (x : ℤ) (r : ℝ) : ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Proof state:
x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Tactic:
rw [← preimage_ball, Real.ball_eq_Ioo, preimage_Ioo]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem typein_one_toType (x : toType 1) : typein (α := toType 1) (· < ·) x = 0

Proof state:
x : toType 1
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding x = 0

Tactic:
rw [one_toType_eq x, typein_enum]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem fun_eq_funMulInvSnorm_mul_eLpNorm {p : ℝ} (f : α → ℝ≥0∞)
    (hf_nonzero : (∫⁻ a, f a ^ p ∂μ) ≠ 0) (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) {a : α} :
    f a = funMulInvSnorm f p μ a * (∫⁻ c, f c ^ p ∂μ) ^ (1 / p)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
a : α
⊢ f a = funMulInvSnorm f p μ a * (∫⁻ (c : α), f c ^ p ∂μ) ^ (1 / p)

Tactic:
simp [funMulInvSnorm, mul_assoc, ENNReal.inv_mul_cancel, hf_nonzero, hf_top]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_zero : sinh 0 = 0

Proof state:
⊢ sinh 0 = 0

Tactic:
simp [sinh]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_add_cancel_right (a b : Int) : a + -b + b = a

Proof state:
a b : Int
⊢ a + -b + b = a

Tactic:
rw [Int.add_assoc, Int.add_left_neg, Int.add_zero]

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
theorem coe_mk (f : M →ₗ[R] N) (h) : ((⟨f, h⟩ : M →ₗ⁅R,L⁆ N) : M → N) = f

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : LieRingModule L M
inst✝ : LieRingModule L N
f : M →ₗ[R] N
h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆
⊢ ⇑{ toLinearMap := f, map_lie' := h } = ⇑f

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Distributions/Poisson.lean
/-- The Poisson pmf is positive for all natural numbers -/
lemma poissonPMFReal_pos {r : ℝ≥0} {n : ℕ} (hr : 0 < r) : 0 < poissonPMFReal r n

Proof state:
r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < rexp (-↑r) * ↑r ^ n / ↑n !

Tactic:
positivity

Result:
no goals

Proof state:
r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < poissonPMFReal r n

Tactic:
rw [poissonPMFReal]

Result:
r : ℝ≥0
n : ℕ
hr : 0 < r
⊢ 0 < rexp (-↑r) * ↑r ^ n / ↑n !
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- See also `Finset.prod_ite_eq`. -/
@[to_additive "See also `Finset.sum_ite_eq`."]
lemma prod_ite_eq (i : ι) (f : ι → α) : ∏ j, (if i = j then f j else 1) = f i

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
i : ι
f : ι → α
⊢ (∏ j : ι, if i = j then f j else 1) = f i

Tactic:
rw [Finset.prod_ite_eq, if_pos (mem_univ _)]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
theorem zeta_eq_tsum_one_div_nat_cpow {s : ℂ} (hs : 1 < re s) :
    riemannZeta s = ∑' n : ℕ, 1 / (n : ℂ) ^ s

Proof state:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
simpa only [QuotientAddGroup.mk_zero, cosZeta_zero, mul_zero, zero_mul, Real.cos_zero,
  ofReal_one] using (hasSum_nat_cosZeta 0 hs).tsum_eq.symm

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem filter_eq_generate (h : IsBasis p s) : h.filter = generate { U | ∃ i, p i ∧ s i = U }

Proof state:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ h.filter = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
rw [IsBasis.filter, ← h.filterBasis.generate, IsBasis.filterBasis]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Cast.lean
@[simp, norm_cast]
lemma cast_abs : (↑|a| : R) = |(a : R)|

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℤ
⊢ ↑|a| = |↑a|

Tactic:
simp [abs_eq_max_neg]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_tail (s : WSeq α) : destruct (tail s) = destruct s >>= tail.aux

Proof state:
α : Type u
s : WSeq α
⊢ s.tail.destruct = s.destruct >>= tail.aux

Tactic:
simp only [tail, destruct_flatten, tail.aux]

Result:
α : Type u
s : WSeq α
⊢ (fun o => Option.rec nil Prod.snd o) <$> s.destruct >>= destruct = s.destruct >>= tail.aux

Proof state:
case h
α : Type u
s : WSeq α
⊢ (fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = tail.aux

Tactic:
ext1 (_ | ⟨a, s⟩) <;> apply (@pure_bind Computation _ _ _ _ _ _).trans _ <;> simp

Result:
no goals

Proof state:
α : Type u
s : WSeq α
⊢ (fun o => Option.rec nil Prod.snd o) <$> s.destruct >>= destruct = s.destruct >>= tail.aux

Tactic:
rw [← bind_pure_comp, LawfulMonad.bind_assoc]

Result:
α : Type u
s : WSeq α
⊢ (s.destruct >>= fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = s.destruct >>= tail.aux

Proof state:
α : Type u
s : WSeq α
⊢ (s.destruct >>= fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = s.destruct >>= tail.aux

Tactic:
apply congr_arg

Result:
case h
α : Type u
s : WSeq α
⊢ (fun x => Pure.pure (Option.rec nil Prod.snd x) >>= destruct) = tail.aux
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean
theorem convexBodySumFun_neg (x : mixedSpace K) :
    convexBodySumFun (- x) = convexBodySumFun x

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ convexBodySumFun (-x) = convexBodySumFun x

Tactic:
simp_rw [convexBodySumFun, normAtPlace_neg]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem succ_ascFactorial (n : ℕ) :
    ∀ k, n * n.succ.ascFactorial k = (n + k) * n.ascFactorial k
  | 0 => by rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]
  | k + 1 => by rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
    ← Nat.add_assoc]

Proof state:
n : ℕ
⊢ n * n.succ.ascFactorial 0 = (n + 0) * n.ascFactorial 0

Tactic:
rw [Nat.add_zero, ascFactorial_zero, ascFactorial_zero]

Result:
no goals

Proof state:
n k : ℕ
⊢ n * n.succ.ascFactorial (k + 1) = (n + (k + 1)) * n.ascFactorial (k + 1)

Tactic:
rw [ascFactorial, Nat.mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add,
← Nat.add_assoc]

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem nil_mem_kstar (l : Language α) : [] ∈ l∗ :=
  ⟨[], rfl, fun _ h ↦ by contradiction⟩

Proof state:
α : Type u_1
l : Language α
x✝ : List α
h : x✝ ∈ []
⊢ x✝ ∈ l

Tactic:
contradiction

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_vandermonde_sub {n : ℕ} (v : Fin n → R) (a : R) :
    (Matrix.vandermonde fun i ↦ v i - a).det = (Matrix.vandermonde v).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i => v i - a).det = (vandermonde fun i => v i + -a).det

Tactic:
simp only [← sub_eq_add_neg]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i => v i - a).det = (vandermonde v).det

Tactic:
rw [← det_vandermonde_add v (- a)]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i => v i - a).det = (vandermonde fun i => v i + -a).det
-- Mathlib/Analysis/Analytic/Basic.lean
theorem radius_eq_top_of_eventually_eq_zero (h : ∀ᶠ n in atTop, p n = 0) : p.radius = ∞ :=
  p.radius_eq_top_of_forall_nnreal_isBigO fun r =>
    (isBigO_zero _ _).congr' (h.mono fun n hn => by simp [hn]) EventuallyEq.rfl

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
h : ∀ᶠ (n : ℕ) in atTop, p n = 0
r : ℝ≥0
n : ℕ
hn : p n = 0
⊢ (fun _x => 0) n = (fun n => ‖p n‖ * ↑r ^ n) n

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Cover/Open.lean
theorem affineBasisCover_map_range (X : Scheme.{u}) (x : X)
    (r : (X.local_affine x).choose_spec.choose) :
    Set.range (X.affineBasisCover.map ⟨x, r⟩).base =
      (X.affineCover.map x).base '' (PrimeSpectrum.basicOpen r).1

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
r : ↑⋯.choose
⊢ Set.range ⇑(ConcreteCategory.hom (X.affineBasisCover.map ⟨x, r⟩).base) =
    ⇑(ConcreteCategory.hom (X.affineCover.map x).base) '' (PrimeSpectrum.basicOpen r).carrier

Tactic:
simp only [affineBasisCover, Cover.bind_map, comp_coeBase, TopCat.hom_comp,
  ContinuousMap.coe_comp, Set.range_comp]

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
r : ↑⋯.choose
⊢ ⇑(TopCat.Hom.hom (X.affineCover.map x).base) ''
      Set.range ⇑(TopCat.Hom.hom ((affineBasisCoverOfAffine ⋯.choose).map r).base) =
    (fun a => (ConcreteCategory.hom (X.affineCover.map x).base) a) '' (PrimeSpectrum.basicOpen r).carrier

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
r : ↑⋯.choose
⊢ Set.range ⇑(TopCat.Hom.hom ((affineBasisCoverOfAffine ⋯.choose).map r).base) = (PrimeSpectrum.basicOpen r).carrier

Tactic:
exact (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r :)

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_map {V W X Y Z : C} (f : V ⟶ W) (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
    lift f g ≫ (h ⊗ k) = lift (f ≫ h) (g ≫ k)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ChosenFiniteProducts C
V W X Y Z : C
f : V ⟶ W
g : V ⟶ X
h : W ⟶ Y
k : X ⟶ Z
⊢ lift f g ≫ (h ⊗ k) = lift (f ≫ h) (g ≫ k)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.map {β γ} {f : β → γ} {g : α → Part β} (hg : ωScottContinuous g) :
    ωScottContinuous fun x ↦ f <$> g x

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : β → γ
g : α → Part β
hg : ωScottContinuous g
⊢ ωScottContinuous fun x => f <$> g x

Tactic:
simpa only [map_eq_bind_pure_comp] using ωScottContinuous.bind hg ωScottContinuous.const

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Ico_pred_left (h : pred a < b) : Ico (pred a) b = insert (pred a) (Ico a b)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : pred a < b
⊢ Ico (pred a) b = insert (pred a) (Ico a b)

Tactic:
simp_rw [← Ici_inter_Iio, Ici_pred, insert_inter_of_mem (mem_Iio.2 h)]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem ne_zero_iff_orderTop {x : HahnSeries Γ R} : x ≠ 0 ↔ orderTop x ≠ ⊤

Proof state:
case mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.orderTop ≠ ⊤ → x ≠ 0

Tactic:
contrapose!

Result:
case mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x = 0 → x.orderTop = ⊤

Proof state:
case mp
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 → x.orderTop ≠ ⊤

Tactic:
exact fun hx => Eq.mpr (congrArg (fun h ↦ h ≠ ⊤) (orderTop_of_ne hx)) WithTop.coe_ne_top

Result:
no goals

Proof state:
case mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x = 0 → x.orderTop = ⊤

Tactic:
simp_all only [orderTop_zero, implies_true]

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 ↔ x.orderTop ≠ ⊤

Tactic:
constructor

Result:
case mp
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x ≠ 0 → x.orderTop ≠ ⊤

case mpr
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
⊢ x.orderTop ≠ ⊤ → x ≠ 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem cons_diff_of_not_mem {a : α} {l₂ : List α} (h : a ∉ l₂) (l₁ : List α) :
    (a :: l₁).diff l₂ = a :: l₁.diff l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l₂ : List α
h : ¬a ∈ l₂
l₁ : List α
⊢ (a :: l₁).diff l₂ = a :: l₁.diff l₂

Tactic:
rw [cons_diff, if_neg h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
theorem hurwitzZetaOdd_neg_two_mul_nat_sub_one (a : UnitAddCircle) (n : ℕ) :
    hurwitzZetaOdd a (-2 * n - 1) = 0

Proof state:
a : UnitAddCircle
n : ℕ
⊢ -2 * ↑n - 1 + 1 = -(2 * ↑n)

Tactic:
rw [neg_mul, sub_add_cancel]

Result:
no goals

Proof state:
a : UnitAddCircle
n : ℕ
⊢ hurwitzZetaOdd a (-2 * ↑n - 1) = 0

Tactic:
rw [hurwitzZetaOdd, Gammaℝ_eq_zero_iff.mpr ⟨n, by rw [neg_mul, sub_add_cancel]⟩, div_zero]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.mul_le {I J P : Ideal R} (hp : IsPrime P) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P

Proof state:
R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P

Tactic:
simp_rw [hp.mul_mem_iff_mem_or_mem, SetLike.le_def, ← forall_or_left, or_comm, forall_or_left]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ I * J ≤ P ↔ I ≤ P ∨ J ≤ P

Tactic:
rw [or_comm, Ideal.mul_le]

Result:
R : Type u
inst✝ : CommSemiring R
I J P : Ideal R
hp : P.IsPrime
⊢ (∀ r ∈ I, ∀ s ∈ J, r * s ∈ P) ↔ J ≤ P ∨ I ≤ P
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem USize.sizeOf (a : USize) : sizeOf a = a.toNat + 3

Proof state:
a : USize
⊢ sizeOf a = a.toNat + 3

Tactic:
cases a

Result:
case mk
toBitVec✝ : BitVec System.Platform.numBits
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Proof state:
case mk
toBitVec✝ : BitVec System.Platform.numBits
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Tactic:
simp_arith [USize.toNat, BitVec.toNat]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_eq_iff_eq_sq (hx : 0 ≤ x) (hy : 0 ≤ y) : √x = y ↔ x = y ^ 2

Proof state:
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ √x = y ↔ x = y ^ 2

Tactic:
rw [sq, sqrt_eq_iff_mul_self_eq hx hy]

Result:
no goals
-- Mathlib/Data/DFinsupp/Multiset.lean
theorem toDFinsupp_inter (s t : Multiset α) : toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toDFinsupp (s ∩ t) = toDFinsupp s ⊓ toDFinsupp t

Tactic:
ext i

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
i : α
⊢ (toDFinsupp (s ∩ t)) i = (toDFinsupp s ⊓ toDFinsupp t) i
-- Mathlib/Data/Matroid/Constructions.lean
lemma uniqueBaseOn_rankPos (hIE : I ⊆ E) (hI : I.Nonempty) : RankPos (uniqueBaseOn I E) where
  empty_not_isBase

Proof state:
α : Type u_1
E I : Set α
hIE : I ⊆ E
hI : I.Nonempty
⊢ ¬(uniqueBaseOn I E).IsBase ∅

Tactic:
simpa [uniqueBaseOn_isBase_iff hIE] using Ne.symm <| hI.ne_empty

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma exists_succAbove_eq_iff {x y : Fin (n + 1)} : (∃ z, x.succAbove z = y) ↔ y ≠ x :=
  ⟨by rintro ⟨y, rfl⟩; exact succAbove_ne _ _, exists_succAbove_eq⟩

Proof state:
n : ℕ
x y : Fin (n + 1)
⊢ (∃ z, x.succAbove z = y) → y ≠ x

Tactic:
rintro ⟨y, rfl⟩

Result:
case intro
n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x

Proof state:
case intro
n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x

Tactic:
exact succAbove_ne _ _

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem ne_zero_of_gcd {x y : ℤ} (hc : gcd x y ≠ 0) : x ≠ 0 ∨ y ≠ 0

Proof state:
x y : ℤ
hc : x.gcd y ≠ 0
⊢ x ≠ 0 ∨ y ≠ 0

Tactic:
contrapose! hc

Result:
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ x.gcd y = 0

Proof state:
x y : ℤ
hc : x = 0 ∧ y = 0
⊢ x.gcd y = 0

Tactic:
rw [hc.left, hc.right, gcd_zero_right, natAbs_zero]

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem truncate_zero_zero {a b : X} (γ : Path a b) :
    γ.truncate 0 0 = (Path.refl a).cast (by rw [min_self, γ.extend_zero]) γ.extend_zero

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
γ : Path a b
⊢ γ.truncate 0 0 = (refl a).cast ⋯ ⋯

Tactic:
convert γ.truncate_self 0

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type u_3
γ✝ : Path x y
a b : X
γ : Path a b
⊢ γ.extend (0 ⊓ 0) = a

Tactic:
rw [min_self, γ.extend_zero]

Result:
no goals