harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤ π / 2) :
    cos x = √(1 - sin x ^ 2)

Proof state:
x : ℝ
hl : -(π / 2) ≤ x
hu : x ≤ π / 2
⊢ cos x = √(1 - sin x ^ 2)

Tactic:
rw [← abs_cos_eq_sqrt_one_sub_sin_sq, abs_of_nonneg (cos_nonneg_of_mem_Icc ⟨hl, hu⟩)]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Comon_.lean
theorem comul_assoc_flip :
    M.comul ≫ (M.comul ▷ M.X) = M.comul ≫ (M.X ◁ M.comul) ≫ (α_ M.X M.X M.X).inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Comon_ C
⊢ M.comul ≫ M.comul ▷ M.X = M.comul ≫ M.X ◁ M.comul ≫ (α_ M.X M.X M.X).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive] lemma MulEquivClass.isMulFreimanIso [EquivLike F α β] [MulEquivClass F α β] (f : F)
    (hfAB : BijOn f A B) : IsMulFreimanIso n A B f where
  bijOn := hfAB
  map_prod_eq_map_prod s t _ _ _ _

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
A : Set α
B : Set β
n : ℕ
inst✝¹ : EquivLike F α β
inst✝ : MulEquivClass F α β
f : F
hfAB : BijOn (⇑f) A B
s t : Multiset α
x✝³ : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝² : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
x✝¹ : s.card = n
x✝ : t.card = n
⊢ (map (⇑f) s).prod = (map (⇑f) t).prod ↔ s.prod = t.prod

Tactic:
rw [← map_multiset_prod, ← map_multiset_prod, EquivLike.apply_eq_iff_eq]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem splitLower_eq_self : I.splitLower i x = I ↔ I.upper i ≤ x

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ I.splitLower i x = ↑I ↔ I.upper i ≤ x

Tactic:
simp [splitLower, update_eq_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
lemma homologyShiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
    ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n a a' ha').hom.app
      ((quotient _ _).obj K) =
    (homologyFunctor _ _ a).map (((quotient _ _).commShiftIso n).inv.app K) ≫
      (homologyFunctorFactors _ _ a).hom.app (K⟦n⟧) ≫
      ((HomologicalComplex.homologyFunctor _ _ 0).shiftIso n a a' ha').hom.app K ≫
      (homologyFunctorFactors _ _ a').inv.app K

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ ((homologyFunctor C (up ℤ) 0).shiftIso n a a' ha').hom.app ((quotient C (up ℤ)).obj K) =
    (homologyFunctor C (up ℤ) a).map (((quotient C (up ℤ)).commShiftIso n).inv.app K) ≫
      (homologyFunctorFactors C (up ℤ) a).hom.app ((shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K) ≫
        ((HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftIso n a a' ha').hom.app K ≫
          (homologyFunctorFactors C (up ℤ) a').inv.app K

Tactic:
apply Functor.ShiftSequence.induced_shiftIso_hom_app_obj

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
lemma monotone_ofReal : Monotone ofReal

Proof state:
x y : ℝ
hxy : x ≤ y
⊢ ↑x ≤ ↑y

Tactic:
simp only [ofRealHom_eq_coe, real_le_real, hxy]

Result:
no goals

Proof state:
⊢ Monotone ofReal

Tactic:
intro x y hxy

Result:
x y : ℝ
hxy : x ≤ y
⊢ ↑x ≤ ↑y
-- Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
theorem hasLineDerivWithinAt_smul_iff {c : 𝕜} (hc : c ≠ 0) :
    HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v) ↔ HasLineDerivWithinAt 𝕜 f f' s x v :=
  ⟨fun h ↦ by simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹), fun h ↦ h.smul c⟩

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type u_2
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type u_3
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
f : E → F
s : Set E
x v : E
f' : F
c : 𝕜
hc : c ≠ 0
h : HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v)
⊢ HasLineDerivWithinAt 𝕜 f f' s x v

Tactic:
simpa [smul_smul, inv_mul_cancel₀ hc] using h.smul (c ⁻¹)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem sInf_toSubfield (S : Set (IntermediateField F E)) :
    (sInf S).toSubfield = sInf (toSubfield '' S) :=
  SetLike.coe_injective <| by simp [Set.sUnion_image]

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
S : Set (IntermediateField F E)
⊢ ↑(sInf S).toSubfield = ↑(sInf (toSubfield '' S))

Tactic:
simp [Set.sUnion_image]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma card_union (s t : Finset α) : #(s ∪ t) = #s + #t - #(s ∩ t)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ #(s ∪ t) = #s + #t - #(s ∩ t)

Tactic:
rw [← card_union_add_card_inter, Nat.add_sub_cancel]

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

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

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

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isRightDescent_inv_iff {w : W} {i : B} :
    cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i

Tactic:
simpa using (cs.isLeftDescent_inv_iff (w := w⁻¹)).symm

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma loopyOn_isLoop_iff {E : Set α} : (loopyOn E).IsLoop e ↔ e ∈ E

Proof state:
α : Type u_1
e : α
E : Set α
⊢ (loopyOn E).IsLoop e ↔ e ∈ E

Tactic:
simp [isLoop_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem nndist_eq : nndist f g = sInf { C | ∀ x : α, nndist (f x) (g x) ≤ C } :=
  Subtype.ext <| dist_eq.trans <| by
    rw [val_eq_coe, coe_sInf, coe_image]
    simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, coe_mk, exists_prop, coe_nndist]

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} = ↑(sInf {C | ∀ (x : α), nndist (f x) (g x) ≤ C})

