harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/FGModuleCat/Basic.lean
theorem evaluation_coevaluation :
    FGModuleCatCoevaluation K V ▷ V ≫
        (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V =
      (λ_ V).hom ≫ (ρ_ V).inv

Proof state:
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ FGModuleCatCoevaluation K V ▷ V ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V =
    (λ_ V).hom ≫ (ρ_ V).inv

Tactic:
ext : 1

Result:
case h
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ ModuleCat.Hom.hom
      (FGModuleCatCoevaluation K V ▷ V ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V) =
    ModuleCat.Hom.hom ((λ_ V).hom ≫ (ρ_ V).inv)

Proof state:
case h
K : Type u
inst✝ : Field K
V : FGModuleCat K
⊢ ModuleCat.Hom.hom
      (FGModuleCatCoevaluation K V ▷ V ≫ (α_ V (FGModuleCatDual K V) V).hom ≫ V ◁ FGModuleCatEvaluation K V) =
    ModuleCat.Hom.hom ((λ_ V).hom ≫ (ρ_ V).inv)

Tactic:
apply contractLeft_assoc_coevaluation' K V

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mulEquivOfQuotient_symm_mk (x y) : (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = mk x y

Tactic:
rw [mk_eq_monoidOf_mk'_apply]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
y : ↥S
⊢ (mulEquivOfQuotient f).symm (f.mk' x y) = (monoidOf S).mk' x y

Tactic:
exact mulEquivOfQuotient_symm_mk' _ _

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem zeroSection (e : Trivialization F (π F E)) [e.IsLinear R] {x : B}
    (hx : x ∈ e.baseSet) : e (zeroSection F E x) = (x, 0)

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
E : B → Type u_4
inst✝⁹ : NontriviallyNormedField R
inst✝⁸ : (x : B) → AddCommMonoid (E x)
inst✝⁷ : (x : B) → Module R (E x)
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace R F
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace (TotalSpace F E)
inst✝² : (x : B) → TopologicalSpace (E x)
inst✝¹ : FiberBundle F E
e : Trivialization F TotalSpace.proj
inst✝ : Trivialization.IsLinear R e
x : B
hx : x ∈ e.baseSet
⊢ ↑e (zeroSection F E x) = (x, 0)

Tactic:
simp_rw [zeroSection, e.apply_eq_prod_continuousLinearEquivAt R x hx 0, map_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma neg_smul (P : Fin 3 → R) (u : R) : W'.neg (u • P) = u • W'.neg P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u • P) x, u ^ 3 * W'.negY P, (u • P) z] = u • W'.neg P

Tactic:
rfl

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.neg (u • P) = u • W'.neg P

Tactic:
rw [neg, negY_smul]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ ![(u • P) x, u ^ 3 * W'.negY P, (u • P) z] = u • W'.neg P
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem sum_incMatrix_apply [Fintype (Sym2 α)] [Fintype (neighborSet G a)] :
    ∑ e, G.incMatrix R a e = G.degree a

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ ∑ e : Sym2 α, incMatrix R G a e = ↑(G.degree a)

Tactic:
simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : NonAssocSemiring R
a : α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Fintype ↑(G.neighborSet a)
⊢ ∑ e : Sym2 α, incMatrix R G a e = ↑(G.degree a)

Tactic:
classical simp [incMatrix_apply', sum_boole, Set.filter_mem_univ_eq_toFinset]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem equivRealProd_symm_apply (p : ℝ × ℝ) : equivRealProd.symm p = p.1 + p.2 * I

Proof state:
p : ℝ × ℝ
⊢ equivRealProd.symm p = ↑p.1 + ↑p.2 * I

Tactic:
ext <;> simp [Complex.equivRealProd, ofReal]

Result:
no goals
-- Mathlib/CategoryTheory/SingleObj.lean
theorem inv_as_inv {x y : SingleObj G} (f : x ⟶ y) : inv f = f⁻¹

Proof state:
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ inv f = f⁻¹

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Result:
case hom_inv_id
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x

Proof state:
case hom_inv_id
G : Type u
inst✝ : Group G
x y : SingleObj G
f : x ⟶ y
⊢ f ≫ f⁻¹ = 𝟙 x

Tactic:
rw [comp_as_mul, inv_mul_cancel, id_as_one]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem restrict_extend_compl_range (f : α → β) (g : α → γ) (g' : β → γ) :
    (range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val

Tactic:
exact restrict_dite_compl _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.restrict (extend f g g') = g' ∘ Subtype.val

Tactic:
classical
exact restrict_dite_compl _ _

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem commute_sub_int (n : ℤ) : Function.Commute f (· - n)

Proof state:
f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ⇑f fun x => x - ↑n

Tactic:
simpa only [sub_eq_add_neg] using
  (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem symm_apply_mem_iff (h : e.IsImage s t) : ∀ ⦃y⦄, y ∈ e.target → (e.symm y ∈ s ↔ y ∈ t) :=
  e.forall_mem_target.mpr fun x hx => by rw [e.left_inv hx, h hx]

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
⊢ ↑e.symm (↑e x) ∈ s ↔ ↑e x ∈ t

Tactic:
rw [e.left_inv hx, h hx]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
@[simp, reassoc]
lemma comp_unit_app (X : C) :
    (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
H : D ⥤ E
I : E ⥤ D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
X : C
⊢ (adj₁.comp adj₂).unit.app X = adj₁.unit.app X ≫ G.map (adj₂.unit.app (F.obj X))

Tactic:
simp [Adjunction.comp]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
@[simp]
lemma isSelfAdjoint_inr : IsSelfAdjoint (a : Unitization R A) ↔ IsSelfAdjoint a

Proof state:
R : Type u_1
A : Type u_2
inst✝² : Semiring R
inst✝¹ : StarAddMonoid R
inst✝ : Star A
a : A
⊢ IsSelfAdjoint ↑a ↔ IsSelfAdjoint a

Tactic:
simp only [isSelfAdjoint_iff, ← inr_star, ← inr_mul, inr_injective.eq_iff]

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem pointCount_eq_pointCount [Finite P] [Finite L] (l m : L) :
    pointCount P l = pointCount P m

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l m : L
⊢ pointCount P l = pointCount P m

Tactic:
apply lineCount_eq_lineCount (Dual P)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem iInf_adj {f : ι → G.Subgraph} : (⨅ i, f i).Adj a b ↔ (∀ i, (f i).Adj a b) ∧ G.Adj a b

Proof state:
ι : Sort u_1
V : Type u
G : SimpleGraph V
a b : V
f : ι → G.Subgraph
⊢ (⨅ i, f i).Adj a b ↔ (∀ (i : ι), (f i).Adj a b) ∧ G.Adj a b

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m

Proof state:
k n m : ℕ
⊢ (n + k).dist (m + k) = n.dist m

Tactic:
apply dist_add_add_right

Result:
no goals

Proof state:
k n m : ℕ
⊢ (k + n).dist (k + m) = n.dist m

Tactic:
rw [add_comm k n, add_comm k m]

Result:
k n m : ℕ
⊢ (n + k).dist (m + k) = n.dist m
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_le_omega0 {a : Cardinal} : a.ord ≤ ω ↔ a ≤ ℵ₀

Proof state:
a : Cardinal.{u_1}
⊢ a.ord ≤ ω ↔ a ≤ ℵ₀

Tactic:
rw [← ord_aleph0, ord_le_ord]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eraseIdx_mk (a : Array α) (h : a.size = n) (i) (h') :
    (Vector.mk a h).eraseIdx i h' = Vector.mk (a.eraseIdx i) (by simp [h]) := rfl

Proof state:
α : Type ?u.6865
n : Nat
a : Array α
h : a.size = n
i : Nat
h' : i < n
⊢ (a.eraseIdx i ⋯).size = n - 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem associator_inv_naturality_middle (X : C) {Y Y' : C} (f : Y ⟶ Y') (Z : C) :
    X ◁ f ▷ Z ≫ (α_ X Y' Z).inv = (α_ X Y Z).inv ≫ (X ◁ f) ▷ Z

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

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem other_eq_other' [DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z) :
    Mem.other h = Mem.other' h

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h = Mem.other' h

Tactic:
rw [← congr_right, other_spec' h, other_spec]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_smul_left_of_pos (x y : V) {r : ℝ} (hr : 0 < r) : angle (r • x) y = angle x y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
r : ℝ
hr : 0 < r
⊢ angle (r • x) y = angle x y

Tactic:
rw [angle_comm, angle_smul_right_of_pos y x hr, angle_comm]

Result:
no goals
-- Mathlib/Algebra/SMulWithZero.lean
lemma ite_zero_smul (a : R) (b : M) : (if p then a else 0 : R) • b = if p then a • b else 0

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : MonoidWithZero R
inst✝² : Zero M
inst✝¹ : MulActionWithZero R M
p : Prop
inst✝ : Decidable p
a : R
b : M
⊢ (if p then a else 0) • b = if p then a • b else 0

Tactic:
rw [ite_smul, zero_smul]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_map_frobenius_le :
    (expand R p f).roots.map (frobenius R p) ≤ p • f.roots

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(frobenius R p)) ((expand R p) f).roots ≤ p • f.roots

Tactic:
rw [← iterateFrobenius_one]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots ≤ p • f.roots

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ Multiset.map (⇑(iterateFrobenius R p 1)) ((expand R p) f).roots ≤ p • f.roots

Tactic:
convert ← roots_expand_pow_map_iterateFrobenius_le p 1 f <;> apply pow_one

Result:
no goals
-- Mathlib/Algebra/Group/Graph.lean
@[to_additive]
lemma graph_eq_range_prod (f : G →* H) : f.graph = range ((id _).prod f)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
⊢ f.graph = ((id G).prod f).range

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem col_cons (x : α) (u : Fin m → α) :
    col ι (vecCons x u) = of (vecCons (fun _ => x) (col ι u))

Proof state:
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
⊢ col ι (vecCons x u) = of (vecCons (fun x_1 => x) (col ι u))

Tactic:
ext i j

Result:
case a
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ col ι (vecCons x u) i j = of (vecCons (fun x_1 => x) (col ι u)) i j

Proof state:
case a
α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
i : Fin m.succ
j : ι
⊢ col ι (vecCons x u) i j = of (vecCons (fun x_1 => x) (col ι u)) i j

Tactic:
refine Fin.cases ?_ ?_ i <;> simp [vecHead, vecTail]

Result:
no goals
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.preimage_add_left (hs : StrictConvex 𝕜 s) (z : E) :
    StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCancelCommMonoid E
inst✝¹ : ContinuousAdd E
inst✝ : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 ((fun x => x + z) ⁻¹' s)

Tactic:
simpa only [add_comm] using hs.preimage_add_right z

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem vectorSpan_eq_span_vsub_finset_right_ne [DecidableEq P] [DecidableEq V] {s : Finset P}
    {p : P} (hp : p ∈ s) :
    vectorSpan k (s : Set P) = Submodule.span k ((s.erase p).image (· -ᵥ p))

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Ring k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
inst✝¹ : DecidableEq P
inst✝ : DecidableEq V
s : Finset P
p : P
hp : p ∈ s
⊢ vectorSpan k ↑s = Submodule.span k ↑(Finset.image (fun x => x -ᵥ p) (s.erase p))

Tactic:
simp [vectorSpan_eq_span_vsub_set_right_ne _ (Finset.mem_coe.mpr hp)]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_span_singleton_eq_map (f : M →ₗ[R] N →ₗ[R] P) (m : M) :
    map₂ f (span R {m}) = map (f m)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
⊢ map₂ f (span R {m}) = map (f m)

Tactic:
funext s

Result:
case h
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
⊢ map₂ f (span R {m}) s = map (f m) s

Proof state:
case h
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
m : M
s : Submodule R N
⊢ map₂ f (span R {m}) s = map (f m) s

Tactic:
rw [← span_eq s, map₂_span_span, image2_singleton_left, map_span]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem integrable_approxOn [BorelSpace E] {f : β → E} {μ : Measure β} (fmeas : Measurable f)
    (hf : Integrable f μ) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s]
    (hi₀ : Integrable (fun _ => y₀) μ) (n : ℕ) : Integrable (approxOn f fmeas s y₀ h₀ n) μ

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f 1 μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) 1 μ
n : ℕ
⊢ MemLp (⇑(approxOn f fmeas s y₀ h₀ n)) 1 μ

Tactic:
exact memLp_approxOn fmeas hf h₀ hi₀ n

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Integrable f μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Integrable (fun x => y₀) μ
n : ℕ
⊢ Integrable (⇑(approxOn f fmeas s y₀ h₀ n)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf hi₀ ⊢

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : MemLp f 1 μ
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : MemLp (fun x => y₀) 1 μ
n : ℕ
⊢ MemLp (⇑(approxOn f fmeas s y₀ h₀ n)) 1 μ
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_le_zpow₀ (ha : 1 ≤ a) (hn : 0 ≤ n) : 1 ≤ a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
n : ℤ
ha : 1 ≤ a
hn : 0 ≤ n
⊢ 1 ≤ a ^ n

Tactic:
simpa using zpow_right_mono₀ ha hn

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_eq_detp_sub_detp (M : Matrix n n R) : M.det = M.detp 1 - M.detp (-1)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign ((Equiv.inv (Perm n)) x) • ∏ i : n, M (((Equiv.inv (Perm n)) x) i) i +
      ∑ x ∈ ofSign (-1), sign ((Equiv.inv (Perm n)) x) • ∏ i : n, M (((Equiv.inv (Perm n)) x) i) i =
    detp 1 M - detp (-1) M

Tactic:
simp_rw [inv_apply, sign_inv, sub_eq_add_neg, detp, ← sum_neg_distrib]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign x • ∏ x_1 : n, M (x⁻¹ x_1) x_1 + ∑ x ∈ ofSign (-1), sign x • ∏ x_1 : n, M (x⁻¹ x_1) x_1 =
    ∑ σ ∈ ofSign 1, ∏ k : n, M k (σ k) + ∑ x ∈ ofSign (-1), -∏ k : n, M k (x k)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ M.det = detp 1 M - detp (-1) M

Tactic:
rw [det_apply, ← Equiv.sum_comp (Equiv.inv (Perm n)), ← ofSign_disjUnion, sum_disjUnion]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ ∑ x ∈ ofSign 1, sign ((Equiv.inv (Perm n)) x) • ∏ i : n, M (((Equiv.inv (Perm n)) x) i) i +
      ∑ x ∈ ofSign (-1), sign ((Equiv.inv (Perm n)) x) • ∏ i : n, M (((Equiv.inv (Perm n)) x) i) i =
    detp 1 M - detp (-1) M
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_eq_mkArray_iff {l : Array α} {f : α → β} {b : β} :
    l.map f = mkArray l.size b ↔ ∀ x ∈ l, f x = b

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
b : β
⊢ map f l = mkArray l.size b ↔ ∀ (x : α), x ∈ l → f x = b

Tactic:
simp [eq_mkArray_iff]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma toLeft_union : (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Proof state:
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (u ∪ v).toLeft = u.toLeft ∪ v.toLeft

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
u v : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
⊢ x ∈ (u ∪ v).toLeft ↔ x ∈ u.toLeft ∪ v.toLeft

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mul_mem_ball_mul_iff {c : E} : a * c ∈ ball (b * c) r ↔ a ∈ ball b r

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
c : E
⊢ a * c ∈ ball (b * c) r ↔ a ∈ ball b r

Tactic:
simp only [mem_ball, dist_eq_norm_div, mul_div_mul_right_eq_div]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_le_of_forall_fin_meas_le [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ]
    (C : ℝ≥0∞) {f : α → ℝ≥0∞}
    (hf : ∀ s, MeasurableSet s → μ s ≠ ∞ → ∫⁻ x in s, f x ∂μ ≤ C) : ∫⁻ x, f x ∂μ ≤ C :=
  have : SigmaFinite (μ.trim le_rfl)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
C : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (s : Set α), MeasurableSet s → μ s ≠ ⊤ → ∫⁻ (x : α) in s, f x ∂μ ≤ C
⊢ SigmaFinite (μ.trim ⋯)

Tactic:
rwa [trim_eq_self]

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem image_orderEmbOfFin_univ (s : Finset α) {k : ℕ} (h : s.card = k) :
    Finset.image (s.orderEmbOfFin h) Finset.univ = s

Proof state:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ ↑(image (⇑(s.orderEmbOfFin h)) univ) = ↑s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ image (⇑(s.orderEmbOfFin h)) univ = s

Tactic:
apply Finset.coe_injective

Result:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
k : ℕ
h : #s = k
⊢ ↑(image (⇑(s.orderEmbOfFin h)) univ) = ↑s
-- Mathlib/LinearAlgebra/Contraction.lean
theorem homTensorHomEquiv_toLinearMap :
    (homTensorHomEquiv R M N P Q).toLinearMap = homTensorHomMap R M N P Q

Proof state:
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ ↑(homTensorHomEquiv R M N P Q) = homTensorHomMap R M N P Q

Tactic:
ext m n

Result:
case H.h.h.H.h.h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
m : M →ₗ[R] P
n : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((TensorProduct.mk R M N).compr₂
          ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ ↑(homTensorHomEquiv R M N P Q)) m) n))
        x✝¹)
      x✝ =
    (((TensorProduct.mk R M N).compr₂
          ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ (homTensorHomMap R M N P Q)) m) n))
        x✝¹)
      x✝

Proof state:
case H.h.h.H.h.h
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : AddCommGroup Q
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R P
inst✝⁴ : Module R Q
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
m : M →ₗ[R] P
n : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((TensorProduct.mk R M N).compr₂
          ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ ↑(homTensorHomEquiv R M N P Q)) m) n))
        x✝¹)
      x✝ =
    (((TensorProduct.mk R M N).compr₂
          ((((TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)).compr₂ (homTensorHomMap R M N P Q)) m) n))
        x✝¹)
      x✝

Tactic:
simp only [homTensorHomEquiv, compr₂_apply, mk_apply, LinearEquiv.coe_toLinearMap,
  LinearEquiv.trans_apply, lift.equiv_apply, LinearEquiv.arrowCongr_apply, LinearEquiv.refl_symm,
  LinearEquiv.refl_apply, rTensorHomEquivHomRTensor_apply, lTensorHomEquivHomLTensor_apply,
  lTensorHomToHomLTensor_apply, rTensorHomToHomRTensor_apply, homTensorHomMap_apply,
  map_tmul]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem zero_inv : (0 : MvPowerSeries σ k)⁻¹ = 0

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
⊢ 0⁻¹ = 0

Tactic:
rw [inv_eq_zero, constantCoeff_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_ΨSq (n : ℤ) : (W.map f).ΨSq n = (W.ΨSq n).map f

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ ((mapRingHom f) (W.preΨ n) ^ 2 * if Even n then (mapRingHom f) W.Ψ₂Sq else 1) =
    (mapRingHom f) (W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)

Tactic:
simp only [ΨSq, map_preΨ, map_Ψ₂Sq, ← coe_mapRingHom]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ ((mapRingHom f) (W.preΨ n) ^ 2 * if Even n then (mapRingHom f) W.Ψ₂Sq else 1) =
    (mapRingHom f) (W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1)