harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertList [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (distinct_both : ∀ (a : α), containsKey a l → (toInsert.map Sigma.fst).contains a = false) :
    (insertList l toInsert).length = l.length + toInsert.length

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
distinct_both : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false
⊢ (insertList l toInsert).length = l.length + toInsert.length

Tactic:
simpa using (perm_insertList distinct_l distinct_toInsert distinct_both).length_eq

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem stabilizer_eq_normalizer (P : Sylow p G) :
    stabilizer G P = P.normalizer

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
⊢ stabilizer G P = (↑P).normalizer

Tactic:
ext

Result:
case h
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
x✝ : G
⊢ x✝ ∈ stabilizer G P ↔ x✝ ∈ (↑P).normalizer

Proof state:
case h
p : ℕ
G : Type u_1
inst✝ : Group G
P : Sylow p G
x✝ : G
⊢ x✝ ∈ stabilizer G P ↔ x✝ ∈ (↑P).normalizer

Tactic:
simp [smul_eq_iff_mem_normalizer]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem tendsto_Iio_atTop {f : β → Iio a} :
    Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] a)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : β → ↑(Iio a)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[<] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : β → ↑(Iio a)
⊢ Tendsto f l atTop ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] a)

Tactic:
rw [← comap_coe_Iio_nhdsLT, tendsto_comap_iff]

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
l : Filter β
f : β → ↑(Iio a)
⊢ Tendsto (Subtype.val ∘ f) l (𝓝[<] a) ↔ Tendsto (fun x => ↑(f x)) l (𝓝[<] a)
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem single_pow [Monoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (a ^ n) (b ^ n)
  | 0 => by
    simp only [pow_zero]
    rfl
  | n + 1 => by simp only [pow_succ, single_pow n, single_mul_single]

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
a : G
b : k
n : ℕ
⊢ single a b ^ (n + 1) = single (a ^ (n + 1)) (b ^ (n + 1))

Tactic:
simp only [pow_succ, single_pow n, single_mul_single]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
a : G
b : k
⊢ 1 = single 1 1

Tactic:
rfl

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
a : G
b : k
⊢ single a b ^ 0 = single (a ^ 0) (b ^ 0)

Tactic:
simp only [pow_zero]

Result:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
a : G
b : k
⊢ 1 = single 1 1
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudoEqual_refl {P : C} : Reflexive (PseudoEqual P) :=
  fun f => ⟨f.1, 𝟙 f.1, 𝟙 f.1, inferInstance, inferInstance, by simp⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : C
f : Over P
⊢ 𝟙 f.left ≫ f.hom = 𝟙 f.left ≫ f.hom

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.finrank_pi {ι : Type v} [Fintype ι] :
    finrank R (ι → R) = Fintype.card ι

Proof state:
R : Type u
inst✝² : Semiring R
inst✝¹ : StrongRankCondition R
ι : Type v
inst✝ : Fintype ι
⊢ finrank R (ι → R) = Fintype.card ι

Tactic:
simp [finrank]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive (attr := simp)]
lemma lipschitzWith_inv_iff : LipschitzWith K f⁻¹ ↔ LipschitzWith K f

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
K : ℝ≥0
f : α → E
⊢ LipschitzWith K f⁻¹ ↔ LipschitzWith K f

Tactic:
simp [LipschitzWith]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Pairwise.lean
theorem pairwise_singleton (R : α → α → Prop) (a) : #[a].Pairwise R

Proof state:
α : Type u_1
R : α → α → Prop
a : α
⊢ List.Pairwise R #[a].toList

Tactic:
exact List.pairwise_singleton ..

Result:
no goals

Proof state:
α : Type u_1
R : α → α → Prop
a : α
⊢ Pairwise R #[a]

Tactic:
unfold Pairwise

Result:
α : Type u_1
R : α → α → Prop
a : α
⊢ List.Pairwise R #[a].toList
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem HasFDerivAt.rpow (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) (h : 0 < f x) :
    HasFDerivAt (fun x => f x ^ g x)
      ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h : 0 < f x
⊢ HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x

Tactic:
exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp x (hf.prod hg)

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem countP_eq_countP_filter_add (s) (p q : α → Prop) [DecidablePred p] [DecidablePred q] :
    countP p s = (filter q s).countP p + (filter (fun a => ¬q a) s).countP p :=
  Quot.inductionOn s fun l => by
    convert l.countP_eq_countP_filter_add (p ·) (q ·)
    simp [countP_filter]

Proof state:
case h.e'_3.h.e'_6
α : Type u_1
s : Multiset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
l : List α
⊢ countP p (filter (fun a => ¬q a) (Quot.mk (⇑(isSetoid α)) l)) =
    List.countP (fun x => decide (p x)) (List.filter (fun a => !decide (q a)) l)

