harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GeomSum.lean
theorem op_geom_sum₂ (x y : α) (n : ℕ) : ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i =
    ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)

Tactic:
rw [mem_range, Nat.lt_iff_add_one_le] at j_in

Result:
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)

Tactic:
refine sum_congr rfl fun j j_in => ?_

Result:
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j ∈ range n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)

Proof state:
case e_a.e_a.h
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ j ≤ n - 1

Tactic:
exact le_tsub_of_add_le_right j_in

Result:
no goals

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)

Tactic:
rw [← sum_range_reflect]

Result:
α : Type u
inst✝ : Semiring α
x y : α
n : ℕ
⊢ ∑ j ∈ range n, op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i)

Proof state:
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ n - 1 - (n - 1 - j) = j

Tactic:
apply tsub_tsub_cancel_of_le

Result:
case e_a.e_a.h
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ j ≤ n - 1

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ op y ^ (n - 1 - (n - 1 - j)) * op x ^ (n - 1 - j) = op y ^ j * op x ^ (n - 1 - j)

Tactic:
congr

Result:
case e_a.e_a
α : Type u
inst✝ : Semiring α
x y : α
n j : ℕ
j_in : j + 1 ≤ n
⊢ n - 1 - (n - 1 - j) = j
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_norm [NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedRing E
inst✝¹ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
inst✝ : NormOneClass E
⊢ ‖ofScalars E c n‖ = ‖c n‖

Tactic:
simp [ofScalars_norm_eq_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast?_flatten {L : List (List α)} :
    (flatten L).getLast? = L.reverse.findSome? fun l => l.getLast?

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten.getLast? = findSome? (fun l => l.getLast?) L.reverse

Tactic:
simp [← flatMap_id, getLast?_flatMap]

Result:
no goals
-- Mathlib/GroupTheory/Solvable.lean
theorem derivedSeries_normal (n : ℕ) : (derivedSeries G n).Normal

Proof state:
case succ
G : Type u_1
inst✝ : Group G
n : ℕ
ih : (derivedSeries G n).Normal
⊢ (derivedSeries G (n + 1)).Normal

Tactic:
exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Result:
no goals

Proof state:
case zero
G : Type u_1
inst✝ : Group G
⊢ (derivedSeries G 0).Normal

Tactic:
exact (⊤ : Subgroup G).normal_of_characteristic

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
n : ℕ
⊢ (derivedSeries G n).Normal

Tactic:
induction n with
| zero => exact (⊤ : Subgroup G).normal_of_characteristic
| succ n ih => exact Subgroup.commutator_normal (derivedSeries G n) (derivedSeries G n)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
lemma ker_Pi_Quotient_mk {ι : Type*} (I : ι → Ideal R) [∀ i, (I i).IsTwoSided] :
    ker (Pi.ringHom fun i : ι ↦ Quotient.mk (I i)) = ⨅ i, I i

Proof state:
R : Type u
inst✝¹ : Ring R
ι : Type u_1
I : ι → Ideal R
inst✝ : ∀ (i : ι), (I i).IsTwoSided
⊢ ker (Pi.ringHom fun i => Quotient.mk (I i)) = ⨅ i, I i

Tactic:
simp [Pi.ker_ringHom, mk_ker]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem compl [BooleanAlgebra α] [BooleanAlgebra β] {l : α → β} {u : β → α}
    (gc : GaloisConnection l u) :
    GaloisConnection (compl ∘ u ∘ compl) (compl ∘ l ∘ compl) := fun a b ↦ by
  dsimp
  rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

Proof state:
α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ

Tactic:
rw [le_compl_iff_le_compl, gc, compl_le_iff_compl_le]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (compl ∘ u ∘ compl) a ≤ b ↔ a ≤ (compl ∘ l ∘ compl) b

Tactic:
dsimp

Result:
α : Type u
β : Type v
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
l : α → β
u : β → α
gc : GaloisConnection l u
a : β
b : α
⊢ (u aᶜ)ᶜ ≤ b ↔ a ≤ (l bᶜ)ᶜ
-- Mathlib/Combinatorics/SimpleGraph/Partition.lean
theorem partOfVertex_mem (v : V) : P.partOfVertex v ∈ P.parts

Proof state:
case intro
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
h : Exists.choose ⋯ ∈ P.parts
⊢ P.partOfVertex v ∈ P.parts

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ P.partOfVertex v ∈ P.parts

Tactic:
obtain ⟨h, -⟩ := (P.isPartition.2 v).choose_spec.1

Result:
case intro
V : Type u
G : SimpleGraph V
P : G.Partition
v : V
h : Exists.choose ⋯ ∈ P.parts
⊢ P.partOfVertex v ∈ P.parts
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem Module.rank_le_one_iff_top_isPrincipal [Module.Free K V] :
    Module.rank K V ≤ 1 ↔ (⊤ : Submodule K V).IsPrincipal

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Free K ↥⊤
⊢ Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal

Tactic:
rw [← Submodule.rank_le_one_iff_isPrincipal, rank_top]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal

Tactic:
haveI := Module.Free.of_equiv (topEquiv (R := K) (M := V)).symm

Result:
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
this : Free K ↥⊤
⊢ Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
-- Mathlib/LinearAlgebra/Contraction.lean
theorem zero_prodMap_dualTensorHom (g : Module.Dual R N) (q : Q) :
    (0 : M →ₗ[R] P).prodMap ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
      dualTensorHom R (M × N) (P × Q) ((g ∘ₗ snd R M N) ⊗ₜ inr R P Q q)

Proof state:
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : Dual R N
q : Q
⊢ prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) =
    (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q)

Tactic:
ext <;>
  simp only [coe_comp, coe_inr, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
    snd_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Additive.lean
lemma left_adjoint_additive [G.Additive] : F.Additive where
  map_add {X Y} f g := (adj.homEquiv _ _).injective (by simp [homEquiv_unit])

Proof state:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.Additive
X Y : C
f g : X ⟶ Y
⊢ (adj.homEquiv X (F.obj Y)) (F.map (f + g)) = (adj.homEquiv X (F.obj Y)) (F.map f + F.map g)

Tactic:
simp [homEquiv_unit]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma preNormEDS'_even (m : ℕ) : preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ 2 * (m + 3) = 2 * m + 1 + 5

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (m + 1 / 2 + 2) ^ 2 * preNormEDS' b c d (m + 1 / 2 + 3) * preNormEDS' b c d (m + 1 / 2 + 5) -
      preNormEDS' b c d (m + 1 / 2 + 1) * preNormEDS' b c d (m + 1 / 2 + 3) * preNormEDS' b c d (m + 1 / 2 + 4) ^ 2 =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
rw [show 2 * (m + 3) = 2 * m + 1 + 5 by rfl, preNormEDS', dif_neg m.not_even_two_mul_add_one]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (let_fun x := ⋯;
    preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Proof state:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ (let_fun x := ⋯;
    preNormEDS' b c d ((2 * m + 1) / 2 + 2) ^ 2 * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 5) -
      preNormEDS' b c d ((2 * m + 1) / 2 + 1) * preNormEDS' b c d ((2 * m + 1) / 2 + 3) *
        preNormEDS' b c d ((2 * m + 1) / 2 + 4) ^ 2) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2

Tactic:
simp only [Nat.mul_add_div two_pos]

Result:
R : Type u
inst✝ : CommRing R
b c d : R
m : ℕ
⊢ preNormEDS' b c d (m + 1 / 2 + 2) ^ 2 * preNormEDS' b c d (m + 1 / 2 + 3) * preNormEDS' b c d (m + 1 / 2 + 5) -
      preNormEDS' b c d (m + 1 / 2 + 1) * preNormEDS' b c d (m + 1 / 2 + 3) * preNormEDS' b c d (m + 1 / 2 + 4) ^ 2 =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNormEssSup_piecewise (f g : α → ε) [DecidablePred (· ∈ s)] (hs : MeasurableSet s) :
    eLpNormEssSup (Set.piecewise s f g) μ
      = max (eLpNormEssSup f (μ.restrict s)) (eLpNormEssSup g (μ.restrict sᶜ))

Proof state:
case e_f.h
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
x : α
⊢ ‖s.piecewise f g x‖ₑ = s.piecewise (fun x => ‖f x‖ₑ) (fun x => ‖g x‖ₑ) x

Tactic:
by_cases hx : x ∈ s <;> simp [hx]

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ eLpNormEssSup (s.piecewise f g) μ = eLpNormEssSup f (μ.restrict s) ⊔ eLpNormEssSup g (μ.restrict sᶜ)

Tactic:
simp only [eLpNormEssSup, ← ENNReal.essSup_piecewise hs]

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ essSup (fun x => ‖s.piecewise f g x‖ₑ) μ = essSup (s.piecewise (fun x => ‖f x‖ₑ) fun x => ‖g x‖ₑ) μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
⊢ essSup (fun x => ‖s.piecewise f g x‖ₑ) μ = essSup (s.piecewise (fun x => ‖f x‖ₑ) fun x => ‖g x‖ₑ) μ

Tactic:
congr with x

Result:
case e_f.h
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝¹ : ENorm ε
s : Set α
f g : α → ε
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
x : α
⊢ ‖s.piecewise f g x‖ₑ = s.piecewise (fun x => ‖f x‖ₑ) (fun x => ‖g x‖ₑ) x
-- Mathlib/Order/UpperLower/Basic.lean
lemma Fibration.isLowerSet_image [LE α] [LE β] (hf : Fibration (· ≤ ·) (· ≤ ·) f)
    {s : Set α} (hs : IsLowerSet s) : IsLowerSet (f '' s)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s

Tactic:
exact ⟨_, hs e' hx, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
⊢ IsLowerSet (f '' s)

Tactic:
rintro _ y' e ⟨x, hx, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
⊢ y' ∈ f '' s

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
⊢ y' ∈ f '' s

Tactic:
obtain ⟨y, e', rfl⟩ := hf e

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LE α
inst✝ : LE β
hf : Fibration (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem continuousAt_const_rpow {a b : ℝ} (h : a ≠ 0) : ContinuousAt (a ^ ·) b

Proof state:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b

Tactic:
refine Complex.continuous_re.continuousAt.comp ?_

Result:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b

Proof state:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x => ↑a ^ ↑x) b

Tactic:
refine (continuousAt_const_cpow ?_).comp Complex.continuous_ofReal.continuousAt

Result:
a b : ℝ
h : a ≠ 0
⊢ ↑a ≠ 0

Proof state:
a b : ℝ
h : a ≠ 0
⊢ ↑a ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x => a ^ x) b

Tactic:
simp only [rpow_def]

Result:
a b : ℝ
h : a ≠ 0
⊢ ContinuousAt (fun x => (↑a ^ ↑x).re) b
-- Mathlib/Topology/ContinuousMap/ZeroAtInfty.lean
theorem isometry_toBCF : Isometry (toBCF : C₀(α, β) → α →ᵇ β)

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : Zero β
⊢ Isometry toBCF

Tactic:
tauto

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Circulant.lean
theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v

Proof state:
u v : Fin 1
⊢ ¬⊥.Adj u v

Tactic:
exact id

Result:
no goals

Proof state:
u v : Fin 1
⊢ ¬(cycleGraph 1).Adj u v

Tactic:
rw [cycleGraph_one_eq_bot]

Result:
u v : Fin 1
⊢ ¬⊥.Adj u v
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem zeroLocus_subset_zeroLocus_iff (I J : Ideal R) :
    zeroLocus (I : Set R) ⊆ zeroLocus (J : Set R) ↔ J ≤ I.radical

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑J ↔ J ≤ I.radical

Tactic:
rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/CocompactMap.lean
theorem isCompact_preimage_of_isClosed (f : CocompactMap α β)
    ⦃s : Set β⦄ (hs : IsCompact s) (h's : IsClosed s) :
    IsCompact (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
t : Set α
ht : IsCompact t
hts : (⇑f ⁻¹' s)ᶜᶜ ⊆ t
⊢ ⇑f ⁻¹' s ⊆ t

Tactic:
simpa using hts

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
⊢ ?m.8444 ∈ cocompact ?m.8418

Tactic:
simpa only [preimage_image_preimage, preimage_compl] using
  mem_map.mp
    (cocompact_tendsto f <|
      mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩)

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
t : Set α
ht : IsCompact t
hts : (⇑f ⁻¹' s)ᶜᶜ ⊆ t
⊢ IsCompact (⇑f ⁻¹' s)

Tactic:
exact
  ht.of_isClosed_subset (h's.preimage <| map_continuous f) (by simpa using hts)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
⊢ IsCompact (⇑f ⁻¹' s)

Tactic:
obtain ⟨t, ht, hts⟩ :=
  mem_cocompact'.mp
    (by
      simpa only [preimage_image_preimage, preimage_compl] using
        mem_map.mp
          (cocompact_tendsto f <|
            mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
t : Set α
ht : IsCompact t
hts : (⇑f ⁻¹' s)ᶜᶜ ⊆ t
⊢ IsCompact (⇑f ⁻¹' s)
-- Mathlib/Topology/Sheaves/LocalPredicate.lean
theorem stalkToFiber_surjective (P : LocalPredicate T) (x : X)
    (w : ∀ t : T x, ∃ (U : OpenNhds x) (f : ∀ y : U.1, T y) (_ : P.pred f), f ⟨x, U.2⟩ = t) :
    Function.Surjective (stalkToFiber P x) := fun t => by
  rcases w t with ⟨U, f, h, rfl⟩
  fconstructor
  · exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩
  · exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩

Proof state:
case intro.intro.intro.w
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥U.obj) → T ↑y
h : P.pred f
⊢ (subsheafToTypes P).presheaf.stalk x

Tactic:
exact (subsheafToTypes P).presheaf.germ _ x U.2 ⟨f, h⟩

Result:
no goals

Proof state:
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
t : T x
⊢ ∃ a, stalkToFiber P x a = t

Tactic:
rcases w t with ⟨U, f, h, rfl⟩

Result:
case intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥U.obj) → T ↑y
h : P.pred f
⊢ ∃ a, stalkToFiber P x a = f ⟨x, ⋯⟩

Proof state:
case intro.intro.intro.h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥U.obj) → T ↑y
h : P.pred f
⊢ stalkToFiber P x ((subsheafToTypes P).presheaf.germ U.obj x ⋯ ⟨f, h⟩) = f ⟨x, ⋯⟩

Tactic:
exact stalkToFiber_germ P U.1 x U.2 ⟨f, h⟩

Result:
no goals

Proof state:
case intro.intro.intro
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥U.obj) → T ↑y
h : P.pred f
⊢ ∃ a, stalkToFiber P x a = f ⟨x, ⋯⟩

Tactic:
fconstructor

Result:
case intro.intro.intro.w
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥U.obj) → T ↑y
h : P.pred f
⊢ (subsheafToTypes P).presheaf.stalk x

case intro.intro.intro.h
X : TopCat
T : ↑X → Type v
P : LocalPredicate T
x : ↑X
w : ∀ (t : T x), ∃ U f, ∃ (_ : P.pred f), f ⟨x, ⋯⟩ = t
U : OpenNhds x
f : (y : ↥U.obj) → T ↑y
h : P.pred f
⊢ stalkToFiber P x ?intro.intro.intro.w = f ⟨x, ⋯⟩
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_roots (hp0 : p ≠ 0) : (Multiset.card (roots p) : WithBot ℕ) ≤ degree p

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(Classical.choose ⋯).card ≤ p.degree

Tactic:
exact (Classical.choose_spec (exists_multiset_roots hp0)).1

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑p.roots.card ≤ p.degree

Tactic:
classical
unfold roots
rw [dif_neg hp0]
exact (Classical.choose_spec (exists_multiset_roots hp0)).1

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑p.roots.card ≤ p.degree

Tactic:
unfold roots

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(if h : p = 0 then ∅ else Classical.choose ⋯).card ≤ p.degree

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(if h : p = 0 then ∅ else Classical.choose ⋯).card ≤ p.degree

Tactic:
rw [dif_neg hp0]

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp0 : p ≠ 0
⊢ ↑(Classical.choose ⋯).card ≤ p.degree
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem signBijAux_surj {n : ℕ} {f : Perm (Fin n)} :
    ∀ a ∈ finPairsLT n, ∃ b ∈ finPairsLT n, signBijAux f b = a :=
  fun ⟨a₁, a₂⟩ ha =>
    if hxa : f⁻¹ a₂ < f⁻¹ a₁ then
      ⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_finPairsLT.2 hxa, by
        dsimp [signBijAux]
        rw [apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 ha)]⟩
    else
      ⟨⟨f⁻¹ a₂, f⁻¹ a₁⟩,
        mem_finPairsLT.2 <|
          (le_of_not_gt hxa).lt_of_ne fun h => by
            simp [mem_finPairsLT, f⁻¹.injective h, lt_irrefl] at ha, by
              dsimp [signBijAux]
              rw [apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 ha).le.not_lt]⟩

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : f⁻¹ a₂ < f⁻¹ a₁
⊢ (if f (f⁻¹ a₂) < f (f⁻¹ a₁) then ⟨f (f⁻¹ a₁), f (f⁻¹ a₂)⟩ else ⟨f (f⁻¹ a₂), f (f⁻¹ a₁)⟩) = ⟨a₁, a₂⟩

Tactic:
rw [apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 ha)]

Result:
no goals

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : f⁻¹ a₂ < f⁻¹ a₁
⊢ f.signBijAux ⟨f⁻¹ a₁, f⁻¹ a₂⟩ = ⟨a₁, a₂⟩

Tactic:
dsimp [signBijAux]

Result:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : f⁻¹ a₂ < f⁻¹ a₁
⊢ (if f (f⁻¹ a₂) < f (f⁻¹ a₁) then ⟨f (f⁻¹ a₁), f (f⁻¹ a₂)⟩ else ⟨f (f⁻¹ a₂), f (f⁻¹ a₁)⟩) = ⟨a₁, a₂⟩

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬f⁻¹ a₂ < f⁻¹ a₁
h : f⁻¹ a₁ = f⁻¹ a₂
⊢ False

Tactic:
simp [mem_finPairsLT, f⁻¹.injective h, lt_irrefl] at ha

Result:
no goals

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬f⁻¹ a₂ < f⁻¹ a₁
⊢ (if f (f⁻¹ a₁) < f (f⁻¹ a₂) then ⟨f (f⁻¹ a₂), f (f⁻¹ a₁)⟩ else ⟨f (f⁻¹ a₁), f (f⁻¹ a₂)⟩) = ⟨a₁, a₂⟩

Tactic:
rw [apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 ha).le.not_lt]

Result:
no goals

Proof state:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬f⁻¹ a₂ < f⁻¹ a₁
⊢ f.signBijAux ⟨f⁻¹ a₂, f⁻¹ a₁⟩ = ⟨a₁, a₂⟩

Tactic:
dsimp [signBijAux]

Result:
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : ⟨a₁, a₂⟩ ∈ finPairsLT n
hxa : ¬f⁻¹ a₂ < f⁻¹ a₁
⊢ (if f (f⁻¹ a₁) < f (f⁻¹ a₂) then ⟨f (f⁻¹ a₂), f (f⁻¹ a₁)⟩ else ⟨f (f⁻¹ a₁), f (f⁻¹ a₂)⟩) = ⟨a₁, a₂⟩
-- Mathlib/CategoryTheory/Abelian/Injective/Resolution.lean
theorem desc_commutes {Y Z : C} (f : Z ⟶ Y) (I : InjectiveResolution Y)
    (J : InjectiveResolution Z) : J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι

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
⊢ J.ι ≫ desc f I J = (CochainComplex.single₀ C).map f ≫ I.ι

Tactic:
ext

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

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

Tactic:
simp [desc, descFOne, descFZero]

Result:
no goals