harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem _root_.Matrix.posDef_natCast_iff [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R]
    [Nonempty n] [Nontrivial R] {d : ℕ} :
    PosDef (d : Matrix n n R) ↔ 0 < d :=
  posDef_diagonal_iff.trans <| by simp

Proof state:
n : Type u_2
R : Type u_3
inst✝⁸ : Fintype n
inst✝⁷ : CommRing R
inst✝⁶ : PartialOrder R
inst✝⁵ : StarRing R
inst✝⁴ : StarOrderedRing R
inst✝³ : DecidableEq n
inst✝² : NoZeroDivisors R
inst✝¹ : Nonempty n
inst✝ : Nontrivial R
d : ℕ
⊢ n → 0 < ↑d ↔ 0 < d

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Root.lean
@[simp] lemma floorRoot_one_right (hn : n ≠ 0) : floorRoot n 1 = 1

Proof state:
n : ℕ
hn : n ≠ 0
⊢ n.floorRoot 1 = 1

Tactic:
simp [floorRoot, hn]

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
/-- **Vertical line test** for group homomorphisms.

Let `G ≤ H × I` be a subgroup of a product of monoids. Assume that `G` maps bijectively to the
first factor. Then `G` is the graph of some monoid homomorphism `f : H → I`. -/
@[to_additive "**Vertical line test** for additive monoid homomorphisms.

Let `G ≤ H × I` be a submonoid of a product of monoids. Assume that `G` surjects onto the first
factor and `G` intersects every \"vertical line\" `{(h, i) | i : I}` at most once. Then `G` is the
graph of some monoid homomorphism `f : H → I`."]
lemma Subgroup.exists_eq_graph {G : Subgroup (H × I)} (hG₁ : Bijective (Prod.fst ∘ G.subtype)) :
    ∃ f : H →* I, G = f.graph

Proof state:
H : Type u_2
I : Type u_3
inst✝¹ : Group H
inst✝ : Group I
G : Subgroup (H × I)
hG₁ : Bijective (Prod.fst ∘ ⇑G.subtype)
⊢ ∃ f, G = f.graph

Tactic:
simpa [SetLike.ext_iff] using Submonoid.exists_eq_mgraph hG₁

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem exists_norm_lt {r : ℝ} (hr : 0 < r) : ∃ x : α, 0 < ‖x‖ ∧ ‖x‖ < r :=
  let ⟨w, hw⟩ := exists_lt_norm α r⁻¹
  ⟨w⁻¹, by rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]⟩

Proof state:
α : Type u_2
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r

Tactic:
rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]

Result:
no goals
-- Mathlib/SetTheory/Game/Basic.lean
theorem quot_mul_neg (x y : PGame) : ⟦x * -y⟧ = (-⟦x * y⟧ : Game) :=
  game_eq (by rw [mul_neg])

Proof state:
x y : PGame
⊢ x * -y ≈ -(x * y)

