harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem of_algebraRat [Algebra ℚ R] : ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)

Proof state:
case cast_injective.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑a - ↑b ≠ 0

Tactic:
simpa only [Ne, sub_eq_zero] using (@Nat.cast_injective ℚ _ _).ne hI

Result:
no goals

Proof state:
case cast_injective.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ (algebraMap ℚ R) (↑a - ↑b) ∈ I

Tactic:
simpa only [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero, map_natCast]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)

Tactic:
constructor

Result:
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ Function.Injective Nat.cast

Proof state:
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ Function.Injective Nat.cast

Tactic:
intro a b h_ab

Result:
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : ↑a = ↑b
⊢ a = b

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
intro I hI

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
⊢ CharZero (R ⧸ I)

Proof state:
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
hI : I ≠ ⊤
a b : ℕ
h_ab : ↑a = ↑b
⊢ a = b

Tactic:
contrapose! hI

Result:
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ I = ⊤

Proof state:
case cast_injective
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ I = ⊤

Tactic:
refine I.eq_top_of_isUnit_mem ?_ (IsUnit.map (algebraMap ℚ R) (IsUnit.mk0 (a - b : ℚ) ?_))

Result:
case cast_injective.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ (algebraMap ℚ R) (↑a - ↑b) ∈ I

case cast_injective.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra ℚ R
I : Ideal R
a b : ℕ
h_ab : ↑a = ↑b
hI : a ≠ b
⊢ ↑a - ↑b ≠ 0
-- Mathlib/Topology/Basic.lean
lemma Equiv.continuous_symm_iff (e : X ≃ Y) : Continuous e.symm ↔ IsOpenMap e

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ Continuous ⇑e.symm ↔ IsOpenMap ⇑e

Tactic:
simp_rw [continuous_def, ← Set.image_equiv_eq_preimage_symm, IsOpenMap]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem IsCoprime.prod_left : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Tactic:
rw [Finset.forall_mem_insert] at H

Result:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
H : IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x

Tactic:
rw [Finset.prod_insert hbt]

Result:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
H : IsCoprime (s b) x ∧ ∀ x_1 ∈ t, IsCoprime (s x_1) x
⊢ IsCoprime (s b * ∏ x ∈ t, s x) x

Tactic:
exact H.1.mul_left (ih H.2)

Result:
no goals

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x

Tactic:
classical
refine Finset.induction_on t (fun _ ↦ isCoprime_one_left) fun b t hbt ih H ↦ ?_
rw [Finset.prod_insert hbt]
rw [Finset.forall_mem_insert] at H
exact H.1.mul_left (ih H.2)

Result:
no goals

Proof state:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t : Finset I
⊢ (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x

Tactic:
refine Finset.induction_on t (fun _ ↦ isCoprime_one_left) fun b t hbt ih H ↦ ?_

Result:
R : Type u
I : Type v
inst✝ : CommSemiring R
x : R
s : I → R
t✝ : Finset I
b : I
t : Finset I
hbt : b ∉ t
ih : (∀ i ∈ t, IsCoprime (s i) x) → IsCoprime (∏ i ∈ t, s i) x
H : ∀ i ∈ insert b t, IsCoprime (s i) x
⊢ IsCoprime (∏ i ∈ insert b t, s i) x
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDeriv_clm_apply_const_apply
    {c : E → F →L[𝕜] G} (hc : ContDiff 𝕜 n c)
    {i : ℕ} (hi : i ≤ n) {x : E} {u : F} {m : Fin i → E} :
    (iteratedFDeriv 𝕜 i (fun y ↦ (c y) u) x) m = (iteratedFDeriv 𝕜 i c x) m u

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : ↑i ≤ n
x : E
u : F
m : Fin i → E
⊢ (iteratedFDeriv 𝕜 i (fun y => (c y) u) x) m = ((iteratedFDeriv 𝕜 i c x) m) u

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : ↑i ≤ n
x : E
u : F
m : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) univ x) m = ((iteratedFDerivWithin 𝕜 i c univ x) m) u

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
c : E → F →L[𝕜] G
hc : ContDiff 𝕜 n c
i : ℕ
hi : ↑i ≤ n
x : E
u : F
m : Fin i → E
⊢ (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) univ x) m = ((iteratedFDerivWithin 𝕜 i c univ x) m) u