Tactic:
rw [val_eq_coe, coe_sInf, coe_image]

Result:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} =
    sInf {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ {C | ∀ (x : α), nndist (f x) (g x) ≤ C}}

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : PseudoMetricSpace β
f g : α →ᵇ β
⊢ sInf {C | 0 ≤ C ∧ ∀ (x : α), dist (f x) (g x) ≤ C} =
    sInf {x | ∃ (h : 0 ≤ x), ⟨x, h⟩ ∈ {C | ∀ (x : α), nndist (f x) (g x) ≤ C}}

Tactic:
simp_rw [mem_setOf_eq, ← NNReal.coe_le_coe, coe_mk, exists_prop, coe_nndist]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem inf (h₁ : IsPartition π₁) (h₂ : IsPartition π₂) : IsPartition (π₁ ⊓ π₂) :=
  isPartition_iff_iUnion_eq.2 <| by simp [h₁.iUnion_eq, h₂.iUnion_eq]

Proof state:
ι : Type u_1
I : Box ι
π₁ π₂ : Prepartition I
h₁ : π₁.IsPartition
h₂ : π₂.IsPartition
⊢ (π₁ ⊓ π₂).iUnion = ↑I

Tactic:
simp [h₁.iUnion_eq, h₂.iUnion_eq]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Icc_add_intCast : ⋃ n : ℤ, Icc (a + n) (a + n + 1) = Set.univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
a : α
⊢ ⋃ n, Icc (a + ↑n) (a + ↑n + 1) = univ

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  iUnion_Icc_add_zsmul zero_lt_one a

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasStrictDerivAt.sum (h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x) :
    HasStrictDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x