Tactic:
rw [mul_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem pentagon_hom_inv_inv_inv_inv :
    W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv =
      (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ W ◁ (α_ X Y Z).hom ≫ (α_ W X (Y ⊗ Z)).inv ≫ (α_ (W ⊗ X) Y Z).inv = (α_ W (X ⊗ Y) Z).inv ≫ (α_ W X Y).inv ▷ Z

Tactic:
simp [← cancel_epi (W ◁ (α_ X Y Z).inv)]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem abs_im_lt_norm {z : ℂ} : |z.im| < ‖z‖ ↔ z.re ≠ 0

Proof state:
z : ℂ
⊢ |z.im| < ‖z‖ ↔ z.re ≠ 0

Tactic:
simpa using @abs_re_lt_norm (z * I)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_or_inj_right_iff :
    ∀ {m x y : Bool}, (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y

Proof state:
⊢ ∀ {m x y : Bool}, (x && m) = (y && m) ∧ (x || m) = (y || m) ↔ x = y

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Nat/Factorization/PrimePow.lean
theorem isPrimePow_iff_card_primeFactors_eq_one {n : ℕ} :
    IsPrimePow n ↔ n.primeFactors.card = 1

Proof state:
n : ℕ
⊢ IsPrimePow n ↔ n.primeFactors.card = 1

Tactic:
simp_rw [isPrimePow_iff_factorization_eq_single, ← Nat.support_factorization,
  Finsupp.card_support_eq_one', pos_iff_ne_zero]

Result:
no goals
-- Mathlib/Data/Set/Accumulate.lean
@[simp]
lemma accumulate_bot [PartialOrder α] [OrderBot α] (s : α → Set β) : Accumulate s ⊥ = s ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
s : α → Set β
⊢ Accumulate s ⊥ = s ⊥

Tactic:
simp [Set.accumulate_def]

Result:
no goals
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_prod_right_iff {x : ℕ} {t : Finset ι} {s : ι → ℕ} :
    Coprime x (∏ i ∈ t, s i) ↔ ∀ i ∈ t, Coprime x (s i)

Proof state:
ι : Type u_1
x : ℕ
t : Finset ι
s : ι → ℕ
⊢ x.Coprime (∏ i ∈ t, s i) ↔ ∀ i ∈ t, x.Coprime (s i)

Tactic:
simpa using coprime_multiset_prod_right_iff (m := t.val.map s)

Result:
no goals
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
@[simp] lemma RelCWComplex.skeletonLT_top [RelCWComplex C D] : skeletonLT C ⊤ = C

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
⊢ skeletonLT C ⊤ = C

Tactic:
simp [skeletonLT, union]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem image_mem_functorPushforward (R : Sieve X) {V} {f : V ⟶ X} (h : R f) :
    R.functorPushforward F (F.map f) :=
  ⟨V, f, 𝟙 _, h, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
R : Sieve X
V : C
f : V ⟶ X
h : R.arrows f
⊢ F.map f = 𝟙 (F.obj V) ≫ F.map f

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the left. -/
lemma iteratedFDeriv_comp_add_left' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (a + z)) = fun x ↦ iteratedFDeriv 𝕜 n f (a + x)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z => f (a + z)) = fun x => iteratedFDeriv 𝕜 n f (a + x)

Tactic:
simpa [← iteratedFDerivWithin_univ] using iteratedFDerivWithin_comp_add_left' n a (s := univ)

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Colimits.lean
@[simp]
lemma Quot.ι_desc [DecidableEq J] (j : J) (x : F.obj j) :
    Quot.desc F c (Quot.ι F j x) = c.ι.app j x

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (QuotientAddGroup.lift (Relations F) (DFinsupp.sumAddHom fun x => Hom.hom (c.ι.app x)) ⋯)
      (((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x) =
    (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
erw [QuotientAddGroup.lift_mk']

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun x => Hom.hom (c.ι.app x)) ((DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x) =
    (ConcreteCategory.hom (c.ι.app j)) x

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (DFinsupp.sumAddHom fun x => Hom.hom (c.ι.app x)) ((DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j) x) =
    (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
simp

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (desc F c) ((ι F j) x) = (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
dsimp [desc, ι]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
c : Cocone F
inst✝ : DecidableEq J
j : J
x : ↑(F.obj j)
⊢ (QuotientAddGroup.lift (Relations F) (DFinsupp.sumAddHom fun x => Hom.hom (c.ι.app x)) ⋯)
      (((QuotientAddGroup.mk' (Relations F)).comp (DFinsupp.singleAddHom (fun j => ↑(F.obj j)) j)) x) =
    (ConcreteCategory.hom (c.ι.app j)) x
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_pow_atBot_iff {c : α} {n : ℕ} :
    Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
c : α
n : ℕ
⊢ Tendsto (fun x => c * x ^ n) atTop atBot ↔ n ≠ 0 ∧ c < 0

Tactic:
simp only [← tendsto_neg_atTop_iff, ← neg_mul, tendsto_const_mul_pow_atTop_iff, neg_pos]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Pi.lean
lemma Pi.uniformSpace_comap_restrict (S : Set ι) :
    UniformSpace.comap (S.restrict) (Pi.uniformSpace (fun i : S ↦ α i)) =
    ⨅ i ∈ S, UniformSpace.comap (eval i) (U i)

Proof state:
ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
S : Set ι
⊢ UniformSpace.comap S.restrict (uniformSpace fun i => α ↑i) = ⨅ i ∈ S, UniformSpace.comap (eval i) (U i)

Tactic:
simp (config := { unfoldPartialApp := true })
  [← iInf_subtype'', ← uniformSpace_comap_precomp' _ ((↑) : S → ι), Set.restrict]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldrM_empty [Monad m] (f : α → β → m β) (init : β) :
    foldrM f init #v[] = return init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
⊢ foldrM f init { toArray := #[], size_toArray := ⋯ } = pure init

Tactic:
simp [foldrM]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem product_zero : s ×ˢ (0 : Multiset β) = 0

Proof state:
α : Type u_1
β : Type v
s : Multiset α
⊢ s ×ˢ 0 = 0

Tactic:
simp [SProd.sprod, product]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_C (ha : a ≠ 0) : degree (C a) = (0 : WithBot ℕ)

Proof state:
R : Type u
a : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a).degree = 0

Tactic:
rw [degree, ← monomial_zero_left, support_monomial 0 ha, max_eq_sup_coe, sup_singleton,
  WithBot.coe_zero]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem coe_normSq_add : normSq (a + b) = normSq a + a * star b + b * star a + normSq b

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ ↑(normSq (a + b)) = ↑(normSq a) + a * star b + b * star a + ↑(normSq b)

Tactic:
simp only [star_add, ← self_mul_star, mul_add, add_mul, add_assoc, add_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mk_append_mk (a b : Array α) (ha : a.size = n) (hb : b.size = m) :
    Vector.mk a ha ++ Vector.mk b hb = Vector.mk (a ++ b) (by simp [ha, hb]) := rfl

Proof state:
α : Type ?u.4413
n m : Nat
a b : Array α
ha : a.size = n
hb : b.size = m
⊢ (a ++ b).size = n + m

Tactic:
simp [ha, hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem count_singleton (a b : α) : count a [b] = if b == a then 1 else 0

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
⊢ count a [b] = if (b == a) = true then 1 else 0

Tactic:
simp [count_cons]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
@[reassoc (attr := simp)]
lemma ιTensorObj₃_tensorHom (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃)
    (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
    ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom f₁ (tensorHom f₂ f₃) j =
      (f₁ i₁ ⊗ f₂ i₂ ⊗ f₃ i₃) ≫ ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Proof state:
I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝³ : X₂.HasTensor X₃
inst✝² : X₁.HasTensor (tensorObj X₂ X₃)
inst✝¹ : Y₂.HasTensor Y₃
inst✝ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
i₁ i₂ i₃ j : I
h : i₁ + i₂ + i₃ = j
⊢ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom f₁ (tensorHom f₂ f₃) j =
    (f₁ i₁ ⊗ f₂ i₂ ⊗ f₃ i₃) ≫ ιTensorObj₃ Y₁ Y₂ Y₃ i₁ i₂ i₃ j h

Tactic:
rw [ιTensorObj₃_eq _ _ _ i₁ i₂ i₃ j h _  rfl,
  ιTensorObj₃_eq _ _ _ i₁ i₂ i₃ j h _  rfl, assoc, ι_tensorHom,
  ← id_tensorHom, ← id_tensorHom, ← MonoidalCategory.tensor_comp_assoc, ι_tensorHom,
  ← MonoidalCategory.tensor_comp_assoc, id_comp, comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem snd_zero : snd (0 : Measure (α × β)) = 0

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
⊢ snd 0 = 0

Tactic:
simp [snd]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem swap_idRel : Prod.swap '' idRel = @idRel α :=
  Set.ext fun ⟨a, b⟩ => by simpa [image_swap_eq_preimage_swap] using eq_comm

Proof state:
α : Type ua
x✝ : α × α
a b : α
⊢ (a, b) ∈ Prod.swap '' idRel ↔ (a, b) ∈ idRel

Tactic:
simpa [image_swap_eq_preimage_swap] using eq_comm

Result:
no goals
-- Mathlib/Logic/Embedding/Basic.lean
theorem equiv_toEmbedding_trans_symm_toEmbedding {α β : Sort*} (e : α ≃ β) :
    e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl _

Proof state:
α : Sort u_1
β : Sort u_2
e : α ≃ β
⊢ e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl α

Tactic:
ext

Result:
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : α
⊢ (e.toEmbedding.trans e.symm.toEmbedding) x✝ = (Embedding.refl α) x✝

Proof state:
case h
α : Sort u_1
β : Sort u_2
e : α ≃ β
x✝ : α
⊢ (e.toEmbedding.trans e.symm.toEmbedding) x✝ = (Embedding.refl α) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem frontier_sphere' (x : E) (r : ℝ) : frontier (sphere x r) = sphere x r

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ frontier (sphere x r) = sphere x r

Tactic:
rw [isClosed_sphere.frontier_eq, interior_sphere' x, diff_empty]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Basic.lean
@[simp]
lemma iSup_obj {ι : Type*} (S : ι → Subpresheaf F) (U : Cᵒᵖ) :
    (⨆ i, S i).obj U = ⋃ i, (S i).obj U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
ι : Type u_1
S : ι → Subpresheaf F
U : Cᵒᵖ
⊢ (⨆ i, S i).obj U = ⋃ i, (S i).obj U

Tactic:
simp [iSup, sSup_obj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_mkArray (a b : α) (n : Nat) : count a (mkArray n b) = if b == a then n else 0

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
n : Nat
⊢ count a (mkArray n b) = if (b == a) = true then n else 0

Tactic:
simp [← List.toArray_replicate, List.count_replicate]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem iInf_toSubalgebra {ι : Sort*} (S : ι → IntermediateField F E) :
    (iInf S).toSubalgebra = ⨅ i, (S i).toSubalgebra :=
  SetLike.coe_injective <| by simp [iInf]

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Sort u_3
S : ι → IntermediateField F E
⊢ ↑(iInf S).toSubalgebra = ↑(⨅ i, (S i).toSubalgebra)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/End.lean
@[reassoc (attr := simp)]
lemma end_.lift_π (j : J) : lift f hf ≫ π F j = f j

Proof state:
J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift f hf ≫ π F j = f j

Tactic:
apply IsLimit.fac

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem real_inner_smul_self_left (x : F) (r : ℝ) : ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
r : ℝ
⊢ ⟪r • x, x⟫_ℝ = r * (‖x‖ * ‖x‖)

Tactic:
rw [real_inner_smul_left, ← real_inner_self_eq_norm_mul_norm]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem pentagon_inv_hom (W X Y Z : C) :
    (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) =
      (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
W X Y Z : C
⊢ (α_ (W ⊗ X) Y Z).inv ≫ ((α_ W X Y).hom ⊗ 𝟙 Z) = (α_ W X (Y ⊗ Z)).hom ≫ (𝟙 W ⊗ (α_ X Y Z).inv) ≫ (α_ W (X ⊗ Y) Z).inv

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem mixedEmbedding_apply_isReal (x : K) (w : {w // IsReal w}) :
    (mixedEmbedding K x).1 w = embedding_of_isReal w.prop x

Proof state:
K : Type u_1
inst✝ : Field K
x : K
w : { w // w.IsReal }
⊢ ((mixedEmbedding K) x).1 w = (embedding_of_isReal ⋯) x

Tactic:
simp_rw [mixedEmbedding, RingHom.prod_apply, Pi.ringHom_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/OfSection.lean
lemma range_eq_ofSection' {X : C} (f : yoneda.obj X ⋙ uliftFunctor.{w} ⟶ F) :
    range f = ofSection ((yonedaCompUliftFunctorEquiv F X) f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : C
f : yoneda.obj X ⋙ uliftFunctor.{w, v} ⟶ F
⊢ range f = ofSection ((yonedaCompUliftFunctorEquiv F X) f)

Tactic:
rw [ofSection_eq_range', Equiv.symm_apply_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem parallelepiped_eq_convexHull (v : ι → E) :
    parallelepiped v = convexHull ℝ (∑ i, {(0 : E), v i})

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ parallelepiped v = (convexHull ℝ) (∑ i : ι, {0, v i})

Tactic:
simp_rw [convexHull_sum, convexHull_pair, parallelepiped_eq_sum_segment]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.eq_false_of_or_eq_false_left {a b : Bool} (h : (a || b) = false) : a = false

Proof state:
a b : Bool
h : (a || b) = false
⊢ a = false

Tactic:
cases a <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_C_mul_X_pow (n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n

Proof state:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (C a * X ^ n).degree = ↑n

Tactic:
rw [C_mul_X_pow_eq_monomial, degree_monomial n ha]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/OpenNhds.lean
theorem map_id_obj_unop (x : X) (U : (OpenNhds x)ᵒᵖ) : (map (𝟙 X) x).obj (unop U) = unop U

Proof state:
X : TopCat
x : ↑X
U : (OpenNhds x)ᵒᵖ
⊢ (map (𝟙 X) x).obj (unop U) = unop U

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_eq_flatMap {L : List (List α)} : flatten L = L.flatMap id

Proof state:
α : Type u_1
L : List (List α)
⊢ L.flatten = flatMap id L

Tactic:
induction L <;> simp [List.flatMap]

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem AddSubmonoid.fg_iff_mul_fg (P : AddSubmonoid N) : P.FG ↔ P.toSubmonoid.FG

Proof state:
N : Type u_2
inst✝ : AddMonoid N
P : AddSubmonoid N
⊢ P.FG ↔ (toSubmonoid P).FG

Tactic:
convert (Submonoid.fg_iff_add_fg (toSubmonoid P)).symm

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Basic.lean
lemma Functor.map_comp_assoc {C : Type u₁} [Category C] {D : Type u₂} [Category D] (F : C ⥤ D)
    {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {W : D} (h : F.obj Z ⟶ W) :
    (F.map (f ≫ g)) ≫ h = F.map f ≫ F.map g ≫ h

Proof state:
C : Type u₁
inst✝¹ : Category.{u_1, u₁} C
D : Type u₂
inst✝ : Category.{u_2, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
W : D
h : F.obj Z ⟶ W
⊢ F.map (f ≫ g) ≫ h = F.map f ≫ F.map g ≫ h

Tactic:
rw [F.map_comp, Category.assoc]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma id :
    (fst φ).1.comp (inl φ) (add_neg_cancel 1) +
      (snd φ).comp (Cochain.ofHom (inr φ)) (add_zero 0) = Cochain.ofHom (𝟙 _)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (↑(fst φ)).comp (inl φ) ⋯ + (snd φ).comp (Cochain.ofHom (inr φ)) ⋯ = Cochain.ofHom (𝟙 (mappingCone φ))

Tactic:
simp [ext_cochain_from_iff φ (-1) 0 (neg_add_cancel 1)]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_sub {R : Type*} [Ring R] {s t : SummableFamily Γ R α} :
    (s - t).hsum = s.hsum - t.hsum

Proof state:
Γ : Type u_1
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
R : Type u_7
inst✝ : Ring R
s t : SummableFamily Γ R α
⊢ (s - t).hsum = s.hsum - t.hsum

Tactic:
rw [← lsum_apply, LinearMap.map_sub, lsum_apply, lsum_apply]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_map {k : β → α} {l : Filter β} : f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
k : β → α
l : Filter β
⊢ f =O[map k l] g ↔ (f ∘ k) =O[l] (g ∘ k)

Tactic:
simp only [IsBigO_def, isBigOWith_map]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sort_insert [DecidableEq α] {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) :
    sort r (insert a s) = a :: sort r s

Proof state:
α : Type u_1
r : α → α → Prop
inst✝⁴ : DecidableRel r
inst✝³ : IsTrans α r
inst✝² : IsAntisymm α r
inst✝¹ : IsTotal α r
inst✝ : DecidableEq α
a : α
s : Finset α
h₁ : ∀ b ∈ s, r a b
h₂ : a ∉ s
⊢ sort r (insert a s) = a :: sort r s

Tactic:
rw [← cons_eq_insert _ _ h₂, sort_cons r h₁]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isSuccPrelimit_of_noMax [NoMinOrder α] : ¬ IsSuccPrelimit a

Proof state:
α : Type u_1
a : α
inst✝⁴ : Preorder α
inst✝³ : SuccOrder α
inst✝² : IsSuccArchimedean α
inst✝¹ : NoMaxOrder α
inst✝ : NoMinOrder α
⊢ ¬IsSuccPrelimit a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Prime.eq_of_factorization_pos {p q : ℕ} (hp : Prime p) (h : p.factorization q ≠ 0) :
    p = q

Proof state:
p q : ℕ
hp : Prime p
h : p.factorization q ≠ 0
⊢ p = q

Tactic:
simpa [hp.factorization, single_apply] using h

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem inv_eqToHom {X Y : C} (h : X = Y) : inv (eqToHom h) = eqToHom h.symm

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ inv (eqToHom h) = eqToHom ⋯

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem algebraMap_eval_C [Algebra R R'] (x : R) (n : ℤ) :
    algebraMap R R' ((C R n).eval x) = (C R' n).eval (algebraMap R R' x)

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R
n : ℤ
⊢ (algebraMap R R') (eval x (C R n)) = eval ((algebraMap R R') x) (C R' n)

Tactic:
rw [← aeval_algebraMap_apply_eq_algebraMap_eval, aeval_C]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem const_mul_lintegral (f : α →ₛ ℝ≥0∞) (x : ℝ≥0∞) :
    (const α x * f).lintegral μ = x * f.lintegral μ :=
  calc
    (f.map fun a => x * a).lintegral μ = ∑ r ∈ f.range, x * r * μ (f ⁻¹' {r}) := map_lintegral _ _
    _ = x * ∑ r ∈ f.range, r * μ (f ⁻¹' {r})

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α →ₛ ℝ≥0∞
x : ℝ≥0∞
⊢ ∑ r ∈ f.range, x * r * μ (⇑f ⁻¹' {r}) = x * ∑ r ∈ f.range, r * μ (⇑f ⁻¹' {r})

Tactic:
simp_rw [Finset.mul_sum, mul_assoc]

Result:
no goals
-- Mathlib/Data/Vector/Zip.lean
theorem zipWith_tail (x : Vector α n) (y : Vector β n) :
    (Vector.zipWith f x y).tail = Vector.zipWith f x.tail y.tail

Proof state:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m✝ : Fin (n - 1)
⊢ (zipWith f x y).tail.get m✝ = (zipWith f x.tail y.tail).get m✝

Tactic:
simp [get_tail]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
⊢ (zipWith f x y).tail = zipWith f x.tail y.tail

Tactic:
ext

Result:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
x : Vector α n
y : Vector β n
m✝ : Fin (n - 1)
⊢ (zipWith f x y).tail.get m✝ = (zipWith f x.tail y.tail).get m✝
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem _root_.MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure
    (μ : VectorMeasure α ℝ≥0∞) :
    toENNRealVectorMeasure (ennrealToMeasure μ) = μ := ext fun s hs => by
  rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ↑μ.ennrealToMeasure.toENNRealVectorMeasure s = ↑μ s

Tactic:
rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]

Result:
no goals