harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
theorem UniqueMDiffWithinAt.preimage_partialHomeomorph (hs : UniqueMDiffWithinAt I s x)
    {e : PartialHomeomorph M M'} (he : e.MDifferentiable I I') (hx : x ∈ e.source) :
    UniqueMDiffWithinAt I' (e.target ∩ e.symm ⁻¹' s) (e x)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : PartialHomeomorph M M'
he : PartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffWithinAt I' (↑e '' (s ∩ e.source)) (↑e x)

Tactic:
exact (hs.inter (e.open_source.mem_nhds hx)).image_denseRange
  (he.mdifferentiableAt hx).hasMFDerivAt.hasMFDerivWithinAt
  (he.mfderiv_surjective hx).denseRange

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : PartialHomeomorph M M'
he : PartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffWithinAt I' (e.target ∩ ↑e.symm ⁻¹' s) (↑e x)

Tactic:
rw [← e.image_source_inter_eq', inter_comm]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set M
x : M
hs : UniqueMDiffWithinAt I s x
e : PartialHomeomorph M M'
he : PartialHomeomorph.MDifferentiable I I' e
hx : x ∈ e.source
⊢ UniqueMDiffWithinAt I' (↑e '' (s ∩ e.source)) (↑e x)
-- Mathlib/Data/List/Rotate.lean
theorem Nodup.rotate_eq_self_iff {l : List α} (hl : l.Nodup) {n : ℕ} :
    l.rotate n = l ↔ n % l.length = 0 ∨ l = []

Proof state:
α : Type u
l : List α
hl : l.Nodup
n : ℕ
⊢ l.rotate n = l ↔ n % l.length = 0 ∨ l = []

Tactic:
rw [← zero_mod, ← hl.rotate_congr_iff, rotate_zero]

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[reassoc, elementwise]
lemma ΓIso_hom_map {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) :
    f.app U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE inf_le_right).op

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op

Tactic:
simp [-ΓIso_inv]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ Scheme.Hom.app f U ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← map_ΓIso_inv]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (Y.presheaf.map (homOfLE ⋯).op ≫ (ΓIso f U).inv) ≫ (ΓIso f U).hom = Y.presheaf.map (homOfLE ⋯).op
-- Mathlib/CategoryTheory/Sites/NonabelianCohomology/H1.lean
lemma symm {γ₁ γ₂ : OneCochain G U} {α : ZeroCochain G U} (h : OneCohomologyRelation γ₁ γ₂ α) :
    OneCohomologyRelation γ₂ γ₁ α⁻¹ := fun i j T a b ↦ by
  rw [← mul_left_inj (G.map b.op (α j)), mul_assoc, ← h i j a b,
    mul_assoc, Cochain₀.inv_apply, map_inv, inv_mul_cancel_left,
    Cochain₀.inv_apply, map_inv, inv_mul_cancel, mul_one]

Proof state:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ Grp
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (α⁻¹ i) * γ₂.ev i j a b =
    γ₁.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (α⁻¹ j)

Tactic:
rw [← mul_left_inj (G.map b.op (α j)), mul_assoc, ← h i j a b,
  mul_assoc, Cochain₀.inv_apply, map_inv, inv_mul_cancel_left,
  Cochain₀.inv_apply, map_inv, inv_mul_cancel, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mkVector_append_mkVector : mkVector n a ++ mkVector m a = mkVector (n + m) a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (mkVector n a ++ mkVector m a).toArray = (mkVector (n + m) a).toArray

Tactic:
simp

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ mkVector n a ++ mkVector m a = mkVector (n + m) a

Tactic:
rw [← toArray_inj]

Result:
n : Nat
α✝ : Type u_1
a : α✝
m : Nat
⊢ (mkVector n a ++ mkVector m a).toArray = (mkVector (n + m) a).toArray
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem contDiff_arctan {n : WithTop ℕ∞} : ContDiff ℝ n arctan :=
  contDiff_iff_contDiffAt.2 fun x =>
    have : cos (arctan x) ≠ 0 := (cos_arctan_pos x).ne'
    tanPartialHomeomorph.contDiffAt_symm_deriv (by simpa) trivial (hasDerivAt_tan this)
      (contDiffAt_tan.2 this)

Proof state:
n : WithTop ℕ∞
x : ℝ
this : cos (arctan x) ≠ 0
⊢ 1 / cos (↑tanPartialHomeomorph.symm x) ^ 2 ≠ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem continuousAt_add_coe_top (a : ℝ) :
    ContinuousAt (fun p : EReal × EReal => p.1 + p.2) (a, ⊤)

Proof state:
a : ℝ
⊢ ContinuousAt (fun p => p.1 + p.2) (↑a, ⊤)

Tactic:
simpa only [add_comm, Function.comp_def, ContinuousAt, Prod.swap]
  using Tendsto.comp (continuousAt_add_top_coe a) (continuous_swap.tendsto ((a : EReal), ⊤))

Result:
no goals
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_int_le (x : R) : ∃ n : ℤ, n ≤ x :=
  let ⟨n, h⟩ := exists_int_ge (-x); ⟨-n, by simpa [neg_le] using h⟩

Proof state:
R : Type u_3
inst✝¹ : OrderedRing R
inst✝ : Archimedean R
x : R
n : ℤ
h : -x ≤ ↑n
⊢ ↑(-n) ≤ x

Tactic:
simpa [neg_le] using h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertMany_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List (α × β)} {k : α}
    (h : (l.map Prod.fst).contains k = false) :
    (insertMany (empty : Raw₀ α (fun _ => β)) l).1.getKey! k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ empty.getKey! k = default

