harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpL1CLM_smul (c : 𝕜) (f : α →₁[μ] F') :
    condExpL1CLM F' hm μ (c • f) = c • condExpL1CLM F' hm μ f

Proof state:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ (condExpL1CLM F' hm μ) (c • f) = c • (condExpL1CLM F' hm μ) f

Tactic:
refine L1.setToL1_smul (dominatedFinMeasAdditive_condExpInd F' hm μ) ?_ c f

Result:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'), (condExpInd F' hm μ s) (c • x) = c • (condExpInd F' hm μ s) x

Proof state:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : ↥(Lp F' 1 μ)
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'), (condExpInd F' hm μ s) (c • x) = c • (condExpInd F' hm μ s) x

Tactic:
exact fun c s x => condExpInd_smul' c x

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem not_mem_uIcc_of_gt : a < c → b < c → c ∉ [[a, b]]

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)

Tactic:
exact Set.not_mem_uIcc_of_gt

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → c ∉ [[a, b]]

Tactic:
rw [mem_uIcc]

Result:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem intervalIntegrable_iff_integrableOn_Ico_of_le [NoAtoms μ] (hab : a ≤ b) :
    IntervalIntegrable f μ a b ↔ IntegrableOn f (Ico a b) μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
inst✝ : NoAtoms μ
hab : a ≤ b
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ico a b) μ

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab, integrableOn_Icc_iff_integrableOn_Ico]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Interval.lean
theorem Iic_mul_Iic_subset' [LocallyFiniteOrderBot α] (a b : α) : Iic a * Iic b ⊆ Iic (a * b) :=
  Finset.coe_subset.mp <| by simpa using Set.Iic_mul_Iic_subset' _ _

Proof state:
α : Type u_1
inst✝⁵ : Mul α
inst✝⁴ : Preorder α
inst✝³ : DecidableEq α
inst✝² : MulLeftMono α
inst✝¹ : MulRightMono α
inst✝ : LocallyFiniteOrderBot α
a b : α
⊢ ↑(Iic a * Iic b) ⊆ ↑(Iic (a * b))

Tactic:
simpa using Set.Iic_mul_Iic_subset' _ _

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem Commute.inv_add_inv (hab : Commute a b) (ha : a ≠ 0) (hb : b ≠ 0) :
    a⁻¹ + b⁻¹ = (a + b) / (a * b)

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)

Tactic:
rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma weightEquiv_mul {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
    weightEquiv P P x * weightEquiv P P y = weightEquiv P P y ≪≫ₗ weightEquiv P P x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
⊢ weightEquiv P P x * weightEquiv P P y = weightEquiv P P y ≪≫ₗ weightEquiv P P x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem lipschitzWith_one_norm' : LipschitzWith 1 (norm : E → ℝ)

Proof state:
E : Type u_2
inst✝ : SeminormedGroup E
⊢ LipschitzWith 1 norm

Tactic:
simpa using LipschitzWith.dist_right (1 : E)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
lemma IsSeparated.of_comp [IsSeparated (f ≫ g)] : IsSeparated f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
⊢ IsSeparated f

Tactic:
have := IsSeparated.diagonal_isClosedImmersion (f := f ≫ g)

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this : IsClosedImmersion (pullback.diagonal (f ≫ g))
⊢ IsSeparated f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this : IsClosedImmersion (pullback.diagonal (f ≫ g))
⊢ IsSeparated f

Tactic:
rw [pullback.diagonal_comp] at this

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this :
  IsClosedImmersion
    (pullback.diagonal f ≫
      (pullbackDiagonalMapIdIso f f g).inv ≫
        pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))
⊢ IsSeparated f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsSeparated (f ≫ g)
this :
  IsClosedImmersion
    (pullback.diagonal f ≫
      (pullbackDiagonalMapIdIso f f g).inv ≫
        pullback.snd (pullback.diagonal g) (pullback.map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))
⊢ IsSeparated f

Tactic:
exact ⟨@IsClosedImmersion.of_comp _ _ _ _ _ this inferInstance⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem range_indicator {s : Set α} (hs : MeasurableSet s) (hs_nonempty : s.Nonempty)
    (hs_ne_univ : s ≠ univ) (x y : β) :
    (piecewise s hs (const α x) (const α y)).range = {x, y}

Proof state:
α : Type u_1
β : Type u_2
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
hs_nonempty : s.Nonempty
hs_ne_univ : s ≠ univ
x y : β
⊢ (piecewise s hs (const α x) (const α y)).range = {x, y}

