harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem left_ne_of_oangle_ne_zero {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ ≠ 0) : p₁ ≠ p₂

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

Tactic:
exact o.left_ne_zero_of_oangle_ne_zero h

Result:
no goals

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

Tactic:
rw [← @vsub_ne_zero V]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ -ᵥ p₂ ≠ 0
-- Mathlib/Probability/Kernel/MeasurableIntegral.lean
theorem StronglyMeasurable.integral_kernel_prod_right' ⦃f : α × β → E⦄ (hf : StronglyMeasurable f) :
    StronglyMeasurable fun x => ∫ y, f (x, y) ∂κ x

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x

Tactic:
rw [← uncurry_curry f] at hf

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : StronglyMeasurable (uncurry (Function.curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : IsSFiniteKernel κ
inst✝ : NormedSpace ℝ E
f : α × β → E
hf : StronglyMeasurable (uncurry (Function.curry f))
⊢ StronglyMeasurable fun x => ∫ (y : β), f (x, y) ∂κ x

Tactic:
exact hf.integral_kernel_prod_right

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma lt_log_of_rpow_lt (hx : 0 < x) (h : x ^ z < y) : z * log x < log y :=
  log_rpow hx _ ▸ log_lt_log (by positivity) h

Proof state:
x y z : ℝ
hx : 0 < x
h : x ^ z < y
⊢ 0 < x ^ z

Tactic:
positivity

Result:
no goals
-- Mathlib/MeasureTheory/Covering/OneDim.lean
theorem Icc_mem_vitaliFamily_at_left {x y : ℝ} (hxy : x < y) :
    Icc x y ∈ (vitaliFamily (volume : Measure ℝ) 1).setsAt y

Proof state:
x y : ℝ
hxy : x < y
⊢ Icc x y ∈ (vitaliFamily volume 1).setsAt y

Tactic:
rw [Icc_eq_closedBall]

Result:
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt y

Proof state:
x y : ℝ
hxy : x < y
⊢ 0 < (y - x) / 2

Tactic:
linarith

Result:
no goals

Proof state:
x y : ℝ
hxy : x < y
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)

Tactic:
rw [Real.dist_eq, abs_of_nonneg] <;> linarith

Result:
no goals

Proof state:
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt y

Tactic:
refine closedBall_mem_vitaliFamily_of_dist_le_mul _ ?_ (by linarith)

Result:
x y : ℝ
hxy : x < y
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)
-- Mathlib/Algebra/Homology/Embedding/TruncLE.lean
lemma truncLE'_d_eq {i j : ι} (hij : c.Rel i j) {i' j' : ι'}
    (hi' : e.f i = i') (hj' : e.f j = j') (hj : ¬ e.BoundaryLE j) :
    (K.truncLE' e).d i j = (K.truncLE'XIso e hi' (e.not_boundaryLE_prev hij)).hom ≫ K.d i' j' ≫
        (K.truncLE'XIso e hj' hj).inv :=
  Quiver.Hom.op_inj (by simpa using K.op.truncGE'_d_eq e.op hij hj' hi' (by simpa))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : ¬e.BoundaryLE j
⊢ ¬e.op.BoundaryGE j

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : ¬e.BoundaryLE j
⊢ ((K.truncLE' e).d i j).op = ((K.truncLE'XIso e hi' ⋯).hom ≫ K.d i' j' ≫ (K.truncLE'XIso e hj' hj).inv).op

Tactic:
simpa using K.op.truncGE'_d_eq e.op hij hj' hi' (by simpa)

Result:
no goals
-- Mathlib/Topology/Algebra/Field.lean
theorem IsLocalMin.inv {f : α → β} {a : α} (h1 : IsLocalMin f a) (h2 : ∀ᶠ z in 𝓝 a, 0 < f z) :
    IsLocalMax f⁻¹ a

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedSemifield β
f : α → β
a : α
h1 : IsLocalMin f a
h2 : ∀ᶠ (z : α) in 𝓝 a, 0 < f z
⊢ IsLocalMax f⁻¹ a

Tactic:
filter_upwards [h1, h2] with z h3 h4 using(inv_le_inv₀ h4 h2.self_of_nhds).mpr h3

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem sSupIndep.disjoint_sSup {x : α} {y : Set α} (hx : x ∈ s) (hy : y ⊆ s) (hxy : x ∉ y) :
    Disjoint x (sSup y)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
⊢ Disjoint x (sSup y)

Tactic:
have := (hs.mono <| insert_subset_iff.mpr ⟨hx, hy⟩) (mem_insert x _)

Result:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup (insert x y \ {x}))
⊢ Disjoint x (sSup y)

Tactic:
rw [insert_diff_of_mem _ (mem_singleton _), diff_singleton_eq_self hxy] at this

Result:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
s : Set α
hs : sSupIndep s
x : α
y : Set α
hx : x ∈ s
hy : y ⊆ s
hxy : x ∉ y
this : Disjoint x (sSup y)
⊢ Disjoint x (sSup y)

Tactic:
exact this

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
theorem directSumRight_symm_lof_tmul (x : M₁') (i : ι₂) (y : M₂ i) :
    (directSumRight R M₁' M₂).symm (DirectSum.lof R _ _ i (x ⊗ₜ[R] y)) =
      x ⊗ₜ[R] DirectSum.lof R _ _ i y

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₂ : Type v₂
inst✝⁴ : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst✝³ : AddCommMonoid M₁'
inst✝² : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝¹ : Module R M₁'
inst✝ : (i₂ : ι₂) → Module R (M₂ i₂)
x : M₁'
i : ι₂
y : M₂ i
⊢ (directSumRight R M₁' M₂).symm ((lof R ι₂ (fun i => M₁' ⊗[R] M₂ i) i) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] (lof R ι₂ M₂ i) y

Tactic:
rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
theorem IntermediateField.splits_iff_mem (h : p.Splits (algebraMap K L)) :
    p.Splits (algebraMap K F) ↔ ∀ x ∈ p.rootSet L, x ∈ F

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
⊢ Splits (algebraMap K ↥F) p → ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
intro hF

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : Splits (algebraMap K ↥F) p
⊢ ∀ x ∈ p.rootSet L, x ∈ F

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : Splits (algebraMap K ↥F) p
⊢ ∀ ⦃x : ↥F⦄, x ∈ p.rootSet ↥F → F.val x ∈ F

Tactic:
exact fun x _ ↦ x.2

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
⊢ Splits (algebraMap K ↥F) p ↔ ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
refine ⟨?_, IntermediateField.splits_of_splits h⟩

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
⊢ Splits (algebraMap K ↥F) p → ∀ x ∈ p.rootSet L, x ∈ F

Proof state:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : Splits (algebraMap K ↥F) p
⊢ ∀ x ∈ p.rootSet L, x ∈ F

Tactic:
rw [← Polynomial.image_rootSet hF F.val, Set.forall_mem_image]

Result:
K : Type v
L : Type w
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
p : K[X]
F : IntermediateField K L
h : Splits (algebraMap K L) p
hF : Splits (algebraMap K ↥F) p
⊢ ∀ ⦃x : ↥F⦄, x ∈ p.rootSet ↥F → F.val x ∈ F
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem compProdFun_tsum_left (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] (a : α)
    (s : Set (β × γ)) : compProdFun κ η a s = ∑' n, compProdFun (seq κ n) η a s

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
⊢ κ.compProdFun η a s = ∑' (n : ℕ), (κ.seq n).compProdFun η a s

Tactic:
simp_rw [compProdFun, (measure_sum_seq κ _).symm, lintegral_sum_measure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_mul_comm (a b : Int) : -a * b = a * -b

Proof state:
a b : Int
⊢ -a * b = a * -b

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem IsOpenMap.restrictPreimage (H : IsOpenMap f) (s : Set β) :
    IsOpenMap (s.restrictPreimage f)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α), IsOpen u → Subtype.val ⁻¹' u = t → ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t

Tactic:
exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
this : ∀ (u : Set α), IsOpen u → Subtype.val ⁻¹' u = t → ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
⊢ IsOpen t → IsOpen (s.restrictPreimage f '' t)

Tactic:
simpa [isOpen_induced_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
⊢ IsOpenMap (s.restrictPreimage f)

Tactic:
intro t

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ IsOpen t → IsOpen (s.restrictPreimage f '' t)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
u : Set α
hu : IsOpen u
e : Subtype.val ⁻¹' u = t
⊢ Subtype.val ⁻¹' (f '' u) = s.restrictPreimage f '' t

Tactic:
simp [← e, image_restrictPreimage]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ IsOpen t → IsOpen (s.restrictPreimage f '' t)

Tactic:
suffices ∀ u, IsOpen u → Subtype.val ⁻¹' u = t →
  ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t by
    simpa [isOpen_induced_iff]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α), IsOpen u → Subtype.val ⁻¹' u = t → ∃ v, IsOpen v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t
-- Mathlib/Data/Rat/Defs.lean
protected lemma zero_add : 0 + a = a

Proof state:
a : ℚ
⊢ 0 + a = a

Tactic:
simp [add_def, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem mem_so [Fintype n] (A : Matrix n n R) : A ∈ so n R ↔ Aᵀ = -A

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ IsSkewAdjoint 1 A ↔ Aᵀ = -A

Tactic:
simp only [Matrix.IsSkewAdjoint, Matrix.IsAdjointPair, Matrix.mul_one, Matrix.one_mul]

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ A ∈ so n R ↔ Aᵀ = -A

Tactic:
rw [so, mem_skewAdjointMatricesLieSubalgebra, mem_skewAdjointMatricesSubmodule]

Result:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
A : Matrix n n R
⊢ IsSkewAdjoint 1 A ↔ Aᵀ = -A
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem innerContent_iUnion_nat [R1Space G] ⦃U : ℕ → Set G⦄
    (hU : ∀ i : ℕ, IsOpen (U i)) :
    μ.innerContent ⟨⋃ i : ℕ, U i, isOpen_iUnion hU⟩ ≤ ∑' i : ℕ, μ.innerContent ⟨U i, hU i⟩

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  μ.innerContent (⨆ i, { carrier := U i, is_open' := ⋯ }) ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
⊢ μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }

Tactic:
rwa [Opens.iSup_def] at this

Result:
no goals

Proof state:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
⊢ μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }

Tactic:
have := μ.innerContent_iSup_nat fun i => ⟨U i, hU i⟩

Result:
G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Set G
hU : ∀ (i : ℕ), IsOpen (U i)
this :
  μ.innerContent (⨆ i, { carrier := U i, is_open' := ⋯ }) ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
⊢ μ.innerContent { carrier := ⋃ i, U i, is_open' := ⋯ } ≤ ∑' (i : ℕ), μ.innerContent { carrier := U i, is_open' := ⋯ }
-- Mathlib/Order/Basic.lean
theorem compl_ge [LinearOrder α] : (· ≥ · : α → α → _)ᶜ = (· < ·)

Proof state:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 ≥ x2)ᶜ x✝¹ x✝ ↔ x✝¹ < x✝

Tactic:
simp [compl]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
⊢ (fun x1 x2 => x1 ≥ x2)ᶜ = fun x1 x2 => x1 < x2

Tactic:
ext

Result:
case h.h.a
α : Type u_2
inst✝ : LinearOrder α
x✝¹ x✝ : α
⊢ (fun x1 x2 => x1 ≥ x2)ᶜ x✝¹ x✝ ↔ x✝¹ < x✝
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_eq_sdiff_sup (h : z ≤ x) : x \ (y \ z) = x \ y ⊔ z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : z ≤ x
⊢ x \ (y \ z) = x \ y ⊔ z

Tactic:
rw [sdiff_sdiff_right', inf_eq_right.2 h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem add_sub_assoc (a b c : Int) : a + b - c = a + (b - c)

Proof state:
a b c : Int
⊢ a + b - c = a + (b - c)

Tactic:
rw [Int.sub_eq_add_neg, Int.add_assoc, ← Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma iInf_sup_eq (f : ι → α) (a : α) : (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a

Proof state:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
f : ι → α
a : α
⊢ (⨅ i, f i) ⊔ a = ⨅ i, f i ⊔ a

Tactic:
rw [iInf, sInf_sup_eq, iInf_range]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_neg_iff_pi_div_two_lt_abs_toReal {θ : Angle} : cos θ < 0 ↔ π / 2 < |θ.toReal|

Proof state:
θ : Angle
⊢ θ.cos < 0 ↔ π / 2 < |θ.toReal|

Tactic:
rw [← not_le, ← not_le, not_iff_not, cos_nonneg_iff_abs_toReal_le_pi_div_two]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_mkVector_iff {l : Vector α n} {f : α → β} {b : β} :
    l.map f = mkVector n b ↔ ∀ x ∈ l, f x = b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : α → β
b : β
⊢ map f l = mkVector n b ↔ ∀ (x : α), x ∈ l → f x = b

Tactic:
simp [eq_mkVector_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologySequence.lean
@[reassoc (attr := simp)]
lemma opcyclesToCycles_iCycles : K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j

Tactic:
dsimp only [opcyclesToCycles]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯ ≫ K.iCycles j = K.fromOpcycles i j

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯ ≫ K.iCycles j = K.fromOpcycles i j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/OpenPos.lean
theorem _root_.IsClosed.measure_eq_univ_iff_eq [OpensMeasurableSpace X] [IsFiniteMeasure μ]
    (hF : IsClosed F) :
    μ F = μ univ ↔ F = univ

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
m : MeasurableSpace X
μ : Measure X
inst✝² : μ.IsOpenPosMeasure
F : Set X
inst✝¹ : OpensMeasurableSpace X
inst✝ : IsFiniteMeasure μ
hF : IsClosed F
⊢ μ F = μ univ ↔ F = univ

Tactic:
rw [← ae_eq_univ_iff_measure_eq hF.measurableSet.nullMeasurableSet, hF.ae_eq_univ_iff_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zipWith_map_right (l₁ : Vector α n) (l₂ : Vector β n) (f : β → β') (g : α → β' → γ) :
    zipWith g l₁ (l₂.map f) = zipWith (fun a b => g a (f b)) l₁ l₂

Proof state:
α : Type u_1
n : Nat
β : Type u_2
β' : Type u_3
γ : Type u_4
l₁ : Vector α n
l₂ : Vector β n
f : β → β'
g : α → β' → γ
⊢ zipWith g l₁ (map f l₂) = zipWith (fun a b => g a (f b)) l₁ l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
f : β → β'
g : α → β' → γ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ zipWith g { toArray := l₁, size_toArray := ⋯ } (map f l₂) =
    zipWith (fun a b => g a (f b)) { toArray := l₁, size_toArray := ⋯ } l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
f : β → β'
g : α → β' → γ
l₁ : Array α
l₂ : Vector β l₁.size
⊢ zipWith g { toArray := l₁, size_toArray := ⋯ } (map f l₂) =
    zipWith (fun a b => g a (f b)) { toArray := l₁, size_toArray := ⋯ } l₂

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
f : β → β'
g : α → β' → γ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ zipWith g { toArray := l₁, size_toArray := ⋯ } (map f { toArray := l₂, size_toArray := h }) =
    zipWith (fun a b => g a (f b)) { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
β' : Type u_3
γ : Type u_4
f : β → β'
g : α → β' → γ
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ zipWith g { toArray := l₁, size_toArray := ⋯ } (map f { toArray := l₂, size_toArray := h }) =
    zipWith (fun a b => g a (f b)) { toArray := l₁, size_toArray := ⋯ } { toArray := l₂, size_toArray := h }

Tactic:
simp [Array.zipWith_map_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma inv [DecidableEq n] {M : Matrix n n R} (hM : M.PosSemidef) : M⁻¹.PosSemidef

Proof state:
case neg
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef 0

Tactic:
exact .zero

Result:
no goals

Proof state:
case pos
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : IsUnit M.det
this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
⊢ M⁻¹.PosSemidef

Tactic:
rwa [mul_nonsing_inv_cancel_right _ _ h, conjTranspose_conjTranspose] at this

Result:
no goals

Proof state:
case pos
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : IsUnit M.det
⊢ M⁻¹.PosSemidef

Tactic:
have := (conjTranspose_mul_mul_same hM M⁻¹).conjTranspose

Result:
case pos
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : IsUnit M.det
this : (M⁻¹ᴴ * M * M⁻¹)ᴴ.PosSemidef
⊢ M⁻¹.PosSemidef

Proof state:
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
⊢ M⁻¹.PosSemidef

Tactic:
by_cases h : IsUnit M.det

Result:
case pos
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : IsUnit M.det
⊢ M⁻¹.PosSemidef

case neg
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ M⁻¹.PosSemidef

Proof state:
case neg
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ M⁻¹.PosSemidef

Tactic:
rw [nonsing_inv_apply_not_isUnit _ h]

Result:
case neg
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype n
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : DecidableEq n
M : Matrix n n R
hM : M.PosSemidef
h : ¬IsUnit M.det
⊢ PosSemidef 0
-- Mathlib/Topology/ContinuousMap/Units.lean
@[to_additive (attr := simp)]
lemma unitsLift_symm_apply_apply_inv' (f : C(X, M)ˣ) (x : X) :
    (ContinuousMap.unitsLift.symm f x)⁻¹ = (↑f⁻¹ : C(X, M)) x

Proof state:
X : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
f : C(X, M)ˣ
x : X
⊢ ↑((unitsLift.symm f) x)⁻¹ = ↑f⁻¹ x

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem fst_expSeries (x : tsze R M) (n : ℕ) :
    fst (expSeries 𝕜 (tsze R M) n fun _ => x) = expSeries 𝕜 R n fun _ => x.fst

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁵ : Field 𝕜
inst✝¹⁴ : Ring R
inst✝¹³ : AddCommGroup M
inst✝¹² : Algebra 𝕜 R
inst✝¹¹ : Module 𝕜 M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower 𝕜 R M
inst✝⁶ : IsScalarTower 𝕜 Rᵐᵒᵖ M
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : IsTopologicalRing R
inst✝² : IsTopologicalAddGroup M
inst✝¹ : ContinuousSMul R M
inst✝ : ContinuousSMul Rᵐᵒᵖ M
x : tsze R M
n : ℕ
⊢ ((expSeries 𝕜 (tsze R M) n) fun x_1 => x).fst = (expSeries 𝕜 R n) fun x_1 => x.fst

Tactic:
simp [expSeries_apply_eq]

Result:
no goals