harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_sub_pos_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x = 0 ∨ y ≠ 0) :
    0 < angle x (x - y)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x - y)

Tactic:
rw [← neg_ne_zero] at h0

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x - y)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x - y)

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x - y)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x + -y)

Tactic:
exact angle_add_pos_of_inner_eq_zero h h0

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x - y)

Tactic:
rw [sub_eq_add_neg]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x + -y)
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_le_one_iff_le : a * b⁻¹ ≤ 1 ↔ a ≤ b :=
  mul_inv_le_iff_le_mul.trans <| by rw [one_mul]

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ a ≤ 1 * b ↔ a ≤ b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_mul (a b) : (⟨a * b⟩ : R[X]) = ⟨a⟩ * ⟨b⟩ :=
  show _ = mul _ _ by rw [mul_def]

Proof state:
R : Type u
inst✝ : Semiring R
a b : R[ℕ]
⊢ { toFinsupp := a * b } = Polynomial.mul { toFinsupp := a } { toFinsupp := b }

Tactic:
rw [mul_def]

Result:
no goals
-- Mathlib/Algebra/Exact.lean
lemma exact_subtype_mkQ (Q : Submodule R N) :
    Exact (Submodule.subtype Q) (Submodule.mkQ Q)

Proof state:
R : Type u_8
N : Type u_10
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : Submodule R N
⊢ Exact ⇑Q.subtype ⇑Q.mkQ

Tactic:
rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_mul_relfinrank (h1 : A ≤ B) (h2 : B ≤ C) :
    relfinrank A B * relfinrank B C = relfinrank A C

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B C : IntermediateField F E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank h1 h2))

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
@[simp] lemma support_mul (f g : ι → M₀) : support (fun x ↦ f x * g x) = support f ∩ support g :=
  ext fun x ↦ by simp [not_or]

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
f g : ι → M₀
x : ι
⊢ (x ∈ support fun x => f x * g x) ↔ x ∈ support f ∩ support g

Tactic:
simp [not_or]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
@[simp] lemma isNilpotent_monomial_iff {n : ℕ} :
    IsNilpotent (monomial (R := R) n r) ↔ IsNilpotent r :=
  exists_congr fun k ↦ by simp

Proof state:
R : Type u_1
r : R
inst✝ : Semiring R
n k : ℕ
⊢ (monomial n) r ^ k = 0 ↔ r ^ k = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem restrict_eq_freeOn_iff : M ↾ I = freeOn I ↔ M.Indep I

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M ↾ I = freeOn I ↔ M.Indep I

Tactic:
rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff,
  and_iff_left Subset.rfl]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_sigma {p : β → Type*} {f : Sigma p → α} : ⨆ x, f x = ⨆ (i) (j), f ⟨i, j⟩ :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, Sigma.forall]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
p : β → Type u_8
f : Sigma p → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f ⟨i, j⟩ ≤ c

Tactic:
simp only [iSup_le_iff, Sigma.forall]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
lemma whiskerRightIso_mapId (f : a ⟶ b) : whiskerRightIso (F.mapId a) (F.map f) =
    (F.mapComp (𝟙 a) f).symm ≪≫ F.map₂Iso (λ_ f) ≪≫ (λ_ (F.map f)).symm

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ whiskerRightIso (F.mapId a) (F.map f) = (F.mapComp (𝟙 a) f).symm ≪≫ F.map₂Iso (λ_ f) ≪≫ (λ_ (F.map f)).symm

Tactic:
simp [mapComp_id_left]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma isMaximalIndepSet_compl (s : Finset α) :
    Maximal Gᶜ.IsIndepSet s ↔ Maximal G.IsClique s

Proof state:
α : Type u_3
G : SimpleGraph α
s : Finset α
⊢ Maximal Gᶜ.IsIndepSet ↑s ↔ Maximal G.IsClique ↑s

Tactic:
simp [isMaximalIndepSet_iff, isMaximalClique_iff]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem joinedIn_univ : JoinedIn univ x y ↔ Joined x y

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ JoinedIn univ x y ↔ Joined x y

