harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Abelian/RightDerived.lean
@[reassoc]
lemma InjectiveResolution.isoRightDerivedObj_hom_naturality
    {X Y : C} (f : X ⟶ Y) (I : InjectiveResolution X) (J : InjectiveResolution Y)
    (φ : I.cocomplex ⟶ J.cocomplex) (comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0)
    (F : C ⥤ D) [F.Additive] (n : ℕ) :
    (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
      (I.isoRightDerivedObj F n).hom ≫
        (F.mapHomologicalComplex _ ⋙ HomologicalComplex.homologyFunctor _ _ n).map φ

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (F.rightDerived n).map f ≫ (J.isoRightDerivedObj F n).hom =
    (I.isoRightDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.up ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map φ

Tactic:
dsimp [isoRightDerivedObj, Functor.rightDerived]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{u_2, u_1} D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
I : InjectiveResolution X
J : InjectiveResolution Y
φ : I.cocomplex ⟶ J.cocomplex
comm : I.ι.f 0 ≫ φ.f 0 = f ≫ J.ι.f 0
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (F.rightDerivedToHomotopyCategory.map f) ≫
      (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (J.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n).map (I.isoRightDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)) ≫
      HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_antiperiodic : Function.Antiperiodic sign (π : Angle) := fun θ => by
  rw [sign, sign, sin_add_pi, Left.sign_neg]

Proof state:
θ : Angle
⊢ (θ + ↑π).sign = -θ.sign

Tactic:
rw [sign, sign, sin_add_pi, Left.sign_neg]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem sInf_apply' {m : Set (OuterMeasure α)} {s : Set α} (h : s.Nonempty) :
    sInf m s =
      ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' n, ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ (t n) :=
  m.eq_empty_or_nonempty.elim (fun hm => by simp [hm, h]) sInf_apply

Proof state:
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : s.Nonempty
hm : m = ∅
⊢ (sInf m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)

Tactic:
simp [hm, h]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem Algebra.restrictScalars_adjoin (F : Type*) [CommSemiring F] {E : Type*} [CommSemiring E]
    [Algebra F E] (K : Subalgebra F E) (S : Set E) :
    (Algebra.adjoin K S).restrictScalars F = Algebra.adjoin F (K ∪ S)

Proof state:
F : Type u_4
inst✝² : CommSemiring F
E : Type u_5
inst✝¹ : CommSemiring E
inst✝ : Algebra F E
K : Subalgebra F E
S : Set E
⊢ Subalgebra.restrictScalars F (adjoin (↥K) S) = adjoin F (↑K ∪ S)

Tactic:
conv_lhs => rw [← Algebra.adjoin_eq K, ← Algebra.adjoin_union_eq_adjoin_adjoin]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem injOn_preimage (h : Semiconj f fa fb) {s : Set β} (hb : InjOn fb s)
    (hf : InjOn f (f ⁻¹' s)) : InjOn fa (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
⊢ InjOn fa (f ⁻¹' s)

Tactic:
intro x hx y hy H

Result:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ x = y

Tactic:
rw [h.eq, h.eq] at this

Result:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
⊢ x = y

Tactic:
have := congr_arg f H

Result:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : fb (f x) = fb (f y)
⊢ x = y

Tactic:
exact hf hx hy (hb hx hy this)

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_finset_sum {ι : Type*} {s : Finset ι}
    [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃)
    (f : ι → M₁ →SL[σ₁₂] M₂) : g.comp (∑ i ∈ s, f i) = ∑ i ∈ s, g.comp (f i)

Proof state:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
⊢ g.comp (∑ i ∈ s, f i) = ∑ i ∈ s, g.comp (f i)

Tactic:
ext

Result:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g.comp (∑ i ∈ s, f i)) x✝ = (∑ i ∈ s, g.comp (f i)) x✝

Proof state:
case h
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g.comp (∑ i ∈ s, f i)) x✝ = (∑ i ∈ s, g.comp (f i)) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_diff_Ico_same (h : a ≤ b) : Icc a b \ Ico a b = {b}

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}

Tactic:
rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_Icc_iff_integrableOn_Ioc :
    IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioc a b) μ :=
  integrableOn_Icc_iff_integrableOn_Ioc' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ μ {a} ≠ ⊤

Tactic:
rw [measure_singleton]

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : PartialOrder α
inst✝¹ : MeasurableSingletonClass α
f : α → E
μ : Measure α
a b : α
inst✝ : NoAtoms μ
⊢ 0 ≠ ⊤

Tactic:
exact ENNReal.zero_ne_top

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_add : (s.bind fun a => f a + g a) = s.bind f + s.bind g

Proof state:
α : Type u_1
β : Type v
s : Multiset α
f g : α → Multiset β
⊢ (s.bind fun a => f a + g a) = s.bind f + s.bind g

Tactic:
simp [bind, join]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n) :
    {p ∈ n.primeFactors | p ∣ m} = m.primeFactors