Tactic:
apply getKey!_empty

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ (insertMany empty l).val.getKey! k = default

Tactic:
rw [getKey!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List (α × β)
k : α
h : (List.map Prod.fst l).contains k = false
⊢ empty.getKey! k = default
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem of_subsingleton [Subsingleton G] : UniqueMul A B a0 b0

Proof state:
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : Subsingleton G
⊢ UniqueMul A B a0 b0

Tactic:
simp [UniqueMul, eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getElem?_mapIdx {l : List α} {i : Nat} :
    (l.mapIdx f)[i]? = Option.map (f i) l[i]?

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
i : Nat
⊢ (mapIdx f l)[i]? = Option.map (f i) l[i]?

Tactic:
simp [mapIdx, getElem?_mapIdx_go]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_edist (x y : α) : dist x y = (edist x y).toReal

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ dist x y = (edist x y).toReal

Tactic:
rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_comp (W : C) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ W ◁ (f ≫ g) = W ◁ f ≫ W ◁ g

Tactic:
simp only [← id_tensorHom, ← tensor_comp, comp_id]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem eq_div_of_mul_eq_left {a b c : R} (hb : b ≠ 0) (h : a * b = c) : a = c / b

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
hb : b ≠ 0
h : a * b = c
⊢ a = c / b

Tactic:
rw [← h, mul_div_cancel_right₀ _ hb]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_erase_self [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} {fallback : β} :
    getD (m.erase k) k fallback = fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
fallback : β
⊢ getD (m.erase k) k fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_erase_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_emod : bmod x m % m = x % m

Proof state:
x : Int
m : Nat
⊢ x.bmod m % ↑m = x % ↑m

Tactic:
dsimp [bmod]

Result:
x : Int
m : Nat
⊢ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) % ↑m = x % ↑m

Proof state:
x : Int
m : Nat
⊢ (if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m) % ↑m = x % ↑m

Tactic:
split <;> simp [Int.sub_emod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_eq_flatten_iff {xs : Array (Array α)} {ys : Array α} {y : α} :
    ys.push y = xs.flatten ↔
      ∃ (as : Array (Array α)) (bs : Array α) (cs : Array (Array α)),
        xs = as.push (bs.push y) ++ cs ∧ (∀ l, l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs

Proof state:
α : Type u_1
xs : Array (Array α)
ys : Array α
y : α
⊢ ys.push y = xs.flatten ↔
    ∃ as bs cs, xs = as.push (bs.push y) ++ cs ∧ (∀ (l : Array α), l ∈ cs → l = #[]) ∧ ys = as.flatten ++ bs

Tactic:
rw [eq_comm, flatten_eq_push_iff]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/CommRing.lean
theorem degreeOf_neg (i : σ) (p : MvPolynomial σ R) : degreeOf i (-p) = degreeOf i p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ degreeOf i (-p) = degreeOf i p

Tactic:
rw [degreeOf, degreeOf, degrees_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Tower.lean
theorem map_smul_left (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (b • f) g = b • map f g

Proof state:
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝

Tactic:
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul,
  smul_apply, smul_tmul']

Result:
no goals

Proof state:
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (b • f) g = b • map f g

Tactic:
ext

Result:
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹⁹ : CommSemiring R
inst✝¹⁸ : Semiring A
inst✝¹⁷ : Semiring B
inst✝¹⁶ : Algebra R A
inst✝¹⁵ : Algebra R B
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
inst✝¹² : Module A M
inst✝¹¹ : IsScalarTower R A M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : IsScalarTower R A P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module B P
inst✝¹ : IsScalarTower R B P
inst✝ : SMulCommClass A B P
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ((curry (map (b • f) g)) x✝¹) x✝ = ((curry (b • map f g)) x✝¹) x✝
-- Mathlib/RingTheory/Presentation.lean
lemma comp_aeval_relation_inl (r : Q.rels) :
    aeval (Sum.elim X (MvPolynomial.C ∘ P.val)) ((Q.comp P).relation (Sum.inl r)) =
      Q.relation r

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
r : Q.rels
⊢ (aeval (Sum.elim X (⇑C ∘ P.val))) ((Q.comp P).relation (Sum.inl r)) = Q.relation r

Tactic:
show (Q.aux P) _ = _

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
r : Q.rels
⊢ (Algebra.Presentation.aux Q P) ((Q.comp P).relation (Sum.inl r)) = Q.relation r

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_3
inst✝³ : CommRing T
inst✝² : Algebra S T
Q : Presentation S T
P : Presentation R S
inst✝¹ : Algebra R T
inst✝ : IsScalarTower R S T
r : Q.rels
⊢ (Algebra.Presentation.aux Q P) ((Q.comp P).relation (Sum.inl r)) = Q.relation r

Tactic:
simp [comp_relation, comp_relation_aux_map]

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem Monovary.sum_comp_perm_smul_eq_sum_smul_iff (hfg : Monovary f g) :
    ∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Monovary (f ∘ σ) g

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedSemiring α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
σ : Perm ι
f : ι → α
g : ι → β
inst✝ : Fintype ι
hfg : Monovary f g
⊢ ∑ i : ι, f (σ i) • g i = ∑ i : ι, f i • g i ↔ Monovary (f ∘ ⇑σ) g

Tactic:
simp [(hfg.monovaryOn _).sum_comp_perm_smul_eq_sum_smul_iff fun _ _ ↦ mem_univ _]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem zpow_neg {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m : ℤ) :
    x ^ (-m) = (x ^ m)⁻¹ :=
  ENNReal.eq_inv_of_mul_eq_one_left (by simp [← ENNReal.zpow_add x_ne_zero x_ne_top])

Proof state:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ⊤
m : ℤ
⊢ x ^ (-m) * x ^ m = 1

Tactic:
simp [← ENNReal.zpow_add x_ne_zero x_ne_top]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_nnreal_pow_eq_lintegral {f : α → ε} {p : ℝ≥0} (hp : p ≠ 0) :
    eLpNorm f p μ ^ (p : ℝ) = ∫⁻ x, ‖f x‖ₑ ^ (p : ℝ) ∂μ

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ eLpNorm f (↑p) μ ^ ↑p = ∫⁻ (x : α), ‖f x‖ₑ ^ ↑p ∂μ

Tactic:
simp [eLpNorm_eq_eLpNorm' (by exact_mod_cast hp) ENNReal.coe_ne_top,
  lintegral_rpow_enorm_eq_rpow_eLpNorm' ((NNReal.coe_pos.trans pos_iff_ne_zero).mpr hp)]

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
p : ℝ≥0
hp : p ≠ 0
⊢ ↑?m.7383 ≠ 0

Tactic:
exact_mod_cast hp

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem ratio_le_opNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) :
    (‖f m‖ / ∏ i, ‖m i‖) ≤ ‖f‖ :=
  div_le_of_le_mul₀ (by positivity) (opNorm_nonneg _) (f.le_opNorm m)

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ 0 ≤ ∏ i : ι, ‖m i‖

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
lemma insert_sdiff_insert' (hab : a ≠ b) (ha : a ∉ s) : insert a s \ insert b s = {a}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s \ insert b s ↔ a✝ ∈ {a}

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
⊢ insert a s \ insert b s = {a}

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : α
hab : a ≠ b
ha : a ∉ s
a✝ : α
⊢ a✝ ∈ insert a s \ insert b s ↔ a✝ ∈ {a}
-- Mathlib/Tactic/Module.lean
theorem add_eq_eval₂ [Semiring R] [AddCommMonoid M] [Module R M] (r₁ r₂ : R) (x : M)
    {l₁ l₂ l : NF R M} (h : l₁.eval + l₂.eval = l.eval) :
    ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (r₂ • x + l₂.eval)) = r₁ • x + (r₂ • x + (l₁.eval + l₂.eval))

Tactic:
congr! 1

Result:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + (r₂ • x + l₂.eval) = r₂ • x + (l₁.eval + l₂.eval)

Proof state:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + (r₂ • x + l₂.eval) = r₂ • x + (l₁.eval + l₂.eval)

Tactic:
simp only [← add_assoc]

Result:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x + l₂.eval = r₂ • x + l₁.eval + l₂.eval

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Tactic:
simp only [← h, eval_cons, add_smul, add_assoc]

Result:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ r₁ • x + (l₁.eval + (r₂ • x + l₂.eval)) = r₁ • x + (r₂ • x + (l₁.eval + l₂.eval))

Proof state:
case h.e'_6
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x + l₂.eval = r₂ • x + l₁.eval + l₂.eval

Tactic:
congr! 1

Result:
case h.e'_6.h.e'_5
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x = r₂ • x + l₁.eval

Proof state:
case h.e'_6.h.e'_5
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ l₁.eval + r₂ • x = r₂ • x + l₁.eval

Tactic:
rw [add_comm]

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

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

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

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem IsOpen.closure_inter (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t)

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
h : IsOpen t
⊢ closure s ∩ t ⊆ closure (s ∩ t)

Tactic:
simpa only [inter_comm t] using h.inter_closure

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_bind_lift {α σ : Type u} [Monad m] [LawfulMonad m] (x : m α) (f : α → StateT σ m β) (s : σ) : (StateT.lift x >>= f).run s = x >>= fun a => (f a).run s

Proof state:
m : Type u → Type u_1
β α σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
f : α → StateT σ m β
s : σ
⊢ (StateT.lift x >>= f).run s = do
    let a ← x
    (f a).run s

Tactic:
simp [StateT.lift, StateT.run, bind, StateT.bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/If.lean
theorem if_as_bool (d l r : Bool) : (if d then l else r) = ((d && l) || (!d && r))

Proof state:
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)

Tactic:
decide

Result:
no goals

Proof state:
d l r : Bool
⊢ (if d = true then l else r) = (d && l || !d && r)

Tactic:
revert d l r

Result:
⊢ ∀ (d l r : Bool), (if d = true then l else r) = (d && l || !d && r)
-- Mathlib/MeasureTheory/OuterMeasure/Operations.lean
theorem iSup_apply {ι} (f : ι → OuterMeasure α) (s : Set α) : (⨆ i : ι, f i) s = ⨆ i, f i s

Proof state:
α : Type u_1
ι : Sort u_3
f : ι → OuterMeasure α
s : Set α
⊢ (⨆ i, f i) s = ⨆ i, (f i) s

Tactic:
rw [iSup, sSup_apply, iSup_range]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ π / 2) : 0 ≤ tan x :=
  match lt_or_eq_of_le h0x, lt_or_eq_of_le hxp with
  | Or.inl hx0, Or.inl hxp => le_of_lt (tan_pos_of_pos_of_lt_pi_div_two hx0 hxp)
  | Or.inl _, Or.inr hxp => by simp [hxp, tan_eq_sin_div_cos]
  | Or.inr hx0, _ => by simp [hx0.symm]

Proof state:
x : ℝ
h0x : 0 ≤ x
hxp✝ : x ≤ π / 2
h✝ : 0 < x
hxp : x = π / 2
⊢ 0 ≤ tan x

Tactic:
simp [hxp, tan_eq_sin_div_cos]

Result:
no goals

Proof state:
x : ℝ
h0x : 0 ≤ x
hxp : x ≤ π / 2
hx0 : 0 = x
x✝ : x < π / 2 ∨ x = π / 2
⊢ 0 ≤ tan x

Tactic:
simp [hx0.symm]

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem J_mem : J l R ∈ symplecticGroup l R

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ J l R ∈ symplecticGroup l R

Tactic:
rw [mem_iff, J, fromBlocks_multiply, fromBlocks_transpose, fromBlocks_multiply]

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks ((0 * 0 + -1 * 1) * 0ᵀ + (0 * -1 + -1 * 0) * (-1)ᵀ) ((0 * 0 + -1 * 1) * 1ᵀ + (0 * -1 + -1 * 0) * 0ᵀ)
      ((1 * 0 + 0 * 1) * 0ᵀ + (1 * -1 + 0 * 0) * (-1)ᵀ) ((1 * 0 + 0 * 1) * 1ᵀ + (1 * -1 + 0 * 0) * 0ᵀ) =
    fromBlocks 0 (-1) 1 0

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
⊢ fromBlocks ((0 * 0 + -1 * 1) * 0ᵀ + (0 * -1 + -1 * 0) * (-1)ᵀ) ((0 * 0 + -1 * 1) * 1ᵀ + (0 * -1 + -1 * 0) * 0ᵀ)
      ((1 * 0 + 0 * 1) * 0ᵀ + (1 * -1 + 0 * 0) * (-1)ᵀ) ((1 * 0 + 0 * 1) * 1ᵀ + (1 * -1 + 0 * 0) * 0ᵀ) =
    fromBlocks 0 (-1) 1 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
@[simp] lemma iSup_zero : ⨆ _ : ι, (0 : ℕ∞) = 0

Proof state:
ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma loopyOn_spanning_iff {E : Set α} : (loopyOn E).Spanning X ↔ X ⊆ E

Proof state:
α : Type u_2
X E : Set α
⊢ (loopyOn E).Spanning X ↔ X ⊆ E

Tactic:
rw [spanning_iff, loopyOn_closure_eq, loopyOn_ground, and_iff_right rfl]

Result:
no goals