Tactic:
exact iteratedFDerivWithin_clm_apply_const_apply uniqueDiffOn_univ hc.contDiffOn hi (mem_univ _)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Continuous.lean
lemma op_comp_isSheaf_of_preservesOneHypercovers
    [PreservesOneHypercovers.{w} F J K] [GrothendieckTopology.IsGeneratedByOneHypercovers.{w} J]
    (P : Dᵒᵖ ⥤ A) (hP : Presheaf.IsSheaf K P) :
    Presheaf.IsSheaf J (F.op ⋙ P)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
⊢ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork (F.op ⋙ P)))

Tactic:
intro X E

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
X : C
E : J.OneHypercover X
⊢ Nonempty (IsLimit (E.multifork (F.op ⋙ P)))

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
X : C
E : J.OneHypercover X
⊢ Nonempty (IsLimit (E.multifork (F.op ⋙ P)))

Tactic:
exact ⟨(E.toPreOneHypercover.isLimitMapMultiforkEquiv F P)
  ((E.map F K).isLimitMultifork ⟨P, hP⟩)⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (F.op ⋙ P)

Tactic:
rw [Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers.{w}]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ A
hP : Presheaf.IsSheaf K P
⊢ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (IsLimit (E.multifork (F.op ⋙ P)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem append_sublist_append_right (l) : l₁ ++ l <+ l₂ ++ l ↔ l₁ <+ l₂ :=
  ⟨fun h => by
    have := h.reverse
    simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this
    exact this,
   fun h => h.append_right l⟩

Proof state:
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : (l₁ ++ l).reverse <+ (l₂ ++ l).reverse
⊢ l₁ <+ l₂

Tactic:
simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this

Result:
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : l₁ <+ l₂
⊢ l₁ <+ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
⊢ l₁ <+ l₂

Tactic:
have := h.reverse

Result:
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : (l₁ ++ l).reverse <+ (l₂ ++ l).reverse
⊢ l₁ <+ l₂

Proof state:
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : l₁ <+ l₂
⊢ l₁ <+ l₂

Tactic:
exact this

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_add_mul_I (x y : ℂ) : sin (x + y * I) = sin x * cosh y + cos x * sinh y * I

Proof state:
x y : ℂ
⊢ sin (x + y * I) = sin x * cosh y + cos x * sinh y * I

Tactic:
rw [sin_add, cos_mul_I, sin_mul_I, mul_assoc]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma mem_corner_iff_mem_range_mul_right (hc : IsMulCentral e) {r : R} :
    r ∈ corner e ↔ r ∈ Set.range (· * e)

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ r ∈ Set.range fun x => x * e

Tactic:
simp_rw [mem_corner_iff_mem_range_mul_left idem hc, hc.comm]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem boundedBy_top : boundedBy (⊤ : Set α → ℝ≥0∞) = ⊤

Proof state:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ ≤ ⊤ s

Tactic:
exact le_rfl

Result:
no goals

Proof state:
α : Type u_1
⊢ boundedBy ⊤ = ⊤

Tactic:
rw [eq_top_iff, le_boundedBy']

Result:
α : Type u_1
⊢ ∀ (s : Set α), s.Nonempty → ⊤ s ≤ ⊤ s

Proof state:
α : Type u_1
⊢ ∀ (s : Set α), s.Nonempty → ⊤ s ≤ ⊤ s

Tactic:
intro s hs

Result:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ s ≤ ⊤ s

Proof state:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ s ≤ ⊤ s

Tactic:
rw [top_apply hs]

Result:
α : Type u_1
s : Set α
hs : s.Nonempty
⊢ ⊤ ≤ ⊤ s
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem dvd_of_dvd_mul_right_of_no_prime_factors {a b c : R} (ha : a ≠ 0)
    (no_factors : ∀ {d}, d ∣ a → d ∣ b → ¬Prime d) : a ∣ b * c → a ∣ c

Proof state:
R : Type u_2
inst✝¹ : CancelCommMonoidWithZero R
inst✝ : UniqueFactorizationMonoid R
a b c : R
ha : a ≠ 0
no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d
⊢ a ∣ b * c → a ∣ c

Tactic:
simpa [mul_comm b c] using dvd_of_dvd_mul_left_of_no_prime_factors ha @no_factors

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
theorem OrderIso.mulLeft₀'_symm {a : α} (ha : a ≠ 0) :
    (OrderIso.mulLeft₀' ha).symm = OrderIso.mulLeft₀' (inv_ne_zero ha)

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ (mulLeft₀' ha).symm = mulLeft₀' ⋯

Tactic:
ext

Result:
case h.h
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ (mulLeft₀' ha).symm x✝ = (mulLeft₀' ⋯) x✝

Proof state:
case h.h
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ (mulLeft₀' ha).symm x✝ = (mulLeft₀' ⋯) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Algebra/Support.lean
theorem HasCompactSupport.mul_right (hf : HasCompactSupport f) : HasCompactSupport (f * f')

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0

Tactic:
exact hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = 0 x
⊢ (f * f') x = 0 x

Tactic:
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : HasCompactSupport f
⊢ HasCompactSupport (f * f')

Tactic:
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢

Result:
α : Type u_2
β : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
hf : f =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
-- Mathlib/RingTheory/Support.lean
lemma Module.support_of_algebra {A : Type*} [Ring A] [Algebra R A] :
    Module.support R A = PrimeSpectrum.zeroLocus (RingHom.ker (algebraMap R A))

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (algebraMap R A) ≤ p.asIdeal

Tactic:
refine ⟨fun ⟨m, hm⟩ x hx ↦ not_not.mp fun hx' ↦ ?_, fun H ↦ ⟨1, fun r hr e ↦ ?_⟩⟩

Result:
case h.refine_1
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
x✝ : ∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0
x : R
hx : x ∈ RingHom.ker (algebraMap R A)
m : A
hm : ∀ r ∉ p.asIdeal, ¬r • m = 0
hx' : x ∉ p.asIdeal
⊢ False

case h.refine_2
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : r • 1 = 0
⊢ False

Proof state:
case h
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ p ∈ support R A ↔ p ∈ PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))

Tactic:
simp only [mem_support_iff', ne_eq, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe]

Result:
case h
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (algebraMap R A) ≤ p.asIdeal

Proof state:
case h.refine_2
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
H : RingHom.ker (algebraMap R A) ≤ p.asIdeal
r : R
hr : r ∉ p.asIdeal
e : r • 1 = 0
⊢ False

Tactic:
exact hr (H ((Algebra.algebraMap_eq_smul_one _).trans e))

Result:
no goals

Proof state:
case h.refine_1
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
x✝ : ∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0
x : R
hx : x ∈ RingHom.ker (algebraMap R A)
m : A
hm : ∀ r ∉ p.asIdeal, ¬r • m = 0
hx' : x ∉ p.asIdeal
⊢ False

Tactic:
simpa [Algebra.smul_def, (show _ = _ from hx)] using hm _ hx'

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
⊢ support R A = PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))

Tactic:
ext p

Result:
case h
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ p ∈ support R A ↔ p ∈ PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))
-- Mathlib/Analysis/RCLike/Inner.lean
lemma wInner_add_right (w : ι → ℝ) (f g₁ g₂ : ∀ i, E i) :
    ⟪f, g₁ + g₂⟫_[𝕜, w] = ⟪f, g₁⟫_[𝕜, w] + ⟪f, g₂⟫_[𝕜, w]

Proof state:
ι : Type u_1
𝕜 : Type u_3
E : ι → Type u_4
inst✝³ : Fintype ι
inst✝² : RCLike 𝕜
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (E i)
w : ι → ℝ
f g₁ g₂ : (i : ι) → E i
⊢ wInner w f (g₁ + g₂) = wInner w f g₁ + wInner w f g₂

Tactic:
simp [wInner, inner_add_right, smul_add, sum_add_distrib]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem replaceF_of_forall_none {l : List α} (h : ∀ a, a ∈ l → p a = none) : l.replaceF p = l

Proof state:
α : Type u_1
p : α → Option α
l : List α
h : ∀ (a : α), a ∈ l → p a = none
⊢ replaceF p l = l

Tactic:
induction l with
| nil => rfl
| cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Option α
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → p a = none) → replaceF p tail✝ = tail✝
h : ∀ (a : α), a ∈ head✝ :: tail✝ → p a = none
⊢ replaceF p (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Option α
h : ∀ (a : α), a ∈ [] → p a = none
⊢ replaceF p [] = []

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Presheaf.lean
lemma isLeftKanExtension_of_preservesColimits
    (L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ) (e : A ≅ yoneda ⋙ L)
    [PreservesColimitsOfSize.{v₁, max u₁ v₁} L] :
    L.IsLeftKanExtension e.hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
e : A ≅ yoneda ⋙ L
inst✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
⊢ IsIso e.hom ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L

Tactic:
exact ⟨inferInstance, ⟨inferInstance⟩⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
e : A ≅ yoneda ⋙ L
inst✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
⊢ L.IsLeftKanExtension e.hom

Tactic:
rw [isLeftKanExtension_along_yoneda_iff]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₁, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : yoneda.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type v₁) ⥤ ℰ
e : A ≅ yoneda ⋙ L
inst✝ : PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
⊢ IsIso e.hom ∧ PreservesColimitsOfSize.{v₁, max u₁ v₁, max u₁ v₁, v₁, max u₁ (v₁ + 1), u₂} L
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem leadingCoeff_div (hpq : q.degree ≤ p.degree) :
    (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
by_cases hq : q = 0

Result:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
rw [div_def, leadingCoeff_mul, leadingCoeff_C,
  leadingCoeff_divByMonic_of_monic (monic_mul_leadingCoeff_inv hq) _, mul_comm,
  div_eq_mul_inv]

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : ¬q = 0
⊢ (q * C q.leadingCoeff⁻¹).degree ≤ p.degree

Proof state:
case pos
R : Type u
inst✝ : Field R
p q : R[X]
hpq : q.degree ≤ p.degree
hq : q = 0
⊢ (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff

Tactic:
simp [hq]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma restrictSubtype_dual : (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E

Proof state:
α : Type u_1
M : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn, Subset.rfl]⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ SurjOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
simp [SurjOn, Subset.rfl]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ MapsTo Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E

Tactic:
simp [MapsTo]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E

Tactic:
rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
  ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]

Result:
α : Type u_1
M : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem IsRegular.ord_pos {c : Cardinal} (H : c.IsRegular) : 0 < c.ord

Proof state:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c

Tactic:
exact H.pos

Result:
no goals

Proof state:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c.ord

Tactic:
rw [Cardinal.lt_ord, card_zero]

Result:
c : Cardinal.{u_1}
H : c.IsRegular
⊢ 0 < c
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma lintegral_condKernel (hf : Measurable f) :
    ∫⁻ b, ∫⁻ ω, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst = ∫⁻ x, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [lintegral_compProd hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_congr {as bs : Array α} (h₀ : as = bs) {f g : α → β → β} (h₁ : f = g)
     {a b : β} (h₂ : a = b) {start start' stop stop' : Nat} (h₃ : start = start') (h₄ : stop = stop') :
    as.foldr f a start stop = bs.foldr g b start' stop'

Proof state:
α : Type u_1
β : Type u_2
as bs : Array α
h₀ : as = bs
f g : α → β → β
h₁ : f = g
a b : β
h₂ : a = b
start start' stop stop' : Nat
h₃ : start = start'
h₄ : stop = stop'
⊢ foldr f a as start stop = foldr g b bs start' stop'

Tactic:
congr

Result:
no goals