⊢ HasStrictDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
simpa [ContinuousLinearMap.sum_apply] using (HasStrictFDerivAt.sum h).hasStrictDerivAt

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem iInf_add_iInf (h : ∀ i j, ∃ k, f k + g k ≤ f i + g j) : iInf f + iInf g = ⨅ a, f a + g a :=
  suffices ⨅ a, f a + g a ≤ iInf f + iInf g from
    le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) (iInf_le _ _)) this
  calc
    ⨅ a, f a + g a ≤ ⨅ (a) (a'), f a + g a' :=
      le_iInf₂ fun a a' => let ⟨k, h⟩ := h a a'; iInf_le_of_le k h
    _ = iInf f + iInf g

Proof state:
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j
⊢ ⨅ a, ⨅ a', f a + g a' = iInf f + iInf g

Tactic:
simp_rw [iInf_add, add_iInf]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem add (hn : IsPeriodicPt f n x) (hm : IsPeriodicPt f m x) :
    IsPeriodicPt f (n + m) x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f (n + m) x

Tactic:
rw [IsPeriodicPt, iterate_add]

Result:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x

Proof state:
α : Type u_1
f : α → α
x : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x

Tactic:
exact hn.comp hm

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_one_cons {α : Type*} [Semiring α] (h : ℕ) (L : List ℕ) :
    ofDigits (1 : α) (h :: L) = h + ofDigits 1 L

Proof state:
α : Type u_1
inst✝ : Semiring α
h : ℕ
L : List ℕ
⊢ ofDigits 1 (h :: L) = ↑h + ofDigits 1 L

Tactic:
simp [ofDigits]

Result:
no goals
-- Mathlib/Geometry/Manifold/PartitionOfUnity.lean
theorem exists_finset_toSmoothPartitionOfUnity_eventuallyEq (i : ι) (x : M) :
    ∃ t : Finset ι,
      fs.toSmoothPartitionOfUnity i =ᶠ[𝓝 x]
        fs i * ∏ j ∈ t.filter fun j => WellOrderingRel j i, ((1 : M → ℝ) - fs j)

Proof state:
ι : Type uι
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type uH
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : FiniteDimensional ℝ E
s : Set M
fs : SmoothBumpCovering ι I M s
inst✝¹ : T2Space M
inst✝ : IsManifold I ∞ M
i : ι
x : M
⊢ ∃ t,
    ⇑(fs.toSmoothPartitionOfUnity i) =ᶠ[𝓝 x]
      ↑(fs.toFun i) * ∏ j ∈ Finset.filter (fun j => WellOrderingRel j i) t, (1 - ↑(fs.toFun j))

Tactic:
simpa using fs.toBumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq i x

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.symm : SameCycle f x y → SameCycle f y x := fun ⟨i, hi⟩ =>
  ⟨-i, by rw [zpow_neg, ← hi, inv_apply_self]⟩

Proof state:
α : Type u_2
f : Perm α
x y : α
x✝ : f.SameCycle x y
i : ℤ
hi : (f ^ i) x = y
⊢ (f ^ (-i)) y = x

Tactic:
rw [zpow_neg, ← hi, inv_apply_self]

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem Codisjoint.bihimp_eq_inf {a b : α} (h : Codisjoint a b) : a ⇔ b = a ⊓ b

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
h : Codisjoint a b
⊢ a ⇔ b = a ⊓ b

Tactic:
rw [bihimp, h.himp_eq_left, h.himp_eq_right]

Result:
no goals
-- Mathlib/Algebra/Homology/ComplexShapeSigns.lean
lemma associative_ε₂_eq_mul (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) :
    ε₂ c₁₂ c₃ c (π c₁ c₂ c₁₂ (i₁, i₂), i₃) =
      (ε₂ c₁ c₂₃ c (i₁, π c₂ c₃ c₂₃ (i₂, i₃)) * ε₂ c₂ c₃ c₂₃ (i₂, i₃))

Proof state:
I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c
inst✝² : TotalComplexShape c₂ c₃ c₂₃
inst✝¹ : TotalComplexShape c₁ c₂₃ c
inst✝ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c
i₁ : I₁
i₂ : I₂
i₃ : I₃
⊢ c₁₂.ε₂ c₃ c (c₁.π c₂ c₁₂ (i₁, i₂), i₃) = c₁.ε₂ c₂₃ c (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₂ c₃ c₂₃ (i₂, i₃)

Tactic:
apply Associative.ε₂_eq_mul

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsGE {a : H} : Tendsto Inv.inv (𝓝[≥] a) (𝓝[≤] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Ici a)) (𝓟 (Iic a⁻¹))

Tactic:
simp [tendsto_principal_principal]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem liminf_compl : (liminf u f)ᶜ = limsup (compl ∘ u) f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (liminf u f)ᶜ = limsup (compl ∘ u) f

Tactic:
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_fiberwise_of_maps_to {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : ι → α) :
    ∏ j ∈ t, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝¹ : CommMonoid α
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → α
⊢ ∏ j ∈ t, ∏ i ∈ filter (fun i => g i = j) s, f i = ∏ i ∈ s, f i

Tactic:
rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformly_iff_tendstoUniformlyOnFilter :
    TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

Tactic:
rw [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, principal_univ]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma zpow_sub₀ (ha : a ≠ 0) (m n : ℤ) : a ^ (m - n) = a ^ m / a ^ n

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m n : ℤ
⊢ a ^ (m - n) = a ^ m / a ^ n

Tactic:
rw [Int.sub_eq_add_neg, zpow_add₀ ha, zpow_neg, div_eq_mul_inv]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem biTotal_iff_isEmpty_left [IsEmpty β] : BiTotal R ↔ IsEmpty α

Proof state:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty β
⊢ BiTotal R ↔ IsEmpty α

Tactic:
simp only [BiTotal, leftTotal_iff_isEmpty_left, rightTotal_empty, and_true]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem DifferentiableAt.rpow (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x)
    (h : f x ≠ 0) : DifferentiableAt ℝ (fun x => f x ^ g x) x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
hg : DifferentiableAt ℝ g x
h : f x ≠ 0
⊢ DifferentiableAt ℝ (fun x => f x ^ g x) x

Tactic:
exact (differentiableAt_rpow_of_ne (f x, g x) h).comp x (hf.prod hg)

Result:
no goals
-- Mathlib/Data/Matrix/Kronecker.lean
theorem trace_kroneckerMapBilinear [CommSemiring R] [Fintype m] [Fintype n] [AddCommMonoid α]
    [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ]
    (f : α →ₗ[R] β →ₗ[R] γ) (A : Matrix m m α) (B : Matrix n n β) :
    trace (kroneckerMapBilinear f A B) = f (trace A) (trace B)

Proof state:
R : Type u_1
α : Type u_2
β : Type u_4
γ : Type u_6
m : Type u_9
n : Type u_10
inst✝⁸ : CommSemiring R
inst✝⁷ : Fintype m
inst✝⁶ : Fintype n
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : AddCommMonoid γ
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : Module R γ
f : α →ₗ[R] β →ₗ[R] γ
A : Matrix m m α
B : Matrix n n β
⊢ (((kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace

Tactic:
simp_rw [Matrix.trace, Matrix.diag, kroneckerMapBilinear_apply_apply, LinearMap.map_sum₂,
  map_sum, ← Finset.univ_product_univ, Finset.sum_product, kroneckerMap_apply]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
lemma self_ne_not : ∀ b : Bool, b ≠ !b

Proof state:
⊢ ∀ (b : Bool), b ≠ !b

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Operations.lean
theorem top_prod (s : Subsemigroup N) : (⊤ : Subsemigroup M).prod s = s.comap (MulHom.snd M N) :=
  ext fun x => by simp [mem_prod, MulHom.coe_snd]

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup N
x : M × N
⊢ x ∈ ⊤.prod s ↔ x ∈ comap (MulHom.snd M N) s

Tactic:
simp [mem_prod, MulHom.coe_snd]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem toList_mapVal (f : α → β → δ) (l : AssocList α β) :
    (mapVal f l).toList = l.toList.map (fun (a, b) => (a, f a b))

Proof state:
α : Type u_1
β : Type u_2
δ : Type u_3
f : α → β → δ
l : AssocList α β
⊢ (mapVal f l).toList =
    List.map
      (fun x =>
        match x with
        | (a, b) => (a, f a b))
      l.toList

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem hasSum_orthogonalProjection {U : Submodule 𝕜 E} [CompleteSpace U]
    (b : HilbertBasis ι 𝕜 U) (x : E) :
    HasSum (fun i => ⟪(b i : E), x⟫ • b i) (orthogonalProjection U x)

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
b : HilbertBasis ι 𝕜 ↥U
x : E
⊢ HasSum (fun i => inner (↑(b i)) x • b i) ((orthogonalProjection U) x)

Tactic:
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
  b.hasSum_repr (orthogonalProjection U x)

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem mul_right_eq_iff_eq_mul_invOf : a * c = b ↔ a = b * ⅟c

Proof state:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ a * c = b ↔ a = b * ⅟c

Tactic:
rw [← mul_left_inj_of_invertible (c := ⅟c), mul_invOf_cancel_right]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem normSq_eq_zero {x : F} : normSqF x = 0 ↔ x = 0 :=
  Iff.trans
    (by simp only [normSq, ext_iff, map_zero, inner_self_im, eq_self_iff_true, and_true])
    (@inner_self_eq_zero 𝕜 _ _ _ _ _ x)

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
cd : Core 𝕜 F
x : F
⊢ normSq x = 0 ↔ ⟪x, x⟫_𝕜 = 0

Tactic:
simp only [normSq, ext_iff, map_zero, inner_self_im, eq_self_iff_true, and_true]

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem bddAbove_empty [Nonempty α] : BddAbove (∅ : Set α)

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddAbove ∅

Tactic:
simp only [BddAbove, upperBounds_empty, univ_nonempty]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_restrict : J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, (J₁ : WithBot (Box ι)) = ↑J ⊓ ↑J'

Proof state:
ι : Type u_1
I J J₁ : Box ι
π : Prepartition I
⊢ J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ⊓ ↑J'

Tactic:
simp [restrict, eq_comm]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem Set.exists_diff_singleton_of_not_minimal (hP : ∀ ⦃s t⦄, P t → t ⊆ s → P s) (hs : P s)
    (h : ¬ Minimal P s) : ∃ x ∈ s, P (s \ {x})

Proof state:
α : Type u_1
P : Set α → Prop
s : Set α
hP : ∀ ⦃s t : Set α⦄, P t → t ⊆ s → P s
hs : P s
h : ¬Minimal P s
⊢ ∃ x ∈ s, P (s \ {x})

Tactic:
simpa [Set.minimal_iff_forall_diff_singleton hP, hs] using h

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
lemma mulLeftMap_ker_eq_bot_iff_linearIndependent_op {ι : Type*} (a : ι → A) :
    LinearMap.ker (Submodule.mulLeftMap (M := toSubmodule A) (toSubmodule B) a) = ⊥ ↔
    LinearIndependent B.op (MulOpposite.op ∘ A.val ∘ a)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
⊢ LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) a) = ⊥ ↔ LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a)

Tactic:
simp_rw [LinearIndependent, LinearMap.ker_eq_bot]

Result:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
A B : Subalgebra R S
ι : Type u_1
a : ι → ↥A
⊢ LinearMap.ker (Submodule.mulLeftMap (toSubmodule B) a) = ⊥ ↔
    Function.Injective ⇑(Finsupp.linearCombination (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ a))
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_one : basicOpen 𝒜 (1 : A) = ⊤ :=
  TopologicalSpace.Opens.ext <| by simp

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ↑(basicOpen 𝒜 1) = ↑⊤

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem pow_sub' (A : M) {m n : ℕ} (ha : IsUnit A.det) (h : n ≤ m) :
    A ^ (m - n) = A ^ m * (A ^ n)⁻¹

Proof state:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ IsUnit (A ^ n).det

Tactic:
simpa using ha.pow n

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ A ^ (m - n) = A ^ m * (A ^ n)⁻¹

Tactic:
rw [← tsub_add_cancel_of_le h, pow_add, Matrix.mul_assoc, mul_nonsing_inv,
  tsub_add_cancel_of_le h, Matrix.mul_one]

Result:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℕ
ha : IsUnit A.det
h : n ≤ m
⊢ IsUnit (A ^ n).det
-- Mathlib/Data/Set/Lattice.lean
lemma compl_range_subset_kernImage {s : Set α} : (range f)ᶜ ⊆ kernImage f s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (range f)ᶜ ⊆ kernImage f s

Tactic:
rw [← kernImage_empty]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f ∅ ⊆ kernImage f s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f ∅ ⊆ kernImage f s

Tactic:
exact kernImage_mono (empty_subset _)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem zero_div (a : G₀) : 0 / a = 0

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ 0 / a = 0

Tactic:
rw [div_eq_mul_inv, zero_mul]

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
@[simp]
lemma restrict_restrict (f : X.PartialMap Y)
    (U : X.Opens) (hU : Dense (U : Set X)) (hU' : U ≤ f.domain)
    (V : X.Opens) (hV : Dense (V : Set X)) (hV' : V ≤ U) :
    (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV (hV'.trans hU')

Proof state:
X Y : Scheme
f : X.PartialMap Y
U : X.Opens
hU : Dense ↑U
hU' : U ≤ f.domain
V : X.Opens
hV : Dense ↑V
hV' : V ≤ U
⊢ (f.restrict U hU hU').restrict V hV hV' = f.restrict V hV ⋯

Tactic:
ext1 <;> simp [restrict_domain]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem cancel_left {g : InfHom β γ} {f₁ f₂ : InfHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => InfHom.ext fun a => hg <| by rw [← InfHom.comp_apply, h, InfHom.comp_apply],
    congr_arg _⟩

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Min α
inst✝¹ : Min β
inst✝ : Min γ
g : InfHom β γ
f₁ f₂ : InfHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← InfHom.comp_apply, h, InfHom.comp_apply]

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem martingale_zero (ℱ : Filtration ι m0) (μ : Measure Ω) : Martingale (0 : ι → Ω → E) ℱ μ :=
  ⟨adapted_zero E ℱ, fun i j _ => by rw [Pi.zero_apply, condExp_zero]; simp⟩

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ℱ : Filtration ι m0
μ : Measure Ω
i j : ι
x✝ : i ≤ j
⊢ μ[0 j|↑ℱ i] =ᶠ[ae μ] 0 i

Tactic:
rw [Pi.zero_apply, condExp_zero]

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ℱ : Filtration ι m0
μ : Measure Ω
i j : ι
x✝ : i ≤ j
⊢ 0 =ᶠ[ae μ] 0 i

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
ℱ : Filtration ι m0
μ : Measure Ω
i j : ι
x✝ : i ≤ j
⊢ 0 =ᶠ[ae μ] 0 i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma eq_div_of_mul_eq_left (hc : c ≠ 0) (h : a * c = b) : a = b / c

Proof state:
a b c : ℕ
hc : c ≠ 0
h : a * c = b
⊢ a = b / c

Tactic:
rw [← h, Nat.mul_div_cancel _ (Nat.pos_iff_ne_zero.2 hc)]

Result:
no goals