harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Max.lean
theorem max'_mem : s.max' H ∈ s :=
  mem_of_max <| by simp only [max', Finset.max, id_eq, coe_sup', Function.comp_def]

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
H : s.Nonempty
⊢ s.max = ↑(s.max' H)

Tactic:
simp only [max', Finset.max, id_eq, coe_sup', Function.comp_def]

Result:
no goals
-- Mathlib/Data/Vector/Mem.lean
theorem mem_map_succ_iff (b : β) (v : Vector α (n + 1)) (f : α → β) :
    b ∈ (v.map f).toList ↔ f v.head = b ∨ ∃ a : α, a ∈ v.tail.toList ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ (map f v).toList ↔ f v.head = b ∨ ∃ a ∈ v.tail.toList, f a = b

Tactic:
rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/WithAbs.lean
theorem uniformSpace_comap_eq_of_comp (h : ∀ x, ‖f x‖ = v x) :
    UniformSpace.comap f inferInstance = (normedField v).toUniformSpace

Proof state:
K : Type u_3
inst✝¹ : Field K
v : AbsoluteValue K ℝ
L : Type u_4
inst✝ : NormedField L
f : WithAbs v →+* L
h : ∀ (x : WithAbs v), ‖f x‖ = v x
⊢ UniformSpace.comap (⇑f) inferInstance = PseudoMetricSpace.toUniformSpace

Tactic:
simp only [← pseudoMetricSpace_induced_of_comp h, PseudoMetricSpace.toUniformSpace]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem congr {X Y : Ω → E} (hXY : X =ᵐ[ℙ] Y) : pdf X ℙ μ = pdf Y ℙ μ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X Y : Ω → E
hXY : X =ᶠ[ae ℙ] Y
⊢ pdf X ℙ μ = pdf Y ℙ μ

Tactic:
rw [pdf_def, pdf_def, map_congr hXY]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem _root_.fourierIntegral_gaussian (hb : 0 < b.re) (t : ℂ) :
    ∫ x : ℝ, cexp (I * t * x) * cexp (-b * x ^ 2) =
    (π / b) ^ (1 / 2 : ℂ) * cexp (-t ^ 2 / (4 * b))

Proof state:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ (-b).re < 0

Tactic:
rwa [neg_re, neg_lt_zero]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ ∫ (x : ℝ), cexp (-b * ↑x ^ 2 + I * t * ↑x + 0) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
rw [integral_cexp_quadratic (show (-b).re < 0 by rwa [neg_re, neg_lt_zero]), neg_neg, zero_sub,
  mul_neg, div_neg, neg_neg, mul_pow, I_sq, neg_one_mul, mul_comm]

Result:
no goals

Proof state:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ ∫ (x : ℝ), cexp (I * t * ↑x) * cexp (-b * ↑x ^ 2) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))

Tactic:
conv => enter [1, 2, x]; rw [← Complex.exp_add, add_comm, ← add_zero (-b * x ^ 2 + I * t * x)]

Result:
b : ℂ
hb : 0 < b.re
t : ℂ
⊢ ∫ (x : ℝ), cexp (-b * ↑x ^ 2 + I * t * ↑x + 0) = (↑π / b) ^ (1 / 2) * cexp (-t ^ 2 / (4 * b))
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem insert_toList {p : Path α} :
    (p.insert t v).toList = p.withList (t.setRoot v).toList

Proof state:
α : Type u_1
t : RBNode α
v : α
p : Path α
⊢ (match t with
      | nil => p.insertNew v
      | node c a v_1 b => p.fill (node c a v b)).toList =
    p.listL ++ ((setRoot v t).toList ++ p.listR)

Tactic:
split <;> simp [setRoot]

Result:
no goals

Proof state:
α : Type u_1
t : RBNode α
v : α
p : Path α
⊢ (p.insert t v).toList = p.withList (setRoot v t).toList

Tactic:
simp [insert]

Result:
α : Type u_1
t : RBNode α
v : α
p : Path α
⊢ (match t with
      | nil => p.insertNew v
      | node c a v_1 b => p.fill (node c a v b)).toList =
    p.listL ++ ((setRoot v t).toList ++ p.listR)
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_natDegree (f : R[X]) : f.reverse.natDegree = f.natDegree - f.natTrailingDegree

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natDegree = f.natDegree - f.natTrailingDegree