Tactic:
simp [JoinedIn, Joined, exists_true_iff_nonempty]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem relabel_moveRight {x : PGame} {xl' xr'} (el : xl' ≃ x.LeftMoves) (er : xr' ≃ x.RightMoves)
    (j : x.RightMoves) : moveRight (relabel el er) (er.symm j) = x.moveRight j

Proof state:
x : PGame
xl' xr' : Type u_1
el : xl' ≃ x.LeftMoves
er : xr' ≃ x.RightMoves
j : x.RightMoves
⊢ (relabel el er).moveRight (er.symm j) = x.moveRight j

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem HasProd.prod_mk {f : β → α} {g : β → γ} {a : α} {b : γ}
    (hf : HasProd f a) (hg : HasProd g b) : HasProd (fun x ↦ (⟨f x, g x⟩ : α × γ)) ⟨a, b⟩

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : CommMonoid γ
inst✝ : TopologicalSpace γ
f : β → α
g : β → γ
a : α
b : γ
hf : HasProd f a
hg : HasProd g b
⊢ HasProd (fun x => (f x, g x)) (a, b)

Tactic:
simp [HasProd, ← prod_mk_prod, Filter.Tendsto.prod_mk_nhds hf hg]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem neg_smul_set : -a • t = -(a • t)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ -a • t = -(a • t)

Tactic:
simp_rw [← image_smul, ← image_neg_eq_neg, image_image, neg_smul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem convex_parallelepiped (v : ι → E) : Convex ℝ (parallelepiped v)

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))

Tactic:
exact convex_sum _ fun _i _hi => convex_segment _ _

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ Convex ℝ (parallelepiped v)

Tactic:
rw [parallelepiped_eq_sum_segment]

Result:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
lemma equicontinuousOn_univ (F : ι → X → α) :
    EquicontinuousOn F univ ↔ Equicontinuous F

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
⊢ EquicontinuousOn F univ ↔ Equicontinuous F

Tactic:
simp [EquicontinuousOn, Equicontinuous]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
/-- Multiplying with `swap R i j` on the right swaps the `i`-th column with the `j`-th column. -/
@[simp]
lemma mul_swap_apply_left (i j : n) (a : m) (g : Matrix m n R) :
    (g * swap R i j) a i = g a j

Proof state:
R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
a : m
g : Matrix m n R
⊢ (g * swap R i j) a i = g a j

Tactic:
simp [swap, PEquiv.mul_toMatrix_toPEquiv]

Result:
no goals
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_fintype_prod_left_iff [Fintype ι] {s : ι → ℕ} {x : ℕ} :
    Coprime (∏ i, s i) x ↔ ∀ i, Coprime (s i) x

Proof state:
ι : Type u_1
inst✝ : Fintype ι
s : ι → ℕ
x : ℕ
⊢ (∏ i : ι, s i).Coprime x ↔ ∀ (i : ι), (s i).Coprime x