Tactic:
simp only [← Finset.coe_inj, coe_range, coe_piecewise, range_piecewise, coe_const,
  Finset.coe_insert, Finset.coe_singleton, hs_nonempty.image_const,
  (nonempty_compl.2 hs_ne_univ).image_const, singleton_union, Function.const]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_le_of_surjective_injective
    (i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j)
    (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) :
    Module.rank R S ≤ Module.rank R' S'

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R →+* R'
j : S →+* S'
hi : Surjective ⇑i
hj : Injective ⇑j
hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)
⊢ Module.rank R S ≤ Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean
@[simp]
lemma residueFieldMap_id (x : X) :
    residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)

Proof state:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ residueFieldMap (𝟙 X) x = 𝟙 (X.residueField x)

Tactic:
ext : 1

Result:
case hf
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom (residueFieldMap (𝟙 X) x) = CommRingCat.Hom.hom (𝟙 (X.residueField x))

Proof state:
case hf
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x))))) =
    CommRingCat.Hom.hom (𝟙 (X.residueField x))

Tactic:
apply IsLocalRing.ResidueField.map_id

Result:
no goals

Proof state:
case hf
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom (residueFieldMap (𝟙 X) x) = CommRingCat.Hom.hom (𝟙 (X.residueField x))

Tactic:
simp only [id_toShHom', SheafedSpace.id_base, TopCat.coe_id, id_eq, residueFieldMap, stalkMap_id]

Result:
case hf
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ CommRingCat.Hom.hom
      (CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (𝟙 (X.presheaf.stalk x))))) =
    CommRingCat.Hom.hom (𝟙 (X.residueField x))
-- Mathlib/Data/Real/Hyperreal.lean
theorem IsSt.inv {x : ℝ*} {r : ℝ} (hi : ¬Infinitesimal x) (hr : IsSt x r) : IsSt x⁻¹ r⁻¹ :=
  hr.map <| continuousAt_inv₀ <| by rintro rfl; exact hi hr

Proof state:
x : ℝ*
r : ℝ
hi : ¬x.Infinitesimal
hr : x.IsSt r
⊢ r ≠ 0

Tactic:
rintro rfl

Result:
x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False

Proof state:
x : ℝ*
hi : ¬x.Infinitesimal
hr : x.IsSt 0
⊢ False

Tactic:
exact hi hr

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem continuousWithinAt_iff'_left [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ Tendsto (fun x => (f x, f b)) (𝓝[s] b) (𝓤 α)

Tactic:
rw [ContinuousWithinAt, tendsto_nhds_left]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem or_eq_true_eq_eq_true_or_eq_true (a b : Bool) :
    ((a || b) = true) = (a = true ∨ b = true)

Proof state:
a b : Bool
⊢ ((a || b) = true) = (a = true ∨ b = true)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigO_atTop_iff_eventually_exists {α : Type*} [SemilatticeSup α] [Nonempty α]
    {f : α → E} {g : α → F} : f =O[atTop] g ↔ ∀ᶠ n₀ in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Proof state:
E : Type u_3
F : Type u_4
inst✝³ : Norm E
inst✝² : Norm F
α : Type u_17
inst✝¹ : SemilatticeSup α
inst✝ : Nonempty α
f : α → E
g : α → F
⊢ f =O[atTop] g ↔ ∀ᶠ (n₀ : α) in atTop, ∃ c, ∀ n ≥ n₀, ‖f n‖ ≤ c * ‖g n‖

Tactic:
rw [isBigO_iff, exists_eventually_atTop]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Curry.lean
theorem MultilinearMap.uncurry_curryRight (f : MultilinearMap R M M₂) :
    f.curryRight.uncurryRight = f

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
⊢ f.curryRight.uncurryRight = f

Tactic:
ext m

Result:
case H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ f.curryRight.uncurryRight m = f m

Proof state:
case H
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : CommSemiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n.succ) → M i
⊢ f.curryRight.uncurryRight m = f m

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_flatten (L : Vector (Vector α m) n) :
    L.flatten.reverse = (L.map reverse).reverse.flatten

Proof state:
α : Type u_1
m n : Nat
L : Vector (Vector α m) n
⊢ L.flatten.reverse = (map reverse L).reverse.flatten

Tactic:
cases L using vector₂_induction

Result:
case of
α : Type u_1
m n : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten.reverse =
    (map reverse
          {
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }).reverse.flatten