Tactic:
rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem one : minpoly A (1 : B) = X - 1

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 1 = X - 1

Tactic:
simpa only [RingHom.map_one, C_1, sub_eq_add_neg] using eq_X_sub_C B (1 : A)

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem lt_sqrt (hx : 0 ≤ x) : x < √y ↔ x ^ 2 < y

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ x < √y ↔ x ^ 2 < y

Tactic:
rw [← sqrt_lt_sqrt_iff (sq_nonneg _), sqrt_sq hx]

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
/-- If `B` is faithfully flat over `A`, every prime of `A` comes from a prime of `B`. -/
lemma Ideal.exists_isPrime_liesOver_of_faithfullyFlat (p : Ideal A) [p.IsPrime] :
    ∃ (P : Ideal B), P.IsPrime ∧ P.LiesOver p

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.FaithfullyFlat A B
p : Ideal A
inst✝ : p.IsPrime
⊢ ∃ P, P.IsPrime ∧ P.LiesOver p

Tactic:
obtain ⟨P, _, hP⟩ := (Ideal.comap_map_eq_self_iff_of_isPrime p).mp <|
  p.comap_map_eq_self_of_faithfullyFlat (B := B)

Result:
case intro.intro
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.FaithfullyFlat A B
p : Ideal A
inst✝ : p.IsPrime
P : Ideal B
left✝ : P.IsPrime
hP : comap (algebraMap A B) P = p
⊢ ∃ P, P.IsPrime ∧ P.LiesOver p

Proof state:
case intro.intro
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.FaithfullyFlat A B
p : Ideal A
inst✝ : p.IsPrime
P : Ideal B
left✝ : P.IsPrime
hP : comap (algebraMap A B) P = p
⊢ ∃ P, P.IsPrime ∧ P.LiesOver p