Tactic:
simp [coprime_prod_left_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/GromovHausdorff.lean
theorem dist_ghDist (p q : GHSpace) : dist p q = ghDist p.Rep q.Rep

Proof state:
p q : GHSpace
⊢ dist p q = ghDist p.Rep q.Rep

Tactic:
rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_ne_top : a⁻¹ ≠ ∞ ↔ a ≠ 0

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ ≠ ⊤ ↔ a ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Comap.lean
theorem comap_preimage (f : α → β) (μ : Measure β) (hf : Injective f) (hf' : Measurable f)
    (h : ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ) {s : Set β} (hs : MeasurableSet s) :
    μ.comap f (f ⁻¹' s) = μ (s ∩ range f)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure β
hf : Injective f
hf' : Measurable f
h : ∀ (t : Set α), MeasurableSet t → NullMeasurableSet (f '' t) μ
s : Set β
hs : MeasurableSet s
⊢ (comap f μ) (f ⁻¹' s) = μ (s ∩ range f)

Tactic:
rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem leadingCoeff_expand {p : ℕ} {f : R[X]} (hp : 0 < p) :
    (expand R p f).leadingCoeff = f.leadingCoeff

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
hp : 0 < p
⊢ ((expand R p) f).leadingCoeff = f.leadingCoeff

Tactic:
simp_rw [leadingCoeff, natDegree_expand, coeff_expand_mul hp]

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem star_ne_zero [AddMonoid R] [StarAddMonoid R] {x : R} : star x ≠ 0 ↔ x ≠ 0

Proof state:
R : Type u
inst✝¹ : AddMonoid R
inst✝ : StarAddMonoid R
x : R
⊢ star x ≠ 0 ↔ x ≠ 0

Tactic:
simp only [ne_eq, star_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/HomCongr.lean
lemma eHomCongr_trans {X₁ Y₁ X₂ Y₂ X₃ Y₃ : C} (α₁ : X₁ ≅ X₂) (β₁ : Y₁ ≅ Y₂)
    (α₂ : X₂ ≅ X₃) (β₂ : Y₂ ≅ Y₃) :
    eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) =
      eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂) = eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂

Tactic:
ext

Result:
case w
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)).hom = (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂).hom

Proof state:
case w
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X₁ Y₁ X₂ Y₂ X₃ Y₃ : C
α₁ : X₁ ≅ X₂
β₁ : Y₁ ≅ Y₂
α₂ : X₂ ≅ X₃
β₂ : Y₂ ≅ Y₃
⊢ (eHomCongr V (α₁ ≪≫ α₂) (β₁ ≪≫ β₂)).hom = (eHomCongr V α₁ β₁ ≪≫ eHomCongr V α₂ β₂).hom

Tactic:
simp [eHom_whisker_exchange_assoc]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma star_nonneg_iff {x : R} : 0 ≤ star x ↔ 0 ≤ x

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 0 ≤ star x ↔ 0 ≤ x

Tactic:
simpa using star_le_star_iff (x := 0) (y := x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_eq_none [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} :
    m.contains a = false → m.getKey? a = none

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
⊢ m.contains a = false → m.getKey? a = none

Tactic:
simp_to_model using List.getKey?_eq_none

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_inv (h : (0 : ℝ) ∉ [[a, b]]) : ∫ x in a..b, x⁻¹ = log (b / a)

Proof state:
a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ x ∈ [[a, b]], x ≠ 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
rw [integral_deriv_eq_sub' _ deriv_log' (fun x hx => differentiableAt_log (h' x hx))
    (continuousOn_inv₀.mono <| subset_compl_singleton_iff.mpr h),
  log_div (h' b right_mem_uIcc) (h' a left_mem_uIcc)]

Result:
no goals

Proof state:
a b : ℝ
h : 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)

Tactic:
have h' := fun x (hx : x ∈ [[a, b]]) => ne_of_mem_of_not_mem hx h

Result:
a b : ℝ
h : 0 ∉ [[a, b]]
h' : ∀ x ∈ [[a, b]], x ≠ 0
⊢ ∫ (x : ℝ) in a..b, x⁻¹ = log (b / a)
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.closedBall_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
    Metric.closedBall (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 ≤ r ^ 2}

Proof state:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ x✝ ∈ Metric.closedBall 0 r ↔ x✝ ∈ {x | ∑ i : n, x i ^ 2 ≤ r ^ 2}

Tactic:
simp_rw [mem_setOf, mem_closedBall_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_le_left hr]

Result:
no goals

Proof state:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Metric.closedBall 0 r = {x | ∑ i : n, x i ^ 2 ≤ r ^ 2}

Tactic:
ext

Result:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x✝ : EuclideanSpace ℝ n
⊢ x✝ ∈ Metric.closedBall 0 r ↔ x✝ ∈ {x | ∑ i : n, x i ^ 2 ≤ r ^ 2}
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_mul_const_atTop_iff_pos [NeBot l] (h : Tendsto f l atTop) :
    Tendsto (fun x => f x * r) l atTop ↔ 0 < r

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedSemifield α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x => f x * r) l atTop ↔ 0 < r

Tactic:
simp only [mul_comm _ r, tendsto_const_mul_atTop_iff_pos h]

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem Icc_mem_nhds_iff [NoMinOrder α] [NoMaxOrder α] {a b x : α} :
    Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b x : α
⊢ Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Icc, mem_interior_iff_mem_nhds]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem coe_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} :
    (↑(⨅ i, S i) : Set A) = ⋂ i, S i

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_nonpos : (q : K) ≤ 0 ↔ q ≤ 0

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
q : ℚ≥0
⊢ ↑q ≤ 0 ↔ q ≤ 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_iff_continuousAt (h : s ∈ 𝓝 x) :
    ContinuousWithinAt f s x ↔ ContinuousAt f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x