Proof state:
m n : ℕ
hn : n ≠ 0
hmn : m ∣ n
⊢ filter (fun p => p ∣ m) n.primeFactors = m.primeFactors

Tactic:
simp_rw [primeFactors_eq_to_filter_divisors_prime, filter_comm,
  divisors_filter_dvd_of_dvd hn hmn]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
/-- The slit plane includes the open unit ball of radius `1` around `1`. -/
lemma ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ slitPlane := fun z hz ↦ .inl <|
  have : -1 < z.re - 1 := neg_lt_of_abs_lt <| (abs_re_le_norm _).trans_lt hz
  by linarith

Proof state:
z : ℂ
hz : z ∈ Metric.ball 1 1
this : -1 < z.re - 1
⊢ 0 < z.re

Tactic:
linarith

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_alls {φ : L.BoundedFormula α n} {v : α → M} :
    φ.alls.Realize v ↔ ∀ xs : Fin n → M, φ.Realize v xs

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
φ : L.BoundedFormula α n
v : α → M
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs

Tactic:
induction' n with n ih

Result:
case zero
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs

case succ
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Proof state:
case zero
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n : ℕ
v : α → M
φ : L.BoundedFormula α 0
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin 0 → M), φ.Realize v xs

Tactic:
exact Unique.forall_iff.symm

Result:
no goals

Proof state:
case succ
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ φ.alls.Realize v ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
simp only [alls, ih, Realize]

Result:
case succ
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc xs x)) ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Proof state:
case succ
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
n✝ : ℕ
v : α → M
n : ℕ
ih : ∀ {φ : L.BoundedFormula α n}, φ.alls.Realize v ↔ ∀ (xs : Fin n → M), φ.Realize v xs
φ : L.BoundedFormula α (n + 1)
⊢ (∀ (xs : Fin n → M) (x : M), φ.Realize v (snoc xs x)) ↔ ∀ (xs : Fin (n + 1) → M), φ.Realize v xs

Tactic:
exact ⟨fun h xs => Fin.snoc_init_self xs ▸ h _ _, fun h xs x => h (Fin.snoc xs x)⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.iff_iff_not_or_and_or_not [Decidable a] [Decidable b] :
    (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → b) ∧ (b → a) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

Tactic:
simp only [imp_iff_not_or, Or.comm]

Result:
no goals

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)

Tactic:
rw [iff_iff_implies_and_implies (a := a) (b := b)]

Result:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (a → b) ∧ (b → a) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
-- Mathlib/Data/Sum/Basic.lean
theorem isSome_getRight?_iff_isRight : x.getRight?.isSome ↔ x.isRight

Proof state:
α : Type u
β : Type v
x : α ⊕ β
⊢ x.getRight?.isSome = true ↔ x.isRight = true

Tactic:
rw [isRight_iff, Option.isSome_iff_exists]

Result:
α : Type u
β : Type v
x : α ⊕ β
⊢ (∃ a, x.getRight? = some a) ↔ ∃ y, x = inr y

