harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
lemma iteratedFDeriv_two_apply (f : E → F) (z : E) (m : Fin 2 → E) :
    iteratedFDeriv 𝕜 2 f z m = fderiv 𝕜 (fderiv 𝕜 f) z (m 0) (m 1)

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
z : E
m : Fin 2 → E
⊢ (iteratedFDeriv 𝕜 2 f z) m = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)

Tactic:
simp only [iteratedFDeriv_succ_apply_right]

Result:
𝕜 : 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
z : E
m : Fin 2 → E
⊢ (((iteratedFDeriv 𝕜 0 (fun y => fderiv 𝕜 (fun y => fderiv 𝕜 f y) y) z) (init (init m))) (init m (last 0)))
      (m (last 1)) =
    ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)

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
z : E
m : Fin 2 → E
⊢ (((iteratedFDeriv 𝕜 0 (fun y => fderiv 𝕜 (fun y => fderiv 𝕜 f y) y) z) (init (init m))) (init m (last 0)))
      (m (last 1)) =
    ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_zero_radius (c x : P) : inversion c 0 x = c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ inversion c 0 x = c

Tactic:
simp [inversion]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Bifunctor.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctorMapMap {X₁ X₂ : GradedObject I C₁} (f : X₁ ⟶ X₂)
    {Y₁ Y₂ : GradedObject J C₂} (g : Y₁ ⟶ Y₂)
    [HasMap (((mapBifunctor F I J).obj X₁).obj Y₁) p]
    [HasMap (((mapBifunctor F I J).obj X₂).obj Y₂) p]
    (i : I) (j : J) (k : K) (h : p ⟨i, j⟩ = k) :
    ιMapBifunctorMapObj F p X₁ Y₁ i j k h ≫ mapBifunctorMapMap F p f g k =
      (F.map (f i)).app (Y₁ j) ≫ (F.obj (X₂ i)).map (g j) ≫
        ιMapBifunctorMapObj F p X₂ Y₂ i j k h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝⁴ : Category.{u_7, u_1} C₁