Tactic:
exact ⟨P, inferInstance, ⟨hP.symm⟩⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem neg_pi_div_two_lt_arcsin {x : ℝ} : -(π / 2) < arcsin x ↔ -1 < x :=
  (lt_arcsin_iff_sin_lt' <| left_mem_Ico.2 <| neg_lt_self pi_div_two_pos).trans <| by
    rw [sin_neg, sin_pi_div_two]

Proof state:
x : ℝ
⊢ sin (-(π / 2)) < x ↔ -1 < x

Tactic:
rw [sin_neg, sin_pi_div_two]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.braiding_map_braiding {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) :
    (biprod.braiding X W).hom ≫ biprod.map f g ≫ (biprod.braiding Y Z).hom = biprod.map g f

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
⊢ (braiding X W).hom ≫ map f g ≫ (braiding Y Z).hom = map g f

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.eq_to_beq (a b : Bool) : (a = b) = ((a == b) = true)

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

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCard_one (s : Multiset α) : powersetCard 1 s = s.map singleton :=
  Quotient.inductionOn s fun l ↦ by
    simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ powersetCard 1 ⟦l⟧ = map singleton ⟦l⟧

Tactic:
simp [powersetCard_coe, sublistsLen_one, map_reverse, Function.comp_def]

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem clog_of_left_le_one {b : ℕ} (hb : b ≤ 1) (r : R) : clog b r = 0

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hb : b ≤ 1
r : R
⊢ clog b r = 0

Tactic:
rw [← neg_log_inv_eq_clog, log_of_left_le_one hb, neg_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem Basis.toMatrix_reindex (b : Basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
    (b.reindex e).toMatrix v = (b.toMatrix v).submatrix e.symm _root_.id

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (b.toMatrix v).submatrix (⇑e.symm) _root_.id i✝ j✝

Tactic:
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.submatrix_apply, _root_.id,
  Finsupp.mapDomain_equiv_apply]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (⇑e.symm) _root_.id

Tactic:
ext

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (b.toMatrix v).submatrix (⇑e.symm) _root_.id i✝ j✝
-- Mathlib/Data/Nat/Init.lean
protected lemma pow_lt_pow_left (h : a < b) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
  | 1, _ => by simpa
  | n + 2, _ => Nat.mul_lt_mul_of_lt_of_le (Nat.pow_lt_pow_left h n.succ_ne_zero) (Nat.le_of_lt h)
    (zero_lt_of_lt h)

Proof state:
a b : ℕ
h : a < b
x✝ : 1 ≠ 0
⊢ a ^ 1 < b ^ 1

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/ContinuousAffineMap.lean
theorem toContinuousAffineMap_map_zero (f : V →L[R] W) : f.toContinuousAffineMap 0 = 0

Proof state:
R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : TopologicalSpace W
f : V →L[R] W
⊢ f.toContinuousAffineMap 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Algebra.lean
theorem prod_apply [CommMonoid β] [ContinuousMul β] {ι : Type*} (s : Finset ι) (f : ι → C(α, β))
    (a : α) : (∏ i ∈ s, f i) a = ∏ i ∈ s, f i a

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
ι : Type u_3
s : Finset ι
f : ι → C(α, β)
a : α
⊢ (∏ i ∈ s, f i) a = ∏ i ∈ s, (f i) a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem compl_mem_comap : sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Filter β
s : Set α
⊢ sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l

Tactic:
rw [mem_comap_iff_compl, compl_compl]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/TVS.lean
theorem isLittleOTVS_iff_smallSets :
    f =o[𝕜; l] g ↔ ∀ U ∈ 𝓝 0, ∀ᶠ V in (𝓝 0).smallSets, ∀ ε ≠ (0 : ℝ≥0),
      ∀ᶠ x in l, egauge 𝕜 U (f x) ≤ ε * egauge 𝕜 V (g x) :=
  forall₂_congr fun U hU ↦ .symm <| eventually_smallSets' fun V₁ V₂ hV hV₂ ε hε ↦
    (hV₂ ε hε).mono fun x hx ↦ hx.trans <| by gcongr

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
l : Filter α
f : α → E
g : α → F
U : Set E
hU : U ∈ 𝓝 0
V₁ V₂ : Set F
hV : V₁ ⊆ V₂
hV₂ : ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V₂ (g x)
ε : ℝ≥0
hε : ε ≠ 0
x : α
hx : egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V₂ (g x)
⊢ ↑ε * egauge 𝕜 V₂ (g x) ≤ ↑ε * egauge 𝕜 V₁ (g x)

Tactic:
gcongr

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bind_const (p : PMF α) (q : PMF β) : (p.bind fun _ => q) = q :=
  PMF.ext fun x => by rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
q : PMF β
x : β
⊢ (p.bind fun x => q) x = q x

Tactic:
rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
lemma strictMonoOn_of_sub_one_lt (hs : s.OrdConnected) :
    (∀ a, ¬ IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f (a - 1) < f a) → StrictMonoOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using strictMonoOn_of_pred_lt hs (f := f)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.gcd_mul_left_cancel_right (n : Nat)
    (H : Coprime k m) : gcd m (k * n) = gcd m n

Proof state:
k m n : Nat
H : k.Coprime m
⊢ m.gcd (k * n) = m.gcd n

Tactic:
rw [gcd_comm m n, gcd_comm m (k * n), H.gcd_mul_left_cancel n]

Result:
no goals
-- Mathlib/Algebra/Star/SelfAdjoint.lean
theorem zpow₀ {x : R} (hx : IsSelfAdjoint x) (n : ℤ) : IsSelfAdjoint (x ^ n)

Proof state:
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
hx : IsSelfAdjoint x
n : ℤ
⊢ IsSelfAdjoint (x ^ n)

Tactic:
simp only [isSelfAdjoint_iff, star_zpow₀, hx.star_eq]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_add : sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Proof state:
x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)

Tactic:
simp [sinh_add]

Result:
no goals

Proof state:
x y : ℝ
⊢ sinh (x + y) = sinh x * cosh y + cosh x * sinh y

Tactic:
rw [← ofReal_inj]

Result:
x y : ℝ
⊢ ↑(sinh (x + y)) = ↑(sinh x * cosh y + cosh x * sinh y)
-- Mathlib/Data/Finsupp/MonomialOrder/DegLex.lean
theorem lt_iff [LT α] {a b : DegLex (α →₀ ℕ)} :
    a < b ↔ (ofDegLex a).degree < (ofDegLex b).degree ∨
    (((ofDegLex a).degree = (ofDegLex b).degree) ∧ toLex (ofDegLex a) < toLex (ofDegLex b))

Proof state:
α : Type u_1
inst✝ : LT α
a b : DegLex (α →₀ ℕ)
⊢ a < b ↔
    (ofDegLex a).degree < (ofDegLex b).degree ∨
      (ofDegLex a).degree = (ofDegLex b).degree ∧ toLex (ofDegLex a) < toLex (ofDegLex b)

Tactic:
simp [lt_def, Prod.Lex.toLex_lt_toLex]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_bool_eq {f : Bool → α} : ⨆ b : Bool, f b = f true ⊔ f false

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
f : Bool → α
⊢ ⨆ b, f b = f true ⊔ f false

Tactic:
rw [iSup, Bool.range_eq, sSup_pair, sup_comm]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
lemma kernImage_compl {s : Set α} : kernImage f (sᶜ) = (f '' s)ᶜ

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

Tactic:
rw [kernImage_eq_compl, compl_compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.reverse p) = denote ctx p

Proof state:
ctx : Context
p : Poly
⊢ denote ctx (List.reverse p) = denote ctx p

Tactic:
simp [List.reverse]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_single_one [DecidableEq n] (v : n → α) (i : n) :
    dotProduct v (Pi.single i 1) = v i

Proof state:
n : Type u_3
α : Type v
inst✝² : Fintype n
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq n
v : n → α
i : n
⊢ v ⬝ᵥ Pi.single i 1 = v i

Tactic:
rw [dotProduct_single, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_eq_some_iff {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i] = a

Proof state:
α : Type u_1
i : Nat
a : α
l : List α
⊢ l[i]? = some a ↔ ∃ h, l[i] = a

Tactic:
simp only [← get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardFactors_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) : Ω (m * n) = Ω m + Ω n

Proof state:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ Ω (m * n) = Ω m + Ω n

Tactic:
rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
  UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq,
  Multiset.card_add, Multiset.coe_card, Multiset.coe_card]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
@[simp] lemma lieBracketWithin_self : lieBracketWithin 𝕜 V V s = 0

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 V V s x = 0 x

Tactic:
simp [lieBracketWithin]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : E → E
s : Set E
⊢ lieBracketWithin 𝕜 V V s = 0

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V : E → E
s : Set E
x : E
⊢ lieBracketWithin 𝕜 V V s x = 0 x
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_mul_of_isRegular_right {f g : MvPolynomial σ R}
    (hf : f ≠ 0) (hg : IsRegular (m.leadingCoeff g)) :
    m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : IsRegular (m.leadingCoeff g)
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
simp only [leadingCoeff, degree_mul_of_isRegular_right hf hg, coeff_mul_of_degree_add]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem mk_univ_quaternionAlgebra : #(Set.univ : Set ℍ[R,c₁,c₂,c₃]) = #R ^ 4

Proof state:
R : Type u_1
c₁ c₂ c₃ : R
⊢ #↑Set.univ = #R ^ 4

Tactic:
rw [mk_univ, mk_quaternionAlgebra]

Result:
no goals
-- Mathlib/Algebra/Group/Prod.lean
theorem coprod_unique (f : M × N →* P) : (f.comp (inl M N)).coprod (f.comp (inr M N)) = f :=
  ext fun x => by simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Proof state:
M : Type u_3
N : Type u_4
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : CommMonoid P
f : M × N →* P
x : M × N
⊢ ((f.comp (inl M N)).coprod (f.comp (inr M N))) x = f x

Tactic:
simp [coprod_apply, inl_apply, inr_apply, ← map_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
@[simp]
lemma natTransLift_id (F : Quotient r ⥤ D) :
    natTransLift r (𝟙 (Quotient.functor r ⋙ F)) = 𝟙 _

Proof state:
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} D
F : Quotient r ⥤ D
⊢ natTransLift r (𝟙 (functor r ⋙ F)) = 𝟙 F

Tactic:
aesop_cat

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

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
this : MulPosStrictMono G₀
⊢ a < b / c ↔ c * a < b

Tactic:
rw [lt_div_iff₀ hc, mul_comm]

Result:
no goals

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
⊢ a < b / c ↔ c * a < b

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
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
this : MulPosStrictMono G₀
⊢ a < b / c ↔ c * a < b
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_sq_eq_one_of_squarefree {l : ℕ} (hl : Squarefree l) : μ l ^ 2 = 1

Proof state:
l : ℕ
hl : Squarefree l
⊢ μ l ^ 2 = 1

Tactic:
rw [moebius_apply_of_squarefree hl, ← pow_mul, mul_comm, pow_mul, neg_one_sq, one_pow]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
theorem Basis.tensorProduct_repr_tmul_apply (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N)
    (i : ι) (j : κ) :
    (Basis.tensorProduct b c).repr (m ⊗ₜ n) (i, j) = c.repr n j • b.repr m i

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring S
inst✝⁶ : Algebra R S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b : Basis ι S M
c : Basis κ R N
m : M
n : N
i : ι
j : κ
⊢ ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i

Tactic:
simp [Basis.tensorProduct, mul_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem mul_prod_erase [DecidableEq α] (s : Finset α) (f : α → β) {a : α} (h : a ∈ s) :
    (f a * ∏ x ∈ s.erase a, f x) = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α → β
a : α
h : a ∈ s
⊢ f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x

Tactic:
rw [← prod_insert (not_mem_erase a s), insert_erase h]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem isChain_univ_iff : IsChain r (univ : Set α) ↔ IsTrichotomous α r

Proof state:
α : Type u_1
r : α → α → Prop
⊢ IsChain r univ ↔ IsTrichotomous α r

Tactic:
refine ⟨fun h => ⟨fun a b => ?_⟩, fun h => @isChain_of_trichotomous _ _ h univ⟩

Result:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ r a b ∨ a = b ∨ r b a

Proof state:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ ¬a = b → r a b ∨ r b a

Tactic:
exact h trivial trivial

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ r a b ∨ a = b ∨ r b a

Tactic:
rw [or_left_comm, or_iff_not_imp_left]

Result:
α : Type u_1
r : α → α → Prop
h : IsChain r univ
a b : α
⊢ ¬a = b → r a b ∨ r b a
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem norm_circleMap_zero (R : ℝ) (θ : ℝ) : ‖circleMap 0 R θ‖= |R|

Proof state:
R θ : ℝ
⊢ ‖circleMap 0 R θ‖ = |R|

Tactic:
simp [circleMap]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Icc_of_neg (a b : α) {c : α} (h : c < 0) :
    (fun x => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : c < 0
⊢ (fun x => x * c) ⁻¹' Icc a b = Icc (b / c) (a / c)

Tactic:
simp [← Ici_inter_Iic, h, inter_comm]

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
lemma natCast_le_toNNReal {n : ℕ} {r : ℝ} (hn : n ≠ 0) : ↑n ≤ r.toNNReal ↔ n ≤ r

Proof state:
n : ℕ
r : ℝ
hn : n ≠ 0
⊢ ↑n ≤ r.toNNReal ↔ ↑n ≤ r

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_totalDegree_le (M : Matrix m n R) (i : m) :
    (M.toMvPolynomial i).totalDegree ≤ 1

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
⊢ (M.toMvPolynomial i).totalDegree ≤ 1

Tactic:
apply (toMvPolynomial_isHomogeneous _ _).totalDegree_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem?_eq (l : BitVec w) (i : Nat) :
    l[i]? = if h : i < w then some l[i] else none

Proof state:
w : Nat
l : BitVec w
i : Nat
⊢ l[i]? = if h : i < w then some l[i] else none

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[parity_simps] lemma odd_pow {n : ℕ} : Odd (m ^ n) ↔ Odd m ∨ n = 0

Proof state:
m : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0

Tactic:
rw [← not_iff_not, not_odd_iff_even, not_or, not_odd_iff_even, even_pow]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem norm_Integral_le_one : ‖Integral‖ ≤ 1 :=
  LinearMap.mkContinuous_norm_le _ zero_le_one fun f ↦ by
    simpa [one_mul] using norm_integral_le_norm f

Proof state:
α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedSpace ℝ E
f : ↥(simpleFunc E 1 μ)
⊢ ‖{ toFun := integral, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ‖f‖

Tactic:
simpa [one_mul] using norm_integral_le_norm f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) :
    (m.modify k f).get? k = (m.get? k).map f

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : β k → β k
h : m.WF
⊢ (m.modify k f).get? k = Option.map f (m.get? k)

Tactic:
simp_to_raw using Raw₀.get?_modify_self

Result:
no goals