Proof state:
α : Type u
β : Type v
x : α ⊕ β
⊢ (∃ a, x.getRight? = some a) ↔ ∃ y, x = inr y

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem exists_pow_neg_lt_rat {ε : ℚ} (hε : 0 < ε) : ∃ k : ℕ, (p : ℚ) ^ (-(k : ℤ)) < ε

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ↑p = ↑↑p

Tactic:
simp

Result:
no goals

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ↑p ^ (-↑k) < ε

Tactic:
rw [show (p : ℝ) = (p : ℚ) by simp] at hk

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑↑p ^ (-↑k) < ↑ε
⊢ ↑p ^ (-↑k) < ε

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ∃ k, ↑p ^ (-↑k) < ε

Tactic:
use k

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ↑p ^ (-↑k) < ε

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑↑p ^ (-↑k) < ↑ε
⊢ ↑p ^ (-↑k) < ε

Tactic:
exact mod_cast hk

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
⊢ ∃ k, ↑p ^ (-↑k) < ε

Tactic:
obtain ⟨k, hk⟩ := @exists_pow_neg_lt p _ ε (mod_cast hε)

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
ε : ℚ
hε : 0 < ε
k : ℕ
hk : ↑p ^ (-↑k) < ↑ε
⊢ ∃ k, ↑p ^ (-↑k) < ε
-- Mathlib/RingTheory/KrullDimension/Basic.lean
lemma Ring.KrullDimLE.mk₁ (H : ∀ I : Ideal R, I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal) :
    Ring.KrullDimLE 1 R

Proof state:
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
⊢ KrullDimLE 1 R

Tactic:
rwa [Ring.krullDimLE_one_iff]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_sub (f g : R[X]) (N : ℕ) : reflect N (f - g) = reflect N f - reflect N g

Proof state:
R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f - g) = reflect N f - reflect N g

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
/-- A transfinite composition of isomorphisms is an isomorphism. -/
lemma isIso : IsIso f

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (isomorphisms C).TransfiniteCompositionOfShape J f
⊢ IsIso (h.isoBot.inv ≫ h.incl.app ⊥)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (isomorphisms C).TransfiniteCompositionOfShape J f
⊢ IsIso f

Tactic:
rw [← h.fac]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type w
inst✝³ : LinearOrder J
inst✝² : SuccOrder J
inst✝¹ : OrderBot J
inst✝ : WellFoundedLT J
X Y : C
f : X ⟶ Y
h : (isomorphisms C).TransfiniteCompositionOfShape J f
⊢ IsIso (h.isoBot.inv ≫ h.incl.app ⊥)
-- Mathlib/Algebra/Homology/Additive.lean
theorem NatTrans.mapHomologicalComplex_comp (c : ComplexShape ι) {F G H : W₁ ⥤ W₂}
    [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms]
    (α : F ⟶ G) (β : G ⟶ H) :
    NatTrans.mapHomologicalComplex (α ≫ β) c =
      NatTrans.mapHomologicalComplex α c ≫ NatTrans.mapHomologicalComplex β c

Proof state:
ι : Type u_1
W₁ : Type u_3
W₂ : Type u_4
inst✝⁶ : Category.{u_5, u_3} W₁
inst✝⁵ : Category.{u_6, u_4} W₂
inst✝⁴ : HasZeroMorphisms W₁
inst✝³ : HasZeroMorphisms W₂
c : ComplexShape ι
F G H : W₁ ⥤ W₂
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : H.PreservesZeroMorphisms
α : F ⟶ G
β : G ⟶ H
⊢ mapHomologicalComplex (α ≫ β) c = mapHomologicalComplex α c ≫ mapHomologicalComplex β c

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_union_inter_subset_union :
    image₂ f (s ∪ s') (t ∩ t') ⊆ image₂ f s t ∪ image₂ f s' t' :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_union_inter_subset_union

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ image2 f (↑s ∪ ↑s') (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∪ image2 f ↑s' ↑t'

Tactic:
exact Set.image2_union_inter_subset_union

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ ↑(image₂ f (s ∪ s') (t ∩ t')) ⊆ ↑(image₂ f s t ∪ image₂ f s' t')

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝² : DecidableEq γ
f : α → β → γ
s s' : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ image2 f (↑s ∪ ↑s') (↑t ∩ ↑t') ⊆ image2 f ↑s ↑t ∪ image2 f ↑s' ↑t'
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_b₈ : (W.map φ).b₈ = φ W.b₈

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).b₈ = φ W.b₈