inst✝³ : Category.{u_8, u_2} C₂
inst✝² : Category.{u_9, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X₁ X₂ : GradedObject I C₁
f : X₁ ⟶ X₂
Y₁ Y₂ : GradedObject J C₂
g : Y₁ ⟶ Y₂
inst✝¹ : (((mapBifunctor F I J).obj X₁).obj Y₁).HasMap p
inst✝ : (((mapBifunctor F I J).obj X₂).obj Y₂).HasMap p
i : I
j : J
k : K
h : p (i, j) = k
⊢ ιMapBifunctorMapObj F p X₁ Y₁ i j k h ≫ mapBifunctorMapMap F p f g k =
    (F.map (f i)).app (Y₁ j) ≫ (F.obj (X₂ i)).map (g j) ≫ ιMapBifunctorMapObj F p X₂ Y₂ i j k h

Tactic:
simp [ιMapBifunctorMapObj, mapBifunctorMapMap]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem contDiffAt_norm {x : E} (hx : x ≠ 0) : ContDiffAt ℝ n norm x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Tactic:
have : ‖id x‖ ^ 2 ≠ 0 := pow_ne_zero 2 (norm_pos_iff.2 hx).ne'

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedSpace ℝ E
n : WithTop ℕ∞
x : E
hx : x ≠ 0
this : ‖id x‖ ^ 2 ≠ 0
⊢ ContDiffAt ℝ n Norm.norm x

Tactic:
simpa only [id, sqrt_sq, norm_nonneg] using (contDiffAt_id.norm_sq 𝕜).sqrt this

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
theorem IsNilpotent.isUnit_add_one [Ring R] {r : R} (hnil : IsNilpotent r) : IsUnit (r + 1)

Proof state:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (r + 1)

Tactic:
rw [← IsUnit.neg_iff, neg_add']

Result:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-r - 1)

Proof state:
R : Type u_1
inst✝ : Ring R
r : R
hnil : IsNilpotent r
⊢ IsUnit (-r - 1)

Tactic:
exact isUnit_sub_one hnil.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_eq_isSome_get? [LawfulBEq α] (h : m.WF) {a : α} :
    m.contains a = (m.get? a).isSome

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
⊢ m.contains a = (m.get? a).isSome

Tactic:
simp_to_raw using Raw₀.contains_eq_isSome_get?

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem relatively_discrete_of_finite [Finite s] :
    ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep

Tactic:
exact einfsep_pos_of_finite

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
rw [← einfsep_pos]

Result:
α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ 0 < s.einfsep
-- Mathlib/Probability/Kernel/Integral.lean
lemma integral_congr_ae₂ {f g : α → β → E} {μ : Measure α} (h : ∀ᵐ a ∂μ, f a =ᵐ[κ a] g a) :
    ∫ a, ∫ b, f a b ∂(κ a) ∂μ = ∫ a, ∫ b, g a b ∂(κ a) ∂μ

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
a✝ : α
ha : f a✝ =ᶠ[ae (κ a✝)] g a✝
⊢ ∫ (b : β), f a✝ b ∂κ a✝ = ∫ (b : β), g a✝ b ∂κ a✝

Tactic:
apply integral_congr_ae

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
a✝ : α
ha : f a✝ =ᶠ[ae (κ a✝)] g a✝
⊢ f a✝ =ᶠ[ae (κ a✝)] g a✝

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
⊢ (fun a => ∫ (b : β), f a b ∂κ a) =ᶠ[ae μ] fun a => ∫ (b : β), g a b ∂κ a

Tactic:
filter_upwards [h] with _ ha

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
a✝ : α
ha : f a✝ =ᶠ[ae (κ a✝)] g a✝
⊢ ∫ (b : β), f a✝ b ∂κ a✝ = ∫ (b : β), g a✝ b ∂κ a✝

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
⊢ ∫ (a : α), ∫ (b : β), f a b ∂κ a ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂κ a ∂μ

Tactic:
apply integral_congr_ae

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
⊢ (fun a => ∫ (b : β), f a b ∂κ a) =ᶠ[ae μ] fun a => ∫ (b : β), g a b ∂κ a

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : α → β → E
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, f a =ᶠ[ae (κ a)] g a
a✝ : α
ha : f a✝ =ᶠ[ae (κ a✝)] g a✝
⊢ f a✝ =ᶠ[ae (κ a✝)] g a✝

Tactic:
filter_upwards [ha] with _ hb using hb

Result:
no goals
-- Mathlib/RingTheory/Ideal/Over.lean
@[simp]
lemma under_smul {G : Type*} [Group G] [MulSemiringAction G B] [SMulCommClass G A B] (g : G) :
    (g • P : Ideal B).under A = P.under A

Proof state:
A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
g : G
⊢ under A (g • P) = under A P

Tactic:
ext a

Result:
case h
A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
g : G
a : A
⊢ a ∈ under A (g • P) ↔ a ∈ under A P

Proof state:
case h
A : Type u_2
inst✝⁵ : CommSemiring A
B : Type u_3
inst✝⁴ : Semiring B
inst✝³ : Algebra A B
P : Ideal B
G : Type u_5
inst✝² : Group G
inst✝¹ : MulSemiringAction G B
inst✝ : SMulCommClass G A B
g : G
a : A
⊢ a ∈ under A (g • P) ↔ a ∈ under A P

Tactic:
rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
/-- The **Sauer-Shelah lemma**. -/
lemma card_shatterer_le_sum_vcDim [Fintype α] :
    #𝒜.shatterer ≤ ∑ k ∈ Iic 𝒜.vcDim, (Fintype.card α).choose k

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, #(powersetCard x univ)

Tactic:
refine (card_le_card fun s hs ↦ mem_biUnion.2 ⟨#s, ?_⟩).trans card_biUnion_le

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ #s ∈ Iic 𝒜.vcDim ∧ s ∈ powersetCard (#s) univ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
s : Finset α
hs : s ∈ 𝒜.shatterer
⊢ #s ∈ Iic 𝒜.vcDim ∧ s ∈ powersetCard (#s) univ

Tactic:
exact ⟨mem_Iic.2 (mem_shatterer.1 hs).card_le_vcDim, mem_powersetCard_univ.2 rfl⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ k ∈ Iic 𝒜.vcDim, (Fintype.card α).choose k

Tactic:
simp_rw [← card_univ, ← card_powersetCard]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Fintype α
⊢ #𝒜.shatterer ≤ ∑ x ∈ Iic 𝒜.vcDim, #(powersetCard x univ)
-- Mathlib/Analysis/Convex/Star.lean
theorem starConvex_iff_ordConnected [LinearOrderedField 𝕜] {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) :
    StarConvex 𝕜 x s ↔ s.OrdConnected

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
x : 𝕜
s : Set 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ s.OrdConnected

Tactic:
simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem isOpen_Ioi : IsOpen (Ioi a)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen (Ioi a)

Tactic:
rw [← compl_Iic]

Result:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen (Iic a)ᶜ

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen (Iic a)ᶜ

Tactic:
exact isClosed_Iic.isOpen_compl

Result:
no goals
-- Mathlib/Geometry/RingedSpace/Stalks.lean
theorem restrictStalkIso_inv_eq_germ {U : TopCat} (X : PresheafedSpace.{_, _, v} C)
    {f : U ⟶ (X : TopCat.{v})} (h : IsOpenEmbedding f) (V : Opens U) (x : U) (hx : x ∈ V) :
    X.presheaf.germ (h.isOpenMap.functor.obj V) (f x) ⟨x, hx, rfl⟩ ≫
        (restrictStalkIso X h x).inv =
      (X.restrict h).presheaf.germ _ x hx

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
V : Opens ↑U
x : ↑U
hx : x ∈ V
⊢ X.presheaf.germ (⋯.functor.obj V) ((ConcreteCategory.hom f) x) ⋯ ≫ (X.restrictStalkIso h x).inv =
    (X.restrict h).presheaf.germ V x hx

Tactic:
rw [← restrictStalkIso_hom_eq_germ, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_C_mul_le (p : MvPolynomial σ R) (i : σ) (c : R) :
    (C c * p).degreeOf i ≤ p.degreeOf i

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i (C c * p).degrees ≤ Multiset.count i p.degrees

Tactic:
convert Multiset.count_le_of_le i degrees_mul_le

Result:
case h.e'_4.h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = (C c).degrees + p.degrees

Proof state:
case h.e'_4.h.e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ p.degrees = (C c).degrees + p.degrees

Tactic:
simp only [degrees_C, zero_add]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ degreeOf i (C c * p) ≤ degreeOf i p

Tactic:
unfold degreeOf

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ Multiset.count i (C c * p).degrees ≤ Multiset.count i p.degrees
-- Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean
theorem unitLattice_rank :
    finrank ℤ (unitLattice K) = Units.rank K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℤ ↥(unitLattice K) = rank K

Tactic:
classical
rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ finrank ℤ ↥(unitLattice K) = rank K

Tactic:
rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem summable_one_div_nat_rpow {p : ℝ} :
    Summable (fun n => 1 / (n : ℝ) ^ p : ℕ → ℝ) ↔ 1 < p

Proof state:
p : ℝ
⊢ (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem mul_basis_toMatrix [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M)
    (b₃ : Basis κ R N) (A : Matrix κ ι R) :
    A * b₁.toMatrix b₂ = LinearMap.toMatrix b₂ b₃ (toLin b₁ b₃ A)

Proof state:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Tactic:
cases nonempty_fintype κ

Result:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
this : (toMatrix b₁ b₃) ((toLin b₁ b₃) A) * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Tactic:
rwa [LinearMap.toMatrix_toLin] at this

Result:
no goals

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)

Tactic:
have := linearMap_toMatrix_mul_basis_toMatrix b₂ b₁ b₃ (Matrix.toLin b₁ b₃ A)

Result:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
R : Type u_5
M : Type u_6
inst✝⁹ : CommSemiring R
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_9
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
inst✝⁴ : Fintype ι'
inst✝³ : Finite κ
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b₁ : Basis ι R M
b₂ : Basis ι' R M
b₃ : Basis κ R N
A : Matrix κ ι R
val✝ : Fintype κ
this : (toMatrix b₁ b₃) ((toLin b₁ b₃) A) * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
⊢ A * b₁.toMatrix ⇑b₂ = (toMatrix b₂ b₃) ((toLin b₁ b₃) A)
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_single (j : ι) (i : ι) (x : β i) :
    (single i x).erase j = if i = j then 0 else single i x

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
j i : ι
x : β i
⊢ erase j (single i x) = if i = j then 0 else single i x

Tactic:
rw [← filter_ne_eq_erase, filter_single, ite_not]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem left_ne_of_oangle_sign_eq_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = 1) : p₁ ≠ p₂ :=
  left_ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : (∡ p₁ p₂ p₃).sign = 1
⊢ 1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
@[simp] lemma reciprocalFactors_zero : reciprocalFactors 0 = [0]

Proof state:
⊢ reciprocalFactors 0 = [0]

Tactic:
unfold reciprocalFactors

Result:
⊢ (if x : 0 = 0 then [0]
    else
      if x : 0 = 1 then []
      else if Even 0 then 3 :: reciprocalFactors (0 / 2) else 0 % 4 * 0 :: reciprocalFactors (0 / 4 + 1)) =
    [0]

Proof state:
⊢ (if x : 0 = 0 then [0]
    else
      if x : 0 = 1 then []
      else if Even 0 then 3 :: reciprocalFactors (0 / 2) else 0 % 4 * 0 :: reciprocalFactors (0 / 4 + 1)) =
    [0]

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Empty.lean
theorem not_mem_empty (a : α) : a ∉ (∅ : Finset α)

Proof state:
α : Type u_1
a : α
⊢ a ∉ ∅

Tactic:
simp only [mem_def, empty_val, not_mem_zero, not_false_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
    (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0))

Proof state:
w : Nat
x : BitVec w
⊢ x &&& 1#w = setWidth w (ofBool (x.getLsbD 0))

Tactic:
ext (_ | i) h <;> simp [Bool.and_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_id'' {f : α → α} (h : ∀ x, f x = x) (l : Vector α n) : map f l = l

Proof state:
α : Type u_1
n : Nat
f : α → α
h : ∀ (x : α), f x = x
l : Vector α n
⊢ map f l = l

Tactic:
simp [show f = id from funext h]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem ppow_zero {f : ArithmeticFunction R} : f.ppow 0 = ζ

Proof state:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f.ppow 0 = ↑ζ

Tactic:
rw [ppow, dif_pos rfl]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem monic_X_pow_sub {n : ℕ} (H : degree p < n) : Monic (X ^ n - p)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (-p).degree < ↑n

Tactic:
rwa [← degree_neg p] at H

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
H : p.degree < ↑n
⊢ (X ^ n - p).Monic

Tactic:
simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) < n by rwa [← degree_neg p] at H)

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma isMulFreimanIso_id : IsMulFreimanIso n A A id where
  bijOn := bijOn_id _
  map_prod_eq_map_prod s t _ _ _ _

Proof state:
α : Type u_2
inst✝ : CommMonoid α
A : Set α
n : ℕ
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
x✝¹ : s.card = n
x✝ : t.card = n
⊢ (map id s).prod = (map id t).prod ↔ s.prod = t.prod

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem IsUniform.symm : Symmetric (IsUniform G ε) := fun s t h t' ht' s' hs' ht hs => by
  rw [edgeDensity_comm _ t', edgeDensity_comm _ t]
  exact h hs' ht' hs ht

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(#t) * ε ≤ ↑(#t')
hs : ↑(#s) * ε ≤ ↑(#s')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε

Tactic:
exact h hs' ht' hs ht

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(#t) * ε ≤ ↑(#t')
hs : ↑(#s) * ε ≤ ↑(#s')
⊢ |↑(G.edgeDensity t' s') - ↑(G.edgeDensity t s)| < ε

Tactic:
rw [edgeDensity_comm _ t', edgeDensity_comm _ t]

Result:
α : Type u_1
𝕜 : Type u_2
inst✝¹ : LinearOrderedField 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(#t) * ε ≤ ↑(#t')
hs : ↑(#s) * ε ≤ ↑(#s')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < ε
-- Mathlib/LinearAlgebra/Eigenspace/Matrix.lean
/-- The spectrum of the diagonal operator is the range of the diagonal viewed as a function. -/
lemma spectrum_diagonal [Field R] (d : n → R) :
    spectrum R (diagonal d) = Set.range d

Proof state:
case h
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d

Tactic:
rw [← AlgEquiv.spectrum_eq (toLinAlgEquiv <| Pi.basisFun R n), ← hasEigenvalue_iff_mem_spectrum]

Result:
case h
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ HasEigenvalue ((toLinAlgEquiv (Pi.basisFun R n)) (diagonal d)) μ ↔ μ ∈ Set.range d

Proof state:
case h
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ HasEigenvalue ((toLinAlgEquiv (Pi.basisFun R n)) (diagonal d)) μ ↔ μ ∈ Set.range d

Tactic:
exact hasEigenvalue_toLin'_diagonal_iff d

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
⊢ spectrum R (diagonal d) = Set.range d

Tactic:
ext μ

Result:
case h
R : Type u_1
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Field R
d : n → R
μ : R
⊢ μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_comap {L : Type v} [Field L] [Algebra F L] (f : L →ₐ[F] E)
    (B : IntermediateField F L) : relrank (A.comap f) B = relrank A (B.map f)

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

Tactic:
simpa only [lift_id] using A.lift_relrank_comap f B

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_uIcc : #(uIcc a b) = (b - a).natAbs + 1 :=
  (card_map _).trans <|
    (Nat.cast_inj (R := ℤ)).mp <| by
      rw [card_range,
        Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.ofNat_add,
        Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]

Proof state:
a b : ℤ
⊢ ↑(#(range (a ⊔ b + 1 - a ⊓ b).toNat)) = ↑((b - a).natAbs + 1)

Tactic:
rw [card_range,
  Int.toNat_of_nonneg (sub_nonneg_of_le <| le_add_one min_le_max), Int.ofNat_add,
  Int.natCast_natAbs, add_comm, add_sub_assoc, max_sub_min_eq_abs, add_comm, Int.ofNat_one]

Result:
no goals