harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderivWithin_snd {s : Set (M × M')} {x : M × M'}
    (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
    mfderivWithin (I.prod I') I' Prod.snd s x =
      ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ mfderivWithin (I.prod I') I' Prod.snd s x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_snd hxs]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ mfderiv (I.prod I') I' Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ mfderiv (I.prod I') I' Prod.snd x = ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
exact mfderiv_snd

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem le_div_iff_mul_le {I J J' : FractionalIdeal R₁⁰ K} (hJ' : J' ≠ 0) :
    I ≤ J / J' ↔ I * J' ≤ J

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ ↑I * ↑J' ≤ ↑J

Tactic:
exact Submodule.le_div_iff_mul_le

Result:
no goals

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ J / J' ↔ I * J' ≤ J

Tactic:
rw [div_nonzero hJ']

Result:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ I * J' ≤ J

Proof state:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ I * J' ≤ J

Tactic:
rw [← coe_le_coe (I := I * J') (J := J), coe_mul]

Result:
R₁ : Type u_3
inst✝⁴ : CommRing R₁
K : Type u_4
inst✝³ : Field K
inst✝² : Algebra R₁ K
inst✝¹ : IsFractionRing R₁ K
inst✝ : IsDomain R₁
I J J' : FractionalIdeal R₁⁰ K
hJ' : J' ≠ 0
⊢ I ≤ ⟨↑J / ↑J', ⋯⟩ ↔ ↑I * ↑J' ≤ ↑J
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insert [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {k a : α} {v : β} :
    get! (m.insert k v) a = if k == a then v else get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
k a : α
v : β
⊢ get! (m.insert k v) a = if (k == a) = true then v else get! m a

Tactic:
simp_to_model [insert] using List.getValue!_insertEntry

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem WSameSide.not_sOppSide {s : AffineSubspace R P} {x y : P} (h : s.WSameSide x y) :
    ¬s.SOppSide x y

Proof state:
case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
hy : y ∈ s
⊢ False

Tactic:
exact ho.2.2 hy

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False

Tactic:
rcases hxy with (hx | hy)

Result:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
hx : x ∈ s
⊢ False

case inr
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
hy : y ∈ s
⊢ False

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
⊢ ¬s.SOppSide x y

Tactic:
intro ho

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
⊢ False

Proof state:
case inl
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
hx : x ∈ s
⊢ False

Tactic:
exact ho.2.1 hx

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
⊢ False

Tactic:
have hxy := wSameSide_and_wOppSide_iff.1 ⟨h, ho.1⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
h : s.WSameSide x y
ho : s.SOppSide x y
hxy : x ∈ s ∨ y ∈ s
⊢ False
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_toNNReal_iff {f : α → ℝ≥0∞} {u : Filter α} (ha : a ≠ ∞) (hf : ∀ x, f x ≠ ∞) :
    Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (a.toNNReal)) ↔ Tendsto f u (𝓝 a)

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ⊤
hf : ∀ (x : α), f x ≠ ⊤
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto ((fun x => ↑x) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)

Tactic:
exact (tendsto_coe_toNNReal ha).comp h

Result:
no goals

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ⊤
hf : ∀ (x : α), f x ≠ ⊤
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto f u (𝓝 a)

Tactic:
rw [← coe_comp_toNNReal_comp hf]

Result:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ⊤
hf : ∀ (x : α), f x ≠ ⊤
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto ((fun x => ↑x) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)

Proof state:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ⊤
hf : ∀ (x : α), f x ≠ ⊤
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal) ↔ Tendsto f u (𝓝 a)

Tactic:
refine ⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩

Result:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ⊤
hf : ∀ (x : α), f x ≠ ⊤
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto f u (𝓝 a)
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv'_symm_apply {n a : ℤ} (f : Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧)
    (a' : ℤ) (h : n + a = a') :
    (opEquiv' n a a' h).symm f =
      (opEquiv n).symm f ≫ (shiftFunctorAdd' C a n a' (by omega)).inv.app _ :=
  rfl

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.52616, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
n a : ℤ
f : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ n).obj (Opposite.op X)
a' : ℤ
h : n + a = a'
⊢ a + n = a'

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem mul_left_eq_one (r : R) (x : tsze R M) (h : r * x.fst = 1) :
    (inl r + inr (-((r •> x.snd) <• r))) * x = 1

Proof state:
case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0

Tactic:
rw [add_zero, zero_add, smul_neg, op_smul_op_smul, h, op_one, one_smul,
  add_neg_cancel]

Result:
no goals

Proof state:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) * x.fst = 1

Tactic:
rw [add_zero, h]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1

Tactic:
ext <;> dsimp

Result:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) * x.fst = 1

case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (r + 0) •> x.snd + (0 + -(r •> x.snd <• r)) <• x.fst = 0
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sqrtTwoAddSeries_one : sqrtTwoAddSeries 0 1 = √2

Proof state:
⊢ sqrtTwoAddSeries 0 1 = √2

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem eq_prime_pow_of_dvd_least_prime_pow {a p k : ℕ} (pp : Prime p) (h₁ : ¬a ∣ p ^ k)
    (h₂ : a ∣ p ^ (k + 1)) : a = p ^ (k + 1)

Proof state:
a p k : ℕ
pp : Prime p
h₁ : ¬a ∣ p ^ k
h₂ : a ∣ p ^ (k + 1)
⊢ a = p ^ (k + 1)

Tactic:
obtain ⟨l, ⟨h, rfl⟩⟩ := (dvd_prime_pow pp).1 h₂

Result:
case intro.intro
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)

Proof state:
case intro.intro
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ p ^ l = p ^ (k + 1)

Tactic:
congr

Result:
case intro.intro.e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1

Proof state:
case intro.intro.e_a
p k : ℕ
pp : Prime p
l : ℕ
h : l ≤ k + 1
h₁ : ¬p ^ l ∣ p ^ k
h₂ : p ^ l ∣ p ^ (k + 1)
⊢ l = k + 1

Tactic:
exact le_antisymm h (not_le.1 ((not_congr (pow_dvd_pow_iff_le_right (Prime.one_lt pp))).1 h₁))

Result:
no goals
-- Mathlib/Data/List/Pairwise.lean
theorem Pairwise.forall_of_forall (H : Symmetric R) (H₁ : ∀ x ∈ l, R x x) (H₂ : l.Pairwise R) :
    ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → R x y :=
  H₂.forall_of_forall_of_flip H₁ <| by rwa [H.flip_eq]

Proof state:
α : Type u_1
R : α → α → Prop
l : List α
H : Symmetric R
H₁ : ∀ (x : α), x ∈ l → R x x
H₂ : Pairwise R l
⊢ Pairwise (flip R) l

Tactic:
rwa [H.flip_eq]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem mul_le_of_le_div (h : a ≤ b / c) : a * c ≤ b

Proof state:
a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c⁻¹⁻¹ ≤ b

Tactic:
exact div_le_of_le_mul h

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c ≤ b

Tactic:
rw [← inv_inv c]

Result:
a b c : ℝ≥0∞
h : a ≤ b / c
⊢ a * c⁻¹⁻¹ ≤ b
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem integral_add_compl₀ (hs : NullMeasurableSet s μ) (hfi : Integrable f μ) :
    ∫ x in s, f x ∂μ + ∫ x in sᶜ, f x ∂μ = ∫ x, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
⊢ ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ

Tactic:
rw [
  ← integral_union_ae disjoint_compl_right.aedisjoint hs.compl hfi.integrableOn hfi.integrableOn,
  union_compl_self, setIntegral_univ]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma awayToSection_germ (f x hx) :
    awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ _ x hx =
      CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 (Submonoid.powers_le.mpr hx)) ≫
        (Proj.stalkIso' 𝒜 x).toCommRingCatIso.inv

Proof state:
case hf.a
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ («Proj».stalkIso' 𝒜 x).toEquiv
      ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z) =
    (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯)).hom' z

Tactic:
apply Proj.stalkIso'_germ

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
⊢ awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv

Tactic:
ext z

Result:
case hf.a
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ (CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv))
      z

Proof state:
case hf.a
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ (CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z =
    (CommRingCat.Hom.hom
        (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯) ≫ («Proj».stalkIso' 𝒜 x).toCommRingCatIso.inv))
      z

Tactic:
apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr

Result:
case hf.a
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(ProjectiveSpectrum.top 𝒜)
hx : x ∈ pbo f
z : ↑(CommRingCat.of (A⁰_ f))
⊢ («Proj».stalkIso' 𝒜 x).toEquiv
      ((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (structureSheaf 𝒜).presheaf.germ (pbo f) x hx)) z) =
    (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯)).hom' z
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_sub (M : Matrix m n α) (N N' : Matrix n o α) :
    M * (N - N') = M * N - M * N'

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N N' : Matrix n o α
⊢ M * (N - N') = M * N - M * N'

Tactic:
rw [sub_eq_add_neg, Matrix.mul_add, Matrix.mul_neg, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem induced_iff_nhds_eq [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) :
    tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b)

Proof state:
α : Type u
β : Type v
tα : TopologicalSpace α
tβ : TopologicalSpace β
f : β → α
⊢ tβ = induced f tα ↔ ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))

Tactic:
simp only [ext_iff_nhds, nhds_induced]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem map_hausdorffMeasure (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) :
    Measure.map f μH[d] = μH[d].restrict (range f)

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
⊢ Measure.map f μH[d] = μH[d].restrict (range f)

Tactic:
ext1 s hs

Result:
case h
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
⊢ (Measure.map f μH[d]) s = (μH[d].restrict (range f)) s

Proof state:
case h
X : Type u_2
Y : Type u_3
inst✝⁵ : EMetricSpace X
inst✝⁴ : EMetricSpace Y
inst✝³ : MeasurableSpace X
inst✝² : BorelSpace X
inst✝¹ : MeasurableSpace Y
inst✝ : BorelSpace Y
f : X → Y
d : ℝ
hf : Isometry f
hd : 0 ≤ d ∨ Surjective f
s : Set Y
hs : MeasurableSet s
⊢ (Measure.map f μH[d]) s = (μH[d].restrict (range f)) s

Tactic:
rw [map_apply hf.continuous.measurable hs, Measure.restrict_apply hs,
  hf.hausdorffMeasure_preimage hd]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
@[reassoc (attr := simp)]
lemma desc_commutes_zero {Y Z : C} (f : Z ⟶ Y)
    (I : InjectiveResolution Y) (J : InjectiveResolution Z) :
    J.ι.f 0 ≫ (desc f I J).f 0 = f ≫ I.ι.f 0 :=
  (HomologicalComplex.congr_hom (desc_commutes f I J) 0).trans (by simp)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Z ⟶ Y
I : InjectiveResolution Y
J : InjectiveResolution Z
⊢ ((CochainComplex.single₀ C).map f ≫ I.ι).f 0 = f ≫ I.ι.f 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_projected_entry {entry : Entrypoint α} :
    ⟦entry.aig, entry.ref, assign⟧ = ⟦entry, assign⟧

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦assign, { aig := { aig := aig✝, ref := ref✝ }.aig, ref := { aig := aig✝, ref := ref✝ }.ref }⟧ =
    ⟦assign, { aig := aig✝, ref := ref✝ }⟧

Tactic:
simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
⊢ ⟦assign, { aig := entry.aig, ref := entry.ref }⟧ = ⟦assign, entry⟧

Tactic:
cases entry

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦assign, { aig := { aig := aig✝, ref := ref✝ }.aig, ref := { aig := aig✝, ref := ref✝ }.ref }⟧ =
    ⟦assign, { aig := aig✝, ref := ref✝ }⟧
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem one_le_norm_one (β) [NormedRing β] [Nontrivial β] : 1 ≤ ‖(1 : β)‖ :=
  (le_mul_iff_one_le_left <| norm_pos_iff.mpr (one_ne_zero : (1 : β) ≠ 0)).mp
    (by simpa only [mul_one] using norm_mul_le (1 : β) 1)

Proof state:
β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖

Tactic:
simpa only [mul_one] using norm_mul_le (1 : β) 1

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_domain_of_mem_graph {f : E →ₗ.[R] F} {x : E} {y : F} (h : (x, y) ∈ f.graph) :
    x ∈ f.domain

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ x ∈ f.domain

Tactic:
rw [mem_domain_iff]

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ f.graph

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E
y : F
h : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ f.graph

Tactic:
exact ⟨y, h⟩

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma inv_smul_lt_iff_of_pos [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
    a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ a⁻¹ • b₁ < b₂ ↔ b₁ < a • b₂

Tactic:
rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Result:
no goals
-- Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@[to_additive]
private lemma exists_mul_right_lt [CommGroup α] [LT α] [DenselyOrdered α]
    [CovariantClass α α (· * ·) (· < ·)] {a b c : α} (hc : a * b < c) :
    ∃ b' > b, a * b' < c

Proof state:
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : a * b < c
⊢ ∃ b', b' > b ∧ a * b' < c

Tactic:
obtain ⟨a', ha', hc'⟩ := exists_between (lt_div_iff_mul_lt'.2 hc)

Result:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : a * b < c
a' : α
ha' : b < a'
hc' : a' < c / a
⊢ ∃ b', b' > b ∧ a * b' < c

Proof state:
case intro.intro
α : Type u_1
inst✝³ : CommGroup α
inst✝² : LT α
inst✝¹ : DenselyOrdered α
inst✝ : CovariantClass α α (fun x1 x2 => x1 * x2) fun x1 x2 => x1 < x2
a b c : α
hc : a * b < c
a' : α
ha' : b < a'
hc' : a' < c / a
⊢ ∃ b', b' > b ∧ a * b' < c

Tactic:
exact ⟨a', ha', lt_div_iff_mul_lt'.1 hc'⟩

Result:
no goals
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nmul_lt_nmul_of_pos_left (h₁ : a < b) (h₂ : 0 < c) : c ⨳ a < c ⨳ b :=
  lt_nmul_iff.2 ⟨0, h₂, a, h₁, by simp⟩

Proof state:
a b c : Ordinal.{u}
h₁ : a < b
h₂ : 0 < c
⊢ c ⨳ a ♯ 0 ⨳ a ≤ 0 ⨳ b ♯ c ⨳ a

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem discr_prime_pow_ne_two' [IsCyclotomicExtension {p ^ (k + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))) (hk : p ^ (k + 1) ≠ 2) :
    discr ℚ (hζ.subOnePowerBasis ℚ).basis =
      (-1) ^ ((p ^ (k + 1) : ℕ).totient / 2) * p ^ ((p : ℕ) ^ k * ((p - 1) * (k + 1) - 1))

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis

Tactic:
exact hζ.discr_zeta_eq_discr_zeta_sub_one.symm

Result:
no goals

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    (-1) ^ (φ (↑p ^ (k + 1)) / 2) * ↑↑p ^ (↑p ^ k * ((↑p - 1) * (k + 1) - 1))

Tactic:
rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (p ^ (k + 1)).pos) hk]

Result:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ Algebra.discr ℚ ⇑(IsPrimitiveRoot.subOnePowerBasis ℚ hζ).basis =
    Algebra.discr ℚ ⇑(IsPrimitiveRoot.powerBasis ℚ hζ).basis
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
lemma Gammaℂ_add_one {s : ℂ} (hs : s ≠ 0) : Gammaℂ (s + 1) = Gammaℂ s * s / 2 / π

Proof state:
s : ℂ
hs : s ≠ 0
⊢ (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑π

Tactic:
rw [Gammaℂ_def, Gammaℂ_def, Gamma_add_one _ hs, neg_add,
  cpow_add _ _ (mul_ne_zero two_ne_zero (ofReal_ne_zero.mpr pi_ne_zero)), cpow_neg_one]

Result:
s : ℂ
hs : s ≠ 0
⊢ 2 * ((2 * ↑π) ^ (-s) * (2 * ↑π)⁻¹) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π

Proof state:
s : ℂ
hs : s ≠ 0
⊢ 2 * ((2 * ↑π) ^ (-s) * (2 * ↑π)⁻¹) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π

Tactic:
field_simp [pi_ne_zero]

Result:
s : ℂ
hs : s ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s

Proof state:
s : ℂ
hs : s ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s

Tactic:
ring

Result:
no goals