Tactic:
simp only [b₈, map_a₁, map_a₂, map_a₃, map_a₄, map_a₆]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.a₁ ^ 2 * φ W.a₆ + 4 * φ W.a₂ * φ W.a₆ - φ W.a₁ * φ W.a₃ * φ W.a₄ + φ W.a₂ * φ W.a₃ ^ 2 - φ W.a₄ ^ 2 =
    φ (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ φ W.a₁ ^ 2 * φ W.a₆ + 4 * φ W.a₂ * φ W.a₆ - φ W.a₁ * φ W.a₃ * φ W.a₄ + φ W.a₂ * φ W.a₃ ^ 2 - φ W.a₄ ^ 2 =
    φ (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2)

Tactic:
map_simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.fromSubtype_toSubtype :
    biproduct.fromSubtype f p ≫ biproduct.toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
⊢ fromSubtype f p ≫ toSubtype f p = 𝟙 (⨁ Subtype.restrict p f)

Tactic:
refine biproduct.hom_ext _ _ fun j => ?_

Result:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ (fromSubtype f p ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j =
    𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ (fromSubtype f p ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j =
    𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j

Tactic:
rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Ultra/Basic.lean
lemma mem_ball_iff {x y : X} {r : ℝ} : y ∈ ball x r ↔ x ∈ ball y r

Proof state:
case inl
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
hr : 0 < r
⊢ y ∈ ball x r ↔ x ∈ ball y r

Tactic:
constructor <;> intro h <;>
rw [← ball_eq_of_mem h] <;>
simp [hr]

Result:
no goals

Proof state:
case inr
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
hr : r ≤ 0
⊢ y ∈ ball x r ↔ x ∈ ball y r

Tactic:
simp [ball_eq_empty.mpr hr]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
inst✝ : IsUltrametricDist X
x y : X
r : ℝ
⊢ y ∈ ball x r ↔ x ∈ ball y r

Tactic:
cases lt_or_le 0 r with
| inl hr =>
  constructor <;> intro h <;>
  rw [← ball_eq_of_mem h] <;>
  simp [hr]
| inr hr => simp [ball_eq_empty.mpr hr]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_mul_le_div_mul_of_div_le_div (h : a / b ≤ c / d) (he : 0 ≤ e) :
    a / (b * e) ≤ c / (d * e)

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b c d e : α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / d * (1 / e)

Tactic:
exact mul_le_mul_of_nonneg_right h (one_div_nonneg.2 he)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b c d e : α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / (b * e) ≤ c / (d * e)

Tactic:
rw [div_mul_eq_div_mul_one_div, div_mul_eq_div_mul_one_div]

Result:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b c d e : α
h : a / b ≤ c / d
he : 0 ≤ e
⊢ a / b * (1 / e) ≤ c / d * (1 / e)
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
@[simp]
protected lemma smul_neg (s : Finset α) (t : Finset β) : s • -t = -(s • t)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • image (fun x => -x) t = image (fun x => -x) (s • t)

Tactic:
exact image_image₂_right_comm smul_neg

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • -t = -(s • t)

Tactic:
simp_rw [← image_neg_eq_neg]

Result:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
s : Finset α
t : Finset β
⊢ s • image (fun x => -x) t = image (fun x => -x) (s • t)
-- Mathlib/Data/Real/EReal.lean
lemma mul_neg_iff {a b : EReal} : a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Proof state:
a b : EReal
⊢ a * b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
nth_rw 1 [← neg_zero]

Result:
a b : EReal
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Proof state:
a b : EReal
⊢ a * b < -0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

Tactic:
rw [lt_neg_comm, ← mul_neg a, mul_pos_iff, neg_lt_comm, lt_neg_comm, neg_zero]

Result:
no goals