Tactic:
simp [countP_filter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α} :
    k ∈ m.insertMany l ↔ k ∈ m ∨ (l.map Sigma.fst).contains k

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
⊢ k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Sigma.fst l).contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_insert_right : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t :=
  disjoint_comm.trans <| by rw [disjoint_insert_left, _root_.disjoint_comm]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ Disjoint (insert a t) s ↔ a ∉ s ∧ Disjoint s t

Tactic:
rw [disjoint_insert_left, _root_.disjoint_comm]

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_comapDomain (hf : Function.Injective f) (l : β →₀ M)
    (hl : ↑l.support ⊆ Set.range f) :
    mapDomain f (comapDomain f l hf.injOn) = l

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
⊢ mapDomain f (comapDomain f l ⋯) =
    mapDomain (⇑{ toFun := f, inj' := hf }) (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
⊢ mapDomain f (comapDomain f l ⋯) = l

Tactic:
conv_rhs => rw [← embDomain_comapDomain (f := ⟨f, hf⟩) hl (M := M), embDomain_eq_mapDomain]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
l : β →₀ M
hl : ↑l.support ⊆ Set.range f
⊢ mapDomain f (comapDomain f l ⋯) =
    mapDomain (⇑{ toFun := f, inj' := hf }) (comapDomain (⇑{ toFun := f, inj' := hf }) l ⋯)
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem diam_image (hf : Isometry f) (s : Set α) : Metric.diam (f '' s) = Metric.diam s

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ Metric.diam (f '' s) = Metric.diam s

Tactic:
rw [Metric.diam, Metric.diam, hf.ediam_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Impl.lean
theorem splitRevAt_eq (n : Nat) (l : List α) : splitRevAt n l = ((l.take n).reverse, l.drop n)

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ splitRevAt n l = ((take n l).reverse, drop n l)

Tactic:
rw [splitRevAt, splitRevAt_go, append_nil]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap_comap_eq_relfinrank_of_le (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A B

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h))

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FullyFaithful.lean
theorem Faithful.of_iso [F.Faithful] (α : F ≅ F') : F'.Faithful :=
  { map_injective := fun h =>
      F.map_injective (by rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]) }

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F F' : C ⥤ D
inst✝ : F.Faithful
α : F ≅ F'
X✝ Y✝ : C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F'.map a₁✝ = F'.map a₂✝
⊢ F.map a₁✝ = F.map a₂✝

Tactic:
rw [← NatIso.naturality_1 α.symm, h, NatIso.naturality_1 α.symm]

Result:
no goals
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem _root_.IsOpen.baireMeasurableSet (h : IsOpen s) : BaireMeasurableSet s

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ BaireMeasurableSet s

Tactic:
exact h.measurableSet.baireMeasurableSet

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen s
⊢ BaireMeasurableSet s

Tactic:
borelize α

Result:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ BaireMeasurableSet s
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppTensorFinsuppRid_apply_apply (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) :
    finsuppTensorFinsuppRid R M ι κ (f ⊗ₜ[R] g) (a, b) = g b • f a

Proof state:
R : Type u_1
M : Type u_3
ι : Type u_5
κ : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : ι →₀ M
g : κ →₀ R
a : ι
b : κ
⊢ ((finsuppTensorFinsuppRid R M ι κ) (f ⊗ₜ[R] g)) (a, b) = g b • f a

Tactic:
simp [finsuppTensorFinsuppRid]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive (attr := simp) mod_natCard_zsmul]
lemma zpow_mod_natCard {G} [Group G] (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n

Proof state:
G : Type u_6
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ (n % ↑(Nat.card G)) = a ^ n

Tactic:
rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
  Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem filter_ne' [DecidableEq β] (s : Finset β) (b : β) : (s.filter fun a => a ≠ b) = s.erase b :=
  _root_.trans (filter_congr fun _ _ => by simp_rw [@ne_comm _ b]) (filter_ne s b)

Proof state:
β : Type u_2
inst✝ : DecidableEq β
s : Finset β
b x✝¹ : β
x✝ : x✝¹ ∈ s
⊢ x✝¹ ≠ b ↔ b ≠ x✝¹

Tactic:
simp_rw [@ne_comm _ b]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem lt_pred_iff {j : Fin n} {i : Fin (n + 1)} (hi : i ≠ 0) : j < pred i hi ↔ succ j < i

Proof state:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j < i.pred hi ↔ j.succ < i

Tactic:
rw [← succ_lt_succ_iff, succ_pred]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/GammaDeriv.lean
lemma hasDerivAt_Gamma_nat (n : ℕ) :
    HasDerivAt Gamma (n ! * (-γ + harmonic n)) (n + 1) :=
  (deriv_Gamma_nat n).symm ▸
    (differentiableAt_Gamma fun m ↦ (by linarith : (n : ℝ) + 1 ≠ -m)).hasDerivAt

Proof state:
n m : ℕ
⊢ ↑n + 1 ≠ -↑m

Tactic:
linarith

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem prod_prod_bipartiteAbove_eq_prod_prod_bipartiteBelow
    [CommMonoid R] (f : α → β → R) [∀ a b, Decidable (r a b)] :
    ∏ a ∈ s, ∏ b ∈ t.bipartiteAbove r a, f a b = ∏ b ∈ t, ∏ a ∈ s.bipartiteBelow r b, f a b

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : CommMonoid R
f : α → β → R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ ∏ a ∈ s, ∏ b ∈ bipartiteAbove r t a, f a b = ∏ b ∈ t, ∏ a ∈ bipartiteBelow r s b, f a b

Tactic:
simp_rw [bipartiteAbove, bipartiteBelow, prod_filter]

Result:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : CommMonoid R
f : α → β → R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ (∏ x ∈ s, ∏ a ∈ t, if r x a then f x a else 1) = ∏ x ∈ t, ∏ a ∈ s, if r a x then f a x else 1

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝¹ : CommMonoid R
f : α → β → R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
⊢ (∏ x ∈ s, ∏ a ∈ t, if r x a then f x a else 1) = ∏ x ∈ t, ∏ a ∈ s, if r a x then f a x else 1

Tactic:
exact prod_comm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem length_filter_lt_length_iff_exists {l} :
    length (filter p l) < length l ↔ ∃ x ∈ l, ¬p x

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : List α✝
⊢ (filter p l).length < l.length ↔ ∃ x, x ∈ l ∧ ¬p x = true

Tactic:
simpa [length_eq_countP_add_countP p l, countP_eq_length_filter] using
  countP_pos_iff (p := fun x => ¬p x)

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma inv_le_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) :
    (↑a⁻¹ : A) ≤ b ↔ (↑b⁻¹ : A) ≤ a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : Aˣ