Tactic:
rw [← univ_inter s, continuousWithinAt_inter h, continuousWithinAt_univ]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_mul_lt_iff₀` for a version with multiplication on the other side. -/
lemma inv_mul_lt_iff₀' (hc : 0 < c) : c⁻¹ * b < a ↔ b < a * c

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulStrictMono G₀
a b c : G₀
hc : 0 < c
⊢ c⁻¹ * b < a ↔ b < a * c

Tactic:
rw [inv_mul_lt_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
theorem ofQuaternion_star (q : ℍ[R,c₁,0,c₂]) : ofQuaternion (star q) = star (ofQuaternion q) :=
  CliffordAlgebraQuaternion.equiv.injective <| by
    rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
      toQuaternion_ofQuaternion]

Proof state:
R : Type u_1
inst✝ : CommRing R
c₁ c₂ : R
q : ℍ[R,c₁,c₂]
⊢ CliffordAlgebraQuaternion.equiv (ofQuaternion (star q)) = CliffordAlgebraQuaternion.equiv (star (ofQuaternion q))

Tactic:
rw [equiv_apply, equiv_apply, toQuaternion_star, toQuaternion_ofQuaternion,
  toQuaternion_ofQuaternion]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_sup [Fintype (edgeSet (G₁ ⊔ G₂))] [DecidableEq V] :
    (G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝³ : Fintype ↑G₁.edgeSet
inst✝² : Fintype ↑G₂.edgeSet
inst✝¹ : Fintype ↑(G₁ ⊔ G₂).edgeSet
inst✝ : DecidableEq V
⊢ (G₁ ⊔ G₂).edgeFinset = G₁.edgeFinset ∪ G₂.edgeFinset

Tactic:
simp [edgeFinset]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem filter_apply_ne_zero_iff (a : α) : (p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support

Proof state:
α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ (p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support

Tactic:
rw [Ne, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem mod_left' {a₁ a₂ : ℤ} {b : ℕ} (h : a₁ % b = a₂ % b) : J(a₁ | b) = J(a₂ | b)

Proof state:
a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₁ | b) = J(a₂ | b)

Tactic:
rw [mod_left, h, ← mod_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_set (a b : α) (l : Array α) (i : Nat) (h : i < l.size) :
    (l.set i a).count b = l.count b - (if l[i] == b then 1 else 0) + (if a == b then 1 else 0)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : Array α
i : Nat
h : i < l.size
⊢ count b (l.set i a h) = (count b l - if (l[i] == b) = true then 1 else 0) + if (a == b) = true then 1 else 0

Tactic:
simp [count_eq_countP, countP_set, h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma nonsingular_neg_iff (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧ (W'.a₁ * W'.negY x y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ W'.negY x y) ↔
    W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)

Tactic:
exact and_congr_right' <| (iff_congr not_and_or.symm not_and_or.symm).mpr <|
  not_congr <| and_congr_left fun h => by rw [← h]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
h : y = W'.negY x y
⊢ W'.a₁ * W'.negY x y = 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ↔ W'.a₁ * y = 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄

Tactic:
rw [← h]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y

Tactic:
rw [nonsingular_iff, equation_neg_iff, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ W'.Equation x y ∧ (W'.a₁ * W'.negY x y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ W'.negY x y) ↔
    W'.Equation x y ∧ (W'.a₁ * y ≠ 3 * x ^ 2 + 2 * W'.a₂ * x + W'.a₄ ∨ y ≠ -y - W'.a₁ * x - W'.a₃)
-- Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
lemma prod_boole : ∏ i, (ite (p i) 1 0 : M₀) = ite (∀ i, p i) 1 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝² : Fintype ι
inst✝¹ : CommMonoidWithZero M₀
p : ι → Prop
inst✝ : DecidablePred p
⊢ (∏ i : ι, if p i then 1 else 0) = if ∀ (i : ι), p i then 1 else 0

Tactic:
simp [Finset.prod_boole]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive] lemma ne_iff_ne_of_mul_eq_mul (h : a * b = c * d) : a ≠ c ↔ b ≠ d

Proof state:
α : Type u_1
inst✝ : CancelCommMonoid α
a b c d : α
h : a * b = c * d
⊢ a ≠ c ↔ b ≠ d

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- A cocircuit is a minimal set whose complement is nonspanning. -/
lemma isCocircuit_iff_minimal_compl_nonspanning :
    M.IsCocircuit K ↔ Minimal (fun X ↦ ¬ M.Spanning (M.E \ X)) K

Proof state:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X => ¬M.Spanning (M.E \ X)) K

Tactic:
convert isCocircuit_iff_minimal with K

Result:
case h.e'_2.h.e'_3.h.a
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Proof state:
case h.e'_2.h.e'_3.h.a
α : Type u_1
M : Matroid α
K✝ K : Set α
⊢ ¬M.Spanning (M.E \ K) ↔ ∀ (B : Set α), M.IsBase B → (K ∩ B).Nonempty

Tactic:
simp_rw [spanning_iff_exists_isBase_subset (S := M.E \ K), not_exists, subset_diff, not_and,
  not_disjoint_iff_nonempty_inter, ← and_imp, and_iff_left_of_imp IsBase.subset_ground,
  inter_comm K]

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_eq_of_map_eq (h : Commute f g) (n : ℕ) {x} (hx : f x = g x) :
    f^[n] x = g^[n] x :=
  Nat.recOn n rfl fun n ihn ↦ by
    simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]

Proof state:
α : Type u
f g : α → α
h : Commute f g
n✝ : ℕ
x : α
hx : f x = g x
n : ℕ
ihn : f^[n] x = g^[n] x
⊢ f^[n.succ] x = g^[n.succ] x

Tactic:
simp only [iterate_succ_apply, hx, (h.iterate_left n).eq, ihn, ((refl g).iterate_right n).eq]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_fixed' {f : α → β → α} {a : α} (hf : ∀ b, f a b = a) : ∀ l : List β, foldl f a l = a
  | [] => rfl
  | b :: l => by rw [foldl_cons, hf b, foldl_fixed' hf l]

Proof state:
α : Type u
β : Type v
f : α → β → α
a : α
hf : ∀ (b : β), f a b = a
b : β
l : List β
⊢ foldl f a (b :: l) = a

Tactic:
rw [foldl_cons, hf b, foldl_fixed' hf l]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_iff {f : Filter α} {P : α → Prop} :
    (∃ᶠ x in f, P x) ↔ ∀ {U}, U ∈ f → ∃ x ∈ U, P x

Proof state:
α : Type u
f : Filter α
P : α → Prop
⊢ (∃ᶠ (x : α) in f, P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Tactic:
simp only [frequently_iff_forall_eventually_exists_and, @and_comm (P _)]

Result:
α : Type u
f : Filter α
P : α → Prop
⊢ (∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, q x ∧ P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Proof state:
α : Type u
f : Filter α
P : α → Prop
⊢ (∀ {q : α → Prop}, (∀ᶠ (x : α) in f, q x) → ∃ x, q x ∧ P x) ↔ ∀ {U : Set α}, U ∈ f → ∃ x ∈ U, P x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem isInducing_pullback_to_prod {X Y Z : TopCat.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) :
    IsInducing <| ⇑(prod.lift (pullback.fst f g) (pullback.snd f g)) :=
  ⟨by simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]⟩

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullback f g).str = induced (⇑(ConcreteCategory.hom (prod.lift (pullback.fst f g) (pullback.snd f g)))) (X ⨯ Y).str

Tactic:
simp [prod_topology, pullback_topology, induced_compose, ← coe_comp]

Result:
no goals