Proof state:
case of
α : Type u_1
m n : Nat
xss✝ : Array (Array α)
h₁✝ : xss✝.size = n
h₂✝ : ∀ (xs : Array α), xs ∈ xss✝ → xs.size = m
⊢ {
          toArray :=
            Array.map
              (fun x =>
                match x with
                | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
              xss✝.attach,
          size_toArray := ⋯ }.flatten.reverse =
    (map reverse
          {
            toArray :=
              Array.map
                (fun x =>
                  match x with
                  | ⟨xs, m_1⟩ => { toArray := xs, size_toArray := ⋯ })
                xss✝.attach,
            size_toArray := ⋯ }).reverse.flatten

Tactic:
simp [Array.reverse_flatten]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_append_getLast (l : List α) (h : l ≠ []) :
    (l.take (l.length - 1)) ++ [l.getLast h] = l

Proof state:
case nil
α : Type u_1
h : [] ≠ []
⊢ take ([].length - 1) [] ++ [[][[].length - 1]] = []

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : l ≠ []
⊢ take (l.length - 1) l ++ [l[l.length - 1]] = l

Tactic:
cases l

Result:
case nil
α : Type u_1
h : [] ≠ []
⊢ take ([].length - 1) [] ++ [[][[].length - 1]] = []

case cons
α : Type u_1
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ ≠ []
⊢ take ((head✝ :: tail✝).length - 1) (head✝ :: tail✝) ++ [(head✝ :: tail✝)[(head✝ :: tail✝).length - 1]] =
    head✝ :: tail✝

Proof state:
α : Type u_1
l : List α
h : l ≠ []
⊢ take (l.length - 1) l ++ [l.getLast h] = l

Tactic:
rw [getLast_eq_getElem]

Result:
α : Type u_1
l : List α
h : l ≠ []
⊢ take (l.length - 1) l ++ [l[l.length - 1]] = l

Proof state:
case cons
α : Type u_1
head✝ : α
tail✝ : List α
h : head✝ :: tail✝ ≠ []
⊢ take ((head✝ :: tail✝).length - 1) (head✝ :: tail✝) ++ [(head✝ :: tail✝)[(head✝ :: tail✝).length - 1]] =
    head✝ :: tail✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem cos_le_one_div_sqrt_sq_add_one {x : ℝ} (hx1 : -(3 * π / 2) ≤ x) (hx2 : x ≤ 3 * π / 2) :
    cos x ≤ (1 : ℝ) / √(x ^ 2 + 1)

Proof state:
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
⊢ cos x ≤ 1 / √(x ^ 2 + 1)

Tactic:
rcases eq_or_ne x 0 with (rfl | hx3)

Result:
case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / √(0 ^ 2 + 1)

case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / √(x ^ 2 + 1)

Proof state:
case inl
hx1 : -(3 * π / 2) ≤ 0
hx2 : 0 ≤ 3 * π / 2
⊢ cos 0 ≤ 1 / √(0 ^ 2 + 1)

Tactic:
simp

Result:
no goals

Proof state:
case inr
x : ℝ
hx1 : -(3 * π / 2) ≤ x
hx2 : x ≤ 3 * π / 2
hx3 : x ≠ 0
⊢ cos x ≤ 1 / √(x ^ 2 + 1)

Tactic:
exact (cos_lt_one_div_sqrt_sq_add_one hx1 hx2 hx3).le

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem IsTensorProduct.map_eq (hf : IsTensorProduct f) (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁)
    (i₂ : M₂ →ₗ[R] N₂) (x₁ : M₁) (x₂ : M₂) : hf.map hg i₁ i₂ (f x₁ x₂) = g (i₁ x₁) (i₂ x₂)

Proof state:
R : Type u_1
inst✝¹² : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ (hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)

Tactic:
delta IsTensorProduct.map

Result:
R : Type u_1
inst✝¹² : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ (↑hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ ↑hf.equiv.symm) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)

Proof state:
R : Type u_1
inst✝¹² : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝¹¹ : AddCommMonoid M₁
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M₁
inst✝⁷ : Module R M₂
inst✝⁶ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N
inst✝² : Module R N₁
inst✝¹ : Module R N₂
inst✝ : Module R N
g : N₁ →ₗ[R] N₂ →ₗ[R] N
hf : IsTensorProduct f
hg : IsTensorProduct g
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
x₁ : M₁
x₂ : M₂
⊢ (↑hg.equiv ∘ₗ TensorProduct.map i₁ i₂ ∘ₗ ↑hf.equiv.symm) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
lemma LinearIndependent.pair_iffₛ {x y : M} :
    LinearIndependent R ![x, y] ↔
      ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![x, y] ↔ ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
simp [Fintype.linearIndependent_iffₛ, Fin.forall_fin_two, ← FinVec.forall_iff]

