harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem pow_div_pow_eventuallyEq_atBot {p q : ℕ} :
    (fun x : 𝕜 => x ^ p / x ^ q) =ᶠ[atBot] fun x => x ^ ((p : ℤ) - q)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ x < 0, (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Tactic:
intro x hx

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ (fun x => x ^ p / x ^ q) =ᶠ[atBot] fun x => x ^ (↑p - ↑q)

Tactic:
apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
⊢ ∀ x < 0, (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ (fun x => x ^ p / x ^ q) x = (fun x => x ^ (↑p - ↑q)) x

Tactic:
simp [zpow_sub₀ hx.ne]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
/-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular
Killing form, the corresponding roots span the dual space of `H`. -/
@[simp]
lemma span_weight_eq_top :
    span K (range (Weight.toLinear K H L)) = ⊤

Proof state:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
⊢ span K (range (Weight.toLinear K (↥H) L)) = ⊤

Tactic:
refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))

Result:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
⊢ ⊤ ≤ LinearMap.range (traceForm K (↥H) L)

Proof state:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
⊢ ⊤ ≤ LinearMap.range (traceForm K (↥H) L)

Tactic:
rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip,
  ker_traceForm_eq_bot_of_isCartanSubalgebra, Submodule.dualAnnihilator_bot]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_eq_zero (h : ¬IsOfFinOrder x) : orderOf x = 0

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
h : ¬IsOfFinOrder x
⊢ orderOf x = 0

Tactic:
rwa [orderOf, minimalPeriod, dif_neg]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem mem_insertP (p : α → Bool) (a l) : a ∈ insertP p a l

Proof state:
case cons
α : Type u_1
p : α → Bool
a head✝ : α
tail✝ : List α
ih : a ∈ insertP p a tail✝
⊢ a ∈
    match p head✝ with
    | true => a :: head✝ :: tail✝
    | false => insertP.loop p a tail✝ [head✝]

Tactic:
split <;> simp [insertP_loop, ih]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ a ∈ insertP p a l

Tactic:
induction l with simp [insertP, insertP.loop, cond]
| cons _ _ ih => split <;> simp [insertP_loop, ih]

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem inv_subst {α} [Field α] {n k e : α} (h2 : e ≠ 0) (h3 : n * e = k) :
    k * (e ⁻¹) = n

Proof state:
α : Type u_1
inst✝ : Field α
n k e : α
h2 : e ≠ 0
h3 : n * e = k
⊢ k * e⁻¹ = n

Tactic:
rw [← div_eq_mul_inv, ← h3, mul_div_cancel_right₀ _ h2]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp, norm_cast]
lemma rpow_intCast (x : ℝ≥0∞) (n : ℤ) : x ^ (n : ℝ) = x ^ n

Proof state:
x : ℝ≥0∞
n : ℤ
⊢ x ^ ↑n = x ^ n

Tactic:
cases n <;> simp only [Int.ofNat_eq_coe, Int.cast_natCast, rpow_natCast, zpow_natCast,
  Int.cast_negSucc, rpow_neg, zpow_negSucc]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
@[simp]
lemma _root_.LieAlgebra.IsKilling.coroot_neg (α : Weight K H L) : coroot (-α) = -coroot α

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
inst✝³ : IsKilling K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ coroot (-α) = -coroot α

Tactic:
simp [coroot]

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
theorem sub_top {a : WithTop α} : a - ⊤ = ⊤

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : WithTop α
⊢ a - ⊤ = ⊤

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma coyonedaEquiv_comp {X : C} {F G : C ⥤ Type v₁} (α : coyoneda.obj (op X) ⟶ F) (β : F ⟶ G) :
    coyonedaEquiv (α ≫ β) = β.app _ (coyonedaEquiv α)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F G : C ⥤ Type v₁
α : coyoneda.obj (op X) ⟶ F
β : F ⟶ G
⊢ coyonedaEquiv (α ≫ β) = β.app X (coyonedaEquiv α)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zero_add (n : ZNum) : 0 + n = n

Proof state:
n : ZNum
⊢ 0 + n = n

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem div_sub_same {a b : K} (h : b ≠ 0) : (a - b) / b = a / b - 1

Proof state:
K : Type u_1
inst✝ : DivisionRing K
a b : K
h : b ≠ 0
⊢ (a - b) / b = a / b - 1

Tactic:
simpa only [← @div_self _ _ b h] using (div_sub_div_same a b b).symm

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightUnshift_zero (a n' : ℤ) (hn' : n' + a = n) :
    (0 : Cochain K (L⟦a⟧) n').rightUnshift n hn' = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ rightUnshift 0 n hn' = 0

Tactic:
change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn').symm 0 = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn').symm 0 = 0

Tactic:
apply _root_.map_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modifyHead_eq_set [Inhabited α] (f : α → α) (l : List α) :
    l.modifyHead f = l.set 0 (f (l[0]?.getD default))

Proof state:
α : Type u_1
inst✝ : Inhabited α
f : α → α
l : List α
⊢ modifyHead f l = l.set 0 (f (l[0]?.getD default))

Tactic:
cases l <;> simp [modifyHead]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_val_succ' {i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α) :
    vecCons x u ⟨i.succ, h⟩ = u ⟨i, Nat.lt_of_succ_lt_succ h⟩

Proof state:
α : Type u
m i : ℕ
h : i.succ < m.succ
x : α
u : Fin m → α
⊢ vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩

Tactic:
simp only [vecCons, Fin.cons, Fin.cases_succ']

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem HasFPowerSeriesOnBall.changeOrigin (hf : HasFPowerSeriesOnBall f p x r)
    (h : (‖y‖₊ : ℝ≥0∞) < r) : HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ‖y‖₊)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑‖y‖₊ < r
⊢ HasFPowerSeriesWithinOnBall f (p.changeOrigin y) univ (x + y) (r - ↑‖y‖₊)

Tactic:
exact hf.changeOrigin h (by simp)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
h : ↑‖y‖₊ < r
⊢ HasFPowerSeriesOnBall f (p.changeOrigin y) (x + y) (r - ↑‖y‖₊)

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf ⊢

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑‖y‖₊ < r
⊢ HasFPowerSeriesWithinOnBall f (p.changeOrigin y) univ (x + y) (r - ↑‖y‖₊)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x y : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : ↑‖y‖₊ < r
⊢ x + y ∈ insert x univ

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem ext (h h' : IsAdjoinRoot S f) (eq : h.root = h'.root) : h = h' :=
  h.ext_map h' fun x => by rw [← h.aeval_eq, ← h'.aeval_eq, eq]

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h h' : IsAdjoinRoot S f
eq : h.root = h'.root
x : R[X]
⊢ h.map x = h'.map x

Tactic:
rw [← h.aeval_eq, ← h'.aeval_eq, eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.leftUnitor_inv_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    (prod.leftUnitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.leftUnitor Y).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem lcm_eq_one_iff [NormalizedGCDMonoid α] (a b : α) : lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1 :=
  Iff.intro (fun eq => eq ▸ ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩) fun ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ =>
    show lcm (Units.mkOfMulEqOne a c hc.symm : α) (Units.mkOfMulEqOne b d hd.symm) = 1 by
      rw [lcm_units_coe_left, normalize_coe_units]

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a b : α
x✝ : a ∣ 1 ∧ b ∣ 1
c : α
hc : 1 = a * c
d : α
hd : 1 = b * d
⊢ lcm ↑(Units.mkOfMulEqOne a c ⋯) ↑(Units.mkOfMulEqOne b d ⋯) = 1

Tactic:
rw [lcm_units_coe_left, normalize_coe_units]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhdsGE_eq_iInf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α}
    (ha : ∃ u, a < u) : 𝓝[≥] a = ⨅ (u) (_ : a < u), 𝓟 (Ico a u)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
ha : ∃ u, a < u
⊢ 𝓝[≥] a = ⨅ u, ⨅ (_ : a < u), 𝓟 (Ico a u)

Tactic:
simp only [nhdsGE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Iio_inter_Ici]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
theorem Complex.hasSum_cos (z : ℂ) :
    HasSum (fun n : ℕ => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (Complex.cos z)

Proof state:
z : ℂ
⊢ HasSum (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) (cos z)

Tactic:
convert Complex.hasSum_cos' z using 1

Result:
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!

Proof state:
case h.e'_5
z : ℂ
⊢ (fun n => (-1) ^ n * z ^ (2 * n) / ↑(2 * n)!) = fun n => (z * I) ^ (2 * n) / ↑(2 * n)!

Tactic:
simp_rw [mul_pow, pow_mul, Complex.I_sq, mul_comm]

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

Proof state:
α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s

Tactic:
simpa [Order.succ_eq_add_one] using strictMonoOn_of_lt_succ hs (f := f)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem deriv_fderiv : smulRight (1 : 𝕜 →L[𝕜] 𝕜) (deriv f x) = fderiv 𝕜 f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ smulRight 1 (deriv f x) = fderiv 𝕜 f x

Tactic:
simp only [deriv, ContinuousLinearMap.smulRight_one_one]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_preimage_of_injOn {f : α → β} {s : Set β} (hf : (f ⁻¹' s).InjOn f) (hsf : s ⊆ range f) :
    Nat.card (f ⁻¹' s) = Nat.card s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : InjOn f (f ⁻¹' s)
hsf : s ⊆ range f
⊢ Nat.card ↑(f ⁻¹' s) = Nat.card ↑s

Tactic:
rw [← Nat.card_image_of_injOn hf, image_preimage_eq_iff.2 hsf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
    (xs.all fun x => x != a) = !xs.contains a

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
xs : Array α
⊢ (xs.all fun x => x != a) = !xs.contains a

Tactic:
simp only [bne_comm, all_bne]

Result:
no goals
-- Mathlib/RingTheory/Norm/Basic.lean
theorem norm_eq_prod_roots [Algebra.IsSeparable K L] [FiniteDimensional K L] {x : L}
    (hF : (minpoly K x).Splits (algebraMap K F)) :
    algebraMap K F (norm K x) =
      ((minpoly K x).aroots F).prod ^ finrank K⟮x⟯ L

Proof state:
K : Type u_4
L : Type u_5
F : Type u_6
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Field F
inst✝³ : Algebra K L
inst✝² : Algebra K F
inst✝¹ : Algebra.IsSeparable K L
inst✝ : FiniteDimensional K L
x : L
hF : Splits (algebraMap K F) (minpoly K x)
⊢ (algebraMap K F) ((norm K) x) = ((minpoly K x).aroots F).prod ^ finrank (↥K⟮x⟯) L

Tactic:
rw [norm_eq_norm_adjoin K x, map_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots _ hF]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem State.sat_def (assign : CNFVar aig → Bool) (state : State aig) :
    state.Sat assign ↔ state.cnf.Sat assign

Proof state:
aig : AIG Nat
assign : aig.CNFVar → Bool
state : State aig
⊢ Sat assign state ↔ CNF.Sat assign state.cnf

Tactic:
rfl

Result:
no goals
-- Mathlib/Tactic/NormNum/Pow.lean
theorem IsNatPowT.bit0 : IsNatPowT (Nat.pow a b = c) a (nat_lit 2 * b) (Nat.mul c c) :=
  ⟨fun h1 => by simp [two_mul, pow_add, ← h1]⟩

Proof state:
a b c : ℕ
h1 : a.pow b = c
⊢ a.pow (2 * b) = c.mul c

Tactic:
simp [two_mul, pow_add, ← h1]

Result:
no goals
-- Mathlib/Algebra/Algebra/Unitization.lean
@[simp]
lemma isStarNormal_inr : IsStarNormal (a : Unitization R A) ↔ IsStarNormal a

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : Semiring R
inst✝⁴ : StarAddMonoid R
inst✝³ : Star A
a : A
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : SMulWithZero R A
⊢ IsStarNormal ↑a ↔ IsStarNormal a

Tactic:
simp only [isStarNormal_iff, commute_iff_eq, ← inr_star, ← inr_mul, inr_injective.eq_iff]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem rotate_length_mul (l : List α) (n : ℕ) : l.rotate (l.length * n) = l

Proof state:
α : Type u
l : List α
n : ℕ
⊢ l.rotate (l.length * n) = l

Tactic:
rw [rotate_eq_rotate', rotate'_length_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Pi.lean
@[to_additive (attr := simp) single_nonneg]
lemma one_le_mulSingle : 1 ≤ mulSingle i a ↔ 1 ≤ a

Proof state:
ι : Type u_6
α : ι → Type u_7
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → One (α i)
inst✝ : (i : ι) → Preorder (α i)
i : ι
a : α i
⊢ 1 ≤ mulSingle i a ↔ 1 ≤ a

Tactic:
simp [mulSingle]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformRight_one : mulETransformRight 1 x = x

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
x : Finset α × Finset α
⊢ mulETransformRight 1 x = x

Tactic:
simp [mulETransformRight]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `b ≠ 0`. See `inv_mul_cancel_right`. -/
lemma le_inv_mul_right (ha : a ≤ 0) : a ≤ a * b⁻¹ * b

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
ha : a ≤ 0
⊢ a ≤ a * b⁻¹ * b

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma isLUB_supClosure : IsLUB (supClosure s) a ↔ IsLUB s a

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
s : Set α
a : α
⊢ IsLUB (supClosure s) a ↔ IsLUB s a

Tactic:
simp [IsLUB]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean
theorem injective_of_adjoint (adj : L ⊣ R) (J : D) [Injective J] : Injective <| R.obj J :=
  ⟨fun {A} {_} g f im =>
    ⟨adj.homEquiv _ _ (factorThru ((adj.homEquiv A J).symm g) (L.map f)),
      (adj.homEquiv _ _).symm.injective
        (by simp [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit])⟩⟩

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝¹ : L.PreservesMonomorphisms
adj : L ⊣ R
J : D
inst✝ : Injective J
A x✝ : C
g : A ⟶ R.obj J
f : A ⟶ x✝
im : Mono f
⊢ (adj.homEquiv A J).symm (f ≫ (adj.homEquiv x✝ J) (factorThru ((adj.homEquiv A J).symm g) (L.map f))) =
    (adj.homEquiv A J).symm g

Tactic:
simp [Adjunction.homEquiv_unit, Adjunction.homEquiv_counit]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem of_leftInverse [MonoidHomClass G N M] {f : F} {x : M} (g : G)
    (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) : IsUnit x

Proof state:
F : Type u_1
G : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : FunLike F M N
inst✝³ : FunLike G N M
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : MonoidHomClass G N M
f : F
x : M
g : G
hfg : LeftInverse ⇑g ⇑f
h : IsUnit (f x)
⊢ IsUnit x

Tactic:
simpa only [hfg x] using h.map g

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem add_pf_zero_add (b : R) : 0 + b = b

Proof state:
R : Type u_1
inst✝ : CommSemiring R
b : R
⊢ 0 + b = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem mem_map₂_iff {c : γ} : c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : γ
⊢ c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Tactic:
simp [map₂, bind_eq_some]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma zpow_lt_iff_lt_log {n : ℤ} (hx : 0 < x) (hy : 0 < y) : x ^ n < y ↔ n * log x < log y

Proof state:
x y : ℝ
n : ℤ
hx : 0 < x
hy : 0 < y
⊢ x ^ n < y ↔ ↑n * log x < log y

Tactic:
rw [← rpow_lt_iff_lt_log hx hy, rpow_intCast]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_finset_sup_eq_iInter (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E) {r : ℝ}
    (hr : 0 ≤ r) : closedBall (s.sup p) x r = ⋂ i ∈ s, closedBall (p i) x r

Proof state:
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ
hr : 0 ≤ r
⊢ (s.sup p).closedBall x r = ⋂ i ∈ s, (p i).closedBall x r

Tactic:
lift r to NNReal using hr

Result:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ (s.sup p).closedBall x ↑r = ⋂ i ∈ s, (p i).closedBall x ↑r

Proof state:
case intro
𝕜 : Type u_3
E : Type u_7
ι : Type u_11
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → Seminorm 𝕜 E
s : Finset ι
x : E
r : ℝ≥0
⊢ (s.sup p).closedBall x ↑r = ⋂ i ∈ s, (p i).closedBall x ↑r

Tactic:
simp_rw [closedBall, iInter_setOf, finset_sup_apply, NNReal.coe_le_coe, Finset.sup_le_iff, ←
  NNReal.coe_le_coe, NNReal.coe_mk]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[continuity, fun_prop]
lemma continuous_inner : Continuous (fun x : E × E => ⟪x.1, x.2⟫_A)

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CStarModule A E
⊢ Continuous fun x => (innerSL x.1) x.2

Tactic:
fun_prop

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CStarModule A E
⊢ Continuous fun x => ⟪x.1, x.2⟫_A

Tactic:
simp_rw [← innerSL_apply]

Result:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CStarModule A E
⊢ Continuous fun x => (innerSL x.1) x.2
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_generate (s : Set (Set α)) :
    (generate s).HasBasis (fun t => Set.Finite t ∧ t ⊆ s) fun t => ⋂₀ t :=
  ⟨fun U => by simp only [mem_generate_iff, exists_prop, and_assoc, and_left_comm]⟩

Proof state:
α : Type u_1
s : Set (Set α)
U : Set α
⊢ U ∈ generate s ↔ ∃ i, (i.Finite ∧ i ⊆ s) ∧ ⋂₀ i ⊆ U

Tactic:
simp only [mem_generate_iff, exists_prop, and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem lcm_mul_left {m n k : ℤ} : (m * n).lcm (m * k) = natAbs m * n.lcm k

Proof state:
m n k : ℤ
⊢ (m * n).lcm (m * k) = m.natAbs * n.lcm k

Tactic:
simp_rw [Int.lcm, natAbs_mul, Nat.lcm_mul_left]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_add_one_pow (R : Type*) [Semiring R] (n k : ℕ) :
    ((X + 1) ^ n).coeff k = (n.choose k : R)

Proof state:
R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ ((X + 1) ^ n).coeff k = ↑(n.choose k)

Tactic:
rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]

Result:
no goals
-- Mathlib/Topology/Order/MonotoneConvergence.lean
theorem tendsto_atTop_isGLB (h_anti : Antitone f) (ha : IsGLB (Set.range f) a) :
    Tendsto f atTop (𝓝 a)

Proof state:
α : Type u_1
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
convert tendsto_atBot_isLUB h_anti.dual ha.dual using 1

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_eq_trim (s : Set α) : μ s = μ.toOuterMeasure.trim s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
⊢ μ s = μ.trim s

Tactic:
rw [μ.trimmed, μ.coe_toOuterMeasure]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem fromRel_bot : fromRel (fun (_ _ : α) z => z : Symmetric ⊥) = ∅

Proof state:
α : Type u_1
⊢ ∀ (e : Sym2 α), e ∉ fromRel ⋯

Tactic:
apply Sym2.ind

Result:
case h
α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∉ fromRel ⋯

Proof state:
α : Type u_1
⊢ fromRel ⋯ = ∅

Tactic:
apply Set.eq_empty_of_forall_not_mem fun e => _

Result:
α : Type u_1
⊢ ∀ (e : Sym2 α), e ∉ fromRel ⋯

Proof state:
case h
α : Type u_1
⊢ ∀ (x y : α), s(x, y) ∉ fromRel ⋯

Tactic:
simp [-Set.bot_eq_empty, Prop.bot_eq_false]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem ne_top_iff_dom {x : PartENat} : x ≠ ⊤ ↔ x.Dom

Proof state:
x : PartENat
⊢ x ≠ ⊤ ↔ x.Dom

Tactic:
exact not_iff_comm.1 Part.eq_none_iff'.symm

Result:
no goals

Proof state:
x : PartENat
⊢ x ≠ ⊤ ↔ x.Dom

Tactic:
classical exact not_iff_comm.1 Part.eq_none_iff'.symm

Result:
no goals
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem nndist_eq {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β]
    [DilationClass F α β] (f : F) (x y : α) :
    nndist (f x) (f y) = ratio f * nndist x y

Proof state:
α : Type u_5
β : Type u_6
F : Type u_7
inst✝³ : PseudoMetricSpace α
inst✝² : PseudoMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ nndist (f x) (f y) = ratio f * nndist x y

Tactic:
simp only [← ENNReal.coe_inj, ← edist_nndist, ENNReal.coe_mul, edist_eq]

Result:
no goals