ha : 0 ≤ ↑a
hb : 0 ≤ ↑b
⊢ ↑a⁻¹ ≤ ↑b ↔ ↑b⁻¹ ≤ ↑a

Tactic:
simpa using CStarAlgebra.inv_le_inv_iff ha (inv_nonneg_of_nonneg b hb)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem mapₗ_congr {f g : α → β} (hf : Measurable f) (hg : Measurable g) (h : f =ᵐ[μ] g) :
    mapₗ f μ = mapₗ g μ

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
⊢ (mapₗ f) μ = (mapₗ g) μ

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
s : Set β
hs : MeasurableSet s
⊢ ((mapₗ f) μ) s = ((mapₗ g) μ) s

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
s : Set β
hs : MeasurableSet s
⊢ ((mapₗ f) μ) s = ((mapₗ g) μ) s

Tactic:
simpa only [mapₗ, hf, hg, hs, dif_pos, liftLinear_apply, OuterMeasure.map_apply]
  using measure_congr (h.preimage s)

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_intCast_smul [Ring R] [AddCommGroup α] [StarAddMonoid α] [Module R α] (c : ℤ)
    (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℤ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
theorem mem_basicOpen_den (x : ProjectiveSpectrum.top 𝒜)
    (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl) :
    x ∈ ProjectiveSpectrum.basicOpen 𝒜 f.den

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 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ x ∈ ProjectiveSpectrum.basicOpen 𝒜 ↑f.den

Tactic:
rw [ProjectiveSpectrum.mem_basicOpen]

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal

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 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ ↑f.den ∉ x.asHomogeneousIdeal

Tactic:
exact f.den_mem

Result:
no goals
-- Mathlib/Order/Bounds/OrderIso.lean
theorem isLUB_image' {s : Set α} {x : α} : IsLUB (f '' s) (f x) ↔ IsLUB s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB (⇑f '' s) (f x) ↔ IsLUB s x

Tactic:
rw [isLUB_image, f.symm_apply_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma pow_eq_one_iff_of_ne_zero (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a : R
n : ℕ
hn : n ≠ 0
⊢ a ^ n = 1 ↔ a = 1 ∨ a = -1 ∧ Even n

Tactic:
simp [← pow_eq_pow_iff_of_ne_zero hn]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem Icc_pred_left (h : pred a ≤ b) : Icc (pred a) b = insert (pred a) (Icc a b)

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

Tactic:
simp_rw [← Ici_inter_Iic, Ici_pred, insert_inter_of_mem (mem_Iic.2 h)]

Result:
no goals
-- Mathlib/Data/Rat/Star.lean
@[simp] lemma addSubmonoid_closure_range_mul_self : closure (range fun x : ℚ≥0 ↦ x * x) = ⊤

Proof state:
⊢ closure (range fun x => x * x) = ⊤

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} :
    k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
⊢ k ∈ insertManyIfNewUnit m l ↔ k ∈ m ∨ l.contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem S_sub_one (n : ℤ) : S R (n - 1) = X * S R n - S R (n + 1)

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℤ
⊢ S R (n - 1) = X * S R n - S R (n + 1)

Tactic:
linear_combination (norm := ring_nf) S_add_two R (n - 1)

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/Ultra.lean
lemma norm_add_one_le_max_norm_one (x : R) :
    ‖x + 1‖ ≤ max ‖x‖ 1

Proof state:
R : Type u_1
inst✝² : SeminormedRing R
inst✝¹ : NormOneClass R
inst✝ : IsUltrametricDist R
x : R
⊢ ‖x + 1‖ ≤ ‖x‖ ⊔ 1

Tactic:
simpa only [le_max_iff, norm_one] using norm_add_le_max x 1

Result:
no goals
-- Mathlib/RingTheory/NonUnitalSubring/Basic.lean
theorem coe_iSup_of_directed {ι} [Nonempty ι] {S : ι → NonUnitalSubring R}
    (hS : Directed (· ≤ ·) S) : ((⨆ i, S i : NonUnitalSubring R) : Set R) = ⋃ i, S i :=
  Set.ext fun x ↦ by simp [mem_iSup_of_directed hS]

Proof state:
R : Type u
inst✝¹ : NonUnitalNonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem beq [DecidableEq α] : Primrec₂ (@BEq.beq α _) :=
  have : PrimrecRel fun a b : ℕ => a = b :=
    (PrimrecPred.and nat_le nat_le.swap).of_eq fun a => by simp [le_antisymm_iff]
  (this.comp₂ (Primrec.encode.comp₂ Primrec₂.left) (Primrec.encode.comp₂ Primrec₂.right)).of_eq
    fun _ _ => encode_injective.eq_iff

Proof state:
α : Type u_1
inst✝¹ : Primcodable α
inst✝ : DecidableEq α
a : ℕ × ℕ
⊢ (fun x1 x2 => x1 ≤ x2) a.1 a.2 ∧ (fun x1 x2 => x1 ≤ x2) a.2 a.1 ↔ (fun a b => a = b) a.1 a.2

Tactic:
simp [le_antisymm_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)}
    (h : m.WF) : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
fallback : β k
f : Option (β k) → Option (β k)
h : m.WF
⊢ (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback

Tactic:
simp_to_raw using Raw₀.getD_alter_self

Result:
no goals
-- Mathlib/Data/Real/GoldenRatio.lean
theorem gold_pos : 0 < φ :=
  mul_pos (by apply add_pos <;> norm_num) <| inv_pos.2 zero_lt_two

Proof state:
⊢ 0 < 1 + √5

Tactic:
apply add_pos <;> norm_num

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem liftMonoidWithZeroHom_apply_div {L : Type*} [CommGroupWithZero L]
    (φ : MonoidWithZeroHom K[X] L) (hφ : K[X]⁰ ≤ L⁰.comap φ) (p q : K[X]) :
    liftMonoidWithZeroHom φ hφ (algebraMap _ _ p / algebraMap _ _ q) = φ p / φ q

Proof state:
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q

Tactic:
rcases eq_or_ne q 0 with (rfl | hq)

Result:
case inl
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) 0) = φ p / φ 0

case inr
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
hq : q ≠ 0
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q

Proof state:
case inl
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p : K[X]
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) 0) = φ p / φ 0

Tactic:
simp only [div_zero, map_zero]

Result:
no goals

Proof state:
case inr
K : Type u
inst✝² : CommRing K
inst✝¹ : IsDomain K
L : Type u_1
inst✝ : CommGroupWithZero L
φ : K[X] →*₀ L
hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰
p q : K[X]
hq : q ≠ 0
⊢ (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q) = φ p / φ q

Tactic:
simp only [← mk_eq_div, mk_eq_localization_mk _ hq,
  liftMonoidWithZeroHom_apply_ofFractionRing_mk]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem lor_assoc (n m k : ℕ) : (n ||| m) ||| k = n ||| (m ||| k)

Proof state:
n m k : ℕ
⊢ n ||| m ||| k = n ||| (m ||| k)

Tactic:
bitwise_assoc_tac

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem constFormalMultilinearSeries_radius {v : F} :
    (constFormalMultilinearSeries 𝕜 E v).radius = ⊤ :=
  (constFormalMultilinearSeries 𝕜 E v).radius_eq_top_of_forall_image_add_eq_zero 1
    (by simp [constFormalMultilinearSeries])

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
v : F
⊢ ∀ (m : ℕ), constFormalMultilinearSeries 𝕜 E v (m + 1) = 0

Tactic:
simp [constFormalMultilinearSeries]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem left_mem_Icc : a ∈ Icc a b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
simp [le_refl]

Result:
no goals