Result:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (FinVec.Forall fun x_1 =>
      FinVec.Forall fun x_2 => x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (FinVec.Forall fun x_1 =>
      FinVec.Forall fun x_2 => x_1 0 • x + x_1 1 • y = x_2 0 • x + x_2 1 • y → x_1 0 = x_2 0 ∧ x_1 1 = x_2 1) ↔
    ∀ (s t s' t' : R), s • x + t • y = s' • x + t' • y → s = s' ∧ t = t'

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_splits_of_dvd {f g : K[X]} (hf0 : f ≠ 0) (hf : Splits i f) (hgf : g ∣ f) :
    Splits i g

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f g : K[X]
hf0 : f ≠ 0
hf : Splits i f
hgf : g ∣ f
⊢ Splits i g

Tactic:
obtain ⟨f, rfl⟩ := hgf

Result:
case intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
g f : K[X]
hf0 : g * f ≠ 0
hf : Splits i (g * f)
⊢ Splits i g

Proof state:
case intro
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
g f : K[X]
hf0 : g * f ≠ 0
hf : Splits i (g * f)
⊢ Splits i g

Tactic:
exact (splits_of_splits_mul i hf0 hf).1

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_X_sub_C (x : R) : (X - C x).natDegree = 1

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
⊢ (X - C x).natDegree = 1

Tactic:
rw [natDegree_sub_C, natDegree_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1

Proof state:
n✝ n : Nat
⊢ ¬n + 2 = 1

Tactic:
exact ne_of_beq_eq_false rfl

Result:
no goals

Proof state:
n : Nat
⊢ 1 % 1 = 0 ↔ 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
n✝ n : Nat
⊢ 1 = 0 ↔ n + 2 = 1

Tactic:
simp only [add_one_ne_zero, false_iff, ne_eq]

Result:
n✝ n : Nat
⊢ ¬n + 2 = 1

Proof state:
n : Nat
⊢ 1 % n = 0 ↔ n = 1

Tactic:
match n with
| 0 => simp
| 1 => simp
| n + 2 =>
  rw [mod_eq_of_lt (by exact Nat.lt_of_sub_eq_succ rfl)]
  simp only [add_one_ne_zero, false_iff, ne_eq]
  exact ne_of_beq_eq_false rfl

Result:
no goals

Proof state:
n : Nat
⊢ 1 % 0 = 0 ↔ 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
n✝ n : Nat
⊢ 1 % (n + 2) = 0 ↔ n + 2 = 1

Tactic:
rw [mod_eq_of_lt (by exact Nat.lt_of_sub_eq_succ rfl)]

Result:
n✝ n : Nat
⊢ 1 = 0 ↔ n + 2 = 1

Proof state:
n✝ n : Nat
⊢ 1 < n + 2

Tactic:
exact Nat.lt_of_sub_eq_succ rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem not_isUnit_iff {z : ℤ_[p]} : ¬IsUnit z ↔ ‖z‖ < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z : ℤ_[p]
⊢ ¬IsUnit z ↔ ‖z‖ < 1

Tactic:
simpa using mem_nonunits

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem snd_apply {s : Set β} (hs : MeasurableSet s) : ρ.snd s = ρ (Prod.snd ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
ρ : Measure (α × β)
s : Set β
hs : MeasurableSet s
⊢ ρ.snd s = ρ (Prod.snd ⁻¹' s)

Tactic:
rw [snd, Measure.map_apply measurable_snd hs]

Result:
no goals
-- Mathlib/Topology/Order/NhdsSet.lean
theorem nhdsSet_Ioc (h : a < b) : 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
@[simp] lemma isUnit_C_add_X_mul_iff :
    IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Proof state:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp

Result:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Proof state:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ (IsUnit ((C r + X * P).coeff 0) ∧ ∀ (i : ℕ), IsNilpotent (P.coeff i)) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero,
  and_congr_right_iff, ← Polynomial.isNilpotent_iff]

Result:
no goals

Proof state:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ IsUnit (C r + X * P) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]

Result:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i
⊢ (IsUnit ((C r + X * P).coeff 0) ∧ ∀ (i : ℕ), IsNilpotent (P.coeff i)) ↔ IsUnit r ∧ IsNilpotent P

Proof state:
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ ∀ (i : ℕ), (C r + X * P).coeff (i + 1) = P.coeff i

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_eval₂ (f : S →+* T) (n : ℕ) (t : T) :
    (ascPochhammer T n).eval t = (ascPochhammer S n).eval₂ f t

Proof state:
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (ascPochhammer T n) = eval₂ f t (ascPochhammer S n)

Tactic:
rw [← ascPochhammer_map f]

Result:
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)

Proof state:
S : Type u
inst✝¹ : Semiring S
T : Type v
inst✝ : Semiring T
f : S →+* T
n : ℕ
t : T
⊢ eval t (map f (ascPochhammer S n)) = eval₂ f t (ascPochhammer S n)

Tactic:
exact eval_map f t

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ℕ → ℂ} {m : ℝ}
    (h : ∀ n ≠ 0, ‖f n‖ ≤ m) {s : ℝ} (hs : 1 < s) :
    LSeriesSummable f s :=
  LSeriesSummable_of_bounded_of_one_lt_re h <| by simp [hs]

Proof state:
f : ℕ → ℂ
m : ℝ
h : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ m
s : ℝ
hs : 1 < s
⊢ 1 < (↑s).re

Tactic:
simp [hs]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiff.sub {f g : E → F} (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
    ContDiff 𝕜 n fun x => f x - g x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f g : E → F
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 n fun x